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

Question

使用模型对象时，我呼叫func_decl get_func_decl (unsigned i)来获取赋予某个函数（变量）的值。我遇到的问题是将该输出（这是一个func_decl）并将其转换为int。

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

Answer 1

Z3提供了功能Z3_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等

此方法适用于常量（即，元数0的func_decls）。为了得到一个（非零元数）函数定义的项目，下面的函数应使用：

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