z3::operator- 导致程序终止

Question

我有这个使用 z3 运算符的 C++ 代码。

    std::vector<z3::expr> bv_vector_immediate = {};
    int immediate_int = immediates[0]->get_immediate_value_int();
    bv_vector_immediate.push_back(z3_ctx.bv_val(immediate_int, 64));
    Z3_LHS = get_register_value(register1).back(); //bv_val(0, 64)
    Z3_RHS = bv_vector_immediate.back();  //bv_val(10, 64)  
    output =  z3::operator-(Z3_LHS,Z3_RHS);
    std::cout << z3_solver.check() << "\n";
    z3::model m = z3_solver.get_model();
    bv_vector_output.push_back(m.eval(output));
    std::cout << Z3_LHS << "-" << Z3_RHS << " = " << m.eval(output).get_numeral_int64() << std::endl;

我得到的输出是：

terminate called after throwing an instance of 'z3::exception'
Aborted (core dumped)

然而，当我通过在此处更改此行将运算符更改为 + 时，代码正常工作。

output =  z3::operator+(Z3_LHS,Z3_RHS);

我相信由于 - 操作的结果产生了一个负值，所以在最后一行 std::cout << Z3_LHS << "-" << Z3_RHS << " = " << m.eval(output).get_numeral_int64() << std::endl; 抛出了一些 z3 异常。那么我该如何解决这个问题，即从较小的位向量值中减去较大的位向量值，从而获得 z3 表达式的数字 int 表示形式。我只能找到那些 z3 函数来获取位向量值 z3 表达式的 int 表示：get_numeral_int64、get_numeral_uint64、get_numeral_int、get_numeral_uint.

Answer 1

请始终post 可重现 代码段。仅 posting 代码的“部分”会使其他人很难诊断问题。

话虽如此，您的问题是值 0-10 不适合作为位向量的 int64 值。这是一个最小的复制器：

#include <z3++.h>

using namespace z3;
using namespace std;

int main ()
{
  context c;
  expr lhs    = c.bv_val( 0, 64);
  expr rhs    = c.bv_val(10, 64);
  expr output = lhs - rhs;

  solver s(c);
  cout << s.check() << endl;
  model m = s.get_model();
  cout << m.eval(output).get_numeral_int64() << endl;

  return 0;
};

当我运行这个时，我得到：

$ g++ -std=c++11 a.cpp -l z3
$ ./a.out
sat
libc++abi: terminating with uncaught exception of type z3::exception

你可能会问为什么会这样？结果，毕竟是 0-10，即 -10，它非常适合 64 位位向量。但是请记住，位向量算术没有符号的概念；这是做带符号算术的操作。所以，在 64 位算法中 -10 实际上与 18446744073709551606 是相同的值，这确实不适合 int64 的范围，其最大值为 9223372036854775807.

你如何解决这个问题？好吧，这实际上取决于您要如何处理这些位向量值。我假设您想将这些视为带符号的整数值。然后，在上面的复制器中，将最后一行更改为：

 cout << (int64_t) m.eval(output).get_numeral_uint64() << endl;

当我运行这样时，我得到：

sat
-10

这可能是您想要的。

总结在 z3 中，位向量值没有与之关联的符号。它们只是一堆比特。但是当你对它们进行操作时，你需要小心选择正确的 signed/unsigned 操作。（请注意，对于某些操作，如 addition/subtraction，它是相同的操作；但对于其他操作，例如比较和提取值，您必须特别注意符号。）您可能需要查看 http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml哪些操作需要小心标志。经验法则：在模型中提取实际值总是必须注意符号。

旁注我进一步认为这实际上是 z3 的 C++ API 的缺点。更高级别的 API 实际上可以跟踪签名并自动为您使用正确的操作，而无需最终用户跟踪相同的操作。不幸的是 C/C++ API 不是那么高级。但那是另一天的讨论。

z3::operator- 导致程序终止

z3::operator- causes program to terminate

c++

z3