Z3打印评估结果

Z3 print evaluation result

本文关键字：结果 评估 打印 Z3      更新时间：2023-10-16

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

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

有时模型并不完整。例如，当什么都不依赖于x的值时，Z3可能根本不会为其分配任何值，即，您可以自由选择适合自己的值。eval函数有第二个参数，当设置为true时，它将启用模型完成，即eval将用一些合法值（通常为0）替换那些不需要的值。

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

相关文章：