From 68188965b0e329d90f9eea6173ee67f71fdb1dcf Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 21:03:42 +0100 Subject: [PATCH 01/15] add transform to ortools, fix default args of transfs --- cpmpy/solvers/gurobi.py | 4 +- cpmpy/solvers/ortools.py | 59 +++++++++++++++++----------- cpmpy/transformations/comparison.py | 4 +- cpmpy/transformations/reification.py | 14 ++++--- docs/adding_solver.md | 10 +++-- 5 files changed, 55 insertions(+), 36 deletions(-) diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 0f8837f62..f74afcbe9 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -264,10 +264,10 @@ def __add__(self, cpm_con): # expressions have to be linearized to fit in MIP model. See /transformations/linearize cpm_cons = flatten_constraint(cpm_con) - cpm_cons = reify_rewrite(cpm_cons) + cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) cpm_cons = only_bv_implies(cpm_cons) cpm_cons = linearize_constraint(cpm_cons) - cpm_cons = only_numexpr_equality(cpm_cons, supported={"sum", "wsum", "sub"}) + cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"])) cpm_cons = only_positive_bv(cpm_cons) for con in cpm_cons: diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 22fd4e799..b22d351af 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -56,7 +56,7 @@ def supported(): try: import ortools return True - except ImportError as e: + except ImportError: return False @@ -297,41 +297,54 @@ def _make_numexpr(self, cpm_expr): raise NotImplementedError("ORTools: Not a know supported numexpr {}".format(cpm_expr)) - def __add__(self, cpm_con): + def __add__(self, cpm_expr): """ - Post a (list of) CPMpy constraints(=expressions) to the solver - - Note that we don't store the constraints in a cpm_model, - we first transform the constraints into primitive constraints, - then post those primitive constraints directly to the native solver + Eagerly add a constraint to the underlying solver. + + Any CPMpy expression given is immediately transformed (throught `transform()`) + and then posted to the solver (through `_post_constraint()`). + + The variables used in expressions given to add are stored as 'user variables'. Those are the only ones + the user knows and cares about. All other variables are auxiliary variables created by transformations. - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) + :param cpm_expr CPMpy expression, or list thereof + :type cpm_expr (list of) Expression(s) """ # add new user vars to the set - self.user_vars.update(get_variables(cpm_con)) + self.user_vars.update(get_variables(cpm_expr)) - # apply transformations, then post internally - cpm_cons = flatten_constraint(cpm_con) - cpm_cons = reify_rewrite(cpm_cons) - cpm_cons = only_numexpr_equality(cpm_cons, supported={"sum", "wsum","sub"}) - cpm_cons = only_bv_implies(cpm_cons) # everything that can create - # reified expr must go before this - for con in cpm_cons: + # transform and post the constraints + for con in self.transform(cpm_expr): self._post_constraint(con) return self + def transform(self, cpm_expr): + """ + Transform arbitrary CPMpy expressions to constraints the solver supports - def _post_constraint(self, cpm_expr, reifiable=False): + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. + + See the 'Adding a new solver' docs on readthedocs for more information. + + :param cpm_expr CPMpy expression, or list thereof + :type cpm_expr (list of) Expression(s) + :returns list of CPMpy expressions """ - Post a primitive CPMpy constraint to the native solver API + cpm_cons = flatten_constraint(cpm_expr) # flat normal form + cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) # constraints that support reification + cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"])) # supports >, <, != + cpm_cons = only_bv_implies(cpm_cons) # everything that can create + # reified expr must go before this + return cpm_cons - What 'primitive' means depends on the solver capabilities, - more specifically on the transformations applied in `__add__()` + def _post_constraint(self, cpm_expr, reifiable=False): + """ + Post a supported CPMpy constraint directly to the underlying solver's API - While the normal form is divided in 'base', 'comparison' and 'reified', we - here regroup the implementation per CPMpy class + What 'supported' means depends on the solver capabilities, and in effect on what transformations + are applied in `__transform()__`. Returns the posted ortools 'Constraint', so that it can be used in reification e.g. self._post_constraint(smth, reifiable=True).onlyEnforceIf(self.solver_var(bvar)) diff --git a/cpmpy/transformations/comparison.py b/cpmpy/transformations/comparison.py index 20a3e8130..c7409ab5f 100644 --- a/cpmpy/transformations/comparison.py +++ b/cpmpy/transformations/comparison.py @@ -18,11 +18,11 @@ - only_numexpr_equality(): transforms `NumExpr IV` to `(NumExpr == A) & (A IV)` if not supported """ -def only_numexpr_equality(constraints, supported=frozenset(["sum","wsum"])): +def only_numexpr_equality(constraints, supported=frozenset()): """ transforms `NumExpr IV` to `(NumExpr == A) & (A IV)` if not supported - argument 'supported' is a list (or set) of expression names that supports all comparisons in the solver + :param supported a (frozen)set of expression names that supports all comparisons in the solver """ # shallow copy (could support inplace too this way...) diff --git a/cpmpy/transformations/reification.py b/cpmpy/transformations/reification.py index 8a72c6e28..ec248331c 100644 --- a/cpmpy/transformations/reification.py +++ b/cpmpy/transformations/reification.py @@ -72,7 +72,7 @@ def only_bv_implies(constraints): return newcons -def reify_rewrite(constraints, supported=frozenset(['sum', 'wsum'])): +def reify_rewrite(constraints, supported=frozenset()): """ Rewrites reified constraints not natively supported by a solver, to a version that uses standard constraints and reification over equalities between variables. @@ -80,10 +80,12 @@ def reify_rewrite(constraints, supported=frozenset(['sum', 'wsum'])): Input is expected to be in Flat Normal Form (so after `flatten_constraint()`) Output will also be in Flat Normal Form - argument 'supported' is a list (or set) of expression names that support reification in the solver - including supported 'Left Hand Side' expressions in reified comparisons, e.g. BV -> (LHS == V) - Boolean expressions 'and', 'or', and '->' are assumed to support reification - (you MUST give an empty supported set if no others are supported...) + Boolean expressions 'and', 'or', and '->' and comparison expression 'IV1==IV2' are assumed to support reification + (actually currently all comparisons in {'==', '!=', '<=', '<', '>=', '>'}, + IV1 IV2 are assumed to support reification BV -> (IV1 IV2)) + + :param supported a (frozen)set of expression names that support reification in the solver, including + supported 'Left Hand Side (LHS)' expressions in reified comparisons, e.g. BV -> (LHS == V) """ if not is_any_list(constraints): # assume list, so make list @@ -130,7 +132,7 @@ def reify_rewrite(constraints, supported=frozenset(['sum', 'wsum'])): # Case 3, BE is Comparison(OP, LHS, RHS) op,(lhs,rhs) = boolexpr.name, boolexpr.args # have list of supported lhs's such as sum and wsum... - # at the very least, (iv1 == iv2) == bv has to be supported (or equivalently, sum: (iv1 - iv2 == 0) == bv) + # at the very least, (iv1 == iv2) == bv has to be supported if isinstance(lhs, _NumVarImpl) or lhs.name in supported: newcons.append(cpm_expr) elif isinstance(lhs, Element) and (lhs.args[1].lb < 0 or lhs.args[1].ub >= len(lhs.args[0])): diff --git a/docs/adding_solver.md b/docs/adding_solver.md index f1851992c..d77aa2bda 100644 --- a/docs/adding_solver.md +++ b/docs/adding_solver.md @@ -17,15 +17,19 @@ Implementing the template consists of the following parts: ## Transformations and posting constraints -CPMpy is designed to separate 'transforming' constraints as much as possible from 'posting' constraints. +CPMpy solver interfaces are *eager*, meaning that any CPMpy expression given to it (through `__add__()`) is immediately transformed (throught `transform()`) and posted to the solver (through `_post_constraint()`). + +CPMpy is designed to separate *transforming* arbitrary CPMpy expressions to constraints the solver supports, from *posting* the supported constraints directly to the solver. For example, a SAT solver only accepts clauses (disjunctions) over Boolean variables as constraints. So, its `_post_constraint()` method should just consists of reading in a CPMpy 'or' expression over decision variables, for which it then calls the solver to create such a clause. All other constraints may not be directly supported by the solver, and can hence be rejected. -What remains is the difficult part of mapping an arbitrary CPMpy expression to CPMpy 'or' expressions. This is exactly the task of a constraint modelling language like CPMpy, and we implement it through multiple independent **transformation functions** in the `cpmpy/transformations/` directory. For any solver you wish to add, chances are that most of the transformations you need are already implemented. If not, read on. +What remains is the difficult part of mapping an arbitrary CPMpy expression to CPMpy 'or' expressions. This is exactly the task of a constraint modelling language like CPMpy, and we implement it through multiple solver-independent **transformation functions** in the `cpmpy/transformations/` directory. + +So for any solver you wish to add, chances are that most of the transformations you need are already implemented. You hence only need to chain the right transformations in the solver's `transform()` method. If you need additional transformations, or want to know how they work, read on. ## Stateless transformation functions -CPMpy solver interfaces are *eager*, meaning that any CPMpy expression given to it (through `__add__()`) is immediately transformed and posted to the solver. That also allows it to be *incremental*, meaning that you can post some constraints, call `solve()` post some more constraints and solve again. If the underlying solver is also incremental, it will reuse knowledge of the previous solve call to speed up this solve call. +Because CPMpy solver interfaces transform and post constraints *eagerly*, they can be used *incremental*, meaning that you can add some constraints, call `solve()` add some more constraints and solve again. If the underlying solver is also incremental, it will reuse knowledge of the previous solve call to speed up this solve call. The way that CPMpy succeeds to be an incremental modeling language, is by making all transformation functions *stateless*. Every transformation function is a python *function* that maps a (list of) CPMpy expressions to (a list of) equivalent CPMpy expressions. Transformations are not classes, they do not store state, they do not know (or care) what model a constraint belongs too. They take expressions as input and compute expressions as output. That means they can be called over and over again, and chained in any combination or order. From 08a0332e8a6c5b9917b55ddb4ad2769a55c8c746 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 22:04:24 +0100 Subject: [PATCH 02/15] solvers: transform() to superclass and template --- cpmpy/solvers/TEMPLATE.py | 47 +++++++++++++---------- cpmpy/solvers/ortools.py | 59 +++++++++++------------------ cpmpy/solvers/solver_interface.py | 63 +++++++++++++++++++++++++------ 3 files changed, 101 insertions(+), 68 deletions(-) diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py index 3d96bab06..2a8cf472f 100644 --- a/cpmpy/solvers/TEMPLATE.py +++ b/cpmpy/solvers/TEMPLATE.py @@ -45,7 +45,7 @@ class CPM_template(SolverInterface): Creates the following attributes (see parent constructor for more): - tpl_model: object, TEMPLATE's model object + - tpl_model: object, TEMPLATE's model object """ @staticmethod @@ -54,7 +54,7 @@ def supported(): try: import TEMPLATEpy as gp return True - except ImportError as e: + except ImportError: return False @@ -158,6 +158,7 @@ def solver_var(self, cpm_var): raise NotImplementedError("Not a know var {}".format(cpm_var)) self._varmap[cpm_var] = revar + # return from cache return self._varmap[cpm_var] @@ -169,7 +170,7 @@ def objective(self, expr, minimize=True): 'objective()' can be called multiple times, only the last one is stored (technical side note: any constraints created during conversion of the objective - are premanently posted to the solver) + are premanently posted to the solver) """ # make objective function non-nested (flat_obj, flat_cons) = flatten_objective(expr) @@ -216,27 +217,28 @@ def _make_numexpr(self, cpm_expr): raise NotImplementedError("TEMPLATE: Not a know supported numexpr {}".format(cpm_expr)) - def __add__(self, cpm_con): + # `__add__()` from the superclass first calls `transform()` then `_post_constraint()`, just implement the latter + def transform(self, cpm_expr): """ - Post a (list of) CPMpy constraints(=expressions) to the solver + Transform arbitrary CPMpy expressions to constraints the solver supports - Note that we don't store the constraints in a cpm_model, - we first transform the constraints into primitive constraints, - then post those primitive constraints directly to the native solver + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) - """ - # add new user vars to the set - self.user_vars.update(get_variables(cpm_con)) + See the 'Adding a new solver' docs on readthedocs for more information. + + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression + :return: list of Expression + """ # apply transformations, then post internally # XXX chose the transformations your solver needs, see cpmpy/transformations/ - cpm_cons = flatten_constraint(cpm_con) - for con in cpm_cons: - self._post_constraint(con) - - return self + cpm_cons = flatten_constraint(cpm_expr) # flat normal form + #cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) # constraints that support reification + #cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"])) # supports >, <, != + # ... + return cpm_cons def _post_constraint(self, cpm_con): """ @@ -252,8 +254,13 @@ def _post_constraint(self, cpm_con): self.TEMPLATE_solver.add_clause([ self.solver_var(cpm_con) ]) elif isinstance(cpm_con, Operator) and cpm_con.name == 'or': self.TEMPLATE_solver.add_clause([ self.solver_var(var) for var in cpm_con.args ]) # TODO, soon: .add_clause(self.solver_vars(cpm_con.args)) - else: - raise NotImplementedError("TEMPLATE: constraint not (yet) supported", cpm_con) + elif hasattr(cpm_expr, 'decompose'): + # global constraint not known, try posting generic decomposition + # side-step `__add__()` as the decomposition can contain non-user (auxiliary) variables + for con in self.transform(cpm_expr.decompose()): + self._post_constraint(con) + + raise NotImplementedError("TEMPLATE: constraint not (yet) supported", cpm_con) # Other functions from SolverInterface that you can overwrite: # solveAll, solution_hint, get_core diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index b22d351af..11ea58ab3 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -29,8 +29,8 @@ from ..expressions.core import Expression, Comparison, Operator from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView from ..expressions.utils import is_num, is_any_list, eval_comparison -from ..transformations.get_variables import get_variables_model, get_variables -from ..transformations.flatten_model import flatten_model, flatten_constraint, flatten_objective, get_or_make_var, negated_normal +from ..transformations.get_variables import get_variables +from ..transformations.flatten_model import flatten_constraint, flatten_objective from ..transformations.reification import only_bv_implies, reify_rewrite from ..transformations.comparison import only_numexpr_equality @@ -297,40 +297,19 @@ def _make_numexpr(self, cpm_expr): raise NotImplementedError("ORTools: Not a know supported numexpr {}".format(cpm_expr)) - def __add__(self, cpm_expr): - """ - Eagerly add a constraint to the underlying solver. - - Any CPMpy expression given is immediately transformed (throught `transform()`) - and then posted to the solver (through `_post_constraint()`). - - The variables used in expressions given to add are stored as 'user variables'. Those are the only ones - the user knows and cares about. All other variables are auxiliary variables created by transformations. - - :param cpm_expr CPMpy expression, or list thereof - :type cpm_expr (list of) Expression(s) - """ - # add new user vars to the set - self.user_vars.update(get_variables(cpm_expr)) - - # transform and post the constraints - for con in self.transform(cpm_expr): - self._post_constraint(con) - - return self - def transform(self, cpm_expr): """ - Transform arbitrary CPMpy expressions to constraints the solver supports + Transform arbitrary CPMpy expressions to constraints the solver supports + + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. - Implemented through chaining multiple solver-independent **transformation functions** from - the `cpmpy/transformations/` directory. + See the 'Adding a new solver' docs on readthedocs for more information. - See the 'Adding a new solver' docs on readthedocs for more information. + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression - :param cpm_expr CPMpy expression, or list thereof - :type cpm_expr (list of) Expression(s) - :returns list of CPMpy expressions + :return: list of Expression """ cpm_cons = flatten_constraint(cpm_expr) # flat normal form cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) # constraints that support reification @@ -348,8 +327,11 @@ def _post_constraint(self, cpm_expr, reifiable=False): Returns the posted ortools 'Constraint', so that it can be used in reification e.g. self._post_constraint(smth, reifiable=True).onlyEnforceIf(self.solver_var(bvar)) - - - reifiable: if True, will throw an error if cpm_expr can not be reified + + :param cpm_expr: list of CPMpy expressions + :type cpm_expr: list of Expression + + :param reifiable: if True, will throw an error if cpm_expr can not be reified by ortools (for safety) """ # Base case: Boolean variable if isinstance(cpm_expr, _BoolVarImpl): @@ -440,16 +422,19 @@ def _post_constraint(self, cpm_expr, reifiable=False): demand = [demand] * len(start) intervals = [self.ort_model.NewIntervalVar(s,d,e,f"interval_{s}-{d}-{e}") for s,d,e in zip(start,dur,end)] return self.ort_model.AddCumulative(intervals, demand, cap) - else: + elif hasattr(cpm_expr, 'decompose'): # NOT (YET?) MAPPED: Automaton, Circuit, # ForbiddenAssignments, Inverse?, NoOverlap, NoOverlap2D, # ReservoirConstraint, ReservoirConstraintWithActive # global constraint not known, try posting generic decomposition - self += cpm_expr.decompose() # assumes a decomposition exists... - # TODO: DirectConstraint/NativeConstraint from cpm_expr.name to API call? see #74 + # side-step `__add__()` as the decomposition can contain non-user (auxiliary) variables + for con in self.transform(cpm_expr.decompose()): + self._post_constraint(con) + return None # will throw error if used in reification - + + # TODO: DirectConstraint/NativeConstraint from cpm_expr.name to API call? see #74 raise NotImplementedError(cpm_expr) # if you reach this... please report on github diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index 30f149d1f..3181da1e6 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -21,6 +21,7 @@ """ from ..expressions.core import Expression +from ..transformations.get_variables import get_variables from ..expressions.utils import is_num, is_any_list from ..expressions.python_builtins import any,all # @@ -118,12 +119,6 @@ def objective(self, expr, minimize): """ raise NotImplementedError("Solver does not support objective functions") - def __add__(self, cpm_cons): - """ - Adds a constraint to the solver, eagerly (e.g. instantly passed to API) - """ - raise NotImplementedError("Solver does not support eagerly adding constraints") - def status(self): return self.cpm_status @@ -170,16 +165,62 @@ def solver_vars(self, cpm_vars): return [self.solver_vars(v) for v in cpm_vars] return self.solver_var(cpm_vars) + # most solvers can inherit this function as is, just implement `transform()` and `__post_constraint()` below + def __add__(self, cpm_expr): + """ + Eagerly add a constraint to the underlying solver. + + Any CPMpy expression given is immediately transformed (throught `transform()`) + and then posted to the solver (through `_post_constraint()`). + + The variables used in expressions given to add are stored as 'user variables'. Those are the only ones + the user knows and cares about. All other variables are auxiliary variables created by transformations. + + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression + + :return: self + """ + # add new user vars to the set + self.user_vars.update(get_variables(cpm_expr)) + + # transform and post the constraints + for con in self.transform(cpm_expr): + self._post_constraint(con) + + return self + + def transform(self, cpm_expr): + """ + Transform arbitrary CPMpy expressions to constraints the solver supports + + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. + + See the 'Adding a new solver' docs on readthedocs for more information. + + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression + + :return: list of Expression + """ + return cpm_expr # overwrite this function and call the transformations you need + def _post_constraint(self, cpm_expr): """ - Post a primitive CPMpy constraint to the native solver API + Post a supported CPMpy constraint directly to the underlying solver's API + + What 'supported' means depends on the solver capabilities, and in effect on what transformations + are applied in `__transform()__`. - What 'primitive' means depends on the solver capabilities, - more specifically on the transformations applied in `__add__()` + Solvers can raise 'NotImplementedError' for any constraint not supported after transformation - Solvers do not need to support all constraints. + :param cpm_expr: list of CPMpy expressions + :type cpm_expr: list of Expression """ - return None + raise NotImplementedError() # abstract function, overwrite + return + # OPTIONAL functions From ed0af00366b369d7bfe1923bc69e0069004b25f8 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 22:04:44 +0100 Subject: [PATCH 03/15] gurobi: use generic transform (UNTESTED! license does not activate from home) --- cpmpy/solvers/gurobi.py | 78 ++++++++++++++++++++--------------------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index f74afcbe9..d1fe61502 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -38,7 +38,7 @@ try: import gurobipy as gp GRB_ENV = None -except ImportError as e: +except ImportError: pass @@ -52,12 +52,8 @@ class CPM_gurobi(SolverInterface): See detailed installation instructions at: https://support.gurobi.com/hc/en-us/articles/360044290292-How-do-I-install-Gurobi-for-Python- - Creates the following attributes: - user_vars: set(), variables in the original (non-transformed) model, - for reverse mapping the values after `solve()` - cpm_status: SolverStatus(), the CPMpy status after a `solve()` - tpl_model: object, TEMPLATE's model object - _varmap: dict(), maps cpmpy variables to native solver variables + Creates the following attributes (see parent constructor for more): + - grb_model: object, TEMPLATE's model object """ @staticmethod @@ -94,6 +90,7 @@ 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) + def solve(self, time_limit=None, solution_callback=None, **kwargs): """ Call the gurobi solver @@ -152,7 +149,8 @@ def solve(self, time_limit=None, solution_callback=None, **kwargs): # True/False depending on self.cpm_status has_sol = self._solve_return(self.cpm_status) - # translate solution values (of user vars only) + # translate solution values (of user specified variables only) + self.objective_value_ = None if has_sol: # fill in variable values for cpm_var in self.user_vars: @@ -167,14 +165,13 @@ def solve(self, time_limit=None, solution_callback=None, **kwargs): return has_sol + def solver_var(self, cpm_var): """ Creates solver variable for cpmpy variable or returns from cache if previously created """ - from gurobipy import GRB - - if is_num(cpm_var): + if is_num(cpm_var): # shortcut, eases posting constraints return cpm_var # special case, negative-bool-view @@ -183,7 +180,8 @@ def solver_var(self, cpm_var): raise Exception("Negative literals should not be part of any equation. See /transformations/linearize for more details") # create if it does not exit - if not cpm_var in self._varmap: + if cpm_var not in self._varmap: + from gurobipy import GRB if isinstance(cpm_var, _BoolVarImpl): revar = self.grb_model.addVar(vtype=GRB.BINARY, name=cpm_var.name) elif isinstance(cpm_var, _IntVarImpl): @@ -195,16 +193,16 @@ def solver_var(self, cpm_var): # return from cache return self._varmap[cpm_var] + def objective(self, expr, minimize=True): """ - Post the expression to optimize to the solver. + Post the given expression to the solver as objective to minimize/maximize - 'objective()' can be called multiple times, onlu the last one is used. + 'objective()' can be called multiple times, only the last one is stored (technical side note: any constraints created during conversion of the objective are premanently posted to the solver) """ - from gurobipy import GRB # make objective function non-nested @@ -212,6 +210,7 @@ def objective(self, expr, minimize=True): self += flat_cons # add potentially created constraints self.user_vars.update(get_variables(flat_obj)) + # make objective function or variable and post obj = self._make_numexpr(flat_obj) if minimize: self.grb_model.setObjective(obj, sense=GRB.MINIMIZE) @@ -246,34 +245,31 @@ def _make_numexpr(self, cpm_expr): raise NotImplementedError("gurobi: Not a know supported numexpr {}".format(cpm_expr)) - def __add__(self, cpm_con): - """ - Post a (list of) CPMpy constraints(=expressions) to the solver - - Note that we don't store the constraints in a cpm_model, - we first transform the constraints into primitive constraints, - then post those primitive constraints directly to the native solver - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) + # `__add__()` from the superclass first calls `transform()` then `_post_constraint()`, just implement the latter + def transform(self, cpm_expr): """ - # add new user vars to the set - self.user_vars.update(get_variables(cpm_con)) + Transform arbitrary CPMpy expressions to constraints the solver supports - # apply transformations, then post internally - # expressions have to be linearized to fit in MIP model. See /transformations/linearize + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. - cpm_cons = flatten_constraint(cpm_con) - cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) - cpm_cons = only_bv_implies(cpm_cons) - cpm_cons = linearize_constraint(cpm_cons) - cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"])) - cpm_cons = only_positive_bv(cpm_cons) + See the 'Adding a new solver' docs on readthedocs for more information. - for con in cpm_cons: - self._post_constraint(con) + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression - return self + :return: list of Expression + """ + # apply transformations, then post internally + # expressions have to be linearized to fit in MIP model. See /transformations/linearize + cpm_cons = flatten_constraint(cpm_expr) # flat normal form + cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) # constraints that support reification + cpm_cons = only_bv_implies(cpm_cons) # anything that can create full reif should go above... + cpm_cons = linearize_constraint(cpm_cons) # the core of the MIP-linearization + cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"])) # supports >, <, != + cpm_cons = only_positive_bv(cpm_cons) # after linearisation, rewrite ~bv into 1-bv + return cpm_cons def _post_constraint(self, cpm_expr): """ @@ -360,12 +356,16 @@ def _post_constraint(self, cpm_expr): return self.grb_model.addGenConstrIndicator(cond, bool_val, lin_expr, GRB.EQUAL, self.solver_var(rhs)) # Global constraints - else: - self += cpm_expr.decompose() + elif hasattr(cpm_expr, 'decompose'): + # global constraint not known, try posting generic decomposition + # side-step `__add__()` as the decomposition can contain non-user (auxiliary) variables + for con in self.transform(cpm_expr.decompose()): + self._post_constraint(con) return raise NotImplementedError(cpm_expr) # if you reach this... please report on github + def solveAll(self, display=None, time_limit=None, solution_limit=None, **kwargs): """ Compute all solutions and optionally display the solutions. From 74a407f03b2ea33fdfd258d98bfa30b7f9fc0c7a Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 22:11:55 +0100 Subject: [PATCH 04/15] minizinc: use generic transform() --- cpmpy/solvers/minizinc.py | 34 +++++++++++++--------------------- cpmpy/solvers/ortools.py | 1 + 2 files changed, 14 insertions(+), 21 deletions(-) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 5b8696624..20efcf4bc 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -322,35 +322,27 @@ def objective(self, expr, minimize): self.mzn_txt_solve = "solve maximize {};\n".format(obj) - def __add__(self, cpm_con): + # `__add__()` from the superclass first calls `transform()` then `_post_constraint()`, just implement the latter + def transform(self, cpm_expr): """ - Post a (list of) CPMpy constraints(=expressions) to the solver + No transformations, just ensure it is a list of constraints - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) - """ - # add new user vars to the set - self.user_vars.update(get_variables(cpm_con)) + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression - # we can't unpack lists in _post_constraint, so must do it upfront - # and can't make assumptions on '.flat' existing either - if is_any_list(cpm_con): - cpm_con = flatlist(cpm_con) + :return: list of Expression + """ + if is_any_list(cpm_expr): + return flatlist(cpm_expr) else: - cpm_con = [cpm_con] - - # no transformations - for con in cpm_con: - self._post_constraint(con) - - return self + return [cpm_expr] - def _post_constraint(self, cpm_expr): + def _post_constraint(self, cpm_con): """ - Post a CPMpy constraint to the native solver API + Translate a CPMpy constraint to MiniZinc string and add it to the solver """ # Get text expression, add to the solver - txt_cons = f"constraint {self._convert_expression(cpm_expr)};\n" + txt_cons = f"constraint {self._convert_expression(cpm_con)};\n" self.mzn_model.add_string(txt_cons) def _convert_expression(self, expr) -> str: diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 11ea58ab3..1d081ebac 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -297,6 +297,7 @@ def _make_numexpr(self, cpm_expr): raise NotImplementedError("ORTools: Not a know supported numexpr {}".format(cpm_expr)) + # `__add__()` from the superclass first calls `transform()` then `_post_constraint()`, just implement the latter def transform(self, cpm_expr): """ Transform arbitrary CPMpy expressions to constraints the solver supports From db05833ef227f23e5afec1340a8ce6dd05f77505 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 22:31:37 +0100 Subject: [PATCH 05/15] pysat/pysdd: use generic transform --- cpmpy/solvers/pysat.py | 36 +++++++++++++++++++----------------- cpmpy/solvers/pysdd.py | 39 ++++++++++++++++++--------------------- tests/test_constraints.py | 8 ++++++-- 3 files changed, 43 insertions(+), 40 deletions(-) diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index eb4e9cbe5..62c2e5588 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -206,30 +206,31 @@ def solver_var(self, cpm_var): raise NotImplementedError(f"CPM_pysat: variable {cpm_var} not supported") - def __add__(self, cpm_con): + # `__add__()` from the superclass first calls `transform()` then `_post_constraint()`, just implement the latter + def transform(self, cpm_expr): """ - Post a (list of) CPMpy constraints(=expressions) to the solver + Transform arbitrary CPMpy expressions to constraints the solver supports - Note that we don't store the constraints in a cpm_model, - we first transform the constraints into primitive constraints, - then post those primitive constraints directly to the native solver + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) - """ - # add new user vars to the set - self.user_vars.update(get_variables(cpm_con)) + See the 'Adding a new solver' docs on readthedocs for more information. - # apply transformations, then post internally - cpm_cons = to_cnf(cpm_con) - for con in cpm_cons: - self._post_constraint(con) + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression - return self + :return: list of Expression + """ + return to_cnf(cpm_expr) def _post_constraint(self, cpm_expr): """ Post a primitive CPMpy constraint to the native solver API + + What 'primitive' means depends on the solver capabilities, + more specifically on the transformations applied in `__add__()` + + Solvers do not need to support all constraints. """ from pysat.card import CardEnc @@ -288,8 +289,9 @@ def _post_constraint(self, cpm_expr): else: raise NotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") - elif cpm_expr.name == 'xor': - for con in to_cnf(cpm_expr.decompose()): + elif hasattr(cpm_expr, 'decompose'): # cpm_expr.name == 'xor': + # for all global constraints: + for con in self.transform(cpm_expr.decompose()): self._post_constraint(con) else: raise NotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index 3350ef0f6..6d1d96862 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -186,37 +186,32 @@ def solver_var(self, cpm_var): return self._varmap[cpm_var] - - def __add__(self, cpm_con): + # `__add__()` from the superclass first calls `transform()` then `_post_constraint()`, just implement the latter + def transform(self, cpm_expr): """ - Post a (list of) CPMpy constraints(=expressions) to the solver + Transform arbitrary CPMpy expressions to constraints the solver supports - Note that we don't store the constraints in a cpm_model, - we first transform the constraints into primitive constraints, - then post those primitive constraints directly to the native solver + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. - For PySDD, it can be beneficial to post a big model (collection of constraints) at once... + See the 'Adding a new solver' docs on readthedocs for more information. - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) - """ - # add new user vars to the set - self.user_vars.update(get_variables(cpm_con)) + For PySDD, it can be beneficial to add a big model (collection of constraints) at once... + + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression + :return: list of Expression + """ + # initialize (arbitrary) vtree from all user-specified vars if self.pysdd_root is None: - # initialize (arbitrary) vtree from vars from pysdd.sdd import SddManager, Vtree self.pysdd_vtree = Vtree(var_count=len(self.user_vars), vtree_type="balanced") self.pysdd_manager = SddManager.from_vtree(self.pysdd_vtree) self.pysdd_root = self.pysdd_manager.true() - # apply transformations, then post internally - cpm_cons = to_cnf(cpm_con) - for con in cpm_cons: - self._post_constraint(con) - - return self + return to_cnf(cpm_expr) def _post_constraint(self, cpm_expr): """ @@ -234,8 +229,10 @@ def _post_constraint(self, cpm_expr): raise NotImplementedError( f"Automatic conversion of Operator {cpm_expr} to CNF not yet supported, please report on github.") #elif isinstance(cpm_expr, Comparison): - elif cpm_expr.name == 'xor': - for con in to_cnf(cpm_expr.decompose()): + + elif hasattr(cpm_expr, 'decompose'): # cpm_expr.name == 'xor': + # for all global constraints: + for con in self.transform(cpm_expr.decompose()): self._post_constraint(con) else: raise NotImplementedError(f"Constraint {cpm_expr} not supported by CPM_pysdd") diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 066f2ff7a..9dee748ec 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -13,12 +13,16 @@ EXCLUDE_GLOBAL = {"ortools": {"circuit"}, "gurobi": {"circuit"}, "minizinc": {"circuit"}, - "pysat": {"circuit", "element","min","max","allequal","alldifferent"}} + "pysat": {"circuit", "element","min","max","allequal","alldifferent"}, + "pysdd": {"circuit", "element","min","max","allequal","alldifferent"}, + } # Exclude certain operators for solvers. # Not all solvers support all operators in CPMpy EXCLUDE_OPERATORS = {"gurobi": {"mod"}, - "pysat": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}} + "pysat": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}, + "pysdd": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}, + } # Some solvers only support a subset of operators in imply-constraints # This subset can differ between left and right hand side of the implication From 8447c5d26c3cdb7ba8d1e67d17d19731cbc61e16 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 22:41:06 +0100 Subject: [PATCH 06/15] z3: use transform --- cpmpy/solvers/z3.py | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 1ae8e8fa9..c888492d2 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -225,23 +225,25 @@ def objective(self, expr, minimize=True): else: self.z3_solver.maximize(obj) - def __add__(self, cpm_con): + # most solvers can inherit this function as is, just implement `transform()` and `__post_constraint()` below + def transform(self, cpm_expr): """ - Post a (list of) CPMpy constraints(=expressions) to the solver + Transform arbitrary CPMpy expressions to constraints the solver supports - Note that we don't store the constraints in a cpm_model, - we first transform the constraints into primitive constraints, - then post those primitive constraints directly to the native solver + Implemented through chaining multiple solver-independent **transformation functions** from + the `cpmpy/transformations/` directory. - :param cpm_con CPMpy constraint, or list thereof - :type cpm_con (list of) Expression(s) + See the 'Adding a new solver' docs on readthedocs for more information. + + :param cpm_expr: CPMpy expression, or list thereof + :type cpm_expr: Expression or list of Expression + + :return: list of Expression """ # Z3 supports nested expressions, so no transformations needed # that also means we don't need to extract user variables here # we store them directly in `solver_var()` itself. - self._post_constraint(cpm_con) - - return self + return cpm_expr def _post_constraint(self, cpm_expr): """ From c8d71f5a3f1fe39a24e61a7a1dd2f2041ad2a05f Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Mon, 2 Jan 2023 11:39:36 +0100 Subject: [PATCH 07/15] z3 transform: ensure it is a list --- cpmpy/solvers/z3.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index c888492d2..276c3c80a 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -243,7 +243,10 @@ def transform(self, cpm_expr): # Z3 supports nested expressions, so no transformations needed # that also means we don't need to extract user variables here # we store them directly in `solver_var()` itself. - return cpm_expr + if is_any_list(cpm_expr): + return cpm_expr + else: + return [cpm_expr] def _post_constraint(self, cpm_expr): """ From 83ae1717470ab47601435c701db253b44fc80fce Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Mon, 2 Jan 2023 20:47:23 +0100 Subject: [PATCH 08/15] solvers: tweaks of transform() --- cpmpy/solvers/TEMPLATE.py | 8 ++++---- cpmpy/solvers/gurobi.py | 8 ++++---- cpmpy/solvers/minizinc.py | 4 ++-- cpmpy/solvers/ortools.py | 2 +- cpmpy/solvers/pysat.py | 8 ++++---- cpmpy/solvers/pysdd.py | 7 ++++++- cpmpy/solvers/solver_interface.py | 7 +++---- cpmpy/solvers/z3.py | 4 ++-- tests/test_constraints.py | 6 +++++- 9 files changed, 31 insertions(+), 23 deletions(-) diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py index 2a8cf472f..c40746db7 100644 --- a/cpmpy/solvers/TEMPLATE.py +++ b/cpmpy/solvers/TEMPLATE.py @@ -242,12 +242,12 @@ def transform(self, cpm_expr): def _post_constraint(self, cpm_con): """ - Post a primitive CPMpy constraint to the native solver API + Post a supported CPMpy constraint directly to the underlying solver's API - What 'primitive' means depends on the solver capabilities, - more specifically on the transformations applied in `__add__()` + What 'supported' means depends on the solver capabilities, and in effect on what transformations + are applied in `transform()`. - Solvers do not need to support all constraints. + Solvers can raise 'NotImplementedError' for any constraint not supported after transformation """ if isinstance(cpm_con, _BoolVarImpl): # base case, just var or ~var diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index d1fe61502..fe0f72aa0 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -273,12 +273,12 @@ def transform(self, cpm_expr): def _post_constraint(self, cpm_expr): """ - Post a primitive CPMpy constraint to the native solver API + Post a supported CPMpy constraint directly to the underlying solver's API - What 'primitive' means depends on the solver capabilities, - more specifically on the transformations applied in `__add__()` + What 'supported' means depends on the solver capabilities, and in effect on what transformations + are applied in `transform()`. - Solvers do not need to support all constraints. + Solvers can raise 'NotImplementedError' for any constraint not supported after transformation """ from gurobipy import GRB diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 20efcf4bc..58759f450 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -342,8 +342,8 @@ def _post_constraint(self, cpm_con): Translate a CPMpy constraint to MiniZinc string and add it to the solver """ # Get text expression, add to the solver - txt_cons = f"constraint {self._convert_expression(cpm_con)};\n" - self.mzn_model.add_string(txt_cons) + mzn_str = f"constraint {self._convert_expression(cpm_con)};\n" + self.mzn_model.add_string(mzn_str) def _convert_expression(self, expr) -> str: """ diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 1d081ebac..4bb4d1b59 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -324,7 +324,7 @@ def _post_constraint(self, cpm_expr, reifiable=False): Post a supported CPMpy constraint directly to the underlying solver's API What 'supported' means depends on the solver capabilities, and in effect on what transformations - are applied in `__transform()__`. + are applied in `transform()`. Returns the posted ortools 'Constraint', so that it can be used in reification e.g. self._post_constraint(smth, reifiable=True).onlyEnforceIf(self.solver_var(bvar)) diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 62c2e5588..c817acc56 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -225,12 +225,12 @@ def transform(self, cpm_expr): def _post_constraint(self, cpm_expr): """ - Post a primitive CPMpy constraint to the native solver API + Post a supported CPMpy constraint directly to the underlying solver's API - What 'primitive' means depends on the solver capabilities, - more specifically on the transformations applied in `__add__()` + What 'supported' means depends on the solver capabilities, and in effect on what transformations + are applied in `transform()`. - Solvers do not need to support all constraints. + Solvers can raise 'NotImplementedError' for any constraint not supported after transformation """ from pysat.card import CardEnc diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index 6d1d96862..c8602990f 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -215,7 +215,12 @@ def transform(self, cpm_expr): def _post_constraint(self, cpm_expr): """ - Post a primitive CPMpy constraint to the native solver API + Post a supported CPMpy constraint directly to the underlying solver's API + + What 'supported' means depends on the solver capabilities, and in effect on what transformations + are applied in `transform()`. + + Solvers can raise 'NotImplementedError' for any constraint not supported after transformation """ if isinstance(cpm_expr, _BoolVarImpl): # base case, just var or ~var diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index 3181da1e6..36c677c9c 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -204,22 +204,21 @@ def transform(self, cpm_expr): :return: list of Expression """ - return cpm_expr # overwrite this function and call the transformations you need + return list(cpm_expr) # overwrite this function and call the transformations you need def _post_constraint(self, cpm_expr): """ Post a supported CPMpy constraint directly to the underlying solver's API What 'supported' means depends on the solver capabilities, and in effect on what transformations - are applied in `__transform()__`. + are applied in `transform()`. Solvers can raise 'NotImplementedError' for any constraint not supported after transformation :param cpm_expr: list of CPMpy expressions :type cpm_expr: list of Expression """ - raise NotImplementedError() # abstract function, overwrite - return + raise NotImplementedError("solver _post_constraint(): abstract function, overwrite") # OPTIONAL functions diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 276c3c80a..d5c69c11e 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -250,7 +250,7 @@ def transform(self, cpm_expr): def _post_constraint(self, cpm_expr): """ - Post a primitive CPMpy constraint to the native solver API + Post a supported CPMpy constraint directly to the underlying solver's API Z3 supports nested expressions so translate expression tree and post to solver API directly """ @@ -431,4 +431,4 @@ def get_core(self): assert (self.cpm_status.exitstatus == ExitStatus.UNSATISFIABLE), "Can only extract core form UNSAT model" assert (len(self.assumption_dict) > 0), "Assumptions must be set using s.solve(assumptions=[...])" - return [self.assumption_dict[z3_var] for z3_var in self.z3_solver.unsat_core()] \ No newline at end of file + return [self.assumption_dict[z3_var] for z3_var in self.z3_solver.unsat_core()] diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 3aa2a690b..94bdbecc2 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -131,9 +131,13 @@ def global_constraints(): - AllDifferent, AllEqual, Circuit, Minimum, Maximum, Element, Xor, Cumulative """ - if SOLVERNAME is None or SOLVERNAME in EXCLUDE_GLOBAL: + if SOLVERNAME is None: return + if SOLVERNAME not in EXCLUDE_GLOBAL: + # add with no exclusions + EXCLUDE_GLOBAL[SOLVERNAME] = {} + global_cons = [AllDifferent, AllEqual, Minimum, Maximum] # TODO: add Circuit for global_type in global_cons: From 1751152bb6c33c7266f0fd71d4e96f601a04d836 Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Mon, 2 Jan 2023 21:10:19 +0100 Subject: [PATCH 09/15] docs: debugging guide to include using a solvers transform() function --- docs/how_to_debug.md | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/docs/how_to_debug.md b/docs/how_to_debug.md index 5e38f61cc..11a8b1878 100644 --- a/docs/how_to_debug.md +++ b/docs/how_to_debug.md @@ -46,7 +46,7 @@ If you have a model that fails in this way, try the following code snippet to se ```python model = ... # your code, a `Model()` -` + for c in model.constraints: print("Trying",c) Model(c).solve() @@ -60,27 +60,38 @@ Or maybe, you got one of CPMpy's NotImplementedErrors. Share your use case with First, print the model: -`print(model)` and check that the output matches what you want to express. Do you see anything unusual? Start there, see why the expression is now what you intended to express, as described in 'Debugging a modeling error'. +```print(model)``` + +and check that the output matches what you want to express. Do you see anything unusual? Start there, see why the expression is not what you intended to express, as described in 'Debugging a modeling error'. -If that does not help, try printing the 'flat normal form' of the model, which also shows the intermediate variables that are automatically created by CPMpy: +If that does not help, try printing the 'transformed' **constraints**, the way that the solver actually sees them, including decompositions and rewrites: ```python -from cpmpy.transformations.flatten_model import flatten_constraint, flatten_model -print(flatten_model(model)) +s = SolverLookup.get("ortools") # or whatever solver you are using +print(s.tranform(model.constraints)) ``` -Note that you can also print individual flattened expressions with `print(flatten_constraint(expression))` which helps to zoom in on the curlpit. +Note that you can also print individual expressions like this, e.g. `print(s.transform(expression))` which helps to zoom in on the curlpit. -If you want to know about the variable domains as well, to see whether something is wrong there, you can do so as follows: +If you want to know about the **variable domains** as well, to see whether something is wrong there, you can do so as follows: ```python -from cpmpy.transformations.flatten_model import flatten_constraint, flatten_model +s = SolverLookup.get("ortools") # or whatever solver you are using +ct = s.tranform(model.constraints) from cpmpy.transformations.get_variables import print_variables -mf = flatten_model(model) -print_variables(mf) -print(mf)` +print_variables(ct) +print(ct) ``` +Printing the **objective** as the solver sees it requires you to look into the solver interface code of that solver. However, the following is a good first check that can already reveal potentially problematic things: + +```python +s = SolverLookup.get("ortools") # or whatever solver you are using +from cpmpy.transformations.flatten_model import flatten_objective +(obj_var, obj_expr) = flatten_objective(model.objective) +print(f"Optimizing {obj_var} subject to", s.transform(obj_expr)) +``` + ### Automatically minimising the UNSAT program If the above is unwieldy because your constraint problem is too large, then consider automatically reducing it to a 'Minimal Unsatisfiable Subset' (MUS). From d94238e6ed1a90075e5f4b052f937446a05851d9 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 24 Jan 2023 17:05:22 +0100 Subject: [PATCH 10/15] cascaded xors, leave new vars to flatten_contraint in solver interfaces --- cpmpy/expressions/globalconstraints.py | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 05fdf6004..038ccc30e 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -390,13 +390,11 @@ def decompose(self): a0, a1 = self.args return [(a0 | a1), (~a0 | ~a1)] # one true and one false - # for more than 2 variables, we chain reified xors - # XXX this will involve many calls to the above decomp, shortcut? - prev_var, cons = get_or_make_var(self.args[0] ^ self.args[1]) + # for more than 2 variables, we cascade xors + cons = self.args[0] ^ self.args[1] for arg in self.args[2:]: - prev_var, new_cons = get_or_make_var(prev_var ^ arg) - cons += new_cons - return cons + [prev_var] + cons = (cons | arg) & (~cons | ~arg) + return [cons] def value(self): return sum(argval(a) for a in self.args) % 2 == 1 From 35950e56f741839678a161c2fda105a578e71d63 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 24 Jan 2023 17:06:10 +0100 Subject: [PATCH 11/15] global xor correctly transformed to cnf by recursive call --- cpmpy/transformations/to_cnf.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 235cc8cb4..5273d29c9 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -126,6 +126,9 @@ def flat2cnf(constraints): cnf += [a0sub | a1 for a0sub in subcnf] continue + elif expr.name == "xor": + cnf += to_cnf(expr.decompose()) + continue # all other cases not covered (e.g. not continue'd) # pass verbatim cnf.append(expr) From a4f9afd0507610c75fa2ee91a02ad40093f69cf1 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 24 Jan 2023 17:08:21 +0100 Subject: [PATCH 12/15] run all supported solvers in testsuite --- tests/test_constraints.py | 103 ++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 59 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 807f6caeb..a21d33143 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -5,10 +5,10 @@ # CHANGE THIS if you want test a different solver -# make sure that `SolverLookup.get(SOLVERNAME)` works +# make sure that `SolverLookup.get(solver)` works # also add exclusions to the 3 EXCLUDE_* below as needed -SOLVERNAME = "ortools" - +SOLVERNAMES = [name for name, solver in SolverLookup.base_solvers() if solver.supported()] +# SOLVERNAMES = ["ortools"] # Exclude some global constraints for solvers # Can be used when .value() method is not implemented/contains bugs @@ -43,8 +43,14 @@ BOOL_ARGS = [boolvar(name=n) for n in "abc"] # Boolean variables BOOL_VAR = boolvar(name="p") # A boolean variable +def _generate_inputs(generator): + exprs = [] + for solver in SOLVERNAMES: + exprs += [(solver, expr) for expr in generator(solver)] + return exprs + -def numexprs(): +def numexprs(solver): """ Generate all numerical expressions Numexpr: @@ -53,12 +59,9 @@ def numexprs(): - Global constraint (non-Boolean) (examples: Max,Min,Element) (CPMpy class 'GlobalConstraint', not is_bool())) """ - if SOLVERNAME is None: - return - names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if not is_bool] - if SOLVERNAME in EXCLUDE_OPERATORS: - names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[SOLVERNAME]] + if solver in EXCLUDE_OPERATORS: + names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[solver]] for name, arity in names: if name == "wsum": operator_args = [list(range(len(NUM_ARGS))), NUM_ARGS] @@ -75,7 +78,7 @@ def numexprs(): # Generate all possible comparison constraints -def comp_constraints(): +def comp_constraints(solver): """ Generate all comparison constraints - Numeric equality: Numexpr == Var (CPMpy class 'Comparison') @@ -85,19 +88,19 @@ def comp_constraints(): - Numeric inequality (>=,>,<,<=): Numexpr >=< Var (CPMpy class 'Comparison') """ for comp_name in Comparison.allowed: - for numexpr in numexprs(): + for numexpr in numexprs(solver): for rhs in [NUM_VAR, 1]: yield Comparison(comp_name, numexpr, rhs) for comp_name in Comparison.allowed: - for glob_expr in global_constraints(): + for glob_expr in global_constraints(solver): if not glob_expr.is_bool(): for rhs in [NUM_VAR, 1]: yield Comparison(comp_name, glob_expr, rhs) - if SOLVERNAME == "z3": + if solver == "z3": for comp_name in Comparison.allowed: - for boolexpr in bool_exprs(): + for boolexpr in bool_exprs(solver): for rhs in [NUM_VAR, 1]: if comp_name == '>' and rhs == 1: rhs = 0 # >1 is unsat for boolean expressions, so change it to 0 @@ -105,18 +108,16 @@ def comp_constraints(): # Generate all possible boolean expressions -def bool_exprs(): +def bool_exprs(solver): """ Generate all boolean expressions: - Boolean operators: and([Var]), or([Var]) (CPMpy class 'Operator', is_bool()) - Boolean equality: Var == Var (CPMpy class 'Comparison') """ - if SOLVERNAME is None: - return names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if is_bool] - if SOLVERNAME in EXCLUDE_OPERATORS: - names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[SOLVERNAME]] + if solver in EXCLUDE_OPERATORS: + names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[solver]] for name, arity in names: if arity != 0: @@ -131,37 +132,30 @@ def bool_exprs(): for eq_name in ["==", "!="]: yield Comparison(eq_name, *BOOL_ARGS[:2]) - for cpm_cons in global_constraints(): + for cpm_cons in global_constraints(solver): if cpm_cons.is_bool(): yield cpm_cons -def global_constraints(): +def global_constraints(solver): """ Generate all global constraints - AllDifferent, AllEqual, Circuit, Minimum, Maximum, Element, Xor, Cumulative """ - if SOLVERNAME is None: - return - - if SOLVERNAME not in EXCLUDE_GLOBAL: - # add with no exclusions - EXCLUDE_GLOBAL[SOLVERNAME] = {} - global_cons = [AllDifferent, AllEqual, Minimum, Maximum] - # TODO: add Circuit for global_type in global_cons: cons = global_type(NUM_ARGS) - if cons.name not in EXCLUDE_GLOBAL[SOLVERNAME]: + if solver not in EXCLUDE_GLOBAL or cons.name not in EXCLUDE_GLOBAL[solver]: yield cons - if "element" not in EXCLUDE_GLOBAL[SOLVERNAME]: + # "special" constructors + if solver not in EXCLUDE_GLOBAL or "element" not in EXCLUDE_GLOBAL[solver]: yield cpm_array(NUM_ARGS)[NUM_VAR] - if "xor" not in EXCLUDE_GLOBAL[SOLVERNAME]: + if solver not in EXCLUDE_GLOBAL or "xor" not in EXCLUDE_GLOBAL[solver]: yield Xor(BOOL_ARGS) - if "cumulative" not in EXCLUDE_GLOBAL[SOLVERNAME]: + if solver not in EXCLUDE_GLOBAL or "cumulative" not in EXCLUDE_GLOBAL[solver]: s = intvar(0,10,shape=3,name="start") e = intvar(0,10,shape=3,name="end") dur = [1,4,3] @@ -170,60 +164,51 @@ def global_constraints(): yield Cumulative(s, dur, e, demand, cap) -def reify_imply_exprs(): +def reify_imply_exprs(solver): """ - Reification (double implication): Boolexpr == Var (CPMpy class 'Comparison') - Implication: Boolexpr -> Var (CPMpy class 'Operator', is_bool()) Var -> Boolexpr (CPMpy class 'Operator', is_bool()) """ - if SOLVERNAME is None: - return - - for bool_expr in bool_exprs(): - if SOLVERNAME not in EXCLUDE_IMPL or \ - bool_expr.name not in EXCLUDE_IMPL[SOLVERNAME]: + for bool_expr in bool_exprs(solver): + if solver not in EXCLUDE_IMPL or \ + bool_expr.name not in EXCLUDE_IMPL[solver]: yield bool_expr.implies(BOOL_VAR) yield BOOL_VAR.implies(bool_expr) yield bool_expr == BOOL_VAR - for comp_expr in comp_constraints(): + for comp_expr in comp_constraints(solver): lhs, rhs = comp_expr.args - if SOLVERNAME not in EXCLUDE_IMPL or \ - (not isinstance(lhs, Expression) or lhs.name not in EXCLUDE_IMPL[SOLVERNAME]) and \ - (not isinstance(rhs, Expression) or rhs.name not in EXCLUDE_IMPL[SOLVERNAME]): + if solver not in EXCLUDE_IMPL or \ + (not isinstance(lhs, Expression) or lhs.name not in EXCLUDE_IMPL[solver]) and \ + (not isinstance(rhs, Expression) or rhs.name not in EXCLUDE_IMPL[solver]): yield comp_expr.implies(BOOL_VAR) yield BOOL_VAR.implies(comp_expr) yield comp_expr == BOOL_VAR -@pytest.mark.parametrize("constraint", bool_exprs(), ids=lambda c: str(c)) -def test_bool_constaints(constraint): +@pytest.mark.parametrize(("solver","constraint"),_generate_inputs(bool_exprs), ids=str) +def test_bool_constaints(solver, constraint): """ Tests boolean constraint by posting it to the solver and checking the value after solve. """ - if SOLVERNAME is None: - return - assert SolverLookup.get(SOLVERNAME, Model(constraint)).solve() + assert SolverLookup.get(solver, Model(constraint)).solve() assert constraint.value() -@pytest.mark.parametrize("constraint", comp_constraints(), ids=lambda c: str(c)) -def test_comparison_constraints(constraint): +@pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) +def test_comparison_constraints(solver, constraint): """ Tests comparison constraint by posting it to the solver and checking the value after solve. """ - if SOLVERNAME is None: - return - assert SolverLookup.get(SOLVERNAME,Model(constraint)).solve() + assert SolverLookup.get(solver,Model(constraint)).solve() assert constraint.value() -@pytest.mark.parametrize("constraint", reify_imply_exprs(), ids=lambda c: str(c)) -def test_reify_imply_constraints(constraint): +@pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) +def test_reify_imply_constraints(solver, constraint): """ Tests boolean expression by posting it to solver and checking the value after solve. """ - if SOLVERNAME is None: - return - assert SolverLookup.get(SOLVERNAME, Model(constraint)).solve() + assert SolverLookup.get(solver, Model(constraint)).solve() assert constraint.value() From 9787f6dec1f974715c6e2547baae34546e49dcf4 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 24 Jan 2023 17:27:53 +0100 Subject: [PATCH 13/15] cumulative constraint duration for minizinc --- cpmpy/solvers/minizinc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 58759f450..b910a6420 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -460,7 +460,7 @@ def _convert_expression(self, expr) -> str: elif expr.name == "cumulative": start, dur, end, _, _ = expr.args - self += (start + dur == end) + self += [s + d == e for s,d,e in zip(start,dur,end)] return "cumulative({},{},{},{})".format(args_str[0], args_str[1], args_str[3], args_str[4]) print_map = {"allequal":"all_equal", "xor":"xorall"} From 8227122dd8115acf6cd1d0864b833eb2cf18825a Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 24 Jan 2023 17:30:04 +0100 Subject: [PATCH 14/15] _post constraint does not support lists of expr --- cpmpy/solvers/ortools.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 4bb4d1b59..ce0bc355b 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -329,8 +329,8 @@ def _post_constraint(self, cpm_expr, reifiable=False): Returns the posted ortools 'Constraint', so that it can be used in reification e.g. self._post_constraint(smth, reifiable=True).onlyEnforceIf(self.solver_var(bvar)) - :param cpm_expr: list of CPMpy expressions - :type cpm_expr: list of Expression + :param cpm_expr: CPMpy expression + :type cpm_expr: Expression :param reifiable: if True, will throw an error if cpm_expr can not be reified by ortools (for safety) """ From c42ddf790fd6fc773dd77d4868eedef8612e79ad Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Wed, 25 Jan 2023 14:14:39 +0100 Subject: [PATCH 15/15] implemented ConstraintNotImplementedError --- cpmpy/exceptions.py | 5 ++ cpmpy/solvers/TEMPLATE.py | 2 +- cpmpy/solvers/gurobi.py | 7 +- cpmpy/solvers/ortools.py | 8 +-- cpmpy/solvers/pysat.py | 13 ++-- cpmpy/solvers/pysdd.py | 6 +- cpmpy/solvers/z3.py | 13 ++-- tests/test_constraints.py | 141 +++++++++++++++++--------------------- 8 files changed, 93 insertions(+), 102 deletions(-) diff --git a/cpmpy/exceptions.py b/cpmpy/exceptions.py index b7526c59b..a50402a6a 100644 --- a/cpmpy/exceptions.py +++ b/cpmpy/exceptions.py @@ -11,3 +11,8 @@ class CPMpyException(Exception): class MinizincPathException(CPMpyException): pass +class ConstraintNotImplementedError(CPMpyException): + """ + Indicates a constraint is not implemented for a specific solver. + Should ONLY be thrown from a solvers _post_constraint method. + """ diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py index c40746db7..b64c041bd 100644 --- a/cpmpy/solvers/TEMPLATE.py +++ b/cpmpy/solvers/TEMPLATE.py @@ -247,7 +247,7 @@ def _post_constraint(self, cpm_con): What 'supported' means depends on the solver capabilities, and in effect on what transformations are applied in `transform()`. - Solvers can raise 'NotImplementedError' for any constraint not supported after transformation + Solvers can raise 'ConstraintNotImplementedError' for any constraint not supported after transformation """ if isinstance(cpm_con, _BoolVarImpl): # base case, just var or ~var diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index fe0f72aa0..6408b4e58 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -27,6 +27,7 @@ """ from .solver_interface import SolverInterface, SolverStatus, ExitStatus +from ..exceptions import ConstraintNotImplementedError from ..expressions.core import * from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar from ..transformations.comparison import only_numexpr_equality @@ -278,7 +279,7 @@ def _post_constraint(self, cpm_expr): What 'supported' means depends on the solver capabilities, and in effect on what transformations are applied in `transform()`. - Solvers can raise 'NotImplementedError' for any constraint not supported after transformation + Solvers can raise 'ConstraintNotImplementedError' for any constraint not supported after transformation """ from gurobipy import GRB @@ -329,7 +330,7 @@ def _post_constraint(self, cpm_expr): assert a == 2, "Gurobi: 'pow', only support quadratic constraints (x**2)" return self.grb_model.addGenConstrPow(x, grbrhs, a) - raise NotImplementedError( + raise ConstraintNotImplementedError( "Not a know supported gurobi comparison '{}' {}".format(lhs.name, cpm_expr)) elif isinstance(cpm_expr, Operator) and cpm_expr.name == "->": @@ -363,7 +364,7 @@ def _post_constraint(self, cpm_expr): self._post_constraint(con) return - raise NotImplementedError(cpm_expr) # if you reach this... please report on github + raise ConstraintNotImplementedError(cpm_expr) # if you reach this... please report on github def solveAll(self, display=None, time_limit=None, solution_limit=None, **kwargs): diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index ce0bc355b..6ae22d634 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -26,6 +26,7 @@ import sys # for stdout checking from .solver_interface import SolverInterface, SolverStatus, ExitStatus +from ..exceptions import ConstraintNotImplementedError from ..expressions.core import Expression, Comparison, Operator from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView from ..expressions.utils import is_num, is_any_list, eval_comparison @@ -357,8 +358,7 @@ def _post_constraint(self, cpm_expr, reifiable=False): # the natively reifiable 'and', 'or' and 'sum' remain here return self._post_constraint(cpm_expr.args[1], reifiable=True).OnlyEnforceIf(lhs) else: - raise NotImplementedError("Not a know supported ORTools Operator '{}' {}".format( - cpm_expr.name, cpm_expr)) + raise ConstraintNotImplementedError(f"Not a know supported ORTools Operator '{cpm_expr.name}' {cpm_expr}") # Comparisons: only numeric ones as the `only_bv_implies()` transformation # has removed the '==' reification for Boolean expressions @@ -404,7 +404,7 @@ def _post_constraint(self, cpm_expr, reifiable=False): assert (lhs.args[1] == 2), "Ort: 'pow', only var**2 supported, no other exponents" b = self.solver_var(lhs.args[0]) return self.ort_model.AddMultiplicationEquality(ortrhs, [b,b]) - raise NotImplementedError( + raise ConstraintNotImplementedError( "Not a know supported ORTools left-hand-side '{}' {}".format(lhs.name, cpm_expr)) @@ -436,7 +436,7 @@ def _post_constraint(self, cpm_expr, reifiable=False): return None # will throw error if used in reification # TODO: DirectConstraint/NativeConstraint from cpm_expr.name to API call? see #74 - raise NotImplementedError(cpm_expr) # if you reach this... please report on github + raise ConstraintNotImplementedError(cpm_expr) # if you reach this... please report on github def solution_hint(self, cpm_vars, vals): diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index c817acc56..5bc461c66 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -30,6 +30,7 @@ CPM_pysat """ from .solver_interface import SolverInterface, SolverStatus, ExitStatus +from ..exceptions import ConstraintNotImplementedError from ..expressions.core import Expression, Comparison, Operator from ..expressions.variables import _BoolVarImpl, NegBoolView, boolvar from ..expressions.utils import is_any_list, is_int @@ -230,7 +231,7 @@ def _post_constraint(self, cpm_expr): What 'supported' means depends on the solver capabilities, and in effect on what transformations are applied in `transform()`. - Solvers can raise 'NotImplementedError' for any constraint not supported after transformation + Solvers can raise 'ConstraintNotImplementedError' for any constraint not supported after transformation """ from pysat.card import CardEnc @@ -241,7 +242,7 @@ def _post_constraint(self, cpm_expr): if cpm_expr.name == 'or': self.pysat_solver.add_clause(self.solver_vars(cpm_expr.args)) else: - raise NotImplementedError( + raise ConstraintNotImplementedError( f"Automatic conversion of Operator {cpm_expr} to CNF not yet supported, please report on github.") elif isinstance(cpm_expr, Comparison): # only handle cardinality encodings (for now) @@ -250,7 +251,7 @@ def _post_constraint(self, cpm_expr): lits = self.solver_vars(cpm_expr.args[0].args) bound = cpm_expr.args[1] if not is_int(bound): - raise NotImplementedError(f"PySAT sum: rhs `{bound}` type {type(bound)} not supported") + raise ConstraintNotImplementedError(f"PySAT sum: rhs `{bound}` type {type(bound)} not supported") clauses = [] if cpm_expr.name == "<": @@ -282,19 +283,19 @@ def _post_constraint(self, cpm_expr): ## add is_atleast or is_atmost clauses.append([is_atleast, is_atmost]) else: - raise NotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") + raise ConstraintNotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") # post the clauses self.pysat_solver.append_formula(clauses) else: - raise NotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") + raise ConstraintNotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") elif hasattr(cpm_expr, 'decompose'): # cpm_expr.name == 'xor': # for all global constraints: for con in self.transform(cpm_expr.decompose()): self._post_constraint(con) else: - raise NotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") + raise ConstraintNotImplementedError(f"Non-operator constraint {cpm_expr} not supported by CPM_pysat") def solution_hint(self, cpm_vars, vals): diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index c8602990f..3e1e9ef68 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -23,6 +23,7 @@ """ from functools import reduce from .solver_interface import SolverInterface, SolverStatus, ExitStatus +from ..exceptions import ConstraintNotImplementedError from ..expressions.core import Expression, Comparison, Operator from ..expressions.variables import _BoolVarImpl, NegBoolView, boolvar from ..expressions.utils import is_any_list @@ -231,16 +232,15 @@ def _post_constraint(self, cpm_expr): clause = reduce(self.pysdd_manager.disjoin, self.solver_vars(cpm_expr.args)) self.pysdd_root &= clause else: - raise NotImplementedError( + raise ConstraintNotImplementedError( f"Automatic conversion of Operator {cpm_expr} to CNF not yet supported, please report on github.") - #elif isinstance(cpm_expr, Comparison): elif hasattr(cpm_expr, 'decompose'): # cpm_expr.name == 'xor': # for all global constraints: for con in self.transform(cpm_expr.decompose()): self._post_constraint(con) else: - raise NotImplementedError(f"Constraint {cpm_expr} not supported by CPM_pysdd") + raise ConstraintNotImplementedError(f"Constraint {cpm_expr} not supported by CPM_pysdd") def dot(self): diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index a3c498185..591ae98c1 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -21,6 +21,7 @@ CPM_z3 """ from .solver_interface import SolverInterface, SolverStatus, ExitStatus +from ..exceptions import ConstraintNotImplementedError from ..expressions.core import Expression, Comparison, Operator from ..expressions.globalconstraints import GlobalConstraint from ..expressions.variables import _BoolVarImpl, NegBoolView, _NumVarImpl, _IntVarImpl @@ -326,7 +327,7 @@ def _z3_expr(self, cpm_con, reify=False): return -self._z3_expr(cpm_con.args[0]) else: - raise NotImplementedError(f"Operator {cpm_con} not (yet) implemented for Z3, please report on github if you need it") + raise ConstraintNotImplementedError(f"Operator {cpm_con} not (yet) implemented for Z3, please report on github if you need it") # Comparisons (just translate the subexpressions and re-post) elif isinstance(cpm_con, Comparison): @@ -351,22 +352,22 @@ def _z3_expr(self, cpm_con, reify=False): if cpm_con.name == "==": if isinstance(lhs, GlobalConstraint) and lhs.name == "max": if reify: - raise NotImplementedError(f"Reification of {cpm_con} not supported yet") + raise ConstraintNotImplementedError(f"Reification of {cpm_con} not supported yet") return z3.And(self._z3_expr(any(a == rhs for a in lhs.args)), self._z3_expr(all([a <= rhs for a in lhs.args]))) if isinstance(rhs, GlobalConstraint) and rhs.name == "max": if reify: - raise NotImplementedError(f"Reification of {cpm_con} not supported yet") + raise ConstraintNotImplementedError(f"Reification of {cpm_con} not supported yet") return z3.And(self._z3_expr(any(lhs == a for a in rhs.args)), self._z3_expr(all([lhs >= a for a in rhs.args]))) if isinstance(lhs, GlobalConstraint) and lhs.name == "min": if reify: - raise NotImplementedError(f"Reification of {cpm_con} not supported yet") + raise ConstraintNotImplementedError(f"Reification of {cpm_con} not supported yet") return z3.And(self._z3_expr(any(a == rhs for a in lhs.args)), self._z3_expr(all([a >= rhs for a in lhs.args]))) if isinstance(rhs, GlobalConstraint) and rhs.name == "min": if reify: - raise NotImplementedError(f"Reification of {cpm_con} not supported yet") + raise ConstraintNotImplementedError(f"Reification of {cpm_con} not supported yet") return z3.And(self._z3_expr(any(lhs == a for a in rhs.args)), self._z3_expr(all([lhs <= a for a in rhs.args]))) @@ -434,7 +435,7 @@ def _z3_expr(self, cpm_con, reify=False): # global constraints return self._z3_expr(all(cpm_con.decompose())) - raise NotImplementedError("Z3: constraint not (yet) supported", cpm_con) + raise ConstraintNotImplementedError("Z3: constraint not (yet) supported", cpm_con) # Other functions from SolverInterface that you can overwrite: # solveAll, solution_hint, get_core diff --git a/tests/test_constraints.py b/tests/test_constraints.py index a21d33143..b0c1593eb 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -1,4 +1,5 @@ from cpmpy import Model, SolverLookup +from cpmpy.exceptions import ConstraintNotImplementedError from cpmpy.expressions.globalconstraints import * import pytest @@ -8,31 +9,7 @@ # make sure that `SolverLookup.get(solver)` works # also add exclusions to the 3 EXCLUDE_* below as needed SOLVERNAMES = [name for name, solver in SolverLookup.base_solvers() if solver.supported()] -# SOLVERNAMES = ["ortools"] - -# Exclude some global constraints for solvers -# Can be used when .value() method is not implemented/contains bugs -EXCLUDE_GLOBAL = {"ortools": {"circuit"}, - "gurobi": {"circuit"}, - "minizinc": {"circuit"}, - "pysat": {"circuit", "element","min","max","allequal","alldifferent","cumulative"}, - "pysdd": {"circuit", "element","min","max","allequal","alldifferent","cumulative"}, - } - -# Exclude certain operators for solvers. -# Not all solvers support all operators in CPMpy -EXCLUDE_OPERATORS = {"gurobi": {"mod"}, - "pysat": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}, - "pysdd": {"sum", "wsum", "sub", "mod", "div", "pow", "abs", "mul","-"}, - } - -# Some solvers only support a subset of operators in imply-constraints -# This subset can differ between left and right hand side of the implication -EXCLUDE_IMPL = {"ortools": {"xor", "element"}, - "z3": {"min", "max", "abs"}, # TODO this will become emtpy after resolving issue #105 - } - - +SOLVERNAMES = ["ortools"] # Variables to use in the rest of the test script NUM_ARGS = [intvar(-3, 5, name=n) for n in "xyz"] # Numerical variables @@ -46,11 +23,11 @@ def _generate_inputs(generator): exprs = [] for solver in SOLVERNAMES: - exprs += [(solver, expr) for expr in generator(solver)] + exprs += [(solver, expr) for expr in generator()] return exprs -def numexprs(solver): +def numexprs(): """ Generate all numerical expressions Numexpr: @@ -60,8 +37,8 @@ def numexprs(solver): (CPMpy class 'GlobalConstraint', not is_bool())) """ names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if not is_bool] - if solver in EXCLUDE_OPERATORS: - names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[solver]] + # if solver in EXCLUDE_OPERATORS: + # names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[solver]] for name, arity in names: if name == "wsum": operator_args = [list(range(len(NUM_ARGS))), NUM_ARGS] @@ -78,7 +55,7 @@ def numexprs(solver): # Generate all possible comparison constraints -def comp_constraints(solver): +def comp_constraints(): """ Generate all comparison constraints - Numeric equality: Numexpr == Var (CPMpy class 'Comparison') @@ -88,27 +65,24 @@ def comp_constraints(solver): - Numeric inequality (>=,>,<,<=): Numexpr >=< Var (CPMpy class 'Comparison') """ for comp_name in Comparison.allowed: - for numexpr in numexprs(solver): + for numexpr in numexprs(): for rhs in [NUM_VAR, 1]: yield Comparison(comp_name, numexpr, rhs) - for comp_name in Comparison.allowed: - for glob_expr in global_constraints(solver): + for boolexpr in bool_exprs(): + for rhs in [BOOL_VAR, NUM_VAR, 1]: + if comp_name == '>' and rhs == 1: + rhs = 0 # >1 is unsat for boolean expressions, so change it to 0 + yield Comparison(comp_name, boolexpr, rhs) + + for glob_expr in global_constraints(): if not glob_expr.is_bool(): for rhs in [NUM_VAR, 1]: yield Comparison(comp_name, glob_expr, rhs) - if solver == "z3": - for comp_name in Comparison.allowed: - for boolexpr in bool_exprs(solver): - for rhs in [NUM_VAR, 1]: - if comp_name == '>' and rhs == 1: - rhs = 0 # >1 is unsat for boolean expressions, so change it to 0 - yield Comparison(comp_name, boolexpr, rhs) - # Generate all possible boolean expressions -def bool_exprs(solver): +def bool_exprs(): """ Generate all boolean expressions: - Boolean operators: and([Var]), or([Var]) (CPMpy class 'Operator', is_bool()) @@ -116,8 +90,8 @@ def bool_exprs(solver): """ names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if is_bool] - if solver in EXCLUDE_OPERATORS: - names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[solver]] + # if solver in EXCLUDE_OPERATORS: + # names = [(name, arity) for name, arity in names if name not in EXCLUDE_OPERATORS[solver]] for name, arity in names: if arity != 0: @@ -132,11 +106,11 @@ def bool_exprs(solver): for eq_name in ["==", "!="]: yield Comparison(eq_name, *BOOL_ARGS[:2]) - for cpm_cons in global_constraints(solver): + for cpm_cons in global_constraints(): if cpm_cons.is_bool(): yield cpm_cons -def global_constraints(solver): +def global_constraints(): """ Generate all global constraints - AllDifferent, AllEqual, Circuit, Minimum, Maximum, Element, @@ -145,46 +119,46 @@ def global_constraints(solver): global_cons = [AllDifferent, AllEqual, Minimum, Maximum] for global_type in global_cons: cons = global_type(NUM_ARGS) - if solver not in EXCLUDE_GLOBAL or cons.name not in EXCLUDE_GLOBAL[solver]: - yield cons + # if solver not in EXCLUDE_GLOBAL or cons.name not in EXCLUDE_GLOBAL[solver]: + yield cons # "special" constructors - if solver not in EXCLUDE_GLOBAL or "element" not in EXCLUDE_GLOBAL[solver]: - yield cpm_array(NUM_ARGS)[NUM_VAR] + # if solver not in EXCLUDE_GLOBAL or "element" not in EXCLUDE_GLOBAL[solver]: + yield cpm_array(NUM_ARGS)[NUM_VAR] - if solver not in EXCLUDE_GLOBAL or "xor" not in EXCLUDE_GLOBAL[solver]: - yield Xor(BOOL_ARGS) + # if solver not in EXCLUDE_GLOBAL or "xor" not in EXCLUDE_GLOBAL[solver]: + yield Xor(BOOL_ARGS) - if solver not in EXCLUDE_GLOBAL or "cumulative" not in EXCLUDE_GLOBAL[solver]: - s = intvar(0,10,shape=3,name="start") - e = intvar(0,10,shape=3,name="end") - dur = [1,4,3] - demand = [4,5,7] - cap = 10 - yield Cumulative(s, dur, e, demand, cap) + # if solver not in EXCLUDE_GLOBAL or "cumulative" not in EXCLUDE_GLOBAL[solver]: + s = intvar(0,10,shape=3,name="start") + e = intvar(0,10,shape=3,name="end") + dur = [1,4,3] + demand = [4,5,7] + cap = 10 + yield Cumulative(s, dur, e, demand, cap) -def reify_imply_exprs(solver): +def reify_imply_exprs(): """ - Reification (double implication): Boolexpr == Var (CPMpy class 'Comparison') - Implication: Boolexpr -> Var (CPMpy class 'Operator', is_bool()) Var -> Boolexpr (CPMpy class 'Operator', is_bool()) """ - for bool_expr in bool_exprs(solver): - if solver not in EXCLUDE_IMPL or \ - bool_expr.name not in EXCLUDE_IMPL[solver]: - yield bool_expr.implies(BOOL_VAR) - yield BOOL_VAR.implies(bool_expr) - yield bool_expr == BOOL_VAR + for bool_expr in bool_exprs(): + # if solver not in EXCLUDE_IMPL or \ + # bool_expr.name not in EXCLUDE_IMPL[solver]: + yield bool_expr.implies(BOOL_VAR) + yield BOOL_VAR.implies(bool_expr) + yield bool_expr == BOOL_VAR - for comp_expr in comp_constraints(solver): + for comp_expr in comp_constraints(): lhs, rhs = comp_expr.args - if solver not in EXCLUDE_IMPL or \ - (not isinstance(lhs, Expression) or lhs.name not in EXCLUDE_IMPL[solver]) and \ - (not isinstance(rhs, Expression) or rhs.name not in EXCLUDE_IMPL[solver]): - yield comp_expr.implies(BOOL_VAR) - yield BOOL_VAR.implies(comp_expr) - yield comp_expr == BOOL_VAR + # if solver not in EXCLUDE_IMPL or \ + # (not isinstance(lhs, Expression) or lhs.name not in EXCLUDE_IMPL[solver]) and \ + # (not isinstance(rhs, Expression) or rhs.name not in EXCLUDE_IMPL[solver]): + yield comp_expr.implies(BOOL_VAR) + yield BOOL_VAR.implies(comp_expr) + yield comp_expr == BOOL_VAR @pytest.mark.parametrize(("solver","constraint"),_generate_inputs(bool_exprs), ids=str) @@ -192,8 +166,11 @@ def test_bool_constaints(solver, constraint): """ Tests boolean constraint by posting it to the solver and checking the value after solve. """ - assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + try: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert constraint.value() + except ConstraintNotImplementedError: + pytest.skip(f"Constraint is not implemented for {solver}") @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) @@ -201,8 +178,11 @@ def test_comparison_constraints(solver, constraint): """ Tests comparison constraint by posting it to the solver and checking the value after solve. """ - assert SolverLookup.get(solver,Model(constraint)).solve() - assert constraint.value() + try: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert constraint.value() + except ConstraintNotImplementedError: + pytest.skip(f"Constraint is not implemented for {solver}") @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) @@ -210,5 +190,8 @@ def test_reify_imply_constraints(solver, constraint): """ Tests boolean expression by posting it to solver and checking the value after solve. """ - assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + try: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert constraint.value() + except ConstraintNotImplementedError: + pytest.skip(f"Constraint is not implemented for {solver}")