Boolean constants not handled in Global constraints

[peerjosse]

erroneous solvers: ortools, choco, gurobi
working solvers: minizinc, z3

In the following program:

• 3 of the 5 tested solvers gave an error
• 2 of those 3 gave the same error on the same line of canonical_comparison
• ortools gave an error I can't really place

import cpmpy as cp

m = cp.Model()

a = cp.boolvar()
b = cp.boolvar()
c = cp.boolvar()

m += cp.Xor([(cp.Xor([a, b, c])) <= True, ~((cp.Xor([a, b, c])) <= True)])

# m.solve(solver='ortools')     # not supported: model.get_or_make_boolean_index(boolval(True)) (in get_or_make_boolean_index)
# m.solve(solver='minizinc')    # returns no error
# m.solve(solver='z3')          # returns no error
# m.solve(solver='choco')       # lhs cannot be an integer at this point! (in canonical_comparison)
# m.solve(solver='gurobi')      # lhs cannot be an integer at this point! (in canonical_comparison)

[IgnaceBleukx]

So the root-cause of this problem is the simplify_bool transformation that should get rid of any Boolean constants in the expression tree.

In your case:

    Xor([(Xor([a, b, c])) <= True, ~((Xor([a, b, c])) <= True)])
=  Xor([(True False])

Which should be further simplifed to just True.
However, we currently do not support simplification of global constraints in this transformation, and I'm also not really sure to implement this generically....

The error triggered in Choco and Gurobi is quite funny: we decompose the XOR constraint to 1 + 0 == 1 which remains an expression... this also requires more thinking on how to get this correct. Probably should be part of normalization code as well.

I will change the title to reflect the root-cause of the problem better.