铸造Z3整数表达的C / C ++ INT(Casting a Z3 integer express

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

我使用的是Z3 4.0 C / C ++ API。 我声明一个未定义的函数d：（中间体智力）中等 ，添加了一些断言，以及计算的模型。 到目前为止，工作正常。

现在，我想提取由模型定义的函数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 ++诠释？

帮助是非常赞赏。 谢谢！

Answer 1:

Z3_get_numeral_int是你在找什么。

下面是从docummentation的摘录：

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

文章来源: Casting a Z3 integer expression to a C/C++ int