将Z3整数表达式转换为C/C++ int

Question

我是Z3的新手,在这里和Google上搜索了我的问题的答案.不幸的是,我没有成功.

我正在使用Z3 4.0 C/C++ API.我声明了一个未定义的函数d:(Int Int)Int,添加了一些断言,并计算了一个模型.到目前为止,这很好.

现在,我想提取模型定义的函数d的某些值,比如d(0,0).以下语句有效,但返回表达式而不是函数值,即d(0,0)的整数.

z3::expr args[] = {c.int_val(0), c.int_val(0)};
z3::expr result = m.eval(d(2, args));

支票

result.is_int();

返回true.

我的(希望不是太愚蠢)问题是如何将返回的表达式转换为C/C++ int？

非常感谢帮助.谢谢!

Answer 1

Z3_get_numeral_int正是您要找的.

以下是文档摘录的摘录:

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

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a 
machine int. Return Z3_TRUE if the call succeeded.

你应该小心.Z3的整数是数学整数,很容易超过32位int的范围.从这个意义上说,使用Z3_get_numeral_string并将字符串解析为大整数是一个更好的选择.