c++ - 在 s.get_model() 之后从模型中获取整数

Question

在Z3 的 C++ API中，我可以通过以下方式搜索模型

model m = s.get_model();

然后：

cout << m.eval(A);

会给我的价值A。

但是，m.eval(A)返回一个 expr 对象，但我想将A的值作为整数存储在我的程序中。如何将 expr 转换为 int？

Answer 1

这个确切的问题以前曾提出过；也许这些有助于澄清：Q1 Q2

Answer 2

C API 公开了从整数表达式中检索整数值的方法。最通用的 API 是：

/**
   \brief Return numeral value, as a string of a numeric constant term
   \pre Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST
   def_API('Z3_get_numeral_string', STRING, (_in(CONTEXT), _in(AST)))
*/

Z3_string Z3_API Z3_get_numeral_string(__in Z3_context c, __in Z3_ast a);

它返回一个string( char*)。这允许返回 bignums（不适合 64 位的数字）。Z3针对特殊情况
公开了一组其他变体。Z3_get_numeral这些记录在 z3_api.h 中，或参见：http ://research.microsoft.com/en-us/um/redmond/projects/z3/code/group__capi.html

Answer 3

使用 Z3py 的可能示例

x= Int('x')
s = Solver()
s.add(x + 3 == 5)
print s.check()
m = s.model()
print m
y = (m.evaluate(x))
z = y + 4
print simplify(z)

输出：

sat
[x = 2]
6