diff --git a/cpmpy/expressions/__init__.py b/cpmpy/expressions/__init__.py index be6fd4647..6163eca2e 100644 --- a/cpmpy/expressions/__init__.py +++ b/cpmpy/expressions/__init__.py @@ -21,10 +21,9 @@ # others need to be imported by the developer explicitely from .variables import boolvar, intvar, cpm_array from .variables import BoolVar, IntVar, cparray # Old, to be deprecated -from .globalconstraints import AllDifferent, AllDifferentExcept0, AllEqual, Circuit, Inverse, Table, Xor, Cumulative, \ - IfThenElse, GlobalCardinalityCount, DirectConstraint, InDomain, Increasing, Decreasing, IncreasingStrict, \ - DecreasingStrict, Precedence, NoOverlap - +from .globalconstraints import AllDifferent, AllDifferentExcept0, AllDifferentLists, AllEqual, Circuit, Inverse, Table, Xor, Cumulative, \ + IfThenElse, GlobalCardinalityCount, DirectConstraint, InDomain, Increasing, Decreasing, IncreasingStrict, DecreasingStrict, + LexLess, LexLessEq, LexChainLess, LexChainLessEq, Precedence, NoOverlap from .globalconstraints import alldifferent, allequal, circuit # Old, to be deprecated from .globalfunctions import Maximum, Minimum, Abs, Element, Count, NValue, NValueExcept from .core import BoolVal diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index a7f9bbabc..b0d4f063d 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -98,6 +98,7 @@ def my_circuit_decomp(self): AllDifferent AllDifferentExcept0 + AllDifferentLists AllEqual Circuit Inverse @@ -196,6 +197,33 @@ def value(self): vals = [argval(a) for a in self.args if argval(a) != 0] return len(set(vals)) == len(vals) + +class AllDifferentLists(GlobalConstraint): + """ + Ensures none of the lists given are exactly the same. + Called 'lex_alldifferent' in the global constraint catalog: + https://sofdem.github.io/gccat/gccat/Clex_alldifferent.html#uid24923 + """ + def __init__(self, lists): + if any(not is_any_list(lst) for lst in lists): + raise TypeError(f"AllDifferentLists expects a list of lists, but got {lists}") + if any(len(lst) != len(lists[0]) for lst in lists): + raise ValueError("Lists should have equal length, but got these lengths:", list(map(len, lists))) + super().__init__("alldifferent_lists", [flatlist(lst) for lst in lists]) + + def decompose(self): + """Returns the decomposition + """ + from .python_builtins import any as cpm_any + constraints = [] + for lst1, lst2 in all_pairs(self.args): + constraints += [cpm_any(var1 != var2 for var1, var2 in zip(lst1, lst2))] + return constraints, [] + + def value(self): + lst_vals = [tuple(argvals(a)) for a in self.args] + return len(set(lst_vals)) == len(self.args) + def allequal(args): warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) return AllEqual(*args) # unfold list as individual arguments @@ -605,9 +633,8 @@ def decompose(self): return [args[i] <= args[i+1] for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all(args[i].value() <= args[i+1].value() for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] <= args[i+1] for i in range(len(args)-1)) class Decreasing(GlobalConstraint): @@ -628,9 +655,8 @@ def decompose(self): return [args[i] >= args[i+1] for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all(args[i].value() >= args[i+1].value() for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] >= args[i+1] for i in range(len(args)-1)) class IncreasingStrict(GlobalConstraint): @@ -651,9 +677,8 @@ def decompose(self): return [args[i] < args[i+1] for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all((args[i].value() < args[i+1].value()) for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] < args[i+1] for i in range(len(args)-1)) class DecreasingStrict(GlobalConstraint): @@ -674,9 +699,134 @@ def decompose(self): return [(args[i] > args[i+1]) for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all((args[i].value() > args[i+1].value()) for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] > args[i+1] for i in range(len(args)-1)) + + +class LexLess(GlobalConstraint): + """ Given lists X,Y, enforcing that X is lexicographically less than Y. + """ + def __init__(self, list1, list2): + X = flatlist(list1) + Y = flatlist(list2) + if len(X) != len(Y): + raise CPMpyException(f"The 2 lists given in LexLess must have the same size: X length is {len(X)} and Y length is {len(Y)}") + super().__init__("lex_less", [X, Y]) + + def decompose(self): + """ + Implementation inspired by Hakan Kjellerstrand (http://hakank.org/cpmpy/cpmpy_hakank.py) + + The decomposition creates auxiliary Boolean variables and constraints that + collectively ensure X is lexicographically less than Y + The auxiliary boolean vars are defined to represent if the given lists are lexicographically ordered + (less or equal) up to the given index. + Decomposition enforces through the constraining part that the first boolean variable needs to be true, and thus + through the defining part it is enforced that if it is not strictly lexicographically less in a given index, + then next index must be lexicographically less or equal. It needs to be strictly less in at least one index. + + The use of auxiliary Boolean variables bvar ensures that the constraints propagate immediately, + maintaining arc-consistency. Each bvar[i] enforces the lexicographic ordering at each position, ensuring that + every value in the domain of X[i] can be extended to a consistent value in the domain of $Y_i$ for all + subsequent positions. + """ + X, Y = cpm_array(self.args) + + bvar = boolvar(shape=(len(X) + 1)) + + # Constraint ensuring that each element in X is less than or equal to the corresponding element in Y, + # until a strict inequality is encountered. + defining = [bvar == ((X <= Y) & ((X < Y) | bvar[1:]))] + # enforce the last element to be true iff (X[-1] < Y[-1]), enforcing strict lexicographic order + defining.append(bvar[-1] == (X[-1] < Y[-1])) + constraining = [bvar[0]] + + return constraining, defining + + def value(self): + X, Y = argvals(self.args) + return any((X[i] < Y[i]) & all(X[j] <= Y[j] for j in range(i)) for i in range(len(X))) + + +class LexLessEq(GlobalConstraint): + """ Given lists X,Y, enforcing that X is lexicographically less than Y (or equal). + """ + def __init__(self, list1, list2): + X = flatlist(list1) + Y = flatlist(list2) + if len(X) != len(Y): + raise CPMpyException(f"The 2 lists given in LexLessEq must have the same size: X length is {len(X)} and Y length is {len(Y)}") + super().__init__("lex_lesseq", [X, Y]) + + def decompose(self): + """ + Implementation inspired by Hakan Kjellerstrand (http://hakank.org/cpmpy/cpmpy_hakank.py) + + The decomposition creates auxiliary Boolean variables and constraints that + collectively ensure X is lexicographically less than Y + The auxiliary boolean vars are defined to represent if the given lists are lexicographically ordered + (less or equal) up to the given index. + Decomposition enforces through the constraining part that the first boolean variable needs to be true, and thus + through the defining part it is enforced that if it is not strictly lexicographically less in a given index, + then next index must be lexicographically less or equal. + + The use of auxiliary Boolean variables bvar ensures that the constraints propagate immediately, + maintaining arc-consistency. Each bvar[i] enforces the lexicographic ordering at each position, ensuring that + every value in the domain of X[i] can be extended to a consistent value in the domain of $Y_i$ for all + subsequent positions. + """ + X, Y = cpm_array(self.args) + + bvar = boolvar(shape=(len(X) + 1)) + defining = [bvar == ((X <= Y) & ((X < Y) | bvar[1:]))] + defining.append(bvar[-1] == (X[-1] <= Y[-1])) + constraining = [bvar[0]] + + return constraining, defining + + def value(self): + X, Y = argvals(self.args) + return any((X[i] < Y[i]) & all(X[j] <= Y[j] for j in range(i)) for i in range(len(X))) | all(X[i] == Y[i] for i in range(len(X))) + + +class LexChainLess(GlobalConstraint): + """ Given a matrix X, LexChainLess enforces that all rows are lexicographically ordered. + """ + def __init__(self, X): + # Ensure the numpy array is 2D + X = cpm_array(X) + assert X.ndim == 2, "Input must be a 2D array or a list of lists" + super().__init__("lex_chain_less", X.tolist()) + + def decompose(self): + """ Decompose to a series of LexLess constraints between subsequent rows + """ + X = self.args + return [LexLess(prev_row, curr_row) for prev_row, curr_row in zip(X, X[1:])], [] + + def value(self): + X = argvals(self.args) + return all(LexLess(prev_row, curr_row).value() for prev_row, curr_row in zip(X, X[1:])) + + +class LexChainLessEq(GlobalConstraint): + """ Given a matrix X, LexChainLessEq enforces that all rows are lexicographically ordered. + """ + def __init__(self, X): + # Ensure the numpy array is 2D + X = cpm_array(X) + assert X.ndim == 2, "Input must be a 2D array or a list of lists" + super().__init__("lex_chain_lesseq", X.tolist()) + + def decompose(self): + """ Decompose to a series of LexLessEq constraints between subsequent rows + """ + X = self.args + return [LexLessEq(prev_row, curr_row) for prev_row, curr_row in zip(X, X[1:])], [] + + def value(self): + X = argvals(self.args) + return all(LexLessEq(prev_row, curr_row).value() for prev_row, curr_row in zip(X, X[1:])) class DirectConstraint(Expression): diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index d1076ddd1..7bec63adc 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -314,12 +314,11 @@ def transform(self, cpm_expr): cpm_cons = toplevel_list(cpm_expr) supported = {"min", "max", "abs", "count", "element", "alldifferent", "alldifferent_except0", "allequal", "table", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue", "increasing", - "precedence", - "decreasing","strictly_increasing","strictly_decreasing"} - + "precedence","decreasing","strictly_increasing","strictly_decreasing","lex_lesseq", "lex_less"} + # choco supports reification of any constraint, but has a bug in increasing and decreasing supported_reified = {"min", "max", "abs", "count", "element", "alldifferent", "alldifferent_except0", - "allequal", "table", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue"} + "allequal", "table", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue","lex_lesseq", "lex_less"} # for when choco new release comes, fixing the bug on increasing and decreasing #supported_reified = supported cpm_cons = decompose_in_tree(cpm_cons, supported, supported_reified) @@ -498,7 +497,7 @@ def _get_constraint(self, cpm_expr): elif isinstance(cpm_expr, GlobalConstraint): # many globals require all variables as arguments - if cpm_expr.name in {"alldifferent", "alldifferent_except0", "allequal", "circuit", "inverse","increasing","decreasing","strictly_increasing","strictly_decreasing"}: + if cpm_expr.name in {"alldifferent", "alldifferent_except0", "allequal", "circuit", "inverse","increasing","decreasing","strictly_increasing","strictly_decreasing","lex_lesseq","lex_less"}: chc_args = self._to_vars(cpm_expr.args) if cpm_expr.name == 'alldifferent': return self.chc_model.all_different(chc_args) @@ -518,6 +517,13 @@ def _get_constraint(self, cpm_expr): return self.chc_model.increasing(chc_args,1) elif cpm_expr.name == "strictly_decreasing": return self.chc_model.decreasing(chc_args,1) + elif cpm_expr.name in ["lex_lesseq", "lex_less"]: + if cpm_expr.name == "lex_lesseq": + return self.chc_model.lex_less_eq(*chc_args) + return self.chc_model.lex_less(*chc_args) +# Ready for when it is fixed in pychoco (https://github.com/chocoteam/pychoco/issues/30) +# elif cpm_expr.name == "lex_chain_less": +# return self.chc_model.lex_chain_less(chc_args) # but not all elif cpm_expr.name == 'table': diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index d488c7826..2d2b11cce 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -34,7 +34,7 @@ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import MinizincNameException, MinizincBoundsException from ..expressions.core import Expression, Comparison, Operator, BoolVal -from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar +from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar, cpm_array from ..expressions.globalconstraints import DirectConstraint from ..expressions.utils import is_num, is_any_list, eval_comparison, argvals, argval from ..transformations.decompose_global import decompose_in_tree @@ -418,9 +418,10 @@ def transform(self, cpm_expr): """ cpm_cons = toplevel_list(cpm_expr) supported = {"min", "max", "abs", "element", "count", "nvalue", "alldifferent", "alldifferent_except0", "allequal", - "inverse", "ite" "xor", "table", "cumulative", "circuit", "gcc", "increasing", + "inverse", "ite" "xor", "table", "cumulative", "circuit", "gcc", "increasing","decreasing", "precedence","no_overlap", - "decreasing","strictly_increasing","strictly_decreasing"} + "strictly_increasing", "strictly_decreasing", "lex_lesseq", "lex_less", "lex_chain_less", + "lex_chain_lesseq"} return decompose_in_tree(cpm_cons, supported, supported_reified=supported - {"circuit", "precedence"}) @@ -504,6 +505,20 @@ def zero_based(array): args_str = [self._convert_expression(e) for e in expr.args] return "alldifferent_except_0([{}])".format(",".join(args_str)) + if expr.name in ["lex_lesseq", "lex_less"]: + X = [self._convert_expression(e) for e in expr.args[0]] + Y = [self._convert_expression(e) for e in expr.args[1]] + return f"{expr.name}({{}}, {{}})".format(X, Y) + + + if expr.name in ["lex_chain_less", "lex_chain_lesseq"]: + X = cpm_array([[self._convert_expression(e) for e in row] for row in expr.args]) + str_X = "[|\n" # opening + for row in X.T: # Minizinc enforces lexicographic order on columns + str_X += ",".join(map(str, row)) + " |" # rows + str_X += "\n|]" # closing + return f"{expr.name}({{}})".format(str_X) + args_str = [self._convert_expression(e) for e in expr.args] # standard expressions: comparison, operator, element if isinstance(expr, Comparison): diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index 2f03726c8..79228d0a9 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -79,7 +79,7 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to _toplevel.extend(define) # definitions should be added toplevel # the `decomposed` expression might contain other global constraints, check it - decomposed = decompose_in_tree(decomposed, supported, supported_reified, [], nested=nested) + decomposed = decompose_in_tree(decomposed, supported, supported_reified, _toplevel, nested=nested) newlist.append(all(decomposed)) else: @@ -146,7 +146,7 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to return toplevel_list(newlist) else: # we are toplevel and some new constraints are introduced, decompose new constraints! - return toplevel_list(newlist) + decompose_in_tree(_toplevel, supported, supported_reified, nested=False) + return toplevel_list(newlist) + decompose_in_tree(toplevel_list(_toplevel), supported, supported_reified, nested=False) # DEPRECATED! diff --git a/cpmpy/transformations/normalize.py b/cpmpy/transformations/normalize.py index c69ac77cb..b5cf35d17 100644 --- a/cpmpy/transformations/normalize.py +++ b/cpmpy/transformations/normalize.py @@ -124,6 +124,8 @@ def simplify_boolean(lst_of_expr, num_context=False): """ if is_boolexpr(lhs) and is_num(rhs): # direct simplification of boolean comparisons + if isinstance(rhs, BoolVal): + rhs = int(rhs.value()) # ensure proper comparisons below if rhs < 0: newlist.append(BoolVal(name in {"!=", ">", ">="})) # all other operators evaluate to False elif rhs == 0: diff --git a/tests/test_constraints.py b/tests/test_constraints.py index d34c276c0..e32d5b9a8 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -14,11 +14,12 @@ ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint # Exclude some global constraints for solvers - NUM_GLOBAL = { - "AllEqual", "AllDifferent", "AllDifferentExcept0" , "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", - "Increasing", "IncreasingStrict", "Decreasing", "DecreasingStrict", + "AllEqual", "AllDifferent", "AllDifferentLists", "AllDifferentExcept0", + "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", + "Increasing", "IncreasingStrict", "Decreasing", "DecreasingStrict", "Precedence", "Cumulative", "NoOverlap", + "LexLess", "LexLessEq", "LexChainLess", "LexChainLessEq", # also global functions "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", "NValueExcept" } @@ -170,7 +171,7 @@ def global_constraints(solver): """ Generate all global constraints - AllDifferent, AllEqual, Circuit, Minimum, Maximum, Element, - Xor, Cumulative, NValue, Count + Xor, Cumulative, NValue, Count, Increasing, Decreasing, IncreasingStrict, DecreasingStrict, LexLessEq, LexLess """ classes = inspect.getmembers(cpmpy.expressions.globalconstraints, inspect.isclass) classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalConstraint) and name != "GlobalConstraint"] @@ -207,14 +208,35 @@ def global_constraints(solver): vals = [1, 2, 3] cnts = intvar(0,10,shape=3) expr = cls(NUM_ARGS, vals, cnts) + elif name == "LexLessEq": + X = intvar(0, 3, shape=3) + Y = intvar(0, 3, shape=3) + expr = LexLessEq(X, Y) + + elif name == "LexLess": + X = intvar(0, 3, shape=3) + Y = intvar(0, 3, shape=3) + expr = LexLess(X, Y) + + elif name == "LexChainLess": + X = intvar(0, 3, shape=(3,3)) + expr = LexChainLess(X) + + elif name == "LexChainLessEq": + X = intvar(0, 3, shape=(3,3)) + expr = LexChainLess(X) + elif name == "AllDifferentLists": + vars = intvar(0,10, shape=(3,4)) + expr = cls(vars) else: # default constructor, list of numvars - expr= cls(NUM_ARGS) + expr= cls(NUM_ARGS) if solver in EXCLUDE_GLOBAL and name in EXCLUDE_GLOBAL[solver]: continue else: yield expr + def reify_imply_exprs(solver): """ - Reification (double implication): Boolexpr == Var (CPMpy class 'Comparison') diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index b86b47f86..c0cbc8bf9 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -55,6 +55,26 @@ def test_alldifferent2(self): var._value = val assert (c.value() == oracle), f"Wrong value function for {vals,oracle}" + def test_alldifferent_lists(self): + # test known input/outputs + tuples = [ + ([(1,2,3),(1,3,3),(1,2,4)], True), + ([(1,2,3),(1,3,3),(1,2,3)], False), + ([(0,0,3),(1,3,3),(1,2,4)], True), + ([(1,2,3),(1,3,3),(3,3,3)], True) + ] + iv = cp.intvar(0,4, shape=(3,3)) + c = cp.AllDifferentLists(iv) + for (vals, oracle) in tuples: + ret = cp.Model(c, iv == vals).solve() + assert (ret == oracle), f"Mismatch solve for {vals,oracle}" + # don't try this at home, forcibly overwrite variable values (so even when ret=false) + for (var,val) in zip(iv,vals): + for (vr, vl) in zip(var, val): + vr._value = vl + assert (c.value() == oracle), f"Wrong value function for {vals,oracle}" + + def test_not_alldifferent(self): # from fuzztester of Ruben Kindt, #143 pos = cp.intvar(lb=0, ub=5, shape=3, name="positions") @@ -253,6 +273,78 @@ def test_InDomain(self): self.assertTrue(model.solve()) self.assertIn(bv.value(), vals) + def test_lex_lesseq(self): + from cpmpy import BoolVal + X = cp.intvar(0, 3, shape=10) + c1 = X[:-1] == 1 + Y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + c = cp.LexLessEq(X, Y) + c2 = c != (BoolVal(True)) + m = cp.Model([c1, c2]) + self.assertTrue(m.solve()) + self.assertTrue(c2.value()) + self.assertFalse(c.value()) + + Y = cp.intvar(0, 0, shape=10) + c = cp.LexLessEq(X, Y) + m = cp.Model(c) + self.assertTrue(m.solve("ortools")) + from cpmpy.expressions.utils import argval + self.assertTrue(sum(argval(X)) == 0) + + def test_lex_less(self): + from cpmpy import BoolVal + X = cp.intvar(0, 3, shape=10) + c1 = X[:-1] == 1 + Y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + c = cp.LexLess(X, Y) + c2 = c != (BoolVal(True)) + m = cp.Model([c1, c2]) + self.assertTrue(m.solve()) + self.assertTrue(c2.value()) + self.assertFalse(c.value()) + + Y = cp.intvar(0, 0, shape=10) + c = cp.LexLess(X, Y) + m = cp.Model(c) + self.assertFalse(m.solve("ortools")) + + Z = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1] + c = cp.LexLess(X, Z) + m = cp.Model(c) + self.assertTrue(m.solve("ortools")) + from cpmpy.expressions.utils import argval + self.assertTrue(sum(argval(X)) == 0) + + + def test_lex_chain(self): + from cpmpy import BoolVal + X = cp.intvar(0, 3, shape=10) + c1 = X[:-1] == 1 + Y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + c = cp.LexChainLess([X, Y]) + c2 = c != (BoolVal(True)) + m = cp.Model([c1, c2]) + self.assertTrue(m.solve()) + self.assertTrue(c2.value()) + self.assertFalse(c.value()) + + Y = cp.intvar(0, 0, shape=10) + c = cp.LexChainLessEq([X, Y]) + m = cp.Model(c) + self.assertTrue(m.solve("ortools")) + from cpmpy.expressions.utils import argval + self.assertTrue(sum(argval(X)) == 0) + + Z = cp.intvar(0, 1, shape=(3,2)) + c = cp.LexChainLess(Z) + m = cp.Model(c) + self.assertTrue(m.solve()) + self.assertTrue(sum(argval(Z[0])) == 0) + self.assertTrue(sum(argval(Z[1])) == 1) + self.assertTrue(sum(argval(Z[2])) >= 1) + + def test_indomain_onearg(self): iv = cp.intvar(0, 10) diff --git a/tests/test_trans_simplify.py b/tests/test_trans_simplify.py index b44c980ef..454e0c0f7 100644 --- a/tests/test_trans_simplify.py +++ b/tests/test_trans_simplify.py @@ -100,3 +100,11 @@ def test_with_floats(self): self.assertEqual(str(self.transform(expr)), '[(iv[0]) == (iv[1])]') + def test_nested_boolval(self): + + bv = cp.boolvar(name="bv") + x = cp.intvar(0, 3, name="x") + cons = (x == 2) == (bv == 4) + self.assertEquals(str(self.transform(cons)), "[x != 2]") + self.assertTrue(cp.Model(cons).solve()) +