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

Casting a Z3 integer expression to a C/C++ int

本文关键字：整数 转换 C++ Z3 表达式      更新时间：2023-10-16

我是Z3的新手，在这里和谷歌上搜索问题的答案。不幸的是，我没有成功。

我使用的是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？

非常感谢您的帮助。非常感谢。

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位整数的范围。从这个意义上说，使用Z3_get_numeral_string并将字符串解析为大整数是一个更好的选择。

相关文章：