From d08868c96eb07dcf284b2cf6c42598bda241d494 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Thu, 18 Jul 2024 11:28:29 +0200 Subject: [PATCH 1/7] allow kwargs in Model.solve() (#502) --- cpmpy/model.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cpmpy/model.py b/cpmpy/model.py index 0b95daeab..d696213e3 100644 --- a/cpmpy/model.py +++ b/cpmpy/model.py @@ -136,7 +136,7 @@ def maximize(self, expr): self.objective(expr, minimize=False) # solver: name of supported solver or any SolverInterface object - def solve(self, solver=None, time_limit=None): + def solve(self, solver=None, time_limit=None, **kwargs): """ Send the model to a solver and get the result :param solver: name of a solver to use. Run SolverLookup.solvernames() to find out the valid solver names on your system. (default: None = first available solver) @@ -156,7 +156,7 @@ def solve(self, solver=None, time_limit=None): s = SolverLookup.get(solver, self) # call solver - ret = s.solve(time_limit=time_limit) + ret = s.solve(time_limit=time_limit, **kwargs) # store CPMpy status (s object has no further use) self.cpm_status = s.status() return ret From 07f6edf00f22565460133425ebfe888c5b6202fe Mon Sep 17 00:00:00 2001 From: Thomas Sergeys <49067410+ThomSerg@users.noreply.github.com> Date: Thu, 18 Jul 2024 11:38:51 +0200 Subject: [PATCH 2/7] Minizinc print (#504) * Minizinc & Flatzinc strings --- cpmpy/solvers/minizinc.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 0aae6579c..111ea3e61 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -697,3 +697,19 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from finally: asyncio.events.set_event_loop(None) loop.close() + + def minizinc_string(self) -> str: + """ + Returns the model as represented in the Minizinc language. + """ + return "".join(self._pre_solve()[1]._code_fragments) + + def flatzinc_string(self, **kwargs) -> str: + """ + Returns the model as represented in the Flatzinc language. + """ + with self._pre_solve()[1].flat(**kwargs) as (fzn, ozn, statistics): + with open(fzn.name) as f: + f.seek(0) + contents = f.readlines() + return "".join(contents) \ No newline at end of file From 2096c57a448baef1dcd08d33da8a687981c4d609 Mon Sep 17 00:00:00 2001 From: Wout Date: Thu, 18 Jul 2024 14:25:23 +0200 Subject: [PATCH 3/7] Pysat updates (#508) * don't give pycryptosat as valid subsolver --- .github/workflows/python-test.yml | 1 - cpmpy/solvers/pysat.py | 5 +++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/python-test.yml b/.github/workflows/python-test.yml index e892f30bd..6bd17645c 100644 --- a/.github/workflows/python-test.yml +++ b/.github/workflows/python-test.yml @@ -19,7 +19,6 @@ jobs: pip install flake8 pytest requests pandas if [ -f requirements.txt ]; then pip install -r requirements.txt; fi pip install python-sat - pip install pycryptosat pip install z3-solver pip install exact pip install pysdd diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 889e48aa8..181444efc 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -50,7 +50,7 @@ class CPM_pysat(SolverInterface): $ pip install python-sat See detailed installation instructions at: - https://pysathq.github.io/installation.html + https://pysathq.github.io/installation Creates the following attributes (see parent constructor for more): - pysat_vpool: a pysat.formula.IDPool for the variable mapping @@ -81,7 +81,8 @@ def solvernames(): from pysat.solvers import SolverNames names = [] for name, attr in vars(SolverNames).items(): - if not name.startswith('__') and isinstance(attr, tuple): + # issue with cryptosat, so we don't include it in our https://github.com/msoos/cryptominisat/issues/765 + if not name.startswith('__') and isinstance(attr, tuple) and not name == 'cryptosat': if name not in attr: name = attr[-1] names.append(name) From 26bc446d1433a6fc3dc5cda31d98bfee7152c060 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Thu, 18 Jul 2024 15:43:04 +0200 Subject: [PATCH 4/7] python_builtins: follow python signature (#503) * python_builtins: follow python signature --- cpmpy/expressions/python_builtins.py | 48 ++++++++++++++++++---------- 1 file changed, 32 insertions(+), 16 deletions(-) diff --git a/cpmpy/expressions/python_builtins.py b/cpmpy/expressions/python_builtins.py index caa26bb71..5a240e0b9 100644 --- a/cpmpy/expressions/python_builtins.py +++ b/cpmpy/expressions/python_builtins.py @@ -18,7 +18,6 @@ min sum """ -import numpy as np import builtins # to use the original Python-builtins from .utils import is_false_cst, is_true_cst @@ -70,7 +69,7 @@ def any(iterable): elif isinstance(elem, Expression) and elem.is_bool(): collect.append(elem) else: - raise Exception("Non-Boolean argument '{}' to 'all'".format(elem)) + raise Exception("Non-Boolean argument '{}' to 'any'".format(elem)) if len(collect) == 1: return collect[0] if len(collect) >= 2: @@ -78,33 +77,50 @@ def any(iterable): return False -def max(iterable): +def max(*iterable, **kwargs): """ - max() overwrites python built-in, - checks if all constants and computes np.max() in that case + max() overwrites the python built-in to support decision variables. + + if iterable does not contain CPMpy expressions, the built-in is called + else a Maximum functional global constraint is constructed; no keyword + arguments are supported in that case """ + if len(iterable) == 1: + iterable = tuple(iterable[0]) if not builtins.any(isinstance(elem, Expression) for elem in iterable): - return np.max(iterable) + return builtins.max(*iterable, **kwargs) + + assert len(kwargs)==0, "max over decision variables does not support keyword arguments" return Maximum(iterable) -def min(iterable): +def min(*iterable, **kwargs): """ - min() overwrites python built-in, - checks if all constants and computes np.min() in that case + min() overwrites the python built-in to support decision variables. + + if iterable does not contain CPMpy expressions, the built-in is called + else a Minimum functional global constraint is constructed; no keyword + arguments are supported in that case """ + if len(iterable) == 1: + iterable = tuple(iterable[0]) if not builtins.any(isinstance(elem, Expression) for elem in iterable): - return np.min(iterable) + return builtins.min(*iterable, **kwargs) + + assert len(kwargs)==0, "min over decision variables does not support keyword arguments" return Minimum(iterable) -def sum(iterable): +def sum(*iterable, **kwargs): """ - sum() overwrites python built-in, - checks if all constants and computes np.sum() in that case - otherwise, makes a sum Operator directly on `iterable` + sum() overwrites the python built-in to support decision variables. + + if iterable does not contain CPMpy expressions, the built-in is called + checks if all constants and uses built-in sum() in that case """ - iterable = list(iterable) # Fix generator polling + iterable = tuple(iterable) # Fix generator polling if not builtins.any(isinstance(elem, Expression) for elem in iterable): - return np.sum(iterable) + return builtins.sum(iterable, **kwargs) + + assert len(kwargs)==0, "sum over decision variables does not support keyword arguments" return Operator("sum", iterable) From cdd80f4494823089b326c2334637c3b5f8243269 Mon Sep 17 00:00:00 2001 From: Thomas Sergeys <49067410+ThomSerg@users.noreply.github.com> Date: Thu, 18 Jul 2024 15:57:34 +0200 Subject: [PATCH 5/7] Native solver unified access (#505) * Unified access to native solver * docs: native solver attribute --- cpmpy/solvers/choco.py | 7 +++++++ cpmpy/solvers/exact.py | 6 ++++++ cpmpy/solvers/gurobi.py | 7 +++++++ cpmpy/solvers/minizinc.py | 8 ++++++++ cpmpy/solvers/ortools.py | 6 ++++++ cpmpy/solvers/pysat.py | 7 +++++++ cpmpy/solvers/solver_interface.py | 7 +++++++ cpmpy/solvers/z3.py | 7 +++++++ docs/modeling.md | 4 ++-- 9 files changed, 57 insertions(+), 2 deletions(-) diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index db9b0afee..1cf4574c2 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -98,6 +98,13 @@ def __init__(self, cpm_model=None, subsolver=None): # initialise everything else and post the constraints/objective super().__init__(name="choco", cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.chc_model + def solve(self, time_limit=None, **kwargs): """ Call the Choco solver diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 5f0598cfb..05549ca3e 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -113,6 +113,12 @@ def __init__(self, cpm_model=None, subsolver=None): # initialise everything else and post the constraints/objective super().__init__(name="exact", cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.xct_solver def _fillObjAndVars(self): if not self.xct_solver.hasSolution(): diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index dbe3618bf..c43761dd1 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -96,6 +96,13 @@ def __init__(self, cpm_model=None, subsolver=None): # it is sufficient to implement __add__() and minimize/maximize() below super().__init__(name="gurobi", cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.grb_model + def solve(self, time_limit=None, solution_callback=None, **kwargs): """ diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 111ea3e61..b01420a1c 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -174,6 +174,14 @@ def __init__(self, cpm_model=None, subsolver=None): # initialise everything else and post the constraints/objective super().__init__(name="minizinc:"+subsolver, cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.mzn_model + + def _pre_solve(self, time_limit=None, **kwargs): """ shared by solve() and solveAll() """ import minizinc diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index b15e12243..b5b55627d 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -98,6 +98,12 @@ def __init__(self, cpm_model=None, subsolver=None): # initialise everything else and post the constraints/objective super().__init__(name="ortools", cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.ort_model def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwargs): diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 181444efc..8ca520fa8 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -125,6 +125,13 @@ def __init__(self, cpm_model=None, subsolver=None): # initialise everything else and post the constraints/objective super().__init__(name="pysat:"+subsolver, cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.pysat_solver + def solve(self, time_limit=None, assumptions=None): """ diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index 9e905fc17..75e0436aa 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -88,6 +88,13 @@ def __init__(self, name="dummy", cpm_model=None, subsolver=None): else: self.maximize(cpm_model.objective_) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + raise NotImplementedError("Solver does not support direct solver access. Look at the solver's API for alternative native objects to access directly.") + # instead of overloading minimize/maximize, better just overload 'objective()' def minimize(self, expr): """ diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 52776ee1e..d02f1c3e3 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -82,6 +82,13 @@ def __init__(self, cpm_model=None, subsolver="sat"): # initialise everything else and post the constraints/objective super().__init__(name="z3", cpm_model=cpm_model) + @property + def native_model(self): + """ + Returns the solver's underlying native model (for direct solver access). + """ + return self.z3_solver + def solve(self, time_limit=None, assumptions=[], **kwargs): """ diff --git a/docs/modeling.md b/docs/modeling.md index 8bf897bc8..3fb1fe16a 100644 --- a/docs/modeling.md +++ b/docs/modeling.md @@ -697,10 +697,10 @@ iv = cp.intvar(1,9, shape=3) s = cp.SolverLookup.get("ortools") s += AllDifferent(iv) # the traditional way, equivalent to: -s.ort_model.AddAllDifferent(s.solver_vars(iv)) # directly calling the API, has to be with native variables +s.native_model.AddAllDifferent(s.solver_vars(iv)) # directly calling the API (OR-Tools' python library), has to be with native variables ``` -observe how we first map the CPMpy variables to native variables by calling `s.solver_vars()`, and then give these to the native solver API directly. This is in fact what happens behind the scenes when posting a DirectConstraint, or any CPMpy constraint. +Observe how we first map the CPMpy variables to native variables by calling `s.solver_vars()`, and then give these to the native solver API directly (in the case of OR-Tools, the `native_model` property returns a `CpModel` instance). This is in fact what happens behind the scenes when posting a DirectConstraint, or any CPMpy constraint. Consult [the solver API documentation](api/solvers.html) for more information on the available solver specific objects which can be accessed directly. While directly calling the solver offers a lot of freedom, it is a bit more cumbersome as you have to map the variables manually each time. Also, you no longer have a declarative model that you can pass along, print or inspect. In contrast, a `DirectConstraint` is a CPMpy expression so it can be part of a model like any other CPMpy constraint. Note that it can only be used as top-level (non-nested, non-reified) constraint. From 32a23d85cee8bfb605430669ac918baaeb2ad808 Mon Sep 17 00:00:00 2001 From: wout4 Date: Thu, 18 Jul 2024 20:36:53 +0200 Subject: [PATCH 6/7] fix sum *args --- cpmpy/expressions/python_builtins.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpmpy/expressions/python_builtins.py b/cpmpy/expressions/python_builtins.py index 5a240e0b9..7fcaa805c 100644 --- a/cpmpy/expressions/python_builtins.py +++ b/cpmpy/expressions/python_builtins.py @@ -118,7 +118,8 @@ def sum(*iterable, **kwargs): if iterable does not contain CPMpy expressions, the built-in is called checks if all constants and uses built-in sum() in that case """ - iterable = tuple(iterable) # Fix generator polling + if len(iterable) == 1: + iterable = tuple(iterable[0]) # Fix generator polling if not builtins.any(isinstance(elem, Expression) for elem in iterable): return builtins.sum(iterable, **kwargs) From 7163f6b0be3ba1fb825b9011f9bc161a76c6b925 Mon Sep 17 00:00:00 2001 From: Wout Date: Fri, 19 Jul 2024 11:03:03 +0200 Subject: [PATCH 7/7] put gcs in solver init (#501) * put gcs in solver init * gcs: Throw exception on verification fail and add doc for veripb installation. * gcs: Don't display output if verification timed out. --------- Co-authored-by: mmcilree --- cpmpy/exceptions.py | 2 ++ cpmpy/solvers/__init__.py | 3 +++ cpmpy/solvers/gcs.py | 43 ++++++++++++++++++++++++++------------- 3 files changed, 34 insertions(+), 14 deletions(-) diff --git a/cpmpy/exceptions.py b/cpmpy/exceptions.py index 7ed0e2143..e141450d5 100644 --- a/cpmpy/exceptions.py +++ b/cpmpy/exceptions.py @@ -32,6 +32,8 @@ class IncompleteFunctionError(CPMpyException): class TypeError(CPMpyException): pass +class GCSVerificationException(CPMpyException): + pass class TransformationNotImplementedError(CPMpyException): pass \ No newline at end of file diff --git a/cpmpy/solvers/__init__.py b/cpmpy/solvers/__init__.py index e66a71d6c..1b1459f80 100644 --- a/cpmpy/solvers/__init__.py +++ b/cpmpy/solvers/__init__.py @@ -19,6 +19,7 @@ z3 exact choco + gcs utils =============== @@ -35,6 +36,7 @@ CPM_z3 CPM_exact CPM_choco + CPM_gcs ================= List of functions @@ -54,4 +56,5 @@ from .z3 import CPM_z3 from .exact import CPM_exact from .choco import CPM_choco +from .gcs import CPM_gcs diff --git a/cpmpy/solvers/gcs.py b/cpmpy/solvers/gcs.py index c54ccccd7..617c9f420 100644 --- a/cpmpy/solvers/gcs.py +++ b/cpmpy/solvers/gcs.py @@ -18,7 +18,7 @@ """ from cpmpy.transformations.comparison import only_numexpr_equality from cpmpy.transformations.reification import reify_rewrite, only_bv_reifies, only_implies -from ..exceptions import NotSupportedError +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 @@ -59,7 +59,7 @@ class CPM_gcs(SolverInterface): - objective_var: optional: the variable used as objective - proof_location: location of the last proof produced by the solver - proof_name: name of the last proof (means .opb and .pbp will be present at the proof location) - - proof_verification_failed: whether the last VeriPB check failed to verify the proof. + - veripb_return_code: return code from the last VeriPB check. - proof_check_timeout: whether the last VeriPB check timed out. """ @@ -92,7 +92,7 @@ def __init__(self, cpm_model=None, subsolver=None): self.proof_location = None self.proof_name = None self.proof_check_timeout = True - self.proof_verification_failed = False + self.veripb_return_code = False # initialise everything else and post the constraints/objective super().__init__(name="Glasgow Constraint Solver", cpm_model=cpm_model) @@ -177,6 +177,10 @@ def solve(self, time_limit=None, prove=False, proof_name=None, proof_location=". if verify: self.verify(name=self.proof_name, location=proof_location, time_limit=verify_time_limit, veripb_args=veripb_args, display_output=display_verifier_output) + + if self.veripb_return_code > 0: + raise GCSVerificationException("Glasgow Constraint Solver: Proof failed to verify.") + return has_sol def solveAll(self, time_limit=None, display=None, solution_limit=None, call_from_model=False, @@ -358,6 +362,8 @@ def verify(self, name=None, location=".", time_limit=None, display_output=False, """ Verify a solver-produced proof using VeriPB. + Requires that the 'veripb' tool is installed and on system path. + See `https://gitlab.com/MIAOresearch/software/VeriPB#installation` for installation instructions. Arguments: - name: name for the the proof files (default to self.proof_name) - location: location for the proof files (default to current working directory). @@ -366,27 +372,38 @@ def verify(self, name=None, location=".", time_limit=None, display_output=False, - display_output: whether to print the output from VeriPB """ if not which("veripb"): - raise Exception("Unable to run VeriPB: check it is installed and on system path") + raise Exception("Unable to run VeriPB: check it is installed and on system path - see https://gitlab.com/MIAOresearch/software/VeriPB#installation.") if name is None: name = self.proof_name + if name is None: # Still None? raise ValueError("No proof to verify") + if not isinstance(veripb_args, list): + raise ValueError("veripb_args should be a list") + + opb_file = path.join(location, name +".opb") + pbp_file = path.join(location, name +".pbp") + + if not path.isfile(opb_file): + raise FileNotFoundError("Can't find " + opb_file) + if not path.isfile(pbp_file): + raise FileNotFoundError("Can't find " + pbp_file) + try: - result = subprocess.run(["veripb", path.join(location, name +".opb"), path.join(location, name +".pbp")] + veripb_args, + result = subprocess.run(["veripb"] + veripb_args + [opb_file, pbp_file], capture_output=True, text=True, timeout=time_limit) self.proof_check_timeout = False - self.proof_verification_failed = result.returncode + self.veripb_return_code = result.returncode + if display_output: + print(result.stdout) + print(result.stderr) except subprocess.TimeoutExpired: self.proof_check_timeout = True - self.proof_verification_failed = False + self.veripb_return_code = 0 - if display_output: - print(result.stdout) - print(result.stderr) - - return self.proof_verification_failed + return self.veripb_return_code def __add__(self, cpm_cons): """ @@ -409,8 +426,6 @@ def __add__(self, cpm_cons): elif isinstance(cpm_expr, BoolVal): if not cpm_expr: self.gcs.post_or([]) - else: - return elif isinstance(cpm_expr, Operator) or \ (cpm_expr.name == '==' and isinstance(cpm_expr.args[0], _BoolVarImpl) \ and not isinstance(cpm_expr.args[1], _NumVarImpl)):