CODEWITHSUNDEEP
c++cz3
Jes
Jes

Reputation: 2694

Z3 print evaluation result

In Z3, how can we write a program to get the result from evaluation? By default model.eval(expression) will return another expression of the evaluation result. How can I assign the result to a type-specific data? Below is what I want to do in my program.

int a = model.eval(x + 1)  // compiler error

Upvotes: 2

Views: 1128

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

Sometimes models are not complete. For instance, when nothing depends on the value of x, then Z3 may not assign any value at all to it, i.e., you're free to chose whatever value suits you. The eval function has a second argument, which, when set to true, will enable model completion, i.e., eval will substitute those don't-cares with some legal value (often 0).

Z3-ints are actual integers, not C/C++-ints smaller than 2^32-1, so the conversion is not performed automatically. If you know that in your application this will always be ok, and that eval will always return a numeral, then you can use Z3_get_numeral_int to perform that conversion.

Upvotes: 1

Related Questions