铸造Z3整数EX pression到C / C ++ INT [英] Casting a Z3 integer expression to a C/C++ int

问题描述

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

我使用的是Z3 4.0 C / C ++ API。我宣布一个未定义功能的 D：（智力智力）智力的，增加了一些断言和计算模型。到目前为止，工作正常。

现在，我想提取功能的 D 的由模型定义，说的 D（0,0）的特定值的。下面的语句的工作，但返回的前pression而不是函数值，即，整数的 D（0,0）的

  Z3 :: EXPR ARGS [] = {c.int_val（0），c.int_val（0）};
Z3 :: expr的结果= m.eval（D（2，参数））;
 

在检查

  result.is_int（）;
 

返回真正的

我（希望不是太傻了），问题是如何转换返回前pression到C / C ++ INT？

帮助非常AP preciated。谢谢！

解决方案

<一个href=\"http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga620c6d7e5f7992451bb97743d53afc63\">Z3_get_numeral_int是你在找什么。

下面是从docummentation的摘录：

  Z3_bool Z3_get_numeral_int（__在Z3_context C，__in Z3_ast V，__out为int * I）类似于Z3_get_numeral_string，但只有成功如果该值可以容纳在一个
机INT。返回Z3_TRUE如果调用成功。
 

您应该小心，虽然。 Z3的整数数学整数很容易超过32位int范围。在这个意义上，使用<一个href=\"http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b\">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整数EX pression到C / C ++ INT的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！