将 Z3 整数表达式转换为 C/C++ int [英] Casting a Z3 integer expression to a C/C++ int

问题描述

我是 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 结果 = 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)与 Z3_get_numeral_string 类似，但只有在值可以放入一个机器内部如果调用成功，则返回 Z3_TRUE.

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

I'm new to Z3 and searched for the answer to my question here and on Google. Unfortunately, I was not successful.

I'm using the Z3 4.0 C/C++ API. I declared an undefined function d: (Int Int) Int, added some assertions, and computed a model. So far, that works fine.

Now, I want to extract certain values of the function d defined by the model, say d(0,0). The following statement works, but returns an expression rather than the function value, i.e., an integer, of d(0,0).

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

The check

result.is_int();

returns true.

My (hopefully not too stupid) question is how to cast the returned expression to a C/C++ int?

Help is very appreciated. Thank you!

解决方案

Z3_get_numeral_int is what you're looking for.

Here is an excerpt from the 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.

You should be careful though. Z3's integer is mathematical integer which can easily exceed the range of 32-bit int. In that sense, using Z3_get_numeral_string and parsing string to big integer is a better option.

这篇关于将 Z3 整数表达式转换为 C/C++ int的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！