如何在c ++中获取z3表达式的整数值答案

【问题标题】：how to get integer value of a z3 expression in c++如何在c ++中获取z3表达式的整数值
【发布时间】：2021-07-29 10:39:57
【问题描述】：

我这里有这段代码，它在 c++ 中添加了两个 z3 位向量值

expr Z3_LHS=z3_ctx.bv_val(0, 64);
expr Z3_RHS=z3_ctx.bv_val(8, 64);
output=Z3_LHS+Z3_RHS;

当我打印我得到的输出时

bvadd #x0000000000000000 #x0000000000000008

请问我怎样才能得到这个输出表达式的整数值，它应该是 8 而不是这条长线。换句话说，我想将此表达式评估为整数值。

【问题讨论】：

您不应该要求 z3::solver 为该表达式生成模型吗？见this example
非常感谢...我更接近我想要实现的目标。然而，将上面的两个位向量值相加的评估结果给出了 #x0000000000000008 是否有办法将此结果作为 c++ 整数 8 返回
从我粘贴的示例中，您应该从求解器生成的模型中提取它。

标签： c++ z3

【解决方案1】：

这有点奇怪，因为您不会使用 z3 来添加常数。但是，这里是你如何使用 C++ api 编写你想要的代码：

#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(8, 64);
  expr out = lhs+rhs;

  solver s(c);
  cout << s.check() << "\n";
  model m = s.get_model();
  cout << m.eval(out).get_numeral_int64() << "\n";

  return 0;
};

假设你把它放在一个名为 a.cpp 的文件中，我得到的是：

$ g++ -std=c++11 a.cpp -l z3
$ ./a.out
sat
8

【讨论】：

谢谢 :).. 正是我通常想要的那些 lhs 和 rhs 中的 0 和 8 被替换为保存先前评估的 z3 表达式的变量......所以是的，为了简单起见，我把它们作为定义的整数对于我的问题:)