More differences with z3 API

[user202729]

• evaluate(x) returns the result in a different context than x
• cvc5.pythonic.Model is not defined, unlike z3.Model
• operator ~ does not work on boolean expression, need to use Not(...)

[alex-ozdemir]

Hi,

Thank you for this inconsistency report.

I'm working on addressing it here: #103. It's is clear what do to about the inconsistency in operator overloading, but for the other issues I could use some more information from you:

1. Could you give an example of how the different between the context of
   evaluate(x) and x is a problem for you?

   I ask because cvc5 and z3 contexts work differently. I'll need to understand
   your use case better to determine the correct fix.

2. Could you give an example of how you want to use the Model function? Again,
   z3 and cvc5 models work somewhat differently, so I need to understand your
   use case better to determine the correct fix.

Cheers,
Alex

[user202729]

In [3]: from cvc5.pythonic import evaluate, BitVecVal

In [4]: BitVecVal(2, 32) + BitVecVal(3, 32)
Out[4]: 2 + 3

In [5]: evaluate(BitVecVal(2, 32) + BitVecVal(3, 32))
Out[5]: 5

In [6]: evaluate(BitVecVal(2, 32) + BitVecVal(3, 32)) + BitVecVal(4, 32)
SMTException: Context mismatch

In [7]: from z3 import Model, BitVecVal

In [8]: Model().evaluate(BitVecVal(2, 32) + BitVecVal(3, 32))
Out[8]: 5

My use case is quite simple, just the above.

Basically because expressions that are "trivially constant" are not simplified to a single constant I need to simplify them somehow. At least simplify works, but the problem is simplify is slower than evaluate in z3 so ideally both can work the same way…

[alex-ozdemir]

Hi,

Thank you for the example of how cvc5.python.evaluate is misbehaving. I've
added a patch for it to the PR above.

I'm still a bit confused about your use-case for Model. Do you only use it to
do evaluation, or also for other things? I ask because I'm considering just not
supporting it (and documenting the non-support), but if there are other
use-cases then supporting it might be important.

Cheers,
Alex

[user202729]

Yes, I used it only for evaluation… for comparison z3 doesn't have z3.evaluate, so it's not entirely unreasonable to not be able to find that one.

It doesn't seem too difficult to have Model() return a dummy object whose evaluate is the evaluation function either… for the sake of z3 compatibility.

[alex-ozdemir]

It doesn't seem too difficult to have Model() return a dummy object whose evaluate is the evaluation function either… for the sake of z3 compatibility.

This is a good approach, and we'll follow it.

Anyways, that resolves the last question then. We'll merge the PR as soon as we can review it.

[alex-ozdemir]

@user202729 The PR has been merged. Let us know if you encounter other problems.