From 659f18a5b6935176a2d8391407d2c44eb11ff8e8 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 16 Apr 2025 11:48:51 +0200 Subject: [PATCH 01/39] Parameters to exact (#616) * add proper warnings for setting parameters at solve time * add test for checking if user-warning is raised * add optional init kwargs in SolverLookup * update warning * update tests * remove extra spaces --- cpmpy/solvers/exact.py | 7 ++++--- cpmpy/solvers/utils.py | 8 ++++++-- tests/test_solvers.py | 24 ++++++++++++++++++++++++ 3 files changed, 34 insertions(+), 5 deletions(-) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 1d860f063..ba3eda98d 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -112,7 +112,6 @@ def __init__(self, cpm_model=None, subsolver=None, **kwargs): assert subsolver is None, "Exact does not allow subsolvers." from exact import Exact as xct - # initialise the native solver object options = list(kwargs.items()) # options is a list of string-pairs, e.g. [("verbosity","1")] options = [(opt[0], str(opt[1])) for opt in options] # Ensure values are also strings @@ -167,10 +166,12 @@ def solve(self, time_limit=None, assumptions=None, **kwargs): - False if no solution is found """ from exact import Exact as xct - + # set additional keyword arguments if(len(kwargs.items())>0): - warnings.warn(f"Exact only supports options at initialization: {kwargs.items()}") + wrn_txt = f"Exact only supports options at initialization. Ignoring additional options {kwargs.items()}\n" + wrn_txt += "Use cp.SolverLookup.lookup('exact', **{parameter-with-hyphen: 42}) to set Exact parameters" + warnings.warn(wrn_txt) # ensure all vars are known to solver self.solver_vars(list(self.user_vars)) diff --git a/cpmpy/solvers/utils.py b/cpmpy/solvers/utils.py index 705744a39..45c35c9f0 100644 --- a/cpmpy/solvers/utils.py +++ b/cpmpy/solvers/utils.py @@ -94,11 +94,15 @@ def solvernames(cls): return names @classmethod - def get(cls, name=None, model=None): + def get(cls, name=None, model=None, **init_kwargs): """ get a specific solver (by name), with 'model' passed to its constructor This is the preferred way to initialise a solver from its name + + :param name: name of the solver to use + :param model: model to pass to the solver constructor + :param init_kwargs: additional keyword arguments to pass to the solver constructor """ solver_cls = cls.lookup(name=name) @@ -106,7 +110,7 @@ def get(cls, name=None, model=None): subname = None if name is not None and ':' in name: _,subname = name.split(':',maxsplit=1) - return solver_cls(model, subsolver=subname) + return solver_cls(model, subsolver=subname, **init_kwargs) @classmethod def lookup(cls, name=None): diff --git a/tests/test_solvers.py b/tests/test_solvers.py index 06824ca18..d23df6bc7 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -1,4 +1,5 @@ import unittest +import tempfile import pytest import numpy as np import cpmpy as cp @@ -489,6 +490,29 @@ def _trixor_callback(): s = cp.SolverLookup.get("exact", m) self.assertEqual(s.solveAll(display=_trixor_callback),7) + @pytest.mark.skipif(not CPM_exact.supported(), + reason="Exact not installed") + def test_parameters_to_exact(self): + + # php with 5 pigeons, 4 holes + p,h = 40,39 + x = cp.boolvar(shape=(p,h)) + m = cp.Model(x.sum(axis=1) >= 1, x.sum(axis=0) <= 1) + + # this should raise a warning + with self.assertWarns(UserWarning): + self.assertFalse(m.solve(solver="exact", verbosity=10)) + + # can we indeed set a parameter? Try with prooflogging + proof_file = tempfile.NamedTemporaryFile(delete=False).name + + # taken from https://gitlab.com/nonfiction-software/exact/-/blob/main/python_examples/proof_logging.py + options = {"proof-log": proof_file, "proof-assumptions":"0"} + exact = cp.SolverLookup.get("exact",m, **options) + self.assertFalse(exact.solve()) + + with open(proof_file+".proof", "r") as f: + self.assertEquals(f.readline()[:-1], "pseudo-Boolean proof version 1.1") # check header of proof-file @pytest.mark.skipif(not CPM_choco.supported(), reason="pychoco not installed") From db3999e2d4e453996c78b3ec18c1a44af0422b28 Mon Sep 17 00:00:00 2001 From: Henk Bierlee Date: Wed, 16 Apr 2025 12:54:20 +0000 Subject: [PATCH 02/39] Discussing whether we support constants for Element decomposition (#630) * Support constants for Element decomposition * Add more general approach to handling constant Element indices * Prevent OR-Tools error by converting integer to constant intvar * Decompose only intersection between idx and array bounds * Use better get_bounds for non-expressions * Fix decomposition (off-by-one + process comments) * Improve implies typing * Refactor test * Fix utils.implies * Use is_[true,false]_cst * Linting * Simplify fixed integer case Element for OT-Tools * Refactor Element decomp using loop --- cpmpy/expressions/globalfunctions.py | 16 ++++++++++++---- cpmpy/expressions/utils.py | 11 +++++++++++ cpmpy/solvers/ortools.py | 16 +++++++++++----- tests/test_constraints.py | 1 + tests/test_globalconstraints.py | 22 ++++++++++++++++++++++ 5 files changed, 57 insertions(+), 9 deletions(-) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 86925a108..d85629163 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -69,9 +69,9 @@ def decompose_comparison(self): import cpmpy as cp from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError -from .core import Expression, Operator, Comparison +from .core import Expression, Operator from .variables import boolvar, intvar, cpm_array -from .utils import flatlist, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, argvals +from .utils import flatlist, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, argvals, get_bounds, implies class GlobalFunction(Expression): @@ -238,6 +238,7 @@ def element(arg_list): warnings.warn("Deprecated, use Element(arr,idx) instead, will be removed in stable version", DeprecationWarning) assert (len(arg_list) == 2), "Element expression takes 2 arguments: Arr, Idx" return Element(arg_list[0], arg_list[1]) + class Element(GlobalFunction): """ The 'Element' global constraint enforces that the result equals Arr[Idx] @@ -286,8 +287,15 @@ def decompose_comparison(self, cpm_op, cpm_rhs): """ arr, idx = self.args - return [(idx == i).implies(eval_comparison(cpm_op, arr[i], cpm_rhs)) for i in range(len(arr))] + \ - [idx >= 0, idx < len(arr)], [] + # 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]) diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 8cfda1b06..b511a83b8 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -194,6 +194,17 @@ def get_bounds(expr): return int(expr), int(expr) return math.floor(expr), math.ceil(expr) +def implies(expr, other): + """ like :func:`~cpmpy.expressions.core.Expression.implies`, but also safe to use for non-expressions """ + if isinstance(expr, cp.expressions.core.Expression): + return expr.implies(other) + elif is_true_cst(expr): + return other + elif is_false_cst(expr): + return BoolVal(True) + else: + return expr.implies(other) + # Specific stuff for ShortTabel global (should this be in globalconstraints.py instead?) STAR = "*" # define constant here def is_star(arg): diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index ef144320c..8cc6bef60 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -41,9 +41,9 @@ from ..exceptions import NotSupportedError from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.globalconstraints import DirectConstraint -from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, boolvar +from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, boolvar, intvar from ..expressions.globalconstraints import GlobalConstraint -from ..expressions.utils import is_num, eval_comparison, flatlist, argval, argvals, get_bounds +from ..expressions.utils import is_num, is_int, eval_comparison, flatlist, argval, argvals, get_bounds from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, flatten_objective, get_or_make_var @@ -480,9 +480,15 @@ def _post_constraint(self, cpm_expr, reifiable=False): elif lhs.name == 'div': return self.ort_model.AddDivisionEquality(ortrhs, *self.solver_vars(lhs.args)) elif lhs.name == 'element': - # arr[idx]==rvar (arr=arg0,idx=arg1), ort: (idx,arr,target) - return self.ort_model.AddElement(self.solver_var(lhs.args[1]), - self.solver_vars(lhs.args[0]), ortrhs) + arr, idx = lhs.args + if is_int(idx): # OR-Tools does not handle all constant integer cases + idx = intvar(idx,idx) + # OR-Tools has slight different in argument order + return self.ort_model.AddElement( + self.solver_var(idx), + self.solver_vars(arr), + ortrhs + ) elif lhs.name == 'mod': # catch tricky-to-find ortools limitation x,y = lhs.args diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 60383da66..ef3684591 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -4,6 +4,7 @@ from cpmpy import Model, SolverLookup, BoolVal from cpmpy.expressions.globalconstraints import * from cpmpy.expressions.globalfunctions import * +from cpmpy.expressions.core import Comparison import pytest diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index 16168ae3f..aaf4efa49 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -1325,3 +1325,25 @@ def test_table(self): self.assertRaises(TypeError, cp.Table, [iv[0], iv[1], iv[2], 5], [(5, 2, 2)]) self.assertRaises(TypeError, cp.Table, [iv[0], iv[1], iv[2], [5]], [(5, 2, 2)]) self.assertRaises(TypeError, cp.Table, [iv[0], iv[1], iv[2], ['a']], [(5, 2, 2)]) + + def test_issue627(self): + for s, cls in cp.SolverLookup.base_solvers(): + if cls.supported(): + try: + # constant look-up + self.assertTrue(cp.Model([cp.boolvar() == cp.Element([0], 0)]).solve(solver=s)) + # constant out-of-bounds look-up + self.assertFalse(cp.Model([cp.boolvar() == cp.Element([0], 1)]).solve(solver=s)) + except (NotImplementedError, NotSupportedError): + pass + + 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], [])" + ) From 357059f3d6468b08b3eabeabf40c0dde1864bebb Mon Sep 17 00:00:00 2001 From: Thomas Sergeys <49067410+ThomSerg@users.noreply.github.com> Date: Wed, 16 Apr 2025 15:09:19 +0200 Subject: [PATCH 03/39] Missing user vars for solveAll (#609) * z3 collect user vars * minizinc post user vars * Add unit test * Exclude test for pysat and pysdd --- Co-authored-by: Tias Guns --- cpmpy/solvers/minizinc.py | 4 ++++ cpmpy/solvers/z3.py | 3 +++ tests/test_solvers.py | 16 ++++++++++++++++ 3 files changed, 23 insertions(+) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 7fb2737c0..9f67b368b 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -350,6 +350,10 @@ def mzn_time_to_seconds(self, time): async def _solveAll(self, display=None, time_limit=None, solution_limit=None, **kwargs): """ Special 'async' function because mzn.solutions() is async """ + + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + # make mzn_inst (kwargs, mzn_inst) = self._pre_solve(time_limit=time_limit, **kwargs) kwargs['all_solutions'] = True diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index e62a34c35..4613918ae 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -35,6 +35,7 @@ Module details ============== """ +from cpmpy.transformations.get_variables import get_variables from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError from ..expressions.core import Expression, Comparison, Operator, BoolVal @@ -317,6 +318,8 @@ def __add__(self, cpm_expr): :return: self """ # all variables are user variables, handled in `solver_var()` + # unless their constraint gets simplified away, so lets collect them anyway + get_variables(cpm_expr, collect=self.user_vars) # transform and post the constraints for cpm_con in self.transform(cpm_expr): diff --git a/tests/test_solvers.py b/tests/test_solvers.py index d23df6bc7..2705df7d1 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -828,3 +828,19 @@ def test_partial_div_mod(self, solver): assert dv * yv + rv == xv assert (Operator('div', [xv, yv])).value() == dv assert (Operator('mod', [xv, yv])).value() == rv + + def test_hidden_user_vars(self, solver): + """ + Tests whether decision variables which are part of a constraint that never gets posted to the underlying solver + still get correctly captured and posted. + """ + if solver == 'pysdd' or solver == 'pysat': # pysat and pysdd don't support integer decision variables + return + + x = cp.intvar(1, 4, shape=1) + # Dubious constraint which enforces nothing, gets decomposed to empty list + # -> resulting CP model is empty + m = cp.Model([cp.AllDifferentExceptN([x], 1)]) + s = cp.SolverLookup().get(solver, m) + assert len(s.user_vars) == 1 # check if var captured as a user_var + assert s.solveAll() == 4 # check if still correct number of solutions, even though empty model From e56b66d45cb670d33d5480eeaf1b47ca12903285 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Wed, 16 Apr 2025 15:18:38 +0200 Subject: [PATCH 04/39] Rework (start of) docs of solvers API (#633) * rework (start of) docs of solvers, based on readthedocs rendering/flow * gurobi: missing line * Fix section title underline must be at least as long, otherwise links are broken * Wrong solver name * Small changes typos, rst syntax, consistent wording, ... * Add example codeblock to solver interface * exact summary wording streamline * add pysat direct instructions again for uniformity at this point * remove poorly explained capabilities from solver docs for now --------- Co-authored-by: Thomas Sergeys --- cpmpy/solvers/TEMPLATE.py | 78 ++++++++++++++++----------- cpmpy/solvers/__init__.py | 51 ++++++++++++------ cpmpy/solvers/choco.py | 31 ++++++----- cpmpy/solvers/cpo.py | 56 ++++++++++--------- cpmpy/solvers/exact.py | 36 ++++++++----- cpmpy/solvers/gcs.py | 52 ++++++++++-------- cpmpy/solvers/gurobi.py | 30 ++++++----- cpmpy/solvers/minizinc.py | 58 ++++++++++---------- cpmpy/solvers/ortools.py | 34 +++++++----- cpmpy/solvers/pysat.py | 50 +++++++++-------- cpmpy/solvers/pysdd.py | 35 ++++++------ cpmpy/solvers/z3.py | 42 +++++++++------ docs/api/solvers/choco.rst | 2 +- docs/api/solvers/solver_interface.rst | 2 +- 14 files changed, 330 insertions(+), 227 deletions(-) diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py index 0b39b92a0..7dddd6bf9 100644 --- a/cpmpy/solvers/TEMPLATE.py +++ b/cpmpy/solvers/TEMPLATE.py @@ -1,16 +1,51 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## TEMPLATE.py +## """ - Template file for a new solver interface + Interface to TEMPLATE's API + + .. note:: + [GUIDELINE] Replace