Boolean comparison in z3

[IgnaceBleukx]

In CPMpy, a user can write something like this:

a,b = boolvar(shape=2)
(a & b) <= 1 

But this is not supported by the z3 API. Currently, the interface raises the following error: TypeError: '<=' not supported between instances of 'BoolRef' and 'int'. We should catch these cases and translate to the proper boolean expression.

[tias]

It goes a bit further even, including (a & b) <= (a | b) as well as (a & 1) or (a & 0) etc, it is simply much stricter on the Booleanness...

So, to fix in next release... (it can be avoided by writing the constraints more carefully as a user, for now)

[Wout4]

We have a fix for this in pull request #189

[Wout4]

(a & 1), a | 0, etc will also crash linearize.py when using other solvers as an integer is not an expression. Will open a separate issue for that

[Dimosts]

I tried to replicate this issue, and I saw that this is resolved, as pull request #189 was merged. I am closing this.