use z3's internal IntVal

[Wout4]

No description provided.

[IgnaceBleukx]

Are we sure we are not wrapping too many integers to IntVals? It seems to me this is only needed if the integer is used in context with boolean variables? Or am I missing something here?
I guess if we wrap every integer in the expression tree this will cause massive slowdowns? For example with large weighted sums this can be a big problem.

Also: we should add some extra tests for this type mixing. Either we can adapt the test_constraints to create such mixed expressions or we can add a new testsuite creating those expressions.

[tias]

I'm not sure why that explicit conversion is needed for int and not for bool, that is a bit unusual.

However about your question on slowdowns, it seems that z3py actually converts all constants to BoolRef/IntRef itself, e.g. https://z3prover.github.io/api/html/z3py_8py_source.html#l08881

In fact, it does a lot of coercing-checking and context creation and ref creation, and that might already cause some slowdowns for it as we have observed.

I know PySMT has moved from the z3py api to the C APi that z3py converts to, and saw a noticable speed-up.

So it could make sense for us to also be more lower-api mindful, e.g. creating a context, making boolref/intrefs with that context; maybe for n-ary constraints even some calls to the underlying c api directly...

That is obviously not for this PR, or even not a priority at all; just to keep in mind in the future.

So by lack of being able to time it for now, the question remains: do we have a good reason to create intrefs ourselves? (and why then not also boolrefs?) [and if yes, maybe save it the lookup of the global context and make a context and give it to it when creating an intref...]

[Wout4]

The intref is needed to allow sums like Sum(bv, 1, bv) #232
weirdly, z3 does allow Sum(iv,bv,1) (so mixing types is ok but there has to be an intref in the sum for it to recognise the integer.)
the same problem does not exist with boolean constants, so we don't need boolref.

[tias]

OK.

For bonus points you could benchmark whether this change has a runtime penalty, and even whether adding our own context reduces that. But if we just want to move ahead you can merge it as is.

[Wout4]

average runtime of IntVal() is 1*10^-5 seconds, probably checking when we need it and when not will not really lead to speedups. Did not time it with adding our own context