to_cnf 0 + 1 == 1

[ThomSerg]

Most likely related to #778

Reproducable model:

import cpmpy as cp
import numpy as np

def model():
    p = cp.boolvar(name='p')
    a = cp.boolvar(name='a')
    b = cp.boolvar(name='b')
    c = cp.boolvar(name='c')

    constraints = [
        cp.Xor([~((p).implies((cp.Xor([a, b, c]) <= cp.BoolVal(True)))), (p).implies((cp.Xor([a, b, c]) <= cp.BoolVal(True)))]),
    ]
    return cp.Model(constraints)


if __name__ == '__main__':
    m = model()
    from cpmpy.transformations.to_cnf import to_cnf
    to_cnf(m.constraints)

Output:

Traceback (most recent call last):
  File "/home/thomserg/Documents/programming/fuzz-tester/bug.py", line 24, in <module>
    to_cnf(m.constraints)
  File "/home/thomserg/Documents/programming/fuzz-tester/libraries/cpmpy/cpmpy/transformations/to_cnf.py", line 44, in to_cnf
    slv += constraints
  File "/home/thomserg/Documents/programming/fuzz-tester/libraries/cpmpy/cpmpy/solvers/pindakaas.py", line 268, in add
    for cpm_expr in self.transform(cpm_expr_orig):
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/thomserg/Documents/programming/fuzz-tester/libraries/cpmpy/cpmpy/solvers/pindakaas.py", line 251, in transform
    cpm_cons = linearize_constraint(
               ^^^^^^^^^^^^^^^^^^^^^
  File "/home/thomserg/Documents/programming/fuzz-tester/libraries/cpmpy/cpmpy/transformations/linearize.py", line 211, in linearize_constraint
    [cpm_expr] = canonical_comparison([cpm_expr])  # just transforms the constraint, not introducing new ones
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/thomserg/Documents/programming/fuzz-tester/libraries/cpmpy/cpmpy/transformations/linearize.py", line 515, in canonical_comparison
    assert not is_num(lhs), f"lhs cannot be an integer at this point! expr: {cpm_expr}"
           ^^^^^^^^^^^^^^^
AssertionError: lhs cannot be an integer at this point! expr: 0 + 1 == 1

[hbierlee]

I've minimized it to this:

a = cp.boolvar(name="a")
cases += [
    cp.Xor(
        [
            (a > 1),
            (a <= 1),
        ]
    ),
]

I'll have a look why this trips the assert in linearize.

[hbierlee]

Ah, ok, this should be revisited when the linked PR is merged, it might fix this indeed.