将 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();

返回真。

我（希望不要太愚蠢）的问题是如何将返回的表达式转换为 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 并将字符串解析为大整数是更好的选择。