From c50f55743fd463f4ecf31570beca39efef5e9bb9 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 26 Jun 2025 10:26:20 +0200 Subject: [PATCH 01/47] add ocus implementation --- cpmpy/tools/explain/mus.py | 55 +++++++++++++++++++++++++++++------- cpmpy/tools/explain/utils.py | 23 +++++++++++++++ 2 files changed, 68 insertions(+), 10 deletions(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index c709cd36c..885f43445 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -8,10 +8,11 @@ import warnings import numpy as np import cpmpy as cp +from cpmpy.solvers.solver_interface import ExitStatus from cpmpy.transformations.get_variables import get_variables from cpmpy.transformations.normalize import toplevel_list -from .utils import make_assump_model +from .utils import make_assump_model, replace_cons_with_assump from ...expressions.utils import is_num @@ -115,10 +116,9 @@ def do_recursion(soft, hard, delta): core = do_recursion(list(assump)[:max_idx + 1], [], []) return [dmap[a] for a in core] - -def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools", do_solution_hint=True): +def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs_solver="ortools", do_solution_hint=True): """ - Find an optimal MUS according to a linear objective function. + Find an optimal and constrained MUS according to a linear objective function. By not providing a weightvector, this function will return the smallest mus. Works by iteratively generating correction subsets and computing optimal hitting sets to those enumerated sets. For better performance of the algorithm, use an incemental solver to compute the hitting sets such as Gurobi. @@ -128,6 +128,9 @@ def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortool :param: soft: list of soft constraints to find an optimal MUS of :param: hard: list of hard constraints, will be added to the model before solving + :param: weights: list of weights for the soft constraints, will be used to compute the objective function + :param: meta_constraint: a Boolean CPMpy expression that contains constraints in `soft` as sub-expressions. + By not providing a meta_constraint, this function will return an optimal mus. :param: solver: name of a solver, must support assumptions (e.g, "ortools", "exact", "z3" or "pysat") :param: hs_solver: the hitting-set solver to use, ideally incremental such as "gurobi" :param: do_solution_hint: when true, will favor large satisfiable subsets generated by the SAT-solver @@ -136,9 +139,9 @@ def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortool Gamba, Emilio, Bart Bogaerts, and Tias Guns. "Efficiently explaining CSPs with unsatisfiable subset optimization." Journal of Artificial Intelligence Research 78 (2023): 709-746. - """ - assert hasattr(cp.SolverLookup.get(solver), "get_core"), f"optimal_mus requires a solver that supports assumption variables, use optimal_mus_naive with {solver} instead" + + assert hasattr(cp.SolverLookup.get(solver), "get_core"), f"ocus requires a solver that supports assumption variables, use ocus_naive with {solver} instead" model, soft, assump = make_assump_model(soft, hard) dmap = dict(zip(assump, soft)) # map assumption variables to constraints @@ -156,6 +159,10 @@ def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortool hs_solver = cp.SolverLookup.get(hs_solver) hs_solver.minimize(cp.sum(assump * np.array(weights))) + assump_constraint = replace_cons_with_assump(meta_constraint, dict(zip(soft, assump))) + assert set(get_variables(assump_constraint)) <= set(assump), f"soft constraints should be replaced with assumption variables by now, but got {assump_constraint}" + hs_solver += assump_constraint + while hs_solver.solve() is True: hitting_set = [a for a in assump if a.value()] if s.solve(assumptions=hitting_set) is False: @@ -176,9 +183,22 @@ def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortool sat_subset += new_corr_subset # extend sat subset with new corr subset, guaranteed to be disjoint hs_solver += cp.sum(new_corr_subset) >= 1 # add new corr subset to hitting set solver + if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: + raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? + return [dmap[a] for a in hitting_set] + +def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools", do_solution_hint=True): + """ + Find an optimal MUS according to a linear objective function. + """ + return ocus(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver, do_solution_hint=do_solution_hint) + def smus(soft, hard=[], solver="ortools", hs_solver="ortools"): + """ + Find a smallest MUS according, equivalent to `optimal_mus` with weights=None + """ return optimal_mus(soft, hard=hard, weights=None, solver=solver, hs_solver=hs_solver) @@ -259,19 +279,22 @@ def do_recursion(soft, hard, delta): core = do_recursion(soft, hard, []) return core -def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools"): +def ocus_naive(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs_solver="ortools", do_solution_hint=True): """ - Naive implementation of `optimal_mus` without assumption variables and incremental solving + Naive implementation of `ocus` without assumption variables and incremental solving """ - soft = toplevel_list(soft, merge_and=False) - bvs = cp.boolvar(shape=len(soft)) + bvs = cp.boolvar(shape=(len(soft),)) if weights is None: weights = np.ones(len(bvs), dtype=int) hs_solver = cp.SolverLookup.get(hs_solver) hs_solver.minimize(cp.sum(bvs * np.array(weights))) + bv_cons = replace_cons_with_assump(meta_constraint, dict(zip(soft, bvs))) + assert set(get_variables(bv_cons)) <= set(bvs), f"soft constraints should be replaced with boolean variables by now, but got {bv_cons}" + hs_solver += bv_cons + while hs_solver.solve() is True: hitting_set = [c for bv, c in zip(bvs, soft) if bv.value()] @@ -294,8 +317,20 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver=" hs_solver += cp.sum(corr_subset) >= 1 sat_subset += false_constraints + if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: + raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? + return hitting_set + + +def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools"): + """ + Naive implementation of `optimal_mus` without assumption variables and incremental solving + """ + return ocus_naive(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver) + + diff --git a/cpmpy/tools/explain/utils.py b/cpmpy/tools/explain/utils.py index 3270707e6..7e271cd15 100644 --- a/cpmpy/tools/explain/utils.py +++ b/cpmpy/tools/explain/utils.py @@ -16,7 +16,10 @@ make_assump_model """ +import copy import cpmpy as cp +from cpmpy.expressions.utils import is_any_list +from cpmpy.expressions.variables import NegBoolView from cpmpy.transformations.normalize import toplevel_list def make_assump_model(soft, hard=[], name=None): @@ -36,3 +39,23 @@ def make_assump_model(soft, hard=[], name=None): model = cp.Model(hard + [assump.implies(soft2)]) # each assumption variable implies a candidate return model, soft2, assump + +def replace_cons_with_assump(cpm_cons, assump_map): + """ + Replace soft constraints with assumption variables in a Boolean CPMpy expression. + """ + + if is_any_list(cpm_cons): + return [replace_cons_with_assump(c, assump_map) for c in cpm_cons] + + if cpm_cons in assump_map: + return assump_map[cpm_cons] + + elif hasattr(cpm_cons, "args"): + cpm_cons = copy.copy(cpm_cons) + cpm_cons.update_args(replace_cons_with_assump(cpm_cons.args, assump_map)) + return cpm_cons + + elif isinstance(cpm_cons, NegBoolView): + return ~replace_cons_with_assump(cpm_cons._bv, assump_map) + return cpm_cons \ No newline at end of file From 30c0bf9b7821ee7b2f2eebeb37f4a7794bfe5a49 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 26 Jun 2025 10:26:28 +0200 Subject: [PATCH 02/47] update tests --- tests/test_tools_mus.py | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py index 54231baa2..911386e95 100644 --- a/tests/test_tools_mus.py +++ b/tests/test_tools_mus.py @@ -3,7 +3,7 @@ import cpmpy as cp from cpmpy.tools import mss_opt, marco -from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs +from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive class MusTests(TestCase): @@ -141,6 +141,35 @@ def test_weighted(self): subset3 = self.mus_func_naive([a, b, c, d], hard) self.assertEqual(set(subset3), {b, d}) +class OCUSTests(OptimalMUSTests): + + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + self.mus_func = ocus + self.naive_func = ocus_naive + + def test_constrained(self): + a, b, c, d = [cp.boolvar(name=n) for n in "abcd"] + + mus1 = [b, d] + mus2 = [a, b, c] + + hard = [~cp.all(mus1), ~cp.all(mus2)] + subset = self.mus_func([a, b, c, d], hard=hard, meta_constraint = ~b | d) + self.assertSetEqual(set(subset), {b,d}) + subset2 = self.mus_func([a,b,c,d], hard, meta_constraint = a & d) + self.assertSetEqual(set(subset2), {a,b,d}) # not subset-minimal + self.assertRaises(ValueError, lambda: self.mus_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist + + hard = [~cp.all(mus1), ~cp.all(mus2)] + subset = self.naive_func([a, b, c, d], hard=hard, meta_constraint = ~b | d) + self.assertSetEqual(set(subset), {b,d}) + subset2 = self.naive_func([a,b,c,d], hard, meta_constraint = a & d) + self.assertSetEqual(set(subset2), {a,b,d}) # not subset-minimal + self.assertRaises(ValueError, lambda: self.naive_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist + + + class MARCOMUSTests(MusTests): def test_php(self): From cb5ae7806aaf54208a5f2674acd7bba1dfd9ca55 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 25 Nov 2025 17:49:11 +0100 Subject: [PATCH 03/47] return custom OCUSException --- cpmpy/tools/explain/mus.py | 2 +- cpmpy/tools/explain/utils.py | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 885f43445..497934f52 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -184,7 +184,7 @@ def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs hs_solver += cp.sum(new_corr_subset) >= 1 # add new corr subset to hitting set solver if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: - raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? + raise OCUSException(f"No unsatisfiable subset adhereing to constraint {meta_constraint} could be found.") return [dmap[a] for a in hitting_set] diff --git a/cpmpy/tools/explain/utils.py b/cpmpy/tools/explain/utils.py index 7e271cd15..1906f5953 100644 --- a/cpmpy/tools/explain/utils.py +++ b/cpmpy/tools/explain/utils.py @@ -58,4 +58,7 @@ def replace_cons_with_assump(cpm_cons, assump_map): elif isinstance(cpm_cons, NegBoolView): return ~replace_cons_with_assump(cpm_cons._bv, assump_map) - return cpm_cons \ No newline at end of file + return cpm_cons + +class OCUSException(Exception): + pass \ No newline at end of file From 27f05e009438b0b62d9c1b97407e5a53400c16ed Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 25 Nov 2025 17:49:17 +0100 Subject: [PATCH 04/47] return custom OCUSException --- cpmpy/tools/explain/mus.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 497934f52..d05f56a01 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -12,8 +12,7 @@ from cpmpy.transformations.get_variables import get_variables from cpmpy.transformations.normalize import toplevel_list -from .utils import make_assump_model, replace_cons_with_assump -from ...expressions.utils import is_num +from .utils import make_assump_model, replace_cons_with_assump, OCUSException def mus(soft, hard=[], solver="ortools"): From 73536eb201323a470b2c498b610c537d35a12f0a Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 25 Nov 2025 17:50:22 +0100 Subject: [PATCH 05/47] return custom OCUSException in naive variant --- cpmpy/tools/explain/mus.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index d05f56a01..6fa385dba 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -317,7 +317,7 @@ def ocus_naive(soft, hard=[], weights=None, meta_constraint=True, solver="ortool sat_subset += false_constraints if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: - raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? + raise OCUSException("No unsatisfiable constrained subset could be found") # TODO: better exception? return hitting_set From 1f9ed22fc3b4cac9acf403b3b510db28d16a4743 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 25 Nov 2025 17:50:26 +0100 Subject: [PATCH 06/47] update tests --- tests/test_tools_mus.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py index 911386e95..eb2e24c70 100644 --- a/tests/test_tools_mus.py +++ b/tests/test_tools_mus.py @@ -2,7 +2,7 @@ from unittest import TestCase import cpmpy as cp -from cpmpy.tools import mss_opt, marco +from cpmpy.tools import mss_opt, marco, OCUSException from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive @@ -159,14 +159,14 @@ def test_constrained(self): self.assertSetEqual(set(subset), {b,d}) subset2 = self.mus_func([a,b,c,d], hard, meta_constraint = a & d) self.assertSetEqual(set(subset2), {a,b,d}) # not subset-minimal - self.assertRaises(ValueError, lambda: self.mus_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist + self.assertRaises(OCUSException, lambda: self.mus_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist hard = [~cp.all(mus1), ~cp.all(mus2)] subset = self.naive_func([a, b, c, d], hard=hard, meta_constraint = ~b | d) self.assertSetEqual(set(subset), {b,d}) subset2 = self.naive_func([a,b,c,d], hard, meta_constraint = a & d) self.assertSetEqual(set(subset2), {a,b,d}) # not subset-minimal - self.assertRaises(ValueError, lambda: self.naive_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist + self.assertRaises(OCUSException, lambda: self.naive_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist From 562265b17900a8117f728c573100752034462a1e Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 26 Nov 2025 19:10:22 +0100 Subject: [PATCH 07/47] replace decompose_comparison with decompose --- cpmpy/expressions/globalfunctions.py | 200 +++++++++++++-------------- 1 file changed, 96 insertions(+), 104 deletions(-) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 515947a6c..9040740c8 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -10,7 +10,7 @@ ------------------------ If a solver does not support such a global function (see solvers/), then it will be automatically - decomposed by calling its `.decompose_comparison()` function. + decomposed by calling its `.decompose()` function. CPMpy GlobalFunctions does not exactly match what is implemented in the solvers. Solvers can have specialised implementations for global functions, when used in a comparison, as global constraints. @@ -42,8 +42,8 @@ class my_global(GlobalFunction): def __init__(self, args): super().__init__("my_global", args) - def decompose_comparison(self): - return [self.args[0] + self.args[1]] # your decomposition + def decompose(self): + return [self.args[0] + self.args[1]], [] # your decomposition Also, implement `.value()` accordingly. @@ -65,6 +65,8 @@ def decompose_comparison(self): """ import warnings # for deprecation warning +from warnings import deprecated + import numpy as np import cpmpy as cp @@ -87,9 +89,10 @@ def is_bool(self): """ return False - def decompose_comparison(self, cmp_op, cmp_rhs): + def decompose(self): """ Returns a decomposition into smaller constraints. + Returns a numerical expression and a list of defining constraints. The decomposition might create auxiliary variables and use other global constraints as long as @@ -97,6 +100,19 @@ def decompose_comparison(self, cmp_op, cmp_rhs): """ raise NotImplementedError("Decomposition for", self, "not available") + @deprecated("Deprecated, will be removed in stable version. Use .decompose() instead.") + def decompose_comparison(self, cmp_op, cmp_rhs): + """ + Returns a decomposition into smaller constraints. + + The decomposition might create auxiliary variables + and use other global constraints as long as + it does not create a circular dependency. + """ + val, tl = self.decompose() + return eval_comparison(cmp_op, val, cmp_rhs), tl + + def get_bounds(self): """ Returns the bounds of the global function @@ -126,20 +142,15 @@ def value(self): else: return min(argvals) - def decompose_comparison(self, cpm_op, cpm_rhs): + def decompose(self): """ - Decomposition if it's part of a comparison - - Returns two lists of constraints: - - 1) constraints representing the comparison - 2) constraints that (totally) define new auxiliary variables needed in the decomposition, - they should be enforced toplevel. + Decomposition of Minimum constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel """ - lb, ub = self.get_bounds() - _min = intvar(lb, ub) - return [eval_comparison(cpm_op, _min, cpm_rhs)], \ - [cp.any(x <= _min for x in self.args), cp.all(x >= _min for x in self.args), ] + _min = intvar(*self.get_bounds()) + return _min, [cp.all(x >= _min for x in self.args), cp.any(x <= _min for x in self.args)] def get_bounds(self): """ @@ -164,20 +175,15 @@ def value(self): else: return max(argvals) - def decompose_comparison(self, cpm_op, cpm_rhs): + def decompose(self): """ - Decomposition if it's part of a comparison - - Returns two lists of constraints: - - 1) constraints representing the comparison - 2) constraints that (totally) define new auxiliary variables needed in the decomposition, - they should be enforced toplevel. + Decomposition of Maximum constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel """ - lb, ub = self.get_bounds() - _max = intvar(lb, ub) - return [eval_comparison(cpm_op, _max, cpm_rhs)], \ - [cp.any(x >= _max for x in self.args), cp.all(x <= _max for x in self.args)] + _max = intvar(*self.get_bounds()) + return _max, [cp.all(x <= _max for x in self.args), cp.any(x >= _max for x in self.args)] def get_bounds(self): """ @@ -197,30 +203,25 @@ def __init__(self, expr): def value(self): return abs(argval(self.args[0])) - def decompose_comparison(self, cpm_op, cpm_rhs): + def decompose(self): """ - Decomposition if it's part of a comparison - - Returns two lists of constraints: - - 1) constraints representing the comparison - 2) constraints that (totally) define new auxiliary variables needed in the decomposition, - they should be enforced toplevel. + Decomposition of Abs constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel """ arg = self.args[0] lb, ub = get_bounds(arg) - # when argument is exclusively on one side of the sign - if lb >= 0: - return [eval_comparison(cpm_op, arg, cpm_rhs)], [] - elif ub <= 0: - return [eval_comparison(cpm_op, -arg, cpm_rhs)], [] - else: # when domain crosses over 0 - newarg = intvar(*self.get_bounds()) - is_pos = boolvar() - return [eval_comparison(cpm_op, newarg, cpm_rhs)], \ - [is_pos == (arg >= 0), is_pos.implies(arg == newarg), (~is_pos).implies(-arg == newarg)] + if lb >= 0: # always positive + return arg, [] + if ub <= 0: # always negative + return -arg, [] + _abs = intvar(*self.get_bounds()) + assert _abs.lb == 0 + is_pos = arg >= 0 + return _abs, [is_pos.implies(arg == _abs), (~is_pos).implies(arg == -_abs)] def get_bounds(self): """ @@ -274,29 +275,22 @@ def value(self): + "\n Use argval(expr) to get the value of expr with relational semantics.") return None # default - def decompose_comparison(self, cpm_op, cpm_rhs): + def decompose(self): """ - `Element(arr,ix)` represents the array lookup itself (a numeric variable) - When used in a comparison relation: Element(arr,idx) CMP_RHS - it is a constraint, and that one can be decomposed. + Decomposition of Abs constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel + """ + arr, idx = self.args - Returns two lists of constraints: + idx_lb, idx_ub = get_bounds(idx) + assert idx_lb >= 0 and idx_ub < len(arr), "Element constraint is unsafe to decompose as it can be partial. Safen first using `cpmpy.transformations.safening.no_partial_functions`" - 1) constraints representing the comparison - 2) constraints that (totally) define new auxiliary variables needed in the decomposition, - they should be enforced toplevel. + _elem = intvar(*self.get_bounds()) + + return _elem, [implies(idx == i, _elem == arr[i]) for i in range(len(arr))] - """ - arr, idx = self.args - # Find where the array indices and the bounds of `idx` intersect - lb, ub = get_bounds(idx) - new_lb, new_ub = max(lb, 0), min(ub, len(arr) - 1) - cons=[] - # For every `i` in that intersection, post `(idx = i) -> idx=i -> arr[i] cpm_rhs`. - for i in range(new_lb, new_ub+1): - cons.append(implies(idx == i, eval_comparison(cpm_op, arr[i], cpm_rhs))) - cons+=[idx >= new_lb, idx <= new_ub] # also enforce the new bounds - return cons, [] # no auxiliary variables def __repr__(self): return "{}[{}]".format(self.args[0], self.args[1]) @@ -320,12 +314,15 @@ def __init__(self,arr,val): raise TypeError("count takes an array and a value as input, not: {} and {}".format(arr,val)) super().__init__("count", [arr,val]) - def decompose_comparison(self, cmp_op, cmp_rhs): + def decompose(self): """ - Count(arr,val) can only be decomposed if it's part of a comparison + Decomposition of the Count constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel """ arr, val = self.args - return [eval_comparison(cmp_op, Operator('sum',[ai==val for ai in arr]), cmp_rhs)], [] + return cp.sum(a == val for a in arr), [] def value(self): arr, val = self.args @@ -353,13 +350,17 @@ def __init__(self,arr,vals): raise TypeError(f"Among takes a set of values as input, not {vals}") super().__init__("among", [arr,vals]) - def decompose_comparison(self, cmp_op, cmp_rhs): + def decompose(self): """ - Among(arr, vals) can only be decomposed if it's part of a comparison' + Decomposition of the Among constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel + """ arr, values = self.args - count_for_each_val = [Count(arr, val) for val in values] - return [eval_comparison(cmp_op, cp.sum(count_for_each_val), cmp_rhs)], [] + return cp.sum(Count(arr, val) for val in values), [] + def value(self): return int(sum(np.isin(argvals(self.args[0]), self.args[1]))) @@ -379,31 +380,27 @@ def __init__(self, arr): raise ValueError("NValue takes an array as input") super().__init__("nvalue", arr) - def decompose_comparison(self, cmp_op, cpm_rhs): + def decompose(self): """ - NValue(arr) can only be decomposed if it's part of a comparison + Decomposition of the Count constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel Based on "simple decomposition" from: - + Bessiere, Christian, et al. "Decomposition of the NValue constraint." International Conference on Principles and Practice of Constraint Programming. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. """ - lbs, ubs = get_bounds(self.args) lb, ub = min(lbs), max(ubs) - constraints = [] - - # introduce boolvar for each possible value - bvars = boolvar(shape=(ub+1-lb,)) # shape is tuple to ensure it is a 1D array + n_values = 0 + for v in range(lb, ub+1): + n_values += cp.any(a == v for a in self.args) - args = cpm_array(self.args) - # bvar is true if the value is taken by any variable - for bv, val in zip(bvars, range(lb, ub+1)): - constraints += [cp.any(args == val) == bv] - - return [eval_comparison(cmp_op, cp.sum(bvars), cpm_rhs)], constraints + return n_values, [] def value(self): return len(set(argval(a) for a in self.args)) @@ -429,9 +426,12 @@ def __init__(self, arr, n): raise ValueError(f"NValueExcept takes an integer as second argument, but got {n} of type {type(n)}") super().__init__("nvalue_except",[arr, n]) - def decompose_comparison(self, cmp_op, cpm_rhs): + def decompose(self): """ - NValue(arr) can only be decomposed if it's part of a comparison + Decomposition of the Count constraint. + Returns + 1) a numerical value to replace the constraint, and + 2) a list of defining constraints, which should be enforced toplevel Based on "simple decomposition" from: @@ -439,27 +439,19 @@ def decompose_comparison(self, cmp_op, cpm_rhs): International Conference on Principles and Practice of Constraint Programming. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. """ - arr, n = self.args - arr = cpm_array(arr) + assert is_num(n) + lbs, ubs = get_bounds(arr) lb, ub = min(lbs), max(ubs) - constraints = [] - - # introduce boolvar for each possible value - bvars = boolvar(shape=(ub+1-lb,)) # shape is tuple to ensure it is a 1D array - idx_of_n = n - lb - if 0 <= idx_of_n < len(bvars): - count_of_vals = cp.sum(bvars[:idx_of_n]) + cp.sum(bvars[idx_of_n+1:]) - else: - count_of_vals = cp.sum(bvars) - - # bvar is true if the value is taken by any variable - for bv, val in zip(bvars, range(lb, ub + 1)): - constraints += [cp.any(arr == val) == bv] + n_values = 0 + for v in range(lb, ub+1): + if v == n: + continue + n_values += cp.any(a == v for a in arr) - return [eval_comparison(cmp_op, count_of_vals, cpm_rhs)], constraints + return n_values, [] def value(self): return len(set(argval(a) for a in self.args[0]) - {self.args[1]}) From 5501e424769915d7132363cc3534f2b4c27c33aa Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 26 Nov 2025 19:10:32 +0100 Subject: [PATCH 08/47] update decomp circuit --- cpmpy/expressions/globalconstraints.py | 48 +++++++------------------- 1 file changed, 13 insertions(+), 35 deletions(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 2be5c53d4..79acb9026 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -309,42 +309,20 @@ def decompose(self): https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/fzn_circuit.mzn """ succ = cpm_array(self.args) - n = len(succ) - order = intvar(0,n-1, shape=n) + + order = [succ[0]] + for i in range(1, len(succ)): + order.append(succ[order[i-1]]) + + # Decomposition must be total, so safen here + nbc = [] defining = [] - constraining = [] - - # We define the auxiliary order variables to represent the order we visit all the nodes. - # `order[i] == succ[order[i - 1]]` - # These constraints need to be in the defining part, since they define our auxiliary vars - # However, this would make it impossible for ~circuit to be satisfied in some cases, - # because there does not always exist a valid ordering - # This happens when the variables in succ don't take values in the domain of 'order', - # i.e. for succ = [9,-1,0], there is no valid ordering, but we satisfy ~circuit(succ) - # We explicitly deal with these cases by defining the variable 'a' that indicates if we can define an ordering. - - lbs, ubs = get_bounds(succ) - if min(lbs) > 0 or max(ubs) < n - 1: - # no way this can be a circuit - return [BoolVal(False)], [] - elif min(lbs) >= 0 and max(ubs) < n: - # there always exists a valid ordering, since our bounds are tight - a = BoolVal(True) - else: - # we may get values in succ that are outside the bounds of it's array length (making the ordering undefined) - a = boolvar() - defining += [a == ((Minimum(succ) >= 0) & (Maximum(succ) < n))] - for i in range(n): - defining += [(~a).implies(order[i] == 0)] # assign arbitrary value, so a is totally defined. - - constraining += [AllDifferent(succ)] # different successors - constraining += [AllDifferent(order)] # different orders - constraining += [order[n - 1] == 0] # symmetry breaking, last one is '0' - defining += [a.implies(order[0] == succ[0])] - for i in range(1, n): - defining += [a.implies( - order[i] == succ[order[i - 1]])] # first one is successor of '0', ith one is successor of i-1 - return constraining, defining + cons = cp.transformations.safening.no_partial_functions([order[-1] == 0], + _toplevel=defining, + _nbc=nbc, + safen_toplevel={"element"}) + + return cons + nbc, defining def value(self): pathlen = 0 From 860978254238a460e96a23df0c8ef13ab6cb8c96 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 26 Nov 2025 19:10:55 +0100 Subject: [PATCH 09/47] remove global function specific stuff from decompose --- cpmpy/transformations/decompose_global.py | 106 +++++----------------- 1 file changed, 22 insertions(+), 84 deletions(-) diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index 0b752080f..e0c5a7a53 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -36,9 +36,6 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to if _toplevel is None: _toplevel = [] - # swap the arguments of a comparison while maintaining its semantics - flipmap = {"==": "==", "!=": "!=", "<": ">", "<=": ">=", ">": "<", ">=": "<="} - newlist = [] # decomposed constraints will go here for expr in lst_of_expr: @@ -63,9 +60,9 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to newlist.append(expr) continue - if any(isinstance(a,GlobalFunction) for a in expr.args): - expr, base_con = normalized_numexpr(expr, csemap=csemap) - _toplevel.extend(base_con) # should be added toplevel + # if any(isinstance(a,GlobalFunction) for a in expr.args): + # expr, base_con = normalized_numexpr(expr, csemap=csemap) + # _toplevel.extend(base_con) # should be added toplevel # recurse into arguments, recreate through constructor (we know it stores no other state) args = decompose_in_tree(expr.args, supported, supported_reified, _toplevel, nested=True, csemap=csemap) newlist.append(Operator(expr.name, args)) @@ -89,93 +86,34 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to expr.update_args(decompose_in_tree(expr.args, supported, supported_reified, _toplevel, nested=True, csemap=csemap)) newlist.append(expr) - else: + else: # unsupported, need to decompose + dec = expr.decompose() + if not isinstance(dec, tuple): + warnings.warn(f"Decomposing an old-style global ({expr}) that does not return a tuple, which is " + "deprecated. Support for old-style globals will be removed in stable version", + DeprecationWarning) + dec = (dec, []) + value, define = dec + if not is_any_list(value): + value = [value] + + _toplevel.extend(define) # definitions should be added toplevel + # the `decomposed` expression might contain other global constraints, check it + decomposed = decompose_in_tree(value, supported, supported_reified, _toplevel, nested=nested, csemap=csemap) if expr.is_bool(): - assert isinstance(expr, GlobalConstraint) - # boolean global constraints - dec = expr.decompose() - if not isinstance(dec, tuple): - warnings.warn(f"Decomposing an old-style global ({expr}) that does not return a tuple, which is " - "deprecated. Support for old-style globals will be removed in stable version", - DeprecationWarning) - dec = (dec, []) - decomposed, define = dec - - _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, _toplevel, nested=nested, csemap=csemap) newlist.append(all(decomposed)) - else: - # global function, replace by a fresh variable and decompose the equality to this - assert isinstance(expr, GlobalFunction) - lb,ub = expr.get_bounds() - - if csemap is not None and expr in csemap: - aux = csemap[expr] - else: - aux = intvar(lb, ub) - if csemap is not None: - csemap[expr] = aux - - # NOTE Do we need to decompose here (the expr's args)? As done in the Comparison's section? - - dec = expr.decompose_comparison("==", aux) - if not isinstance(dec, tuple): - warnings.warn(f"Decomposing an old-style global ({expr}) that does not return a tuple, which is " - "deprecated. Support for old-style globals will be removed in stable version", - DeprecationWarning) - dec = (dec, []) - auxdef, otherdef = dec - - _toplevel.extend(auxdef + otherdef) # all definitions should be added toplevel - newlist.append(aux) # replace original expression by aux + assert len(decomposed) == 1, "Global functions should return a single numerical value, not a list" + newlist.append(decomposed[0]) elif isinstance(expr, Comparison): if not expr.has_subexpr(): # Only recurse if there are nested expressions newlist.append(expr) continue - # if one of the two children is a (numeric) global constraint, we can decompose the comparison directly - # otherwise e.g., min(x,y,z) == a would become `min(x,y,z).decompose_comparison('==',aux) + [aux == a]` - lhs, rhs = expr.args - exprname = expr.name # can change when rhs needs decomp - - decomp_lhs = isinstance(lhs, GlobalFunction) and not lhs.name in supported - decomp_rhs = isinstance(rhs, GlobalFunction) and not rhs.name in supported - - if not decomp_lhs: - if not decomp_rhs: - # nothing special, create a fresh version and recurse into arguments - expr = copy.copy(expr) - expr.update_args(decompose_in_tree(expr.args, supported, supported_reified, _toplevel, nested=True, csemap=csemap)) - newlist.append(expr) - - else: - # only rhs needs decomposition, so flip comparison to make lhs needing the decomposition - exprname = flipmap[expr.name] - lhs, rhs = rhs, lhs - decomp_lhs, decomp_rhs = True, False # continue into next 'if' - - if decomp_lhs: - if lhs.has_subexpr(): - # recurse into lhs args and decompose nested subexpressions - lhs = copy.copy(lhs) - lhs.update_args(decompose_in_tree(lhs.args, supported, supported_reified, _toplevel, nested=True, csemap=csemap)) - - # decompose comparison of lhs and rhs - dec = lhs.decompose_comparison(exprname, rhs) - if not isinstance(dec, tuple): - warnings.warn(f"Decomposing an old-style global ({lhs}) that does not return a tuple, which is " - f"deprecated. Support for old-style globals will be removed in stable version", - DeprecationWarning) - dec = (dec, []) - decomposed, define = dec - - _toplevel.extend(define) # definitions should be added toplevel - # the `decomposed` expression (and rhs) might contain other global constraints, check it - decomposed = decompose_in_tree(decomposed, supported, supported_reified, _toplevel, nested=True, csemap=csemap) - newlist.append(all(decomposed)) + expr = copy.copy(expr) + expr.update_args(decompose_in_tree(expr.args, supported, supported_reified, _toplevel, nested=True, csemap=csemap)) + newlist.append(expr) else: # constants, variables, direct constraints newlist.append(expr) From bc68db3386b7f0105865dd15b8d00b89c63248e5 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 27 Nov 2025 10:48:11 +0100 Subject: [PATCH 10/47] fix deprecation warning --- cpmpy/expressions/globalfunctions.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 9040740c8..0d7882197 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -65,7 +65,6 @@ def decompose(self): """ import warnings # for deprecation warning -from warnings import deprecated import numpy as np import cpmpy as cp @@ -100,7 +99,6 @@ def decompose(self): """ raise NotImplementedError("Decomposition for", self, "not available") - @deprecated("Deprecated, will be removed in stable version. Use .decompose() instead.") def decompose_comparison(self, cmp_op, cmp_rhs): """ Returns a decomposition into smaller constraints. @@ -109,6 +107,8 @@ def decompose_comparison(self, cmp_op, cmp_rhs): and use other global constraints as long as it does not create a circular dependency. """ + warnings.warn(f"Deprecated, use {self}.decompose() instead, will be removed in " + "stable version", DeprecationWarning) val, tl = self.decompose() return eval_comparison(cmp_op, val, cmp_rhs), tl From c216d3bd215905b2290586bb4320fc553983b6a2 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 27 Nov 2025 10:48:31 +0100 Subject: [PATCH 11/47] Revert "update decomp circuit" This reverts commit 5501e424769915d7132363cc3534f2b4c27c33aa. --- cpmpy/expressions/globalconstraints.py | 48 +++++++++++++++++++------- 1 file changed, 35 insertions(+), 13 deletions(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 79acb9026..2be5c53d4 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -309,20 +309,42 @@ def decompose(self): https://github.com/MiniZinc/libminizinc/blob/master/share/minizinc/std/fzn_circuit.mzn """ succ = cpm_array(self.args) - - order = [succ[0]] - for i in range(1, len(succ)): - order.append(succ[order[i-1]]) - - # Decomposition must be total, so safen here - nbc = [] + n = len(succ) + order = intvar(0,n-1, shape=n) defining = [] - cons = cp.transformations.safening.no_partial_functions([order[-1] == 0], - _toplevel=defining, - _nbc=nbc, - safen_toplevel={"element"}) - - return cons + nbc, defining + constraining = [] + + # We define the auxiliary order variables to represent the order we visit all the nodes. + # `order[i] == succ[order[i - 1]]` + # These constraints need to be in the defining part, since they define our auxiliary vars + # However, this would make it impossible for ~circuit to be satisfied in some cases, + # because there does not always exist a valid ordering + # This happens when the variables in succ don't take values in the domain of 'order', + # i.e. for succ = [9,-1,0], there is no valid ordering, but we satisfy ~circuit(succ) + # We explicitly deal with these cases by defining the variable 'a' that indicates if we can define an ordering. + + lbs, ubs = get_bounds(succ) + if min(lbs) > 0 or max(ubs) < n - 1: + # no way this can be a circuit + return [BoolVal(False)], [] + elif min(lbs) >= 0 and max(ubs) < n: + # there always exists a valid ordering, since our bounds are tight + a = BoolVal(True) + else: + # we may get values in succ that are outside the bounds of it's array length (making the ordering undefined) + a = boolvar() + defining += [a == ((Minimum(succ) >= 0) & (Maximum(succ) < n))] + for i in range(n): + defining += [(~a).implies(order[i] == 0)] # assign arbitrary value, so a is totally defined. + + constraining += [AllDifferent(succ)] # different successors + constraining += [AllDifferent(order)] # different orders + constraining += [order[n - 1] == 0] # symmetry breaking, last one is '0' + defining += [a.implies(order[0] == succ[0])] + for i in range(1, n): + defining += [a.implies( + order[i] == succ[order[i - 1]])] # first one is successor of '0', ith one is successor of i-1 + return constraining, defining def value(self): pathlen = 0 From 824574526fcc8428cef950829c7880857e140580 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 27 Nov 2025 10:56:16 +0100 Subject: [PATCH 12/47] Revert "return custom OCUSException in naive variant" This reverts commit 73536eb201323a470b2c498b610c537d35a12f0a. --- cpmpy/tools/explain/mus.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 6fa385dba..d05f56a01 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -317,7 +317,7 @@ def ocus_naive(soft, hard=[], weights=None, meta_constraint=True, solver="ortool sat_subset += false_constraints if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: - raise OCUSException("No unsatisfiable constrained subset could be found") # TODO: better exception? + raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? return hitting_set From e689dbcf9181608701937f08ae94130a503e574c Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 27 Nov 2025 10:56:21 +0100 Subject: [PATCH 13/47] Revert "return custom OCUSException" This reverts commit 27f05e009438b0b62d9c1b97407e5a53400c16ed. --- cpmpy/tools/explain/mus.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index d05f56a01..497934f52 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -12,7 +12,8 @@ from cpmpy.transformations.get_variables import get_variables from cpmpy.transformations.normalize import toplevel_list -from .utils import make_assump_model, replace_cons_with_assump, OCUSException +from .utils import make_assump_model, replace_cons_with_assump +from ...expressions.utils import is_num def mus(soft, hard=[], solver="ortools"): From 6f8357bd091370effce754765713fa4b5a1db94e Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 27 Nov 2025 10:56:26 +0100 Subject: [PATCH 14/47] Revert "return custom OCUSException" This reverts commit cb5ae7806aaf54208a5f2674acd7bba1dfd9ca55. --- cpmpy/tools/explain/mus.py | 2 +- cpmpy/tools/explain/utils.py | 5 +---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 497934f52..885f43445 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -184,7 +184,7 @@ def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs hs_solver += cp.sum(new_corr_subset) >= 1 # add new corr subset to hitting set solver if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: - raise OCUSException(f"No unsatisfiable subset adhereing to constraint {meta_constraint} could be found.") + raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? return [dmap[a] for a in hitting_set] diff --git a/cpmpy/tools/explain/utils.py b/cpmpy/tools/explain/utils.py index 1906f5953..7e271cd15 100644 --- a/cpmpy/tools/explain/utils.py +++ b/cpmpy/tools/explain/utils.py @@ -58,7 +58,4 @@ def replace_cons_with_assump(cpm_cons, assump_map): elif isinstance(cpm_cons, NegBoolView): return ~replace_cons_with_assump(cpm_cons._bv, assump_map) - return cpm_cons - -class OCUSException(Exception): - pass \ No newline at end of file + return cpm_cons \ No newline at end of file From 88a72a9a152658caaa200d230115482d44aaa5e4 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Thu, 27 Nov 2025 10:58:59 +0100 Subject: [PATCH 15/47] Revert "add ocus implementation" This reverts commit c50f55743fd463f4ecf31570beca39efef5e9bb9. --- cpmpy/tools/explain/mus.py | 55 +++++++----------------------------- cpmpy/tools/explain/utils.py | 23 --------------- 2 files changed, 10 insertions(+), 68 deletions(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 885f43445..c709cd36c 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -8,11 +8,10 @@ import warnings import numpy as np import cpmpy as cp -from cpmpy.solvers.solver_interface import ExitStatus from cpmpy.transformations.get_variables import get_variables from cpmpy.transformations.normalize import toplevel_list -from .utils import make_assump_model, replace_cons_with_assump +from .utils import make_assump_model from ...expressions.utils import is_num @@ -116,9 +115,10 @@ def do_recursion(soft, hard, delta): core = do_recursion(list(assump)[:max_idx + 1], [], []) return [dmap[a] for a in core] -def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs_solver="ortools", do_solution_hint=True): + +def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools", do_solution_hint=True): """ - Find an optimal and constrained MUS according to a linear objective function. + Find an optimal MUS according to a linear objective function. By not providing a weightvector, this function will return the smallest mus. Works by iteratively generating correction subsets and computing optimal hitting sets to those enumerated sets. For better performance of the algorithm, use an incemental solver to compute the hitting sets such as Gurobi. @@ -128,9 +128,6 @@ def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs :param: soft: list of soft constraints to find an optimal MUS of :param: hard: list of hard constraints, will be added to the model before solving - :param: weights: list of weights for the soft constraints, will be used to compute the objective function - :param: meta_constraint: a Boolean CPMpy expression that contains constraints in `soft` as sub-expressions. - By not providing a meta_constraint, this function will return an optimal mus. :param: solver: name of a solver, must support assumptions (e.g, "ortools", "exact", "z3" or "pysat") :param: hs_solver: the hitting-set solver to use, ideally incremental such as "gurobi" :param: do_solution_hint: when true, will favor large satisfiable subsets generated by the SAT-solver @@ -139,9 +136,9 @@ def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs Gamba, Emilio, Bart Bogaerts, and Tias Guns. "Efficiently explaining CSPs with unsatisfiable subset optimization." Journal of Artificial Intelligence Research 78 (2023): 709-746. - """ - assert hasattr(cp.SolverLookup.get(solver), "get_core"), f"ocus requires a solver that supports assumption variables, use ocus_naive with {solver} instead" + """ + assert hasattr(cp.SolverLookup.get(solver), "get_core"), f"optimal_mus requires a solver that supports assumption variables, use optimal_mus_naive with {solver} instead" model, soft, assump = make_assump_model(soft, hard) dmap = dict(zip(assump, soft)) # map assumption variables to constraints @@ -159,10 +156,6 @@ def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs hs_solver = cp.SolverLookup.get(hs_solver) hs_solver.minimize(cp.sum(assump * np.array(weights))) - assump_constraint = replace_cons_with_assump(meta_constraint, dict(zip(soft, assump))) - assert set(get_variables(assump_constraint)) <= set(assump), f"soft constraints should be replaced with assumption variables by now, but got {assump_constraint}" - hs_solver += assump_constraint - while hs_solver.solve() is True: hitting_set = [a for a in assump if a.value()] if s.solve(assumptions=hitting_set) is False: @@ -183,22 +176,9 @@ def ocus(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs sat_subset += new_corr_subset # extend sat subset with new corr subset, guaranteed to be disjoint hs_solver += cp.sum(new_corr_subset) >= 1 # add new corr subset to hitting set solver - if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: - raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? - return [dmap[a] for a in hitting_set] - -def optimal_mus(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools", do_solution_hint=True): - """ - Find an optimal MUS according to a linear objective function. - """ - return ocus(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver, do_solution_hint=do_solution_hint) - def smus(soft, hard=[], solver="ortools", hs_solver="ortools"): - """ - Find a smallest MUS according, equivalent to `optimal_mus` with weights=None - """ return optimal_mus(soft, hard=hard, weights=None, solver=solver, hs_solver=hs_solver) @@ -279,22 +259,19 @@ def do_recursion(soft, hard, delta): core = do_recursion(soft, hard, []) return core -def ocus_naive(soft, hard=[], weights=None, meta_constraint=True, solver="ortools", hs_solver="ortools", do_solution_hint=True): +def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools"): """ - Naive implementation of `ocus` without assumption variables and incremental solving + Naive implementation of `optimal_mus` without assumption variables and incremental solving """ + soft = toplevel_list(soft, merge_and=False) - bvs = cp.boolvar(shape=(len(soft),)) + bvs = cp.boolvar(shape=len(soft)) if weights is None: weights = np.ones(len(bvs), dtype=int) hs_solver = cp.SolverLookup.get(hs_solver) hs_solver.minimize(cp.sum(bvs * np.array(weights))) - bv_cons = replace_cons_with_assump(meta_constraint, dict(zip(soft, bvs))) - assert set(get_variables(bv_cons)) <= set(bvs), f"soft constraints should be replaced with boolean variables by now, but got {bv_cons}" - hs_solver += bv_cons - while hs_solver.solve() is True: hitting_set = [c for bv, c in zip(bvs, soft) if bv.value()] @@ -317,20 +294,8 @@ def ocus_naive(soft, hard=[], weights=None, meta_constraint=True, solver="ortool hs_solver += cp.sum(corr_subset) >= 1 sat_subset += false_constraints - if hs_solver.status().exitstatus == ExitStatus.UNSATISFIABLE: - raise ValueError("No unsatisfiable constrained subset could be found") # TODO: better exception? - return hitting_set - - -def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver="ortools"): - """ - Naive implementation of `optimal_mus` without assumption variables and incremental solving - """ - return ocus_naive(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver) - - diff --git a/cpmpy/tools/explain/utils.py b/cpmpy/tools/explain/utils.py index 7e271cd15..3270707e6 100644 --- a/cpmpy/tools/explain/utils.py +++ b/cpmpy/tools/explain/utils.py @@ -16,10 +16,7 @@ make_assump_model """ -import copy import cpmpy as cp -from cpmpy.expressions.utils import is_any_list -from cpmpy.expressions.variables import NegBoolView from cpmpy.transformations.normalize import toplevel_list def make_assump_model(soft, hard=[], name=None): @@ -39,23 +36,3 @@ def make_assump_model(soft, hard=[], name=None): model = cp.Model(hard + [assump.implies(soft2)]) # each assumption variable implies a candidate return model, soft2, assump - -def replace_cons_with_assump(cpm_cons, assump_map): - """ - Replace soft constraints with assumption variables in a Boolean CPMpy expression. - """ - - if is_any_list(cpm_cons): - return [replace_cons_with_assump(c, assump_map) for c in cpm_cons] - - if cpm_cons in assump_map: - return assump_map[cpm_cons] - - elif hasattr(cpm_cons, "args"): - cpm_cons = copy.copy(cpm_cons) - cpm_cons.update_args(replace_cons_with_assump(cpm_cons.args, assump_map)) - return cpm_cons - - elif isinstance(cpm_cons, NegBoolView): - return ~replace_cons_with_assump(cpm_cons._bv, assump_map) - return cpm_cons \ No newline at end of file From 96f59d0ee4dfa275e96b958a8a486bc6b15d4d7f Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 28 Nov 2025 13:01:49 +0100 Subject: [PATCH 16/47] revert ocus related tests --- tests/test_tools_mus.py | 33 ++------------------------------- 1 file changed, 2 insertions(+), 31 deletions(-) diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py index eb2e24c70..54231baa2 100644 --- a/tests/test_tools_mus.py +++ b/tests/test_tools_mus.py @@ -2,8 +2,8 @@ from unittest import TestCase import cpmpy as cp -from cpmpy.tools import mss_opt, marco, OCUSException -from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive +from cpmpy.tools import mss_opt, marco +from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs class MusTests(TestCase): @@ -141,35 +141,6 @@ def test_weighted(self): subset3 = self.mus_func_naive([a, b, c, d], hard) self.assertEqual(set(subset3), {b, d}) -class OCUSTests(OptimalMUSTests): - - def __init__(self, *args, **kwargs): - super().__init__(*args, **kwargs) - self.mus_func = ocus - self.naive_func = ocus_naive - - def test_constrained(self): - a, b, c, d = [cp.boolvar(name=n) for n in "abcd"] - - mus1 = [b, d] - mus2 = [a, b, c] - - hard = [~cp.all(mus1), ~cp.all(mus2)] - subset = self.mus_func([a, b, c, d], hard=hard, meta_constraint = ~b | d) - self.assertSetEqual(set(subset), {b,d}) - subset2 = self.mus_func([a,b,c,d], hard, meta_constraint = a & d) - self.assertSetEqual(set(subset2), {a,b,d}) # not subset-minimal - self.assertRaises(OCUSException, lambda: self.mus_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist - - hard = [~cp.all(mus1), ~cp.all(mus2)] - subset = self.naive_func([a, b, c, d], hard=hard, meta_constraint = ~b | d) - self.assertSetEqual(set(subset), {b,d}) - subset2 = self.naive_func([a,b,c,d], hard, meta_constraint = a & d) - self.assertSetEqual(set(subset2), {a,b,d}) # not subset-minimal - self.assertRaises(OCUSException, lambda: self.naive_func([a,b,c,d], hard, meta_constraint = ~b)) # does not exist - - - class MARCOMUSTests(MusTests): def test_php(self): From 1678c6044c23891883854c2be535b5cb50881d39 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 28 Nov 2025 14:21:01 +0100 Subject: [PATCH 17/47] small refactor in decompose --- cpmpy/transformations/decompose_global.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index e0c5a7a53..3ab5610e1 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -11,7 +11,7 @@ from ..expressions.core import Expression, Comparison, Operator from ..expressions.variables import intvar, cpm_array, NDVarArray from ..expressions.utils import is_any_list, eval_comparison -from ..expressions.python_builtins import all +from ..expressions.python_builtins import all as cpm_all from .flatten_model import flatten_constraint, normalized_numexpr @@ -101,10 +101,15 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to # the `decomposed` expression might contain other global constraints, check it decomposed = decompose_in_tree(value, supported, supported_reified, _toplevel, nested=nested, csemap=csemap) if expr.is_bool(): - newlist.append(all(decomposed)) + value = cpm_all(decomposed) + else: assert len(decomposed) == 1, "Global functions should return a single numerical value, not a list" - newlist.append(decomposed[0]) + value = decomposed[0] + + newlist.append(value) + # TODO save decomp in csemap? Seems to not work with flatten_objective... + elif isinstance(expr, Comparison): if not expr.has_subexpr(): # Only recurse if there are nested expressions From d289506bf94d8c9aaefea39b654c7049eee4d1fd Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 28 Nov 2025 14:23:33 +0100 Subject: [PATCH 18/47] re-add cse to decompose --- cpmpy/transformations/decompose_global.py | 7 ++++++- tests/test_cse.py | 22 ++++++++++++++-------- 2 files changed, 20 insertions(+), 9 deletions(-) diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index 3ab5610e1..a0707c940 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -87,6 +87,10 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to newlist.append(expr) else: # unsupported, need to decompose + # check if it is in the csemap + if csemap is not None and expr in csemap: + newlist.append(csemap[expr]) + dec = expr.decompose() if not isinstance(dec, tuple): warnings.warn(f"Decomposing an old-style global ({expr}) that does not return a tuple, which is " @@ -108,7 +112,8 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to value = decomposed[0] newlist.append(value) - # TODO save decomp in csemap? Seems to not work with flatten_objective... + if csemap is not None: + csemap[expr] = value elif isinstance(expr, Comparison): diff --git a/tests/test_cse.py b/tests/test_cse.py index 125dfd7c0..35c5ca091 100644 --- a/tests/test_cse.py +++ b/tests/test_cse.py @@ -70,23 +70,29 @@ def test_decompose(self): csemap = dict() decomp = decompose_in_tree([nested_cons], csemap=csemap) - self.assertEqual(len(decomp), 6) + self.assertEqual(len(decomp), 5) self.assertEqual(str(decomp[0]), "(b) == ((IV0) + (q) <= 10)") - self.assertEqual(str(decomp[1]), "(IV1) == (IV0)") # TODO... this seems stupid, why do we need this (comes from _max in Maximul decomp)? - self.assertEqual(str(decomp[2]), "or([(x) >= (IV1), (y) >= (IV1), (z) >= (IV1)])") - self.assertEqual(str(decomp[3]), "(x) <= (IV1)") - self.assertEqual(str(decomp[4]), "(y) <= (IV1)") - self.assertEqual(str(decomp[5]), "(z) <= (IV1)") + self.assertEqual(str(decomp[1]), "(x) <= (IV0)") + self.assertEqual(str(decomp[2]), "(y) <= (IV0)") + self.assertEqual(str(decomp[3]), "(z) <= (IV0)") + self.assertEqual(str(decomp[4]), "or([(x) >= (IV0), (y) >= (IV0), (z) >= (IV0)])") + # next time we use max([x,y,z]) it should replace the max-constraint with IV0 - # ... it seems like we should be able to do more here e.g., cp.max([x,y,z]) != 42 should be replaced with IV0 != 42 - # ... but the current code-flow of decompose_in_tree and .decompose_comparison does not allow this nested2 = (q + cp.max([x,y,z]) != 42) decomp = decompose_in_tree([nested2], csemap=csemap) self.assertEqual(len(decomp), 1) self.assertEqual(str(decomp[0]), "(q) + (IV0) != 42") + # also in non-nested cases + nested3 = (cp.max([x, y, z]) == 42) + decomp = decompose_in_tree([nested3], csemap=csemap) + + self.assertEqual(len(decomp), 1) + self.assertEqual(str(decomp[0]), "IV0 == 42") + + def test_only_numexpr_equality(self): x,y,z = cp.intvar(0,10, shape=3, name=tuple("xyz")) From 86d6d496ad839258f0a4ba0fecec786e949eaf22 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 28 Nov 2025 14:23:53 +0100 Subject: [PATCH 19/47] update decompose tests --- tests/test_transf_decompose.py | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/tests/test_transf_decompose.py b/tests/test_transf_decompose.py index afe9c2b83..74673b8ea 100644 --- a/tests/test_transf_decompose.py +++ b/tests/test_transf_decompose.py @@ -55,22 +55,22 @@ def test_decompose_num(self): bv = boolvar(name="bv") cons = [min(ivs) <= 1] - self.assertEqual(str(decompose_in_tree(cons)), - "[IV0 <= 1, ((x) <= (IV0)) or ((y) <= (IV0)), (x) >= (IV0), (y) >= (IV0)]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), + {"IV0 <= 1", "((x) <= (IV0)) or ((y) <= (IV0))", "(x) >= (IV0)", "(y) >= (IV0)"}) # reified cons = [bv.implies(min(ivs) <= 1)] - self.assertEqual(str(decompose_in_tree(cons)), - "[(bv) -> (IV1 <= 1), ((x) <= (IV1)) or ((y) <= (IV1)), (x) >= (IV1), (y) >= (IV1)]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), + {"(bv) -> (IV1 <= 1)", "((x) <= (IV1)) or ((y) <= (IV1))", "(x) >= (IV1)", "(y) >= (IV1)"}) self.assertEqual(str(decompose_in_tree(cons, supported={"min"})),str(cons)) cons = [(min(ivs) <= 1).implies(bv)] - self.assertEqual(str(decompose_in_tree(cons)), - "[(IV2 <= 1) -> (bv), ((x) <= (IV2)) or ((y) <= (IV2)), (x) >= (IV2), (y) >= (IV2)]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), + {"(IV2 <= 1) -> (bv)", "((x) <= (IV2)) or ((y) <= (IV2))", "(x) >= (IV2)", "(y) >= (IV2)"}) self.assertEqual(str(decompose_in_tree(cons, supported={"min"})), str(cons)) cons = [(min(ivs) <= 1) == (bv)] - self.assertEqual(str(decompose_in_tree(cons)), - "[(IV3 <= 1) == (bv), ((x) <= (IV3)) or ((y) <= (IV3)), (x) >= (IV3), (y) >= (IV3)]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), + {"(IV3 <= 1) == (bv)", "((x) <= (IV3)) or ((y) <= (IV3))", "(x) >= (IV3)", "(y) >= (IV3)"}) self.assertEqual(str(decompose_in_tree(cons, supported={"min"})), str(cons)) @@ -79,25 +79,25 @@ def test_decompose_nested(self): ivs = [intvar(1,9,name=n) for n in "xyz"] cons = [AllDifferent(ivs) == 0] - self.assertEqual(str(decompose_in_tree(cons)), "[not([and([(x) != (y), (x) != (z), (y) != (z)])])]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), {"not([and([(x) != (y), (x) != (z), (y) != (z)])])"}) cons = [0 == AllDifferent(ivs)] - self.assertEqual(str(decompose_in_tree(cons)), "[not([and([(x) != (y), (x) != (z), (y) != (z)])])]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), {"not([and([(x) != (y), (x) != (z), (y) != (z)])])"}) cons = [AllDifferent(ivs) == AllEqual(ivs[:-1])] - self.assertEqual(str(decompose_in_tree(cons)), "[(and([(x) != (y), (x) != (z), (y) != (z)])) == ((x) == (y))]") + self.assertSetEqual(set(map(str,decompose_in_tree(cons))), {"(and([(x) != (y), (x) != (z), (y) != (z)])) == ((x) == (y))"}) cons = [min(ivs) == max(ivs)] - self.assertEqual(str(decompose_in_tree(cons, supported={"min"})), - '[(IV0) == (min(x,y,z)), or([(x) >= (IV0), (y) >= (IV0), (z) >= (IV0)]), (x) <= (IV0), (y) <= (IV0), (z) <= (IV0)]') + self.assertSetEqual(set(map(str,decompose_in_tree(cons, supported={"min"}))), + {"(min(x,y,z)) == (IV0)", "or([(x) >= (IV0), (y) >= (IV0), (z) >= (IV0)])", "(x) <= (IV0)", "(y) <= (IV0)", "(z) <= (IV0)"}) - self.assertEqual(str(decompose_in_tree(cons, supported={"max"})), - "[(IV1) == (max(x,y,z)), or([(x) <= (IV1), (y) <= (IV1), (z) <= (IV1)]), (x) >= (IV1), (y) >= (IV1), (z) >= (IV1)]") + self.assertEqual(set(map(str,decompose_in_tree(cons, supported={"max"}))), + {"(IV1) == (max(x,y,z))", "or([(x) <= (IV1), (y) <= (IV1), (z) <= (IV1)])", "(x) >= (IV1)", "(y) >= (IV1)", "(z) >= (IV1)"}) # numerical in non-comparison context cons = [AllEqual([min(ivs[:-1]),ivs[-1]])] - self.assertEqual(str(decompose_in_tree(cons, supported={"allequal"})), - "[allequal(IV2,z), (IV3) == (IV2), ((x) <= (IV3)) or ((y) <= (IV3)), (x) >= (IV3), (y) >= (IV3)]") + self.assertEqual(set(map(str,decompose_in_tree(cons, supported={"allequal"}))), + {"allequal(IV2,z)", "((x) <= (IV2)) or ((y) <= (IV2))", "(x) >= (IV2)", "(y) >= (IV2)"}) self.assertEqual(str(decompose_in_tree(cons, supported={"min"})), "[(min(x,y)) == (z)]") From 63c5cff81f8224f6e1da2630b64f08f68ba7e7b9 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 09:23:08 +0100 Subject: [PATCH 20/47] add tests checking all numexprs as objective --- tests/test_solvers.py | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/tests/test_solvers.py b/tests/test_solvers.py index b0416e7e9..4820372dc 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -21,6 +21,7 @@ from cpmpy import SolverLookup from cpmpy.exceptions import MinizincNameException, NotSupportedError +from test_constraints import numexprs from utils import skip_on_missing_pblib pysat_available = CPM_pysat.supported() @@ -821,10 +822,9 @@ def test_count_mzn(self): m = cp.Model([x + y == 2, wsum == 9]) self.assertTrue(m.solve(solver="minizinc")) -@pytest.mark.parametrize( - "solver", - [name for name, solver in SolverLookup.base_solvers() if solver.supported()] -) + +solvers = [name for name, solver in SolverLookup.base_solvers() if solver.supported()] +@pytest.mark.parametrize("solver", solvers) class TestSupportedSolvers: def test_installed_solvers(self, solver): # basic model @@ -1192,4 +1192,18 @@ def test_optimisation_direction(self, solver): # 4) Minimisation - solver s = cp.SolverLookup.get(solver, m) assert s.solve() - assert s.objective_value() == 5 \ No newline at end of file + assert s.objective_value() == 5 + + + +@pytest.mark.parametrize(("solver", "expr"), [(s, expr) for s in solvers for expr in numexprs(s)], ids=str) +def test_objective_numexprs(solver, expr): + + if solver == "z3": pytest.skip("Optimization in z3 is too slow for testing here.") + + model = cp.Model(cp.intvar(0, 10, shape=3) >= 1) # just to have some constraints + try: + model.minimize(expr) + assert model.solve(solver=solver) + except NotSupportedError: + pytest.skip(reason=f"{solver} does not support optimisation") From ed8e62ebdd2f2b1cf63ed76ac07ac53428cf29a6 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 09:23:22 +0100 Subject: [PATCH 21/47] add safen_objective function --- cpmpy/transformations/safening.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/cpmpy/transformations/safening.py b/cpmpy/transformations/safening.py index f2e9e0f1d..626bcca7c 100644 --- a/cpmpy/transformations/safening.py +++ b/cpmpy/transformations/safening.py @@ -6,7 +6,7 @@ from ..expressions.variables import _NumVarImpl, boolvar, intvar, NDVarArray, cpm_array from ..expressions.core import Expression, Operator, BoolVal -from ..expressions.utils import get_bounds, is_num +from ..expressions.utils import get_bounds, is_num, is_any_list from ..expressions.globalfunctions import GlobalFunction, Element from ..expressions.globalconstraints import DirectConstraint from ..expressions.python_builtins import all as cpm_all @@ -249,3 +249,12 @@ def _safen_hole(cpm_expr, exclude, idx_to_safen): return is_defined, output_var, toplevel +def safen_objective(expr): + if is_any_list(expr): + raise ValueError(f"Expected numerical expression as objective but got a list {expr}") + + toplevel, nbc = [],[] + safe_expr = no_partial_functions([expr], _toplevel=toplevel, _nbc=nbc) + assert len(safe_expr) == 1 + return safe_expr[0], toplevel + nbc + From 8e351f433868796980eb39ec892e7b9707724979 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 09:23:40 +0100 Subject: [PATCH 22/47] add decompose_objective function --- cpmpy/transformations/decompose_global.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index a0707c940..7d76adf44 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -138,6 +138,16 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to return toplevel_list(newlist) + decompose_in_tree(toplevel_list(_toplevel), supported, supported_reified, nested=False, csemap=csemap) +def decompose_objective(expr, supported=set(), csemap=None): + if is_any_list(expr): + raise ValueError(f"Expected a numerical expression as objective but got a list {expr}") + + toplevel = [] + decomp_expr = decompose_in_tree([expr], supported=supported, _toplevel=toplevel, nested=True, csemap=csemap) + assert len(decomp_expr) == 1, f"Expected {expr} to be decomposed into a single expression, but got {decomp_expr}.\nPlease report on github." + return decomp_expr[0], toplevel + + # DEPRECATED! # old way of doing decompositions post-flatten # will be removed in any future version! From fbe3d9320fe6b0f110c340603b7c495cbcc60be2 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 09:23:54 +0100 Subject: [PATCH 23/47] fix objective ortools --- cpmpy/solvers/ortools.py | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index afc68026f..c0a2e9c18 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -56,13 +56,13 @@ from ..expressions.globalconstraints import GlobalConstraint from ..expressions.utils import is_num, is_int, eval_comparison, flatlist, argval, argvals, get_bounds, is_true_cst, \ is_false_cst -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, flatten_objective, get_or_make_var from ..transformations.normalize import toplevel_list from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies from ..transformations.comparison import only_numexpr_equality -from ..transformations.safening import no_partial_functions +from ..transformations.safening import no_partial_functions, safen_objective class CPM_ortools(SolverInterface): @@ -339,17 +339,20 @@ def objective(self, expr, minimize): technical side note: any constraints created during conversion of the objective are premanently posted to the solver """ - # make objective function non-nested - (flat_obj, flat_cons) = flatten_objective(expr, csemap=self._csemap) - self += flat_cons # add potentially created constraints - get_variables(flat_obj, collect=self.user_vars) # add objvars to vars + + # transform objective + obj, safe_cons = safen_objective(expr) + obj, decomp_cons = decompose_objective(obj, supported={"min", "max", "abs", "element"}, csemap=self._csemap) + obj, flat_cons = flatten_objective(obj, csemap=self._csemap) + + self.add(safe_cons+decomp_cons+flat_cons) # make objective function or variable and post - obj = self._make_numexpr(flat_obj) + ort_obj = self._make_numexpr(obj) if minimize: - self.ort_model.Minimize(obj) + self.ort_model.Minimize(ort_obj) else: - self.ort_model.Maximize(obj) + self.ort_model.Maximize(ort_obj) def has_objective(self): return self.ort_model.HasObjective() From 5e2957d51586c80811f47a90dbc8236f29119363 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 09:27:54 +0100 Subject: [PATCH 24/47] fix objective choco --- cpmpy/solvers/choco.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index de432e0da..03c3a83b2 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -59,7 +59,7 @@ from ..expressions.utils import is_num, is_int, is_boolexpr, is_any_list, get_bounds, argval, argvals, STAR from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables -from ..transformations.flatten_model import flatten_constraint +from ..transformations.flatten_model import flatten_constraint, get_or_make_var from ..transformations.comparison import only_numexpr_equality from ..transformations.linearize import canonical_comparison from ..transformations.safening import no_partial_functions @@ -351,13 +351,13 @@ def objective(self, expr, minimize): .. note:: technical side note: constraints created during conversion of the objective - are premanently posted to the solver. Choco accepts variables to maximize or minimize + are permanently posted to the solver. Choco accepts variables to maximize or minimize so it is needed to post constraints and create auxiliary variables """ # make objective function non-nested - obj_var = intvar(*get_bounds(expr)) - self += obj_var == expr + obj_var, obj_cons = get_or_make_var(expr, csemap=self._csemap) + self.add(obj_cons) self.obj = obj_var self.minimize_obj = minimize # Choco has as default to maximize From 95412933b863aa969c195453d445aff8461396b7 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 09:40:55 +0100 Subject: [PATCH 25/47] missing `continue` in decompose --- cpmpy/transformations/decompose_global.py | 1 + 1 file changed, 1 insertion(+) diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index 7d76adf44..328217aa9 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -90,6 +90,7 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to # check if it is in the csemap if csemap is not None and expr in csemap: newlist.append(csemap[expr]) + continue # no need to decompose, just use the variable we already have dec = expr.decompose() if not isinstance(dec, tuple): From c8926806114abc921bac0162e64593bb537cc896 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 13:42:04 +0100 Subject: [PATCH 26/47] save user variables from objective --- cpmpy/solvers/ortools.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index c0a2e9c18..6f28895fd 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -340,6 +340,9 @@ def objective(self, expr, minimize): are premanently posted to the solver """ + # save user varables + get_variables(expr, self.user_vars) + # transform objective obj, safe_cons = safen_objective(expr) obj, decomp_cons = decompose_objective(obj, supported={"min", "max", "abs", "element"}, csemap=self._csemap) From d5576c3bc85c9b528432d5b53b0781540f39cf5d Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 13:42:26 +0100 Subject: [PATCH 27/47] update objective posting gurobi --- cpmpy/solvers/gurobi.py | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 9d1e6f012..82f5bcdf9 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -52,13 +52,13 @@ from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar from ..expressions.globalconstraints import DirectConstraint from ..transformations.comparison import only_numexpr_equality -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.flatten_model import flatten_constraint, flatten_objective from ..transformations.get_variables import get_variables from ..transformations.linearize import linearize_constraint, only_positive_bv, only_positive_bv_wsum from ..transformations.normalize import toplevel_list from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies -from ..transformations.safening import no_partial_functions +from ..transformations.safening import no_partial_functions, safen_objective try: import gurobipy as gp @@ -284,18 +284,20 @@ def objective(self, expr, minimize=True): """ from gurobipy import GRB - # make objective function non-nested - (flat_obj, flat_cons) = flatten_objective(expr, csemap=self._csemap) - flat_obj = only_positive_bv_wsum(flat_obj) # remove negboolviews - get_variables(flat_obj, collect=self.user_vars) # add potentially created variables - self += flat_cons + # transform objective + obj, safe_cons = safen_objective(expr) + obj, decomp_cons = decompose_objective(obj, supported={"min", "max", "abs"}, csemap=self._csemap) + obj, flat_cons = flatten_objective(obj, csemap=self._csemap) + obj = only_positive_bv_wsum(obj) # remove negboolviews + + self.add(safe_cons + decomp_cons + flat_cons) # make objective function or variable and post - obj = self._make_numexpr(flat_obj) + grb_obj = self._make_numexpr(obj) if minimize: - self.grb_model.setObjective(obj, sense=GRB.MINIMIZE) + self.grb_model.setObjective(grb_obj, sense=GRB.MINIMIZE) else: - self.grb_model.setObjective(obj, sense=GRB.MAXIMIZE) + self.grb_model.setObjective(grb_obj, sense=GRB.MAXIMIZE) self.grb_model.update() def has_objective(self): @@ -347,7 +349,7 @@ def transform(self, cpm_expr): # apply transformations, then post internally # expressions have to be linearized to fit in MIP model. See /transformations/linearize cpm_cons = toplevel_list(cpm_expr) - cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div"}) # linearize expects safe exprs + cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"}) # linearize and decompose expect safe exprs supported = {"min", "max", "abs", "alldifferent"} # alldiff has a specialized MIP decomp in linearize cpm_cons = decompose_in_tree(cpm_cons, supported, csemap=self._csemap) cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form From 7b9d3cf5f7d84d7a1e5b0b6d6522e94271c2caad Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 13:46:08 +0100 Subject: [PATCH 28/47] update template --- cpmpy/solvers/TEMPLATE.py | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py index dd3626779..ad2488e54 100644 --- a/cpmpy/solvers/TEMPLATE.py +++ b/cpmpy/solvers/TEMPLATE.py @@ -59,10 +59,12 @@ from ..expressions.utils import is_num, is_any_list, is_boolexpr from ..transformations.get_variables import get_variables from ..transformations.normalize import toplevel_list -from ..transformations.decompose_global import decompose_in_tree -from ..transformations.flatten_model import flatten_constraint +from ..transformations.decompose_global import decompose_in_tree, decompose_objective +from ..transformations.flatten_model import flatten_constraint, flatten_objective from ..transformations.comparison import only_numexpr_equality from ..transformations.reification import reify_rewrite, only_bv_reifies +from ..transformations.safening import safen_objective + class CPM_template(SolverInterface): """ @@ -292,21 +294,28 @@ def objective(self, expr, minimize=True): are permanently posted to the solver) """ - # make objective function non-nested - (flat_obj, flat_cons) = flatten_objective(expr, csemap=self._csemap) - self += flat_cons # add potentially created constraints - self.user_vars.update(get_variables(flat_obj)) # add objvars to vars + + # save user variables + get_variables(expr, self.user_vars) + + # transform objective + obj, safe_cons = safen_objective(expr) + # [GUIDELINE] all globals which unsupported in a nested context should be decomposed here. + obj, decomp_cons = decompose_objective(obj, supported={"min", "max", "element"}, csemap=self._csemap) + obj, flat_cons = flatten_objective(obj, csemap=self._csemap) + + self.add(safe_cons + decomp_cons + flat_cons) # make objective function or variable and post - obj = self._make_numexpr(flat_obj) + tpl_obj = self._make_numexpr(obj) # [GUIDELINE] if the solver interface does not provide a solver native "numeric expression" object, # _make_numexpr may be removed and an objective can be posted as: # self.TPL_solver.MinimizeWeightedSum(obj.args[0], self.solver_vars(obj.args[1]) or similar if minimize: - self.TPL_solver.Minimize(obj) + self.TPL_solver.Minimize(tpl_obj) else: - self.TPL_solver.Maximize(obj) + self.TPL_solver.Maximize(tpl_obj) def has_objective(self): return self.TPL_solver.hasObjective() From 9e87e6548c50066e3211556d2d736a5fa17b3af1 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:33:16 +0100 Subject: [PATCH 29/47] update choco objective --- cpmpy/solvers/choco.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index 03c3a83b2..2a7431e45 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -57,7 +57,7 @@ from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar from ..expressions.globalconstraints import GlobalConstraint from ..expressions.utils import is_num, is_int, is_boolexpr, is_any_list, get_bounds, argval, argvals, STAR -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, get_or_make_var from ..transformations.comparison import only_numexpr_equality @@ -355,9 +355,18 @@ def objective(self, expr, minimize): so it is needed to post constraints and create auxiliary variables """ + # save user vars + get_variables(expr, self.user_vars) + # transform objective + supported = {"min", "max", "abs", "count", "element", "alldifferent", "alldifferent_except0", "allequal", + "table", 'negative_table', "short_table", "regular", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue", "increasing", + "decreasing","strictly_increasing","strictly_decreasing","lex_lesseq", "lex_less", "among", "precedence"} + obj, decomp_cons = decompose_objective(expr, supported=supported, csemap=self._csemap) + # make objective function non-nested - obj_var, obj_cons = get_or_make_var(expr, csemap=self._csemap) - self.add(obj_cons) + obj_var, obj_cons = get_or_make_var(obj, csemap=self._csemap) + + self.add(decomp_cons + obj_cons) self.obj = obj_var self.minimize_obj = minimize # Choco has as default to maximize From e485f6c8739a930bafc742318fc36d05ec3db79c Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:33:32 +0100 Subject: [PATCH 30/47] update cpo objective --- cpmpy/solvers/cpo.py | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/cpmpy/solvers/cpo.py b/cpmpy/solvers/cpo.py index f20913f34..89b9f6c6c 100644 --- a/cpmpy/solvers/cpo.py +++ b/cpmpy/solvers/cpo.py @@ -56,7 +56,7 @@ from ..expressions.utils import is_num, is_any_list, eval_comparison, argval, argvals, get_bounds from ..transformations.get_variables import get_variables from ..transformations.normalize import toplevel_list -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.safening import no_partial_functions @@ -379,14 +379,23 @@ def objective(self, expr, minimize=True): technical side note: any constraints created during conversion of the objective are permanently posted to the solver """ + + # save user variables + get_variables(expr, self.user_vars) + + supported = {'max', 'min', 'abs', 'element', 'nvalue', 'alldifferent', 'table', 'indomain', 'negative_table'} + obj, decomp_cons = decompose_objective(expr, supported=supported) + self.add(decomp_cons) + dom = self.get_docp().modeler if self.has_objective(): self.cpo_model.remove(self.cpo_model.get_objective_expression()) - expr = self._cpo_expr(expr) + + cpo_obj = self._cpo_expr(obj) if minimize: - self.cpo_model.add(dom.minimize(expr)) + self.cpo_model.add(dom.minimize(cpo_obj)) else: - self.cpo_model.add(dom.maximize(expr)) + self.cpo_model.add(dom.maximize(cpo_obj)) def has_objective(self): return self.cpo_model.get_objective() is not None From 4f73a6d3d06a9664c71df3a6299dc678a95dd189 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:33:54 +0100 Subject: [PATCH 31/47] update gcs objective --- cpmpy/solvers/gcs.py | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/cpmpy/solvers/gcs.py b/cpmpy/solvers/gcs.py index 39321f406..e9b4a54d0 100644 --- a/cpmpy/solvers/gcs.py +++ b/cpmpy/solvers/gcs.py @@ -58,12 +58,12 @@ from ..exceptions import NotSupportedError, GCSVerificationException from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..expressions.core import Expression, Comparison, Operator, BoolVal -from ..expressions.variables import _BoolVarImpl, _IntVarImpl, _NumVarImpl, NegBoolView, boolvar +from ..expressions.variables import _BoolVarImpl, _IntVarImpl, _NumVarImpl, NegBoolView, boolvar, intvar from ..expressions.globalconstraints import GlobalConstraint from ..expressions.utils import is_num, argval, argvals -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.get_variables import get_variables -from ..transformations.flatten_model import flatten_constraint, flatten_objective, get_or_make_var +from ..transformations.flatten_model import flatten_constraint, get_or_make_var from ..transformations.safening import no_partial_functions from ..transformations.normalize import toplevel_list @@ -385,20 +385,22 @@ def objective(self, expr, minimize=True): technical side note: any constraints created during conversion of the objective are permanently posted to the solver """ - # make objective function non-nested - (flat_obj, flat_cons) = flatten_objective(expr, csemap=self._csemap) - self += flat_cons # add potentially created constraints - self.user_vars.update(get_variables(flat_obj)) # add objvars to vars - (obj, obj_cons) = get_or_make_var(flat_obj, csemap=self._csemap) - self += obj_cons + # save variables + get_variables(expr, collect=self.user_vars) - self.objective_var = obj + # transform objective + obj, decomp_cons = decompose_objective(expr, csemap=self._csemap, + supported={"min", "max", "abs", "element", "nvalue", "count"}) + obj_var, obj_cons = get_or_make_var(obj, csemap=self._csemap) + self.add(decomp_cons + obj_cons) + + self.objective_var = obj_var if minimize: - self.gcs.minimise(self.solver_var(obj)) + self.gcs.minimise(self.solver_var(obj_var)) else: - self.gcs.maximise(self.solver_var(obj)) + self.gcs.maximise(self.solver_var(obj_var)) def transform(self, cpm_expr): """ From cdf3365af1e291348c4c69bd9cdacbf57d73dd62 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:34:01 +0100 Subject: [PATCH 32/47] save user vars in gurobi --- cpmpy/solvers/gurobi.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 82f5bcdf9..df81baa6f 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -284,6 +284,9 @@ def objective(self, expr, minimize=True): """ from gurobipy import GRB + # save user variables + get_variables(expr, self.user_vars) + # transform objective obj, safe_cons = safen_objective(expr) obj, decomp_cons = decompose_objective(obj, supported={"min", "max", "abs"}, csemap=self._csemap) From 326d52319584ebd557e10b471c1d7df8b78fb904 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:34:11 +0100 Subject: [PATCH 33/47] update objective in minizinc --- cpmpy/solvers/minizinc.py | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index d1227ec91..02cd224b0 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -71,7 +71,7 @@ from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, cpm_array from ..expressions.globalconstraints import DirectConstraint from ..expressions.utils import is_num, is_any_list, argvals, argval -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..exceptions import MinizincPathException, NotSupportedError from ..transformations.get_variables import get_variables from ..transformations.normalize import toplevel_list @@ -555,15 +555,27 @@ def objective(self, expr, minimize): 'objective()' can be called multiple times, only the last one is stored """ - # get_variables(expr, collect=self.user_vars) # add objvars to vars # all are user vars + + # save user variables + get_variables(expr, collect=self.user_vars) # add objvars to vars + + supported = {"min", "max", "abs", "element", "count", "nvalue", "alldifferent", "alldifferent_except0", "allequal", + "inverse", "ite" "xor", "table", "cumulative", "gcc", "increasing", "decreasing", + "no_overlap", "strictly_increasing", "strictly_decreasing", "lex_lesseq", "lex_less", "lex_chain_less", + "lex_chain_lesseq", "among"} + + # transform objective + obj, decomp_cons = decompose_objective(expr, supported=supported) + self.add(decomp_cons) # make objective function or variable and post - obj = self._convert_expression(expr) + + mzn_obj = self._convert_expression(obj) # do not add it to the mzn_model yet, supports only one 'solve' entry if minimize: - self.mzn_txt_solve = "solve minimize {};\n".format(obj) + self.mzn_txt_solve = "solve minimize {};\n".format(mzn_obj) else: - self.mzn_txt_solve = "solve maximize {};\n".format(obj) + self.mzn_txt_solve = "solve maximize {};\n".format(mzn_obj) def has_objective(self): return self.mzn_txt_solve != "solve satisfy;" From 6b420ea10ea33e5cb7af8607127e8076d56a9617 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:34:29 +0100 Subject: [PATCH 34/47] update objective in exact --- cpmpy/solvers/exact.py | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 37c00c1b0..642ea986c 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -59,11 +59,11 @@ from ..transformations.comparison import only_numexpr_equality from ..transformations.flatten_model import flatten_constraint, flatten_objective from ..transformations.get_variables import get_variables -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.linearize import linearize_constraint, only_positive_bv, only_positive_bv_wsum from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies from ..transformations.normalize import toplevel_list -from ..transformations.safening import no_partial_functions +from ..transformations.safening import no_partial_functions, safen_objective from ..expressions.globalconstraints import DirectConstraint from ..expressions.utils import flatlist, argvals, argval from ..exceptions import NotSupportedError @@ -436,14 +436,19 @@ def objective(self, expr, minimize): self.objective_ = expr self.objective_is_min_ = minimize - # make objective function non-nested and with positive BoolVars only - (flat_obj, flat_cons) = flatten_objective(expr, csemap=self._csemap) - flat_obj = only_positive_bv_wsum(flat_obj) # remove negboolviews - self.user_vars.update(get_variables(flat_obj)) # add objvars to vars - self += flat_cons # add potentially created constraints + # save user variables + get_variables(expr, self.user_vars) + + # transform objective + obj, safe_cons = safen_objective(expr) + obj, decomp_cons = decompose_objective(obj, csemap=self._csemap) + obj, flat_cons = flatten_objective(obj, csemap=self._csemap) + obj = only_positive_bv_wsum(obj) # remove negboolviews + + self.add(safe_cons + decomp_cons + flat_cons) # make objective function or variable and post - xct_cfvars,xct_rhs = self._make_numexpr(flat_obj,0) + xct_cfvars,xct_rhs = self._make_numexpr(obj,0) # TODO: make this a custom transformation? newcfvrs = [] From 665aaf4c74212d8a0d17ba6e12c5da65a9555282 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:34:44 +0100 Subject: [PATCH 35/47] update objective in cplex --- cpmpy/solvers/cplex.py | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index 79d256ca7..0c502843a 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -60,13 +60,15 @@ from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar from ..expressions.globalconstraints import DirectConstraint from ..transformations.comparison import only_numexpr_equality -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.flatten_model import flatten_constraint, flatten_objective from ..transformations.get_variables import get_variables -from ..transformations.linearize import linearize_constraint, only_positive_bv, only_positive_bv_wsum +from ..transformations.linearize import linearize_constraint, only_positive_bv, only_positive_bv_wsum, \ + only_positive_bv_wsum_const from ..transformations.normalize import toplevel_list from ..transformations.reification import only_implies, reify_rewrite, only_bv_reifies -from ..transformations.safening import no_partial_functions +from ..transformations.safening import no_partial_functions, safen_objective + class CPM_cplex(SolverInterface): """ @@ -148,6 +150,7 @@ def __init__(self, cpm_model=None, subsolver=None): from docplex.mp.model import Model self.cplex_model = Model() + self._obj_offset = 0 super().__init__(name="cplex", cpm_model=cpm_model) @property @@ -299,18 +302,23 @@ def objective(self, expr, minimize=True): technical side note: any constraints created during conversion of the objective are premanently posted to the solver """ - # make objective function non-nested - (flat_obj, flat_cons) = flatten_objective(expr) - flat_obj = only_positive_bv_wsum(flat_obj) # remove negboolviews - get_variables(flat_obj, collect=self.user_vars) # add potentially created variables - self.add(flat_cons) + # save user vars + get_variables(expr, self.user_vars) + + # transform objective + obj, safe_cons = safen_objective(expr) + obj, decomp_cons = decompose_objective(obj, supported={"min", "max", "abs"}, csemap=self._csemap) + obj, flat_cons = flatten_objective(obj, csemap=self._csemap) + obj, self._obj_offset = only_positive_bv_wsum_const(obj) # remove negboolviews + + self.add(safe_cons + decomp_cons + flat_cons) # make objective function or variable and post - obj = self._make_numexpr(flat_obj) + cplex_obj = self._make_numexpr(obj) if minimize: - self.cplex_model.set_objective('min',obj) + self.cplex_model.set_objective('min', cplex_obj) else: - self.cplex_model.set_objective('max', obj) + self.cplex_model.set_objective('max', cplex_obj) def has_objective(self): return self.cplex_model.is_optimized() @@ -600,7 +608,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from # Translate objective if self.has_objective(): - self.objective_value_ = sol_obj_val + self.objective_value_ = sol_obj_val + self._obj_offset if display is not None: if isinstance(display, Expression): From ec3eb69d14c6a82b0cf371ed14dba52b92efc1f3 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:34:51 +0100 Subject: [PATCH 36/47] update objective in pumpkin --- cpmpy/solvers/pumpkin.py | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/cpmpy/solvers/pumpkin.py b/cpmpy/solvers/pumpkin.py index f1f5d0034..a2e6fd3c4 100644 --- a/cpmpy/solvers/pumpkin.py +++ b/cpmpy/solvers/pumpkin.py @@ -52,8 +52,8 @@ from ..transformations.get_variables import get_variables from ..transformations.linearize import canonical_comparison from ..transformations.normalize import toplevel_list -from ..transformations.decompose_global import decompose_in_tree -from ..transformations.flatten_model import flatten_constraint +from ..transformations.decompose_global import decompose_in_tree, decompose_objective +from ..transformations.flatten_model import flatten_constraint, get_or_make_var from ..transformations.comparison import only_numexpr_equality from ..transformations.reification import reify_rewrite, only_bv_reifies, only_implies from ..transformations.safening import no_partial_functions @@ -290,11 +290,21 @@ def objective(self, expr, minimize=True): technical side note: any constraints created during conversion of the objective are premanently posted to the solver """ - # make objective function non-nested - obj_var = intvar(*get_bounds(expr)) - self += expr == obj_var - # make objective function or variable and post + # save user variables + get_variables(expr, self.user_vars) + + # transform objective + obj, decomp_cons = decompose_objective(expr, supported={"min", "max", "element", "abs"}, csemap=self._csemap) + obj_var, obj_cons = get_or_make_var(obj, csemap=self._csemap) + if expr.is_bool(): + ivar = intvar(0,1) + obj_cons += [ivar == obj_var] + obj_var = ivar + + self.add(decomp_cons + obj_cons) + + # save objective function self._objective = obj_var self.objective_is_min = minimize From 2583444b94d910a71648dfa31f398a09bbdb662f Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:34:56 +0100 Subject: [PATCH 37/47] update objective in z3 --- cpmpy/solvers/z3.py | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 3451583d3..93f310e8a 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -56,9 +56,9 @@ from ..expressions.globalfunctions import GlobalFunction from ..expressions.variables import _BoolVarImpl, NegBoolView, _NumVarImpl, _IntVarImpl, intvar from ..expressions.utils import is_num, is_any_list, is_bool, is_int, is_boolexpr, eval_comparison -from ..transformations.decompose_global import decompose_in_tree +from ..transformations.decompose_global import decompose_in_tree, decompose_objective from ..transformations.normalize import toplevel_list -from ..transformations.safening import no_partial_functions +from ..transformations.safening import no_partial_functions, safen_objective class CPM_z3(SolverInterface): @@ -312,17 +312,20 @@ def objective(self, expr, minimize=True): if not isinstance(self.z3_solver, z3.Optimize): raise NotSupportedError("Use the z3 optimizer for optimization problems") - if isinstance(expr, GlobalFunction): # not supported by Z3 - obj_var = intvar(*expr.get_bounds()) - self += expr == obj_var - expr = obj_var + # transform objective + obj, safe_cons = safen_objective(expr) + obj, decomp_cons = decompose_objective(obj, csemap=self._csemap) - obj = self._z3_expr(expr) + self.add(safe_cons + decomp_cons) + + z3_obj = self._z3_expr(obj) + if isinstance(z3_obj, z3.BoolRef): + z3_obj = z3.If(z3_obj, 1, 0) # must be integer if minimize: - self.obj_handle = self.z3_solver.minimize(obj) + self.obj_handle = self.z3_solver.minimize(z3_obj) self._minimize = True # record direction of optimisation else: - self.obj_handle = self.z3_solver.maximize(obj) + self.obj_handle = self.z3_solver.maximize(z3_obj) self._minimize = False # record direction of optimisation From 3e063ba1128632c9fa37d25dc8c874f7cc07c7f4 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 14:35:16 +0100 Subject: [PATCH 38/47] update tests --- tests/test_solvers.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/test_solvers.py b/tests/test_solvers.py index 4820372dc..c687fcce2 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -1205,5 +1205,9 @@ def test_objective_numexprs(solver, expr): try: model.minimize(expr) assert model.solve(solver=solver) + assert expr.value() < expr.get_bounds()[1] # bounds are not always tight, but should be smaller than ub for sure + model.maximize(expr) + assert model.solve(solver=solver) + assert expr.value() > expr.get_bounds()[0] # bounds are not always tight, but should be larger than lb for sure except NotSupportedError: pytest.skip(reason=f"{solver} does not support optimisation") From abe9d65ddf467644bb160b80f5cfa72b78dfaa57 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:23:32 +0100 Subject: [PATCH 39/47] call safening before decompose for all solvers --- cpmpy/solvers/exact.py | 2 +- cpmpy/solvers/pindakaas.py | 2 +- cpmpy/solvers/pysat.py | 2 ++ cpmpy/solvers/z3.py | 2 +- 4 files changed, 5 insertions(+), 3 deletions(-) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 642ea986c..6938f714c 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -509,7 +509,7 @@ def transform(self, cpm_expr): """ cpm_cons = toplevel_list(cpm_expr) - cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div"}) # linearize expects safe exprs + cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"}) # linearize and decompose expects safe exprs cpm_cons = decompose_in_tree(cpm_cons, supported=frozenset({'alldifferent', 'abs'}), csemap=self._csemap) # Abs and Alldiff have a specialized MIP decomp cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum']), csemap=self._csemap) # constraints that support reification diff --git a/cpmpy/solvers/pindakaas.py b/cpmpy/solvers/pindakaas.py index 20540903a..64189319e 100755 --- a/cpmpy/solvers/pindakaas.py +++ b/cpmpy/solvers/pindakaas.py @@ -231,7 +231,7 @@ def solver_var(self, cpm_var): def transform(self, cpm_expr): cpm_cons = toplevel_list(cpm_expr) - cpm_cons = no_partial_functions(cpm_cons) + cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"div", "mod", "element"}) cpm_cons = decompose_in_tree(cpm_cons, csemap=self._csemap) cpm_cons = simplify_boolean(cpm_cons) cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index def9e6804..835a9281c 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -70,6 +70,7 @@ from ..transformations.normalize import toplevel_list, simplify_boolean from ..transformations.reification import only_implies, only_bv_reifies from ..transformations.int2bool import int2bool, _encode_int_var, _decide_encoding +from ..transformations.safening import no_partial_functions class CPM_pysat(SolverInterface): @@ -366,6 +367,7 @@ def transform(self, cpm_expr): :return: list of Expression """ cpm_cons = toplevel_list(cpm_expr) + cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"div", "mod", "element"}) cpm_cons = decompose_in_tree(cpm_cons, supported=frozenset({"alldifferent"}), csemap=self._csemap) cpm_cons = simplify_boolean(cpm_cons) cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 93f310e8a..d5a003f8b 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -345,7 +345,7 @@ def transform(self, cpm_expr): """ cpm_cons = toplevel_list(cpm_expr) - cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"div", "mod"}) + cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"div", "mod", "element"}) supported = {"alldifferent", "xor", "ite"} # z3 accepts these reified too cpm_cons = decompose_in_tree(cpm_cons, supported, supported, csemap=self._csemap) return cpm_cons From 8757ac797eaef2a887d2c5fbd6c94d521e230843 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:30:34 +0100 Subject: [PATCH 40/47] update element decompose test --- tests/test_globalconstraints.py | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index 2b8c8e20e..e3a19c2da 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -8,6 +8,8 @@ from cpmpy.exceptions import TypeError, NotSupportedError from cpmpy.expressions.utils import STAR, argvals from cpmpy.solvers import CPM_minizinc +from cpmpy.transformations.decompose_global import decompose_in_tree +from cpmpy.transformations.safening import no_partial_functions from utils import skip_on_missing_pblib @@ -1449,8 +1451,17 @@ def test_element_index_dom_mismatched(self): Check transform of `[0,1,2][x in -1..1] == y in 1..5` Note the index variable has a lower bound *outside* the indexable range, and an upper bound inside AND lower than the indexable range upper bound """ - constraint=cp.Element([0,1,2], cp.intvar(-1,1, name="x")) - self.assertEqual( - str(constraint.decompose_comparison("==", cp.intvar(1,5, name="y"))), - "([(x == 0) -> (y == 0), (x == 1) -> (y == 1), x >= 0, x <= 1], [])" - ) + constraint=cp.Element([0,1,2], cp.intvar(-1,1, name="x")) <= cp.intvar(1,5, name="y") + decomposed = decompose_in_tree(no_partial_functions([constraint], safen_toplevel={"element"})) + self.assertSetEqual(set(map(str, decomposed)), { + # safening constraints + "(BV0) == ((x >= 0) and (x <= 2))", + "(BV0) -> ((IV0) == (x))", + "(~BV0) -> (IV0 == 0)", + "BV0", + # actual decomposition + '(IV0 == 0) -> (IV1 == 0)', + '(IV0 == 1) -> (IV1 == 1)', + '(IV0 == 2) -> (IV1 == 2)', + '(IV1) <= (y)' + }) \ No newline at end of file From 3603f3037fee60c150451f27cda410031a4d267e Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:36:48 +0100 Subject: [PATCH 41/47] linear friendly element decomposition --- cpmpy/expressions/globalfunctions.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 0d7882197..80c3001cf 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -283,13 +283,10 @@ def decompose(self): 2) a list of defining constraints, which should be enforced toplevel """ arr, idx = self.args - idx_lb, idx_ub = get_bounds(idx) assert idx_lb >= 0 and idx_ub < len(arr), "Element constraint is unsafe to decompose as it can be partial. Safen first using `cpmpy.transformations.safening.no_partial_functions`" - _elem = intvar(*self.get_bounds()) - - return _elem, [implies(idx == i, _elem == arr[i]) for i in range(len(arr))] + return sum((idx == i) * arr[i] for i in range(len(arr))), [] def __repr__(self): From cd12409171f4388b868b735ca4888f32797c35f2 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:36:54 +0100 Subject: [PATCH 42/47] update test --- tests/test_globalconstraints.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index e3a19c2da..d84c7f446 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -1460,8 +1460,5 @@ def test_element_index_dom_mismatched(self): "(~BV0) -> (IV0 == 0)", "BV0", # actual decomposition - '(IV0 == 0) -> (IV1 == 0)', - '(IV0 == 1) -> (IV1 == 1)', - '(IV0 == 2) -> (IV1 == 2)', - '(IV1) <= (y)' + '(sum([0, 1, 2] * [IV0 == 0, IV0 == 1, IV0 == 2])) <= (y)' }) \ No newline at end of file From 8b0cf5b3ea2ed5e32944d7ebfb88106af7546d72 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:40:55 +0100 Subject: [PATCH 43/47] Revert "update test" This reverts commit cd12409171f4388b868b735ca4888f32797c35f2. --- tests/test_globalconstraints.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index d84c7f446..e3a19c2da 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -1460,5 +1460,8 @@ def test_element_index_dom_mismatched(self): "(~BV0) -> (IV0 == 0)", "BV0", # actual decomposition - '(sum([0, 1, 2] * [IV0 == 0, IV0 == 1, IV0 == 2])) <= (y)' + '(IV0 == 0) -> (IV1 == 0)', + '(IV0 == 1) -> (IV1 == 1)', + '(IV0 == 2) -> (IV1 == 2)', + '(IV1) <= (y)' }) \ No newline at end of file From c1f2bf1d2840181b4f1e123bf08c32e1a47f324d Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:41:01 +0100 Subject: [PATCH 44/47] Revert "linear friendly element decomposition" This reverts commit 3603f3037fee60c150451f27cda410031a4d267e. --- cpmpy/expressions/globalfunctions.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 80c3001cf..0d7882197 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -283,10 +283,13 @@ def decompose(self): 2) a list of defining constraints, which should be enforced toplevel """ arr, idx = self.args + idx_lb, idx_ub = get_bounds(idx) assert idx_lb >= 0 and idx_ub < len(arr), "Element constraint is unsafe to decompose as it can be partial. Safen first using `cpmpy.transformations.safening.no_partial_functions`" - return sum((idx == i) * arr[i] for i in range(len(arr))), [] + _elem = intvar(*self.get_bounds()) + + return _elem, [implies(idx == i, _elem == arr[i]) for i in range(len(arr))] def __repr__(self): From 350fffe0c628ba3fe3b460d5bbb3a5eb2f2a3a76 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 15:41:24 +0100 Subject: [PATCH 45/47] safen element in cplex --- cpmpy/solvers/cplex.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index 0c502843a..c294b9d5c 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -369,7 +369,7 @@ def transform(self, cpm_expr): # apply transformations, then post internally # expressions have to be linearized to fit in MIP model. See /transformations/linearize cpm_cons = toplevel_list(cpm_expr) - cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div"}) # linearize expects safe exprs + cpm_cons = no_partial_functions(cpm_cons, safen_toplevel={"mod", "div", "element"}) # linearize and decompose expect safe exprs supported = {"min", "max", "abs", "alldifferent"} # alldiff has a specialized MIP decomp in linearize cpm_cons = decompose_in_tree(cpm_cons, supported, csemap=self._csemap) cpm_cons = flatten_constraint(cpm_cons, csemap=self._csemap) # flat normal form From a5ddb03c950698fec82b6686d112ece628618a87 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 19:07:53 +0100 Subject: [PATCH 46/47] do not pass csemap to get_or_make_var --- cpmpy/solvers/choco.py | 3 ++- cpmpy/solvers/gcs.py | 2 +- cpmpy/solvers/pumpkin.py | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index 2a7431e45..773e6d561 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -357,6 +357,7 @@ def objective(self, expr, minimize): # save user vars get_variables(expr, self.user_vars) + # transform objective supported = {"min", "max", "abs", "count", "element", "alldifferent", "alldifferent_except0", "allequal", "table", 'negative_table', "short_table", "regular", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue", "increasing", @@ -364,7 +365,7 @@ def objective(self, expr, minimize): obj, decomp_cons = decompose_objective(expr, supported=supported, csemap=self._csemap) # make objective function non-nested - obj_var, obj_cons = get_or_make_var(obj, csemap=self._csemap) + obj_var, obj_cons = get_or_make_var(obj) # do not pass csemap here, we will still transform obj_var == obj... self.add(decomp_cons + obj_cons) diff --git a/cpmpy/solvers/gcs.py b/cpmpy/solvers/gcs.py index e9b4a54d0..4dff7866d 100644 --- a/cpmpy/solvers/gcs.py +++ b/cpmpy/solvers/gcs.py @@ -392,7 +392,7 @@ def objective(self, expr, minimize=True): # transform objective obj, decomp_cons = decompose_objective(expr, csemap=self._csemap, supported={"min", "max", "abs", "element", "nvalue", "count"}) - obj_var, obj_cons = get_or_make_var(obj, csemap=self._csemap) + obj_var, obj_cons = get_or_make_var(obj) # do not pass csemap here, we will still transform obj_var == obj... self.add(decomp_cons + obj_cons) self.objective_var = obj_var diff --git a/cpmpy/solvers/pumpkin.py b/cpmpy/solvers/pumpkin.py index a2e6fd3c4..31bd1d35f 100644 --- a/cpmpy/solvers/pumpkin.py +++ b/cpmpy/solvers/pumpkin.py @@ -296,7 +296,7 @@ def objective(self, expr, minimize=True): # transform objective obj, decomp_cons = decompose_objective(expr, supported={"min", "max", "element", "abs"}, csemap=self._csemap) - obj_var, obj_cons = get_or_make_var(obj, csemap=self._csemap) + obj_var, obj_cons = get_or_make_var(obj) # do not pass csemap here, we will still transform obj_var == obj... if expr.is_bool(): ivar = intvar(0,1) obj_cons += [ivar == obj_var] From 416a94f243ec0fe24d5ca1836bf6a228fd7eceee Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 4 Dec 2025 19:08:03 +0100 Subject: [PATCH 47/47] disable element test --- tests/test_globalconstraints.py | 39 +++++++++++++++++---------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index e3a19c2da..6e9c171e4 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -1446,22 +1446,23 @@ def test_issue_699(self): self.assertTrue(cp.Model(cp.AllDifferentExceptN([x,3,y,0], [3,0]).decompose()).solve()) - def test_element_index_dom_mismatched(self): - """ - Check transform of `[0,1,2][x in -1..1] == y in 1..5` - Note the index variable has a lower bound *outside* the indexable range, and an upper bound inside AND lower than the indexable range upper bound - """ - constraint=cp.Element([0,1,2], cp.intvar(-1,1, name="x")) <= cp.intvar(1,5, name="y") - decomposed = decompose_in_tree(no_partial_functions([constraint], safen_toplevel={"element"})) - self.assertSetEqual(set(map(str, decomposed)), { - # safening constraints - "(BV0) == ((x >= 0) and (x <= 2))", - "(BV0) -> ((IV0) == (x))", - "(~BV0) -> (IV0 == 0)", - "BV0", - # actual decomposition - '(IV0 == 0) -> (IV1 == 0)', - '(IV0 == 1) -> (IV1 == 1)', - '(IV0 == 2) -> (IV1 == 2)', - '(IV1) <= (y)' - }) \ No newline at end of file + # disabled after #793, unsafe element can no longer be decomposed + # def test_element_index_dom_mismatched(self): + # """ + # Check transform of `[0,1,2][x in -1..1] == y in 1..5` + # Note the index variable has a lower bound *outside* the indexable range, and an upper bound inside AND lower than the indexable range upper bound + # """ + # constraint=cp.Element([0,1,2], cp.intvar(-1,1, name="x")) <= cp.intvar(1,5, name="y") + # decomposed = decompose_in_tree(no_partial_functions([constraint], safen_toplevel={"element"})) + # self.assertSetEqual(set(map(str, decomposed)), { + # # safening constraints + # "(BV0) == ((x >= 0) and (x <= 2))", + # "(BV0) -> ((IV0) == (x))", + # "(~BV0) -> (IV0 == 0)", + # "BV0", + # # actual decomposition + # '(IV0 == 0) -> (IV1 == 0)', + # '(IV0 == 1) -> (IV1 == 1)', + # '(IV0 == 2) -> (IV1 == 2)', + # '(IV1) <= (y)' + # }) \ No newline at end of file