From ab97945ede2a2ecfc11e0c1eeae7578f335ff439 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 08:58:28 +0200 Subject: [PATCH 1/7] call simplify_bool after decompose of xor --- cpmpy/expressions/globalconstraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 2be5c53d4..ced328b31 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -658,7 +658,7 @@ def decompose(self): decomp = [sum(self.args[:2]) == 1] if len(self.args) > 2: decomp = Xor([decomp,self.args[2:]]).decompose()[0] - return decomp, [] + return cp.transformations.normalize.simplify_boolean(decomp), [] def value(self): return sum(argvals(self.args)) % 2 == 1 From b8184d161f0570c05423674a684fc25ac1cd9855 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 08:59:13 +0200 Subject: [PATCH 2/7] update tests --- tests/test_constraints.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index d2d1cada8..4276769af 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -196,6 +196,7 @@ def global_constraints(solver): if name == "Xor": yield Xor(BOOL_ARGS) yield Xor(BOOL_ARGS + [True,False]) + yield Xor([True, BOOL_ARGS[0]]) continue elif name == "Inverse": expr = cls(NUM_ARGS, [1,0,2]) From ac13e6dfdd63f28d3c4730284086cf7d222339cb Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 09:08:16 +0200 Subject: [PATCH 3/7] simplify trivial comparisons --- cpmpy/transformations/normalize.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/cpmpy/transformations/normalize.py b/cpmpy/transformations/normalize.py index f45e4401c..abc416390 100644 --- a/cpmpy/transformations/normalize.py +++ b/cpmpy/transformations/normalize.py @@ -9,7 +9,7 @@ from ..expressions.core import BoolVal, Expression, Comparison, Operator from ..expressions.globalfunctions import GlobalFunction -from ..expressions.utils import eval_comparison, is_false_cst, is_true_cst, is_boolexpr, is_num, is_bool +from ..expressions.utils import eval_comparison, is_false_cst, is_true_cst, is_boolexpr, is_num, is_bool, get_bounds from ..expressions.variables import NDVarArray, _BoolVarImpl from ..exceptions import NotSupportedError from ..expressions.globalconstraints import GlobalConstraint @@ -169,6 +169,13 @@ def simplify_boolean(lst_of_expr, num_context=False): elif isinstance(expr, Comparison): lhs, rhs = simplify_boolean(expr.args, num_context=True) name = expr.name + if all(eval_comparison(expr.name, x,y) for x in get_bounds(lhs) for y in get_bounds(rhs)): + newlist.append(1 if num_context else BoolVal(True)) + continue + if not any(eval_comparison(expr.name, x,y) for x in get_bounds(lhs) for y in get_bounds(rhs)): + newlist.append(0 if num_context else BoolVal(False)) + continue + if is_num(lhs) and is_boolexpr(rhs): # flip arguments of comparison to reduct nb of cases if name == "<": name = ">" elif name == ">": name = "<" From 0b1aa52b8f936428f0e26de8c37eda66d609c46d Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 09:11:10 +0200 Subject: [PATCH 4/7] update test --- tests/test_globalconstraints.py | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index 2b8c8e20e..309b6d53d 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -721,6 +721,23 @@ def test_xor_with_constants(self): self.assertFalse(cp.Model(cp.Xor([False, False])).solve()) self.assertFalse(cp.Model(cp.Xor([False, False, False])).solve()) + def test_issue_620(self): + a = cp.boolvar() + b = cp.boolvar() + c = cp.boolvar() + + model = cp.Model(cp.Xor([(cp.Xor([a, b, c])) <= True, ~((cp.Xor([a, b, c])) <= True)])) + + self.assertTrue(model.solve(solver='ortools')) + if "minizinc" in cp.SolverLookup.supported(): + self.assertTrue(model.solve(solver='minizinc')) + if "z3" in cp.SolverLookup.supported(): + self.assertTrue(model.solve(solver='z3')) + if "choco" in cp.SolverLookup.supported(): + self.assertTrue(model.solve(solver='choco')) + if "gurobi" in cp.SolverLookup.supported(): + self.assertTrue(model.solve(solver='gurobi')) + def test_ite_with_constants(self): x,y,z = cp.boolvar(shape=3) expr = cp.IfThenElse(True, y, z) From c86bb735abf1fe359fa10dea6018e98573665443 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 16:47:23 +0200 Subject: [PATCH 5/7] impelement bound computation for comparison --- cpmpy/expressions/core.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index aeebf9d58..fd3089263 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -566,6 +566,28 @@ def value(self): elif self.name == ">=": return arg_vals[0] >= arg_vals[1] return None # default + def get_bounds(self): + (lb1, ub1), (lb2, ub2) = get_bounds(self.args[0]), get_bounds(self.args[1]) + if self.name == "==": + if lb1 == ub1 == lb2 == ub2: return (1,1) # equal domains, trivially true + if ub1 < lb2 or ub2 < lb1: return (0,0) # disjoint, trivially false + if self.name == "!=": + if ub1 < lb2 or ub2 < lb1: return (1,1) # disjoint, trivially true + if lb1 == ub1 == lb2 == ub2: return (0,0) # equal domains, trivially false + if self.name == "<=": + if ub1 <= lb2: return (1,1) # domain of lhs is leq domain of rhs + if lb1 > ub2: return (0,0) # domain of lhs is gt domain of rhs + if self.name == "<": + if ub1 < lb2: return (1,1) # domain of lhs is lt domain of rhs + if lb1 >= ub2: return (0,0) # domain of lhs is geq domain of rhs + if self.name == ">=": + if lb1 >= ub2: return (1,1) # domain of lhs is geq domain of rhs + if ub1 < lb2: return (0,0) # domain of lhs is lt domain of rhs + if self.name == ">": + if lb1 > ub2: return (1,1) # domain of lhs is gt domain of rhs + if ub1 <= lb2: return (0,0) # domain of lhs is leq domain of rhs + return (0,1) + class Operator(Expression): """ From 905bce8bc5680062b235ae0b8d1b07f6b5a1bdb3 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 16:47:35 +0200 Subject: [PATCH 6/7] use bounds in simplify_bool --- cpmpy/transformations/normalize.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/cpmpy/transformations/normalize.py b/cpmpy/transformations/normalize.py index abc416390..53c68922b 100644 --- a/cpmpy/transformations/normalize.py +++ b/cpmpy/transformations/normalize.py @@ -169,12 +169,14 @@ def simplify_boolean(lst_of_expr, num_context=False): elif isinstance(expr, Comparison): lhs, rhs = simplify_boolean(expr.args, num_context=True) name = expr.name - if all(eval_comparison(expr.name, x,y) for x in get_bounds(lhs) for y in get_bounds(rhs)): - newlist.append(1 if num_context else BoolVal(True)) - continue - if not any(eval_comparison(expr.name, x,y) for x in get_bounds(lhs) for y in get_bounds(rhs)): + + lb, ub = get_bounds(eval_comparison(name, lhs, rhs)) + if lb == 0 == ub: newlist.append(0 if num_context else BoolVal(False)) continue + if lb == 1 == ub: + newlist.append(1 if num_context else BoolVal(True)) + continue if is_num(lhs) and is_boolexpr(rhs): # flip arguments of comparison to reduct nb of cases if name == "<": name = ">" From cf347f85f2bcb3eeefe294ccbed088267b478005 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 24 Oct 2025 16:49:22 +0200 Subject: [PATCH 7/7] add tests --- tests/test_expressions.py | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/tests/test_expressions.py b/tests/test_expressions.py index 74520dc2b..ca2524797 100644 --- a/tests/test_expressions.py +++ b/tests/test_expressions.py @@ -6,7 +6,8 @@ from cpmpy.expressions import * from cpmpy.expressions.variables import NDVarArray from cpmpy.expressions.core import Comparison, Operator, Expression -from cpmpy.expressions.utils import eval_comparison, get_bounds, argval +from cpmpy.expressions.utils import eval_comparison, get_bounds, argval, all_pairs + class TestComparison(unittest.TestCase): def test_comps(self): @@ -450,6 +451,29 @@ def test_bounds_unary(self): self.assertGreaterEqual(val,lb) self.assertLessEqual(val,ub) + def test_bounds_comparison(self): + + x_00 = intvar(0,0, name="x00") + x_01 = intvar(0,1, name="x01") + x_12= intvar(1,2, name="x12") + x_23 = intvar(2,3, name="x23") + + for x,y in all_pairs([0, x_00, x_01, x_12, x_23]): + for comp in ['==','!=','<=','<','>=','>']: + x_bounds = get_bounds(x) + y_bounds = get_bounds(y) + + total_vals = len(range(x_bounds[0],x_bounds[1]+1)) * len(range(y_bounds[0],y_bounds[1]+1)) + + for expr in [Comparison(comp, x,y), Comparison(comp, y,x)]: + lb, ub = expr.get_bounds() + + if lb == 0 == ub: + self.assertEqual(cp.Model(expr).solveAll(), 0) + elif lb == 1 == ub: + self.assertEqual(cp.Model(expr).solveAll(), total_vals) + else: + self.assertNotEqual(cp.Model(expr).solveAll(), total_vals) def test_incomplete_func(self): # element constraint