From d7e4125b3902d0dcc3f32d4c2cc2784b043f2337 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Mon, 4 Aug 2025 13:43:57 +0200 Subject: [PATCH 01/10] add tests --- tests/test_solvers.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/test_solvers.py b/tests/test_solvers.py index 292890299..77a4a86b3 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -845,6 +845,9 @@ def test_incremental_assumptions(self, solver): assert s.solve(assumptions=[]) + # better for user experience: allow to use set of assumptions too + assert s.solve(assumptions={x,y}) + def test_vars_not_removed(self, solver): bvs = cp.boolvar(shape=3) m = cp.Model([cp.any(bvs) <= 2]) From fddeaeb63fd52ff143859226ed7ce648e42189f7 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Mon, 4 Aug 2025 13:44:12 +0200 Subject: [PATCH 02/10] update for ortools --- cpmpy/solvers/ortools.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 2029110f5..174f2a054 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -193,7 +193,7 @@ def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwa self.ort_solver.parameters.max_time_in_seconds = float(time_limit) if assumptions is not None: - ort_assum_vars = self.solver_vars(assumptions) + ort_assum_vars = self.solver_vars(list(assumptions)) # dict mapping ortools vars to CPMpy vars self.assumption_dict = {ort_var.Index(): cpm_var for (cpm_var, ort_var) in zip(assumptions, ort_assum_vars)} self.ort_model.ClearAssumptions() # because add just appends From 4d56d67906deaec1d863b8c387454f69f9a09ab3 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Mon, 4 Aug 2025 13:44:20 +0200 Subject: [PATCH 03/10] update pysat --- cpmpy/solvers/pysat.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 1b4502fef..b3751187e 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -228,7 +228,7 @@ def solve(self, time_limit=None, assumptions=None): if assumptions is None: pysat_assum_vars = [] # default if no assumptions else: - pysat_assum_vars = self.solver_vars(assumptions) + pysat_assum_vars = self.solver_vars(list(assumptions)) self.assumption_vars = assumptions import time From 1fcdd0e0a6b03122d16e770934f4f7c5617547b6 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Mon, 4 Aug 2025 13:44:30 +0200 Subject: [PATCH 04/10] update for z3 --- cpmpy/solvers/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 26b84622f..549237a36 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -54,7 +54,7 @@ from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.globalconstraints import GlobalConstraint, DirectConstraint from ..expressions.globalfunctions import GlobalFunction -from ..expressions.variables import _BoolVarImpl, NegBoolView, _NumVarImpl, _IntVarImpl, intvar +from ..expressions.variables import _BfoolVarImpl, 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.normalize import toplevel_list @@ -184,7 +184,7 @@ def solve(self, time_limit=None, assumptions=[], **kwargs): self.z3_solver.set(timeout=int(time_limit*1000)) - z3_assum_vars = self.solver_vars(assumptions) + z3_assum_vars = self.solver_vars(list(assumptions)) self.assumption_dict = {z3_var : cpm_var for (cpm_var, z3_var) in zip(assumptions, z3_assum_vars)} From 1cd3ea197ea60d897c59002ae02bb7f71041f621 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Mon, 4 Aug 2025 13:48:40 +0200 Subject: [PATCH 05/10] undo typo --- cpmpy/solvers/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 549237a36..a8a02ddf5 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -54,7 +54,7 @@ from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.globalconstraints import GlobalConstraint, DirectConstraint from ..expressions.globalfunctions import GlobalFunction -from ..expressions.variables import _BfoolVarImpl, NegBoolView, _NumVarImpl, _IntVarImpl, intvar +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.normalize import toplevel_list From f206d487858a8308d8add8922d33c52d4f31c095 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Wed, 6 Aug 2025 12:08:33 +0200 Subject: [PATCH 06/10] update pumpkin to use flat assumptions --- cpmpy/solvers/pumpkin.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/pumpkin.py b/cpmpy/solvers/pumpkin.py index 1cbbb7d96..57d2bf306 100644 --- a/cpmpy/solvers/pumpkin.py +++ b/cpmpy/solvers/pumpkin.py @@ -47,7 +47,7 @@ from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.globalconstraints import GlobalConstraint from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar, boolvar -from ..expressions.utils import is_num, is_any_list, get_bounds +from ..expressions.utils import flatlist, is_num, is_any_list, get_bounds from ..transformations.get_variables import get_variables from ..transformations.linearize import canonical_comparison from ..transformations.normalize import toplevel_list @@ -151,6 +151,7 @@ def solve(self, time_limit=None, prove=False, proof_name="proof.drcp", proof_loc elif assumptions is not None: assert not prove, "Proof-logging under assumptions is not supported" + assumptions = flatlist(assumptions) pum_assumptions = [self.to_predicate(a) for a in assumptions] self.assump_map = dict(zip(pum_assumptions, assumptions)) solve_func = self.pum_solver.satisfy_under_assumptions From c4e3cc3607fb95b8971206751e0a35d65a690426 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Wed, 6 Aug 2025 12:08:46 +0200 Subject: [PATCH 07/10] update pysat to use flat assumptions --- cpmpy/solvers/pysat.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index e9bdbd849..e5b681152 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -251,7 +251,8 @@ def solve(self, time_limit=None, assumptions=None): if assumptions is None: pysat_assum_vars = [] # default if no assumptions else: - pysat_assum_vars = self.solver_vars(list(assumptions)) + assumptions = flatlist(assumptions) + pysat_assum_vars = self.solver_vars(assumptions) self.assumption_vars = assumptions # set time limit From b183132665b829458afd7396ac508bc8bc212ae1 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Wed, 6 Aug 2025 12:08:56 +0200 Subject: [PATCH 08/10] update z3 --- cpmpy/solvers/z3.py | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index a8a02ddf5..9c40eee7a 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -55,7 +55,7 @@ from ..expressions.globalconstraints import GlobalConstraint, DirectConstraint 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 ..expressions.utils import flatlist, is_num, is_any_list, is_bool, is_int, is_boolexpr, eval_comparison from ..transformations.decompose_global import decompose_in_tree from ..transformations.normalize import toplevel_list from ..transformations.safening import no_partial_functions @@ -139,7 +139,7 @@ def native_model(self): return self.z3_solver - def solve(self, time_limit=None, assumptions=[], **kwargs): + def solve(self, time_limit=None, assumptions=None, **kwargs): """ Call the z3 solver @@ -184,8 +184,12 @@ def solve(self, time_limit=None, assumptions=[], **kwargs): self.z3_solver.set(timeout=int(time_limit*1000)) - z3_assum_vars = self.solver_vars(list(assumptions)) - self.assumption_dict = {z3_var : cpm_var for (cpm_var, z3_var) in zip(assumptions, z3_assum_vars)} + if assumptions is not None: + assumptions = flatlist(assumptions) + z3_assum_vars = self.solver_vars(assumptions) + self.assumption_dict = {z3_var : cpm_var for (cpm_var, z3_var) in zip(assumptions, z3_assum_vars)} + else: + z3_assum_vars = [] # call the solver, with parameters From 1bb3b5484d7f800f4c09d82361a8e6a03957dc85 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Wed, 6 Aug 2025 12:09:14 +0200 Subject: [PATCH 09/10] update ortools --- cpmpy/solvers/ortools.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 174f2a054..920402d38 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -193,7 +193,7 @@ def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwa self.ort_solver.parameters.max_time_in_seconds = float(time_limit) if assumptions is not None: - ort_assum_vars = self.solver_vars(list(assumptions)) + ort_assum_vars = self.solver_vars(flatlist(assumptions)) # dict mapping ortools vars to CPMpy vars self.assumption_dict = {ort_var.Index(): cpm_var for (cpm_var, ort_var) in zip(assumptions, ort_assum_vars)} self.ort_model.ClearAssumptions() # because add just appends From af6387318d7d51b543956ccef7aa2ebdafeac91c Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Wed, 6 Aug 2025 12:09:29 +0200 Subject: [PATCH 10/10] update exact interface --- cpmpy/solvers/exact.py | 1 + 1 file changed, 1 insertion(+) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 96e4441ab..cb974dda0 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -203,6 +203,7 @@ def solve(self, time_limit=None, assumptions=None, **kwargs): # set assumptions if assumptions is not None: + assumptions = flatlist(assumptions) assert all(v.is_bool() for v in assumptions), "Non-Boolean assumptions given to Exact: " + str([v for v in assumptions if not v.is_bool()]) assump_vals = [int(not isinstance(v, NegBoolView)) for v in assumptions] assump_vars = [self.solver_var(v._bv if isinstance(v, NegBoolView) else v) for v in assumptions]