c++ - 将 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并将字符串解析为大整数是一个更好的选择。