z3 - 如何将变量的值转换为模型中的 int？

Question

使用模型对象时，我调用func_decl get_func_decl (unsigned i)以获取分配给某个函数（变量）的值。我遇到的问题是将其输出（即 a func_decl）并将其转换为int.

例如，如果模型是{x |-> 4, y |-> 12, z |-> 6}，我想获得这 3 个变量（和）的实际int值。4126

Answer 1

Z3Z3_get_numeral_int为此提供了功能：

Z3_bool Z3_API Z3_get_numeral_int(__in Z3_context c, __in Z3_ast v, __out int* i);

请注意，最后一个参数指向一个整数，如果调用成功，它将用正确的值填充（对于非数字或不能表示为 int 的数字，它将失败）。

还调用了其他函数Z3_get_numeral_*来获取不同类型的值，例如 uint64 等。

此方法适用于常量（即 func_decls of arity 0）。要获取（非零元）函数定义的条目，应使用以下函数：

Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i);