c++ - Z3打印评估结果

Question

在Z3中，我们如何编写程序来获取评估结果？默认情况下，model.eval(expression) 将返回评估结果的另一个表达式。如何将结果分配给特定类型的数据？以下是我想在我的程序中执行的操作。

int a = model.eval(x + 1)  // compiler error

Answer 1

有时模型并不完整。例如，当没有任何东西依赖于 x 的值时，Z3 可能根本不会为其分配任何值，即您可以自由选择适合您的任何值。 eval 函数有第二个参数，当设置为 true 时，将启用模型完成，即 eval 将替换那些不- 关心一些合法值(通常为 0)。

Z3-ints 是实际整数，而不是小于 2^32-1 的 C/C++-ints，因此不会自动执行转换。如果您知道在您的应用程序中这总是可以的，并且 eval 将始终返回一个数字，那么您可以使用 Z3_get_numeral_int执行该转换。