Repository: CPMpy/cpmpy

Issue:
linearization of modulo fails with constants.
The current implementation of linearize handles the modulo when 2 variables are present, it however crashes when there is only one variable, like in the example below:

```
m = Model()
m += x1 % 2 == 0
print(m.solve('gurobi'))
```

I think we should also add a case where the rhs is a constant, which will simplify the linearization, and also allows us to linearize modulo (or division but still in a pr) even when the solver does not support multiplication of 2 variables.

Discussion:
@OrestisLomis: What if the lhs would be constant and the rhs a variable?@Wout4: pretty sure the expression will always be on the left during linearization@IgnaceBleukx: Closed after #581 and #516 

Solution patch:
diff --git a/cpmpy/transformations/linearize.py b/cpmpy/transformations/linearize.py
index 317d0d20..7d5379c0 100644
--- a/cpmpy/transformations/linearize.py
+++ b/cpmpy/transformations/linearize.py
@@ -48,7 +48,7 @@ from ..exceptions import TransformationNotImplementedError
 
 from ..expressions.core import Comparison, Operator, BoolVal
 from ..expressions.globalconstraints import GlobalConstraint, DirectConstraint
-from ..expressions.utils import is_num, eval_comparison, get_bounds
+from ..expressions.utils import is_num, eval_comparison, get_bounds, is_true_cst, is_false_cst
 
 from ..expressions.variables import _BoolVarImpl, boolvar, NegBoolView, _NumVarImpl, intvar
 
@@ -157,7 +157,13 @@ def linearize_constraint(lst_of_expr, supported={"sum","wsum"}, reified=False):
                                                       "Please safen the expression first.")
                         k = intvar(*get_bounds((x - rhs) // y))
                         mult_res, newcons = get_or_make_var(k * y)
-                        newlist += linearize_constraint([rhs < abs(y)]+newcons, supported, reified=reified)
+                        remainder = rhs < abs(y)
+                        if is_true_cst(remainder):
+                            remainder = BoolVal(True)
+                        elif is_false_cst(remainder):
+                            remainder = BoolVal(False)
+                        newcons.append(remainder)
+                        newlist += linearize_constraint(newcons, supported, reified=reified)
 
                         cpm_expr = (mult_res + rhs) == x
 


Test patch:
diff --git a/tests/test_constraints.py b/tests/test_constraints.py
index 10b98b4c..195bc42b 100644
--- a/tests/test_constraints.py
+++ b/tests/test_constraints.py
@@ -40,10 +40,10 @@ EXCLUDE_GLOBAL = {"pysat": NUM_GLOBAL,
 
 # Exclude certain operators for solvers.
 # Not all solvers support all operators in CPMpy
-EXCLUDE_OPERATORS = {"gurobi": {"mod"},
+EXCLUDE_OPERATORS = {"gurobi": {},
                      "pysat": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"},
                      "pysdd": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"},
-                     "exact": {"mod","div"},
+                     "exact": {'div'},
                      }
 
 # Variables to use in the rest of the test script
diff --git a/tests/test_trans_linearize.py b/tests/test_trans_linearize.py
index b49304af..2ff7e275 100644
--- a/tests/test_trans_linearize.py
+++ b/tests/test_trans_linearize.py
@@ -118,11 +118,21 @@ class TestTransLinearize(unittest.TestCase):
         n_sols = cp.Model(lincons).solveAll(display=cb)
         self.assertEqual(n_sols, 3 * 2 * 1) # 1 and 3 not allowed
 
+    def test_issue_580(self):
+        x = cp.intvar(1, 5, name='x')
+        lin_mod = linearize_constraint([x % 2 == 0], supported={"mul","sum", "wsum"})
+        self.assertEqual(str(lin_mod), '[sum([2, -1] * [IV5, IV6]) == 0, boolval(True), sum([1, -1] * [IV6, x]) == 0]')
+
+        lin_mod = linearize_constraint([x % 2 <= 0], supported={"mul", "sum", "wsum"})
+        self.assertEqual(str(lin_mod), '[IV7 <= 0, sum([2, -1] * [IV8, IV9]) == 0, sum([IV7]) <= 1, sum([1, 1, -1] * [IV9, IV7, x]) == 0]')
+
+        lin_mod = linearize_constraint([x % 2 == 1], supported={"mul", "sum", "wsum"})
+        self.assertEqual(str(lin_mod), '[sum([2, -1] * [IV10, IV11]) == 0, boolval(True), sum([1, -1] * [IV11, x]) == -1]')
 
 
 class TestConstRhs(unittest.TestCase):
 
-    def  test_numvar(self):
+    def test_numvar(self):
         a, b = [cp.intvar(0, 10, name=n) for n in "ab"]
 
         cons = linearize_constraint([a <= b])[0]
@@ -336,3 +346,4 @@ class testCanonical_comparison(unittest.TestCase):
         a, b, c, x, y = [cp.boolvar(name=n) for n in "abc"] + [cp.intvar(0, 3, name=n) for n in "xy"]
         only_pos = only_positive_coefficients([Operator("wsum",[[1,1,-1,1,-1],[a,b,c,x,y]]) > 0])
         self.assertEqual(str([Operator("wsum",[[1,1,1,1,-1],[a,b,~c,x,y]]) > 1]), str(only_pos))
+