From 68188965b0e329d90f9eea6173ee67f71fdb1dcf Mon Sep 17 00:00:00 2001 From: Tias Guns Date: Sun, 1 Jan 2023 21:03:42 +0100 Subject: [PATCH 01/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] 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/48] _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/48] 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}") From 4845676f174fd8c10fedf69404358f4ca03196f2 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 2 May 2024 10:27:23 +0200 Subject: [PATCH 16/48] ensure solver assigns value to any user var --- cpmpy/solvers/choco.py | 3 +++ cpmpy/solvers/exact.py | 3 +++ cpmpy/solvers/gurobi.py | 9 ++++++--- cpmpy/solvers/minizinc.py | 4 ++++ cpmpy/solvers/ortools.py | 2 ++ cpmpy/solvers/pysat.py | 9 ++++++--- cpmpy/solvers/pysdd.py | 4 ++++ cpmpy/solvers/z3.py | 3 +++ 8 files changed, 31 insertions(+), 6 deletions(-) diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index f161b1360..85122cef2 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -107,6 +107,8 @@ def solve(self, time_limit=None, **kwargs): - kwargs: any keyword argument, sets parameters of solver object """ + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) # call the solver, with parameters self.chc_solver = self.chc_model.get_solver() @@ -338,6 +340,7 @@ def __add__(self, cpm_expr): """ # add new user vars to the set get_variables(cpm_expr, collect=self.user_vars) + # ensure all vars are known to solver # transform and post the constraints for con in self.transform(cpm_expr): diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index f19b71377..dffcaf703 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -155,6 +155,9 @@ def solve(self, time_limit=None, assumptions=None, **kwargs): """ from exact import Exact as xct + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + if not self.solver_is_initialized: assert not self.objective_given # NOTE: initialization of exact is also how it fixes the objective function. diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index ccf557769..0b6f6e9d8 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -83,9 +83,9 @@ def __init__(self, cpm_model=None, subsolver=None): Arguments: - cpm_model: a CPMpy Model() """ - if not self.supported(): - raise Exception( - "CPM_gurobi: Install the python package 'gurobipy' and make sure your licence is activated!") + # if not self.supported(): + # raise Exception( + # "CPM_gurobi: Install the python package 'gurobipy' and make sure your licence is activated!") import gurobipy as gp # TODO: subsolver could be a GRB_ENV if a user would want to hand one over @@ -115,6 +115,9 @@ def solve(self, time_limit=None, solution_callback=None, **kwargs): """ from gurobipy import GRB + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + if time_limit is not None: self.grb_model.setParam("TimeLimit", time_limit) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index e35133dfb..32b16444c 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -201,6 +201,10 @@ def solve(self, time_limit=None, **kwargs): Does not store the minizinc.Instance() or minizinc.Result() """ + + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + # make mzn_inst (mzn_kwargs, mzn_inst) = self._pre_solve(time_limit=time_limit, **kwargs) diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 986853814..6180790f6 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -133,6 +133,8 @@ def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwa """ from ortools.sat.python import cp_model as ort + # ensure all user vars are known to solver + self.solver_vars(list(self.user_vars)) # set time limit? if time_limit is not None: diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 690cbf21a..32c0b1edf 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -137,6 +137,10 @@ def solve(self, time_limit=None, assumptions=None): For use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together. Note: the PySAT interface is statefull, so you can incrementally call solve() with assumptions and it will reuse learned clauses """ + + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + if assumptions is None: pysat_assum_vars = [] # default if no assumptions else: @@ -185,9 +189,8 @@ def solve(self, time_limit=None, assumptions=None): cpm_var._value = True elif -lit in sol: cpm_var._value = False - else: - # not specified... - cpm_var._value = None + else: # not specified, dummy val + cpm_var._value = True return has_sol diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index 6fd6238e7..fecfc7ae5 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -94,6 +94,10 @@ def solve(self, time_limit=None, assumptions=None): - building it is the (computationally) hard part - checking for a solution is trivial after that """ + + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + has_sol = True if self.pysdd_root is not None: # if root node is false (empty), no solutions diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 4302c6677..52776ee1e 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -112,6 +112,9 @@ def solve(self, time_limit=None, assumptions=[], **kwargs): """ import z3 + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + if time_limit is not None: # z3 expects milliseconds in int self.z3_solver.set(timeout=int(time_limit*1000)) From 068f83e6252f61f44fd4ade08c0d1f4a071fe358 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 2 May 2024 10:27:30 +0200 Subject: [PATCH 17/48] add test --- tests/test_solvers.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/test_solvers.py b/tests/test_solvers.py index 0297afc6c..cce86757d 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -669,3 +669,16 @@ def test_gurobi_element(self): s = cp.SolverLookup.get("gurobi", model) self.assertTrue(s.solve()) self.assertTrue(iv.value()[idx.value(), idx2.value()] == 8) + + + def test_vars_not_removed(self): + bvs = cp.boolvar(shape=3) + m = cp.Model([cp.any(bvs) <= 2]) + for name, cls in cp.SolverLookup.base_solvers(): + print(f"Testing with {name}") + if cls.supported(): + # reset value for vars + bvs.clear() + self.assertTrue(m.solve(solver=name)) + for v in bvs: + self.assertIsNotNone(v.value()) From 3847201ea0d48f3843038b2e72340a7bdeae1bfc Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 2 May 2024 12:14:22 +0200 Subject: [PATCH 18/48] extend and clean automatic testsuite --- tests/test_constraints.py | 149 ++++++++++++++++++++++++-------------- 1 file changed, 94 insertions(+), 55 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 40b7e1590..b63f1f6b7 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -1,3 +1,6 @@ +import inspect + +import cpmpy from cpmpy import Model, SolverLookup, BoolVal from cpmpy.expressions.globalconstraints import * from cpmpy.expressions.globalfunctions import * @@ -9,6 +12,8 @@ # also add exclusions to the 3 EXCLUDE_* below as needed SOLVERNAMES = [name for name, solver in SolverLookup.base_solvers() if solver.supported()] +ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint + # Exclude some global constraints for solvers # Can be used when .value() method is not implemented/contains bugs EXCLUDE_GLOBAL = {"ortools": {}, @@ -60,8 +65,7 @@ def numexprs(solver): Numexpr: - Operator (non-Boolean) with all args Var/constant (examples: +,*,/,mod,wsum) (CPMpy class 'Operator', not is_bool()) - - Global constraint (non-Boolean) (examples: Max,Min,Element) - (CPMpy class 'GlobalConstraint', not is_bool())) + - Global functions (examples: Max,Min,Element) (CPMpy class 'GlobalFunction') """ names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if not is_bool] if solver in EXCLUDE_OPERATORS: @@ -80,6 +84,29 @@ def numexprs(solver): yield Operator(name, operator_args) + # boolexprs are also numeric + for expr in bool_exprs(solver): + yield expr + + # also global functions + classes = inspect.getmembers(cpmpy.expressions.globalfunctions, inspect.isclass) + classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalFunction) and name != "GlobalFunction"] + for name, cls in classes: + if name == "Abs": + expr = cls(NUM_ARGS[0]) + elif name == "Count": + expr = cls(NUM_ARGS, NUM_VAR) + elif name == "Element": + expr = cls(NUM_ARGS, POS_VAR) + else: + expr = cls(NUM_ARGS) + + if solver in EXCLUDE_GLOBAL and expr.name in EXCLUDE_GLOBAL[solver]: + continue + else: + yield expr + + # Generate all possible comparison constraints def comp_constraints(solver): @@ -92,30 +119,17 @@ def comp_constraints(solver): - Numeric inequality (>=,>,<,<=): Numexpr >=< Var (CPMpy class 'Comparison') """ for comp_name in Comparison.allowed: + for numexpr in numexprs(solver): - for rhs in [NUM_VAR, BOOL_VAR, 1, BoolVal(True)]: + # numeric vs bool/num var/val (incl global func) + lb, ub = get_bounds(numexpr) + for rhs in [NUM_VAR, BOOL_VAR, BoolVal(True), 1]: + if comp_name == ">" and ub <= get_bounds(rhs)[1]: + continue + if comp_name == "<" and lb >= get_bounds(rhs)[0]: + continue yield Comparison(comp_name, numexpr, rhs) - for comp_name in Comparison.allowed: - for glob_expr in global_constraints(solver): - if not glob_expr.is_bool(): - for rhs in [NUM_VAR, BOOL_VAR, 1, BoolVal(True)]: - if comp_name == "<" and get_bounds(glob_expr)[0] >= get_bounds(rhs)[1]: - continue - 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, BOOL_VAR, 1, BoolVal(True)]: - if comp_name == '>': - # >1 is unsat for boolean expressions, so change it to 0 - if isinstance(rhs, int) and rhs == 1: - rhs = 0 - if isinstance(rhs, BoolVal) and rhs.args[0] == True: - rhs = BoolVal(False) - yield Comparison(comp_name, boolexpr, rhs) - # Generate all possible boolean expressions def bool_exprs(solver): @@ -123,6 +137,7 @@ 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') + - Global constraints """ names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if is_bool] @@ -143,8 +158,7 @@ def bool_exprs(solver): yield Comparison(eq_name, *BOOL_ARGS[:2]) for cpm_cons in global_constraints(solver): - if cpm_cons.is_bool(): - yield cpm_cons + yield cpm_cons def global_constraints(solver): """ @@ -152,30 +166,39 @@ def global_constraints(solver): - AllDifferent, AllEqual, Circuit, Minimum, Maximum, Element, Xor, Cumulative, NValue, Count """ - global_cons = [AllDifferent, AllEqual, Minimum, Maximum, NValue] - 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 - - # "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 "xor" not in EXCLUDE_GLOBAL[solver]: - yield Xor(BOOL_ARGS) - - if solver not in EXCLUDE_GLOBAL or "count" not in EXCLUDE_GLOBAL[solver]: - yield Count(NUM_ARGS, NUM_VAR) - - 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) - + classes = inspect.getmembers(cpmpy.expressions.globalconstraints, inspect.isclass) + classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalConstraint) and name != "GlobalConstraint"] + + for name, cls in classes: + + if name == "Xor": + expr = cls(BOOL_ARGS) + elif name == "Inverse": + expr = cls(NUM_ARGS, NUM_ARGS) + elif name == "Table": + expr = cls(NUM_ARGS, [[0,1,2],[1,2,0],[1,0,2]]) + elif name == "IfThenElse": + expr = cls(*BOOL_ARGS) + elif name == "InDomain": + expr = cls(NUM_VAR, [0,1,6]) + elif name == "Cumulative": + 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 + expr = Cumulative(s, dur, e, demand, cap) + elif name == "GlobalCardinalityCount": + vals = intvar(0,3, shape=3) + cnts = intvar(0,10,shape=3) + expr = cls(NUM_ARGS, vals, cnts) + else: # default constructor, list of numvars + expr= cls(NUM_ARGS) + + if solver in EXCLUDE_GLOBAL and name in EXCLUDE_GLOBAL[solver]: + continue + else: + yield expr def reify_imply_exprs(solver): """ @@ -200,13 +223,21 @@ def reify_imply_exprs(solver): yield comp_expr == BOOL_VAR +def verify(cons): + assert cons.value() + + @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. """ - assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + if ALL_SOLS: + n_sols = SolverLookup.get(solver, Model(constraint)).solveAll(display=lambda: verify(constraint)) + assert n_sols >= 1 + else: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert constraint.value() @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) @@ -214,8 +245,12 @@ 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() + if ALL_SOLS: + n_sols = SolverLookup.get(solver, Model(constraint)).solveAll(display= lambda: verify(constraint)) + assert n_sols >= 1 + else: + assert SolverLookup.get(solver,Model(constraint)).solve() + assert constraint.value() @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) @@ -223,5 +258,9 @@ 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() + if ALL_SOLS: + n_sols = SolverLookup.get(solver, Model(constraint)).solveAll(display=lambda: verify(constraint)) + assert n_sols >= 1 + else: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert constraint.value() From 6d21c8b36b364e30a4f54c603d26e5f922b86f74 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 2 May 2024 12:15:30 +0200 Subject: [PATCH 19/48] undefinedness -> False in neirest Bool context --- cpmpy/expressions/core.py | 13 ++++- cpmpy/expressions/globalconstraints.py | 76 +++++++++++++++++++------- 2 files changed, 67 insertions(+), 22 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index 1b210e680..12b3fbeb7 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -400,7 +400,11 @@ def __repr__(self): # return the value of the expression # optional, default: None def value(self): - arg_vals = [argval(a) for a in self.args] + try: + arg_vals = [argval(a) for a in self.args] + except IncompleteFunctionError: + return False + if any(a is None for a in arg_vals): return None if self.name == "==": return arg_vals[0] == arg_vals[1] elif self.name == "!=": return arg_vals[0] != arg_vals[1] @@ -526,11 +530,16 @@ def wrap_bracket(arg): return "{}({})".format(self.name, self.args) def value(self): + if self.name == "wsum": # wsum: arg0 is list of constants, no .value() use as is arg_vals = [self.args[0], [argval(arg) for arg in self.args[1]]] else: - arg_vals = [argval(arg) for arg in self.args] + try: + arg_vals = [argval(arg) for arg in self.args] + except IncompleteFunctionError as e: + if self.is_bool(): return False + raise e if any(a is None for a in arg_vals): return None diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index cb792bd89..ea9cfddb2 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -171,7 +171,11 @@ def decompose(self): return [var1 != var2 for var1, var2 in all_pairs(self.args)], [] def value(self): - return len(set(a.value() for a in self.args)) == len(self.args) + try: + values = [argval(a) for a in self.args] + return len(set(values)) == len(self.args) + except IncompleteFunctionError: + return False class AllDifferentExcept0(GlobalConstraint): @@ -186,9 +190,11 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - vals = [a.value() for a in self.args if a.value() != 0] - return len(set(vals)) == len(vals) - + try: + vals = [a.value() for a in self.args if a.value() != 0] + return len(set(vals)) == len(vals) + except IncompleteFunctionError: + return False def allequal(args): warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -208,8 +214,11 @@ def decompose(self): return [var1 == var2 for var1, var2 in zip(self.args[:-1], self.args[1:])], [] def value(self): - return len(set(a.value() for a in self.args)) == 1 - + try: + values = [argval(a) for a in self.args] + return len(set(values)) == 1 + except IncompleteFunctionError: + return False def circuit(args): warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -252,7 +261,11 @@ def value(self): pathlen = 0 idx = 0 visited = set() - arr = [argval(a) for a in self.args] + try: + arr = [argval(a) for a in self.args] + except IncompleteFunctionError: + return False + while idx not in visited: if idx is None: return False @@ -287,9 +300,16 @@ def decompose(self): return [all(rev[x] == i for i, x in enumerate(fwd))], [] def value(self): - fwd = [argval(a) for a in self.args[0]] - rev = [argval(a) for a in self.args[1]] - return all(rev[x] == i for i, x in enumerate(fwd)) + try: + fwd = [argval(a) for a in self.args[0]] + rev = [argval(a) for a in self.args[1]] + except IncompleteFunctionError: + return False + # args are fine, now evaluate actual inverse cons + try: + return all(rev[x] == i for i, x in enumerate(fwd)) + except IndexError: # partiality of Element constraint + raise IncompleteFunctionError class Table(GlobalConstraint): @@ -308,8 +328,12 @@ def decompose(self): def value(self): arr, tab = self.args - arrval = [argval(a) for a in arr] - return arrval in tab + try: + arrval = [argval(a) for a in arr] + return arrval in tab + except IncompleteFunctionError: + return False + # syntax of the form 'if b then x == 9 else x == 0' is not supported (no override possible) @@ -323,10 +347,13 @@ def __init__(self, condition, if_true, if_false): def value(self): condition, if_true, if_false = self.args - if argval(condition): - return argval(if_true) - else: - return argval(if_false) + try: + if argval(condition): + return argval(if_true) + else: + return argval(if_false) + except IncompleteFunctionError: + return False def decompose(self): condition, if_true, if_false = self.args @@ -374,7 +401,10 @@ def decompose(self): def value(self): - return argval(self.args[0]) in argval(self.args[1]) + try: + return argval(self.args[0]) in argval(self.args[1]) + except IncompleteFunctionError: + return False def __repr__(self): return "{} in {}".format(self.args[0], self.args[1]) @@ -404,7 +434,10 @@ def decompose(self): return decomp, [] def value(self): - return sum(argval(a) for a in self.args) % 2 == 1 + try: + return sum(argval(a) for a in self.args) % 2 == 1 + except IncompleteFunctionError: + return False def __repr__(self): if len(self.args) == 2: @@ -473,8 +506,11 @@ def decompose(self): return cons, [] def value(self): - argvals = [np.array([argval(a) for a in arg]) if is_any_list(arg) - else argval(arg) for arg in self.args] + try: + argvals = [np.array([argval(a) for a in arg]) if is_any_list(arg) + else argval(arg) for arg in self.args] + except IncompleteFunctionError: + return False if any(a is None for a in argvals): return None From 240976ac293f7cc8378c9f68c3936e1c380c686c Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Thu, 2 May 2024 12:15:51 +0200 Subject: [PATCH 20/48] fix simplication when comparison is used as num argument --- cpmpy/transformations/normalize.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/cpmpy/transformations/normalize.py b/cpmpy/transformations/normalize.py index ec0c5e756..c69ac77cb 100644 --- a/cpmpy/transformations/normalize.py +++ b/cpmpy/transformations/normalize.py @@ -132,15 +132,15 @@ def simplify_boolean(lst_of_expr, num_context=False): if name == "==" or name == "<=": newlist.append(recurse_negation(lhs)) if name == "<": - newlist.append(BoolVal(False)) + newlist.append(0 if num_context else BoolVal(False)) if name == ">=": - newlist.append(BoolVal(True)) + newlist.append(1 if num_context else BoolVal(True)) elif 0 < rhs < 1: # a floating point value if name == "==": - newlist.append(BoolVal(False)) + newlist.append(0 if num_context else BoolVal(False)) if name == "!=": - newlist.append(BoolVal(True)) + newlist.append(1 if num_context else BoolVal(True)) if name == "<" or name == "<=": newlist.append(recurse_negation(lhs)) if name == ">" or name == ">=": @@ -151,9 +151,9 @@ def simplify_boolean(lst_of_expr, num_context=False): if name == "!=" or name == "<": newlist.append(recurse_negation(lhs)) if name == ">": - newlist.append(BoolVal(False)) + newlist.append(0 if num_context else BoolVal(False)) if name == "<=": - newlist.append(BoolVal(True)) + newlist.append(1 if num_context else BoolVal(True)) elif rhs > 1: newlist.append(BoolVal(name in {"!=", "<", "<="})) # all other operators evaluate to False else: From f1bbd685a888fb490bdf5b6bd3fb91bd2d19c479 Mon Sep 17 00:00:00 2001 From: Dimos Tsouros Date: Thu, 2 May 2024 18:28:19 +0200 Subject: [PATCH 21/48] vals in gcc are ints --- tests/test_constraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index b63f1f6b7..046db1e14 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -189,7 +189,7 @@ def global_constraints(solver): cap = 10 expr = Cumulative(s, dur, e, demand, cap) elif name == "GlobalCardinalityCount": - vals = intvar(0,3, shape=3) + vals = [1, 2, 3] cnts = intvar(0,10,shape=3) expr = cls(NUM_ARGS, vals, cnts) else: # default constructor, list of numvars From d95fad2923f905cd3cad8e82770c3697cae7b294 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 7 May 2024 10:22:16 +0200 Subject: [PATCH 22/48] cleanup of test_constraints file --- tests/test_constraints.py | 54 +++++++++++++++++---------------------- 1 file changed, 24 insertions(+), 30 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 046db1e14..2bed73ee7 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -15,14 +15,18 @@ ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint # Exclude some global constraints for solvers -# Can be used when .value() method is not implemented/contains bugs -EXCLUDE_GLOBAL = {"ortools": {}, - "gurobi": {}, - "minizinc": {"circuit"}, - "pysat": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative"}, - "pysdd": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative",'xor'}, - "exact": {}, - "choco": {} +NUM_GLOBAL = { + "AllEqual", "AllDifferent", "AllDifferentExcept0", "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", + # also global functions + "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", +} + +# Solvers not supporting arithmetic constraints +SAT_SOLVERS = {"pysat", "pysdd"} + +EXCLUDE_GLOBAL = {"minizinc": {"circuit"}, + "pysat": NUM_GLOBAL, + "pysdd": NUM_GLOBAL | {"Xor"}, } # Exclude certain operators for solvers. @@ -33,16 +37,6 @@ "exact": {"mod","pow","div","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": {}, - "minizinc": {}, - "z3": {}, - "pysat": {}, - "pysdd": {}, - "exact": {"mod","pow","div","mul"}, - } - # Variables to use in the rest of the test script NUM_ARGS = [intvar(-3, 5, name=n) for n in "xyz"] # Numerical variables NN_VAR = intvar(0, 10, name="n_neg") # Non-negative variable, needed in power functions @@ -91,6 +85,8 @@ def numexprs(solver): # also global functions classes = inspect.getmembers(cpmpy.expressions.globalfunctions, inspect.isclass) classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalFunction) and name != "GlobalFunction"] + classes = [(name, cls) for name, cls in classes if name not in EXCLUDE_GLOBAL.get(solver, {})] + for name, cls in classes: if name == "Abs": expr = cls(NUM_ARGS[0]) @@ -124,6 +120,8 @@ def comp_constraints(solver): # numeric vs bool/num var/val (incl global func) lb, ub = get_bounds(numexpr) for rhs in [NUM_VAR, BOOL_VAR, BoolVal(True), 1]: + if solver in SAT_SOLVERS and not is_num(rhs): + continue if comp_name == ">" and ub <= get_bounds(rhs)[1]: continue if comp_name == "<" and lb >= get_bounds(rhs)[0]: @@ -168,13 +166,14 @@ def global_constraints(solver): """ classes = inspect.getmembers(cpmpy.expressions.globalconstraints, inspect.isclass) classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalConstraint) and name != "GlobalConstraint"] + classes = [(name, cls) for name, cls in classes if name not in EXCLUDE_GLOBAL.get(solver, {})] for name, cls in classes: if name == "Xor": expr = cls(BOOL_ARGS) elif name == "Inverse": - expr = cls(NUM_ARGS, NUM_ARGS) + expr = cls(NUM_ARGS, [1,2,0]) elif name == "Table": expr = cls(NUM_ARGS, [[0,1,2],[1,2,0],[1,0,2]]) elif name == "IfThenElse": @@ -207,20 +206,15 @@ def reify_imply_exprs(solver): 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 + yield bool_expr.implies(BOOL_VAR) + yield BOOL_VAR.implies(bool_expr) + yield bool_expr == BOOL_VAR for comp_expr in comp_constraints(solver): 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 + yield comp_expr.implies(BOOL_VAR) + yield BOOL_VAR.implies(comp_expr) + yield comp_expr == BOOL_VAR def verify(cons): From 88705ebdd0e1118fc9e7c16aff11ea7a94332d05 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 7 May 2024 10:22:56 +0200 Subject: [PATCH 23/48] ensure comparisons of Bool to constant are translated properly --- cpmpy/solvers/pysat.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 32c0b1edf..889e48aa8 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -38,7 +38,7 @@ from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint -from ..transformations.normalize import toplevel_list +from ..transformations.normalize import toplevel_list, simplify_boolean from ..transformations.reification import only_implies, only_bv_reifies @@ -233,6 +233,7 @@ def transform(self, cpm_expr): """ cpm_cons = toplevel_list(cpm_expr) cpm_cons = decompose_in_tree(cpm_cons) + cpm_cons = simplify_boolean(cpm_cons) cpm_cons = flatten_constraint(cpm_cons) cpm_cons = only_bv_reifies(cpm_cons) cpm_cons = only_implies(cpm_cons) From 2efbe75691af71de3080950baf309bea011b82dc Mon Sep 17 00:00:00 2001 From: wout4 Date: Wed, 8 May 2024 14:14:21 +0200 Subject: [PATCH 24/48] introduce argvals() helper function Use NaN for undefined values --- cpmpy/expressions/core.py | 26 ++--- cpmpy/expressions/globalconstraints.py | 152 ++++++++++++------------- cpmpy/expressions/globalfunctions.py | 25 ++-- cpmpy/expressions/utils.py | 11 +- 4 files changed, 97 insertions(+), 117 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index 12b3fbeb7..e416adb6d 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -72,8 +72,8 @@ import numpy as np -from .utils import is_num, is_any_list, flatlist, argval, get_bounds, is_boolexpr, is_true_cst, is_false_cst -from ..exceptions import IncompleteFunctionError, TypeError +from .utils import is_num, is_any_list, flatlist, get_bounds, is_boolexpr, is_true_cst, is_false_cst, argvals +from ..exceptions import TypeError class Expression(object): @@ -400,10 +400,7 @@ def __repr__(self): # return the value of the expression # optional, default: None def value(self): - try: - arg_vals = [argval(a) for a in self.args] - except IncompleteFunctionError: - return False + arg_vals = argvals(self.args) if any(a is None for a in arg_vals): return None if self.name == "==": return arg_vals[0] == arg_vals[1] @@ -533,14 +530,9 @@ def value(self): if self.name == "wsum": # wsum: arg0 is list of constants, no .value() use as is - arg_vals = [self.args[0], [argval(arg) for arg in self.args[1]]] + arg_vals = [self.args[0], argvals(self.args[1])] else: - try: - arg_vals = [argval(arg) for arg in self.args] - except IncompleteFunctionError as e: - if self.is_bool(): return False - raise e - + arg_vals = argvals(self.args) if any(a is None for a in arg_vals): return None # non-boolean @@ -555,10 +547,12 @@ def value(self): try: return arg_vals[0] // arg_vals[1] except ZeroDivisionError: - raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}") + return np.nan # we use NaN to represent undefined values + + # boolean context, replace NaN with False + arg_vals = [False if np.isnan(x) else x for x in arg_vals] - # boolean - elif self.name == "and": return all(arg_vals) + if self.name == "and": return all(arg_vals) elif self.name == "or" : return any(arg_vals) elif self.name == "->": return (not arg_vals[0]) or arg_vals[1] elif self.name == "not": return not arg_vals[0] diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index ea9cfddb2..823513550 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -1,5 +1,5 @@ #!/usr/bin/env python -#-*- coding:utf-8 -*- +# -*- coding:utf-8 -*- ## ## globalconstraints.py ## @@ -108,13 +108,14 @@ def my_circuit_decomp(self): """ import copy -import warnings # for deprecation warning +import warnings # for deprecation warning import numpy as np -from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError +from ..exceptions import CPMpyException, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl, _IntVarImpl -from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds -from .globalfunctions import * # XXX make this file backwards compatible +from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, \ + is_true_cst, argvals +from .globalfunctions import * # XXX make this file backwards compatible # Base class GlobalConstraint @@ -155,13 +156,15 @@ def get_bounds(self): # Global Constraints (with Boolean return type) def alldifferent(args): - warnings.warn("Deprecated, use AllDifferent(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) - return AllDifferent(*args) # unfold list as individual arguments + warnings.warn("Deprecated, use AllDifferent(v1,v2,...,vn) instead, will be removed in stable version", + DeprecationWarning) + return AllDifferent(*args) # unfold list as individual arguments class AllDifferent(GlobalConstraint): """All arguments have a different (distinct) value """ + def __init__(self, *args): super().__init__("alldifferent", flatlist(args)) @@ -171,17 +174,18 @@ def decompose(self): return [var1 != var2 for var1, var2 in all_pairs(self.args)], [] def value(self): - try: - values = [argval(a) for a in self.args] - return len(set(values)) == len(self.args) - except IncompleteFunctionError: + values = argvals(self.args) + if any([np.isnan(x) for x in values]): return False + else: + return len(set(values)) == len(self.args) class AllDifferentExcept0(GlobalConstraint): """ All nonzero arguments have a distinct value """ + def __init__(self, *args): super().__init__("alldifferent_except0", flatlist(args)) @@ -190,20 +194,23 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - try: - vals = [a.value() for a in self.args if a.value() != 0] - return len(set(vals)) == len(vals) - except IncompleteFunctionError: + vals = [a.value() for a in self.args if a.value() != 0] + if any([np.isnan(x) for x in vals]): return False + else: + return len(set(vals)) == len(vals) + def allequal(args): - warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) - return AllEqual(*args) # unfold list as individual arguments + warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", + DeprecationWarning) + return AllEqual(*args) # unfold list as individual arguments class AllEqual(GlobalConstraint): """All arguments have the same value """ + def __init__(self, *args): super().__init__("allequal", flatlist(args)) @@ -214,20 +221,22 @@ def decompose(self): return [var1 == var2 for var1, var2 in zip(self.args[:-1], self.args[1:])], [] def value(self): - try: - values = [argval(a) for a in self.args] - return len(set(values)) == 1 - except IncompleteFunctionError: + values = argvals(self.args) + if any([np.isnan(x) for x in values]): return False + return len(set(values)) == 1 + def circuit(args): - warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) - return Circuit(*args) # unfold list as individual arguments + warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", + DeprecationWarning) + return Circuit(*args) # unfold list as individual arguments class Circuit(GlobalConstraint): """The sequence of variables form a circuit, where x[i] = j means that j is the successor of i. """ + def __init__(self, *args): flatargs = flatlist(args) if any(is_boolexpr(arg) for arg in flatargs): @@ -246,14 +255,15 @@ def decompose(self): """ succ = cpm_array(self.args) n = len(succ) - order = intvar(0,n-1, shape=n) + order = intvar(0, n - 1, shape=n) constraining = [] - constraining += [AllDifferent(succ)] # different successors - constraining += [AllDifferent(order)] # different orders - constraining += [order[n-1] == 0] # symmetry breaking, last one is '0' + constraining += [AllDifferent(succ)] # different successors + constraining += [AllDifferent(order)] # different orders + constraining += [order[n - 1] == 0] # symmetry breaking, last one is '0' defining = [order[0] == succ[0]] - defining += [order[i] == succ[order[i-1]] for i in range(1,n)] # first one is successor of '0', ith one is successor of i-1 + defining += [order[i] == succ[order[i - 1]] for i in + range(1, n)] # first one is successor of '0', ith one is successor of i-1 return constraining, defining @@ -261,11 +271,7 @@ def value(self): pathlen = 0 idx = 0 visited = set() - try: - arr = [argval(a) for a in self.args] - except IncompleteFunctionError: - return False - + arr = argvals(self.args) while idx not in visited: if idx is None: return False @@ -274,7 +280,6 @@ def value(self): visited.add(idx) pathlen += 1 idx = arr[idx] - return pathlen == len(self.args) and idx == 0 @@ -286,8 +291,9 @@ class Inverse(GlobalConstraint): fwd[i] == x <==> rev[x] == i """ + def __init__(self, fwd, rev): - flatargs = flatlist([fwd,rev]) + flatargs = flatlist([fwd, rev]) if any(is_boolexpr(arg) for arg in flatargs): raise TypeError("Only integer arguments allowed for global constraint Inverse: {}".format(flatargs)) assert len(fwd) == len(rev) @@ -300,21 +306,19 @@ def decompose(self): return [all(rev[x] == i for i, x in enumerate(fwd))], [] def value(self): - try: - fwd = [argval(a) for a in self.args[0]] - rev = [argval(a) for a in self.args[1]] - except IncompleteFunctionError: - return False + fwd = argvals(self.args[0]) + rev = argvals(self.args[1]) # args are fine, now evaluate actual inverse cons try: return all(rev[x] == i for i, x in enumerate(fwd)) - except IndexError: # partiality of Element constraint - raise IncompleteFunctionError + except IndexError: # if index is out of range then it's definitely not Inverse. + return False class Table(GlobalConstraint): """The values of the variables in 'array' correspond to a row in 'table' """ + def __init__(self, array, table): array = flatlist(array) if not all(isinstance(x, Expression) for x in array): @@ -328,12 +332,8 @@ def decompose(self): def value(self): arr, tab = self.args - try: - arrval = [argval(a) for a in arr] - return arrval in tab - except IncompleteFunctionError: - return False - + arrval = [argval(a) for a in arr if not np.isnan(argval(a))] + return arrval in tab # syntax of the form 'if b then x == 9 else x == 0' is not supported (no override possible) @@ -347,13 +347,10 @@ def __init__(self, condition, if_true, if_false): def value(self): condition, if_true, if_false = self.args - try: - if argval(condition): - return argval(if_true) - else: - return argval(if_false) - except IncompleteFunctionError: - return False + if is_true_cst((argval(condition))): + return argval(if_true) + else: + return argval(if_false) def decompose(self): condition, if_true, if_false = self.args @@ -364,15 +361,14 @@ def __repr__(self): return "If {} Then {} Else {}".format(condition, if_true, if_false) - class InDomain(GlobalConstraint): """ The "InDomain" constraint, defining non-interval domains for an expression """ def __init__(self, expr, arr): - assert not (is_boolexpr(expr) or any(is_boolexpr(a) for a in arr)), \ - "The expressions in the InDomain constraint should not be boolean" + # assert not (is_boolexpr(expr) or any(is_boolexpr(a) for a in arr)), \ + # "The expressions in the InDomain constraint should not be boolean" super().__init__("InDomain", [expr, arr]) def decompose(self): @@ -387,8 +383,8 @@ def decompose(self): lb, ub = expr.get_bounds() defining = [] - #if expr is not a var - if not isinstance(expr,_IntVarImpl): + # if expr is not a var + if not isinstance(expr, _IntVarImpl): aux = intvar(lb, ub) defining.append(aux == expr) expr = aux @@ -399,12 +395,9 @@ def decompose(self): else: return [expr != val for val in range(lb, ub + 1) if val not in arr], defining - def value(self): - try: - return argval(self.args[0]) in argval(self.args[1]) - except IncompleteFunctionError: - return False + val = argval(self.args[0]) + return val in argval(self.args[1]) and not np.isnan(val) def __repr__(self): return "{} in {}".format(self.args[0], self.args[1]) @@ -430,14 +423,11 @@ def decompose(self): # there are multiple decompositions possible, Recursively using sum allows it to be efficient for all solvers. decomp = [sum(self.args[:2]) == 1] if len(self.args) > 2: - decomp = Xor([decomp,self.args[2:]]).decompose()[0] + decomp = Xor([decomp, self.args[2:]]).decompose()[0] return decomp, [] def value(self): - try: - return sum(argval(a) for a in self.args) % 2 == 1 - except IncompleteFunctionError: - return False + return sum(argvals(self.args)) % 2 == 1 def __repr__(self): if len(self.args) == 2: @@ -451,6 +441,7 @@ class Cumulative(GlobalConstraint): Ensures no overlap between tasks and never exceeding the capacity of the resource Supports both varying demand across tasks or equal demand for all jobs """ + def __init__(self, start, duration, end, demand, capacity): assert is_any_list(start), "start should be a list" assert is_any_list(duration), "duration should be a list" @@ -469,7 +460,7 @@ def __init__(self, start, duration, end, demand, capacity): if is_any_list(demand): demand = flatlist(demand) assert len(demand) == n_jobs, "Demand should be supplied for each task or be single constant" - else: # constant demand + else: # constant demand demand = [demand] * n_jobs super(Cumulative, self).__init__("cumulative", [start, duration, end, demand, capacity]) @@ -493,7 +484,7 @@ def decompose(self): # demand doesn't exceed capacity lb, ub = min(s.lb for s in start), max(s.ub for s in end) - for t in range(lb,ub+1): + for t in range(lb, ub + 1): demand_at_t = 0 for job in range(len(start)): if is_num(demand): @@ -506,24 +497,21 @@ def decompose(self): return cons, [] def value(self): - try: - argvals = [np.array([argval(a) for a in arg]) if is_any_list(arg) - else argval(arg) for arg in self.args] - except IncompleteFunctionError: - return False + vals = [np.array(argvals(arg)) if is_any_list(arg) + else argval(arg) for arg in self.args] - if any(a is None for a in argvals): + if any(a is None for a in vals): return None # start, dur, end are np arrays - start, dur, end, demand, capacity = argvals + start, dur, end, demand, capacity = vals # start and end seperated by duration if not (start + dur == end).all(): return False # demand doesn't exceed capacity lb, ub = min(start), max(end) - for t in range(lb, ub+1): + for t in range(lb, ub + 1): if capacity < sum(demand * ((start <= t) & (t < end))): return False @@ -540,7 +528,7 @@ def __init__(self, vars, vals, occ): flatargs = flatlist([vars, vals, occ]) if any(is_boolexpr(arg) for arg in flatargs): raise TypeError("Only numerical arguments allowed for gcc global constraint: {}".format(flatargs)) - super().__init__("gcc", [vars,vals,occ]) + super().__init__("gcc", [vars, vals, occ]) def decompose(self): from .globalfunctions import Count @@ -566,6 +554,7 @@ class DirectConstraint(Expression): If you want/need to use what the solver returns (e.g. an identifier for use in other constraints), then use `directvar()` instead, or access the solver object from the solver interface directly. """ + def __init__(self, name, arguments, novar=None): """ name: name of the solver function that you wish to call @@ -603,4 +592,3 @@ def callSolver(self, CPMpy_solver, Native_solver): solver_args[i] = CPMpy_solver.solver_vars(solver_args[i]) # len(native_args) should match nr of arguments of `native_function` return solver_function(*solver_args) - diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 8c1eeecca..ff4656c21 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -64,10 +64,10 @@ def decompose_comparison(self): import copy import warnings # for deprecation warning import numpy as np -from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError +from ..exceptions import CPMpyException, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl -from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds +from .utils import flatlist, argval, argvals, eval_comparison, is_any_list, is_boolexpr, get_bounds class GlobalFunction(Expression): @@ -116,11 +116,12 @@ def __init__(self, arg_list): super().__init__("min", flatlist(arg_list)) def value(self): - argvals = [argval(a) for a in self.args] - if any(val is None for val in argvals): + vals = argvals(self.args) + if any(val is None for val in vals): return None else: - return min(argvals) + return min(vals) # will always return nan if any argument is nan. + # This is in line with how solvers handle undefinedness in Min and Max. def decompose_comparison(self, cpm_op, cpm_rhs): """ @@ -157,11 +158,11 @@ def __init__(self, arg_list): super().__init__("max", flatlist(arg_list)) def value(self): - argvals = [argval(a) for a in self.args] - if any(val is None for val in argvals): + vals = argvals(self.args) + if any(val is None for val in vals): return None else: - return max(argvals) + return max(vals) def decompose_comparison(self, cpm_op, cpm_rhs): """ @@ -257,8 +258,8 @@ def value(self): if idxval is not None: if idxval >= 0 and idxval < len(arr): return argval(arr[idxval]) - raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}") - return None # default + return np.nan + return None # default def decompose_comparison(self, cpm_op, cpm_rhs): """ @@ -271,8 +272,6 @@ def decompose_comparison(self, cpm_op, cpm_rhs): they should be enforced toplevel. """ - from .python_builtins import any - 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)], [] @@ -356,7 +355,7 @@ def decompose_comparison(self, cmp_op, cpm_rhs): return [eval_comparison(cmp_op, sum(bvars), cpm_rhs)], constraints def value(self): - return len(set(argval(a) for a in self.args)) + return len(set(argval(a) for a in self.args if not np.isnan(argval(a)))) def get_bounds(self): """ diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index a42e88c82..88442d290 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -118,14 +118,13 @@ def all_pairs(args): def argval(a): """ returns .value() of Expression, otherwise the variable itself - We check with hasattr instead of isinstance to avoid circular dependency """ - try: - return a.value() if hasattr(a, "value") else a - except IncompleteFunctionError as e: - if a.is_bool(): return False - raise e + return a.value() if hasattr(a, "value") else a + + +def argvals(arr): + return [argval(a) for a in arr] def eval_comparison(str_op, lhs, rhs): From 3f8ef4e3697b138e704c8cea9aa0aa0dbbf43ebe Mon Sep 17 00:00:00 2001 From: wout4 Date: Wed, 8 May 2024 14:26:07 +0200 Subject: [PATCH 25/48] exclude inverse from tests --- tests/test_constraints.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 046db1e14..b04208b1e 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -16,13 +16,13 @@ # Exclude some global constraints for solvers # Can be used when .value() method is not implemented/contains bugs -EXCLUDE_GLOBAL = {"ortools": {}, - "gurobi": {}, - "minizinc": {"circuit"}, - "pysat": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative"}, - "pysdd": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative",'xor'}, - "exact": {}, - "choco": {} +EXCLUDE_GLOBAL = {"ortools": {'inverse'}, + "gurobi": {'inverse'}, + "minizinc": {"circuit", 'inverse'}, + "pysat": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative", 'inverse'}, + "pysdd": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative",'xor', 'inverse'}, + "exact": {'inverse'}, + "choco": {'inverse'} } # Exclude certain operators for solvers. From daf505d5e1a2614d99ebbed82a4e5d8dcc629fc0 Mon Sep 17 00:00:00 2001 From: wout4 Date: Wed, 8 May 2024 16:17:27 +0200 Subject: [PATCH 26/48] include inverse again, test are failing anyway --- tests/test_constraints.py | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index b04208b1e..046db1e14 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -16,13 +16,13 @@ # Exclude some global constraints for solvers # Can be used when .value() method is not implemented/contains bugs -EXCLUDE_GLOBAL = {"ortools": {'inverse'}, - "gurobi": {'inverse'}, - "minizinc": {"circuit", 'inverse'}, - "pysat": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative", 'inverse'}, - "pysdd": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative",'xor', 'inverse'}, - "exact": {'inverse'}, - "choco": {'inverse'} +EXCLUDE_GLOBAL = {"ortools": {}, + "gurobi": {}, + "minizinc": {"circuit"}, + "pysat": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative"}, + "pysdd": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative",'xor'}, + "exact": {}, + "choco": {} } # Exclude certain operators for solvers. From 8adcf5b22b34d797dadaf394185092de6821c75c Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 10 May 2024 14:39:32 +0200 Subject: [PATCH 27/48] Revert "introduce argvals() helper function" This reverts commit 2efbe75691af71de3080950baf309bea011b82dc. --- cpmpy/expressions/core.py | 26 +++-- cpmpy/expressions/globalconstraints.py | 152 +++++++++++++------------ cpmpy/expressions/globalfunctions.py | 25 ++-- cpmpy/expressions/utils.py | 11 +- 4 files changed, 117 insertions(+), 97 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index e416adb6d..12b3fbeb7 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -72,8 +72,8 @@ import numpy as np -from .utils import is_num, is_any_list, flatlist, get_bounds, is_boolexpr, is_true_cst, is_false_cst, argvals -from ..exceptions import TypeError +from .utils import is_num, is_any_list, flatlist, argval, get_bounds, is_boolexpr, is_true_cst, is_false_cst +from ..exceptions import IncompleteFunctionError, TypeError class Expression(object): @@ -400,7 +400,10 @@ def __repr__(self): # return the value of the expression # optional, default: None def value(self): - arg_vals = argvals(self.args) + try: + arg_vals = [argval(a) for a in self.args] + except IncompleteFunctionError: + return False if any(a is None for a in arg_vals): return None if self.name == "==": return arg_vals[0] == arg_vals[1] @@ -530,9 +533,14 @@ def value(self): if self.name == "wsum": # wsum: arg0 is list of constants, no .value() use as is - arg_vals = [self.args[0], argvals(self.args[1])] + arg_vals = [self.args[0], [argval(arg) for arg in self.args[1]]] else: - arg_vals = argvals(self.args) + try: + arg_vals = [argval(arg) for arg in self.args] + except IncompleteFunctionError as e: + if self.is_bool(): return False + raise e + if any(a is None for a in arg_vals): return None # non-boolean @@ -547,12 +555,10 @@ def value(self): try: return arg_vals[0] // arg_vals[1] except ZeroDivisionError: - return np.nan # we use NaN to represent undefined values - - # boolean context, replace NaN with False - arg_vals = [False if np.isnan(x) else x for x in arg_vals] + raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}") - if self.name == "and": return all(arg_vals) + # boolean + elif self.name == "and": return all(arg_vals) elif self.name == "or" : return any(arg_vals) elif self.name == "->": return (not arg_vals[0]) or arg_vals[1] elif self.name == "not": return not arg_vals[0] diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 823513550..ea9cfddb2 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -1,5 +1,5 @@ #!/usr/bin/env python -# -*- coding:utf-8 -*- +#-*- coding:utf-8 -*- ## ## globalconstraints.py ## @@ -108,14 +108,13 @@ def my_circuit_decomp(self): """ import copy -import warnings # for deprecation warning +import warnings # for deprecation warning import numpy as np -from ..exceptions import CPMpyException, TypeError +from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl, _IntVarImpl -from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, \ - is_true_cst, argvals -from .globalfunctions import * # XXX make this file backwards compatible +from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds +from .globalfunctions import * # XXX make this file backwards compatible # Base class GlobalConstraint @@ -156,15 +155,13 @@ def get_bounds(self): # Global Constraints (with Boolean return type) def alldifferent(args): - warnings.warn("Deprecated, use AllDifferent(v1,v2,...,vn) instead, will be removed in stable version", - DeprecationWarning) - return AllDifferent(*args) # unfold list as individual arguments + warnings.warn("Deprecated, use AllDifferent(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) + return AllDifferent(*args) # unfold list as individual arguments class AllDifferent(GlobalConstraint): """All arguments have a different (distinct) value """ - def __init__(self, *args): super().__init__("alldifferent", flatlist(args)) @@ -174,18 +171,17 @@ def decompose(self): return [var1 != var2 for var1, var2 in all_pairs(self.args)], [] def value(self): - values = argvals(self.args) - if any([np.isnan(x) for x in values]): - return False - else: + try: + values = [argval(a) for a in self.args] return len(set(values)) == len(self.args) + except IncompleteFunctionError: + return False class AllDifferentExcept0(GlobalConstraint): """ All nonzero arguments have a distinct value """ - def __init__(self, *args): super().__init__("alldifferent_except0", flatlist(args)) @@ -194,23 +190,20 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - vals = [a.value() for a in self.args if a.value() != 0] - if any([np.isnan(x) for x in vals]): - return False - else: + try: + vals = [a.value() for a in self.args if a.value() != 0] return len(set(vals)) == len(vals) - + except IncompleteFunctionError: + return False def allequal(args): - warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", - DeprecationWarning) - return AllEqual(*args) # unfold list as individual arguments + warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) + return AllEqual(*args) # unfold list as individual arguments class AllEqual(GlobalConstraint): """All arguments have the same value """ - def __init__(self, *args): super().__init__("allequal", flatlist(args)) @@ -221,22 +214,20 @@ def decompose(self): return [var1 == var2 for var1, var2 in zip(self.args[:-1], self.args[1:])], [] def value(self): - values = argvals(self.args) - if any([np.isnan(x) for x in values]): + try: + values = [argval(a) for a in self.args] + return len(set(values)) == 1 + except IncompleteFunctionError: return False - return len(set(values)) == 1 - def circuit(args): - warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", - DeprecationWarning) - return Circuit(*args) # unfold list as individual arguments + warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) + return Circuit(*args) # unfold list as individual arguments class Circuit(GlobalConstraint): """The sequence of variables form a circuit, where x[i] = j means that j is the successor of i. """ - def __init__(self, *args): flatargs = flatlist(args) if any(is_boolexpr(arg) for arg in flatargs): @@ -255,15 +246,14 @@ def decompose(self): """ succ = cpm_array(self.args) n = len(succ) - order = intvar(0, n - 1, shape=n) + order = intvar(0,n-1, shape=n) constraining = [] - constraining += [AllDifferent(succ)] # different successors - constraining += [AllDifferent(order)] # different orders - constraining += [order[n - 1] == 0] # symmetry breaking, last one is '0' + constraining += [AllDifferent(succ)] # different successors + constraining += [AllDifferent(order)] # different orders + constraining += [order[n-1] == 0] # symmetry breaking, last one is '0' defining = [order[0] == succ[0]] - defining += [order[i] == succ[order[i - 1]] for i in - range(1, n)] # first one is successor of '0', ith one is successor of i-1 + defining += [order[i] == succ[order[i-1]] for i in range(1,n)] # first one is successor of '0', ith one is successor of i-1 return constraining, defining @@ -271,7 +261,11 @@ def value(self): pathlen = 0 idx = 0 visited = set() - arr = argvals(self.args) + try: + arr = [argval(a) for a in self.args] + except IncompleteFunctionError: + return False + while idx not in visited: if idx is None: return False @@ -280,6 +274,7 @@ def value(self): visited.add(idx) pathlen += 1 idx = arr[idx] + return pathlen == len(self.args) and idx == 0 @@ -291,9 +286,8 @@ class Inverse(GlobalConstraint): fwd[i] == x <==> rev[x] == i """ - def __init__(self, fwd, rev): - flatargs = flatlist([fwd, rev]) + flatargs = flatlist([fwd,rev]) if any(is_boolexpr(arg) for arg in flatargs): raise TypeError("Only integer arguments allowed for global constraint Inverse: {}".format(flatargs)) assert len(fwd) == len(rev) @@ -306,19 +300,21 @@ def decompose(self): return [all(rev[x] == i for i, x in enumerate(fwd))], [] def value(self): - fwd = argvals(self.args[0]) - rev = argvals(self.args[1]) + try: + fwd = [argval(a) for a in self.args[0]] + rev = [argval(a) for a in self.args[1]] + except IncompleteFunctionError: + return False # args are fine, now evaluate actual inverse cons try: return all(rev[x] == i for i, x in enumerate(fwd)) - except IndexError: # if index is out of range then it's definitely not Inverse. - return False + except IndexError: # partiality of Element constraint + raise IncompleteFunctionError class Table(GlobalConstraint): """The values of the variables in 'array' correspond to a row in 'table' """ - def __init__(self, array, table): array = flatlist(array) if not all(isinstance(x, Expression) for x in array): @@ -332,8 +328,12 @@ def decompose(self): def value(self): arr, tab = self.args - arrval = [argval(a) for a in arr if not np.isnan(argval(a))] - return arrval in tab + try: + arrval = [argval(a) for a in arr] + return arrval in tab + except IncompleteFunctionError: + return False + # syntax of the form 'if b then x == 9 else x == 0' is not supported (no override possible) @@ -347,10 +347,13 @@ def __init__(self, condition, if_true, if_false): def value(self): condition, if_true, if_false = self.args - if is_true_cst((argval(condition))): - return argval(if_true) - else: - return argval(if_false) + try: + if argval(condition): + return argval(if_true) + else: + return argval(if_false) + except IncompleteFunctionError: + return False def decompose(self): condition, if_true, if_false = self.args @@ -361,14 +364,15 @@ def __repr__(self): return "If {} Then {} Else {}".format(condition, if_true, if_false) + class InDomain(GlobalConstraint): """ The "InDomain" constraint, defining non-interval domains for an expression """ def __init__(self, expr, arr): - # assert not (is_boolexpr(expr) or any(is_boolexpr(a) for a in arr)), \ - # "The expressions in the InDomain constraint should not be boolean" + assert not (is_boolexpr(expr) or any(is_boolexpr(a) for a in arr)), \ + "The expressions in the InDomain constraint should not be boolean" super().__init__("InDomain", [expr, arr]) def decompose(self): @@ -383,8 +387,8 @@ def decompose(self): lb, ub = expr.get_bounds() defining = [] - # if expr is not a var - if not isinstance(expr, _IntVarImpl): + #if expr is not a var + if not isinstance(expr,_IntVarImpl): aux = intvar(lb, ub) defining.append(aux == expr) expr = aux @@ -395,9 +399,12 @@ def decompose(self): else: return [expr != val for val in range(lb, ub + 1) if val not in arr], defining + def value(self): - val = argval(self.args[0]) - return val in argval(self.args[1]) and not np.isnan(val) + try: + return argval(self.args[0]) in argval(self.args[1]) + except IncompleteFunctionError: + return False def __repr__(self): return "{} in {}".format(self.args[0], self.args[1]) @@ -423,11 +430,14 @@ def decompose(self): # there are multiple decompositions possible, Recursively using sum allows it to be efficient for all solvers. decomp = [sum(self.args[:2]) == 1] if len(self.args) > 2: - decomp = Xor([decomp, self.args[2:]]).decompose()[0] + decomp = Xor([decomp,self.args[2:]]).decompose()[0] return decomp, [] def value(self): - return sum(argvals(self.args)) % 2 == 1 + try: + return sum(argval(a) for a in self.args) % 2 == 1 + except IncompleteFunctionError: + return False def __repr__(self): if len(self.args) == 2: @@ -441,7 +451,6 @@ class Cumulative(GlobalConstraint): Ensures no overlap between tasks and never exceeding the capacity of the resource Supports both varying demand across tasks or equal demand for all jobs """ - def __init__(self, start, duration, end, demand, capacity): assert is_any_list(start), "start should be a list" assert is_any_list(duration), "duration should be a list" @@ -460,7 +469,7 @@ def __init__(self, start, duration, end, demand, capacity): if is_any_list(demand): demand = flatlist(demand) assert len(demand) == n_jobs, "Demand should be supplied for each task or be single constant" - else: # constant demand + else: # constant demand demand = [demand] * n_jobs super(Cumulative, self).__init__("cumulative", [start, duration, end, demand, capacity]) @@ -484,7 +493,7 @@ def decompose(self): # demand doesn't exceed capacity lb, ub = min(s.lb for s in start), max(s.ub for s in end) - for t in range(lb, ub + 1): + for t in range(lb,ub+1): demand_at_t = 0 for job in range(len(start)): if is_num(demand): @@ -497,21 +506,24 @@ def decompose(self): return cons, [] def value(self): - vals = [np.array(argvals(arg)) if is_any_list(arg) - else argval(arg) for arg in self.args] + try: + argvals = [np.array([argval(a) for a in arg]) if is_any_list(arg) + else argval(arg) for arg in self.args] + except IncompleteFunctionError: + return False - if any(a is None for a in vals): + if any(a is None for a in argvals): return None # start, dur, end are np arrays - start, dur, end, demand, capacity = vals + start, dur, end, demand, capacity = argvals # start and end seperated by duration if not (start + dur == end).all(): return False # demand doesn't exceed capacity lb, ub = min(start), max(end) - for t in range(lb, ub + 1): + for t in range(lb, ub+1): if capacity < sum(demand * ((start <= t) & (t < end))): return False @@ -528,7 +540,7 @@ def __init__(self, vars, vals, occ): flatargs = flatlist([vars, vals, occ]) if any(is_boolexpr(arg) for arg in flatargs): raise TypeError("Only numerical arguments allowed for gcc global constraint: {}".format(flatargs)) - super().__init__("gcc", [vars, vals, occ]) + super().__init__("gcc", [vars,vals,occ]) def decompose(self): from .globalfunctions import Count @@ -554,7 +566,6 @@ class DirectConstraint(Expression): If you want/need to use what the solver returns (e.g. an identifier for use in other constraints), then use `directvar()` instead, or access the solver object from the solver interface directly. """ - def __init__(self, name, arguments, novar=None): """ name: name of the solver function that you wish to call @@ -592,3 +603,4 @@ def callSolver(self, CPMpy_solver, Native_solver): solver_args[i] = CPMpy_solver.solver_vars(solver_args[i]) # len(native_args) should match nr of arguments of `native_function` return solver_function(*solver_args) + diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index ff4656c21..8c1eeecca 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -64,10 +64,10 @@ def decompose_comparison(self): import copy import warnings # for deprecation warning import numpy as np -from ..exceptions import CPMpyException, TypeError +from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl -from .utils import flatlist, argval, argvals, eval_comparison, is_any_list, is_boolexpr, get_bounds +from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds class GlobalFunction(Expression): @@ -116,12 +116,11 @@ def __init__(self, arg_list): super().__init__("min", flatlist(arg_list)) def value(self): - vals = argvals(self.args) - if any(val is None for val in vals): + argvals = [argval(a) for a in self.args] + if any(val is None for val in argvals): return None else: - return min(vals) # will always return nan if any argument is nan. - # This is in line with how solvers handle undefinedness in Min and Max. + return min(argvals) def decompose_comparison(self, cpm_op, cpm_rhs): """ @@ -158,11 +157,11 @@ def __init__(self, arg_list): super().__init__("max", flatlist(arg_list)) def value(self): - vals = argvals(self.args) - if any(val is None for val in vals): + argvals = [argval(a) for a in self.args] + if any(val is None for val in argvals): return None else: - return max(vals) + return max(argvals) def decompose_comparison(self, cpm_op, cpm_rhs): """ @@ -258,8 +257,8 @@ def value(self): if idxval is not None: if idxval >= 0 and idxval < len(arr): return argval(arr[idxval]) - return np.nan - return None # default + raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}") + return None # default def decompose_comparison(self, cpm_op, cpm_rhs): """ @@ -272,6 +271,8 @@ def decompose_comparison(self, cpm_op, cpm_rhs): they should be enforced toplevel. """ + from .python_builtins import any + 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)], [] @@ -355,7 +356,7 @@ def decompose_comparison(self, cmp_op, cpm_rhs): return [eval_comparison(cmp_op, sum(bvars), cpm_rhs)], constraints def value(self): - return len(set(argval(a) for a in self.args if not np.isnan(argval(a)))) + return len(set(argval(a) for a in self.args)) def get_bounds(self): """ diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 88442d290..a42e88c82 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -118,13 +118,14 @@ def all_pairs(args): def argval(a): """ returns .value() of Expression, otherwise the variable itself + We check with hasattr instead of isinstance to avoid circular dependency """ - return a.value() if hasattr(a, "value") else a - - -def argvals(arr): - return [argval(a) for a in arr] + try: + return a.value() if hasattr(a, "value") else a + except IncompleteFunctionError as e: + if a.is_bool(): return False + raise e def eval_comparison(str_op, lhs, rhs): From 3a84ded40b295c8bfb34f8f6425c19990f001b26 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 10 May 2024 14:54:18 +0200 Subject: [PATCH 28/48] hack: ensure all variables have a value --- cpmpy/solvers/pysdd.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index fecfc7ae5..0c5af83fe 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -121,7 +121,8 @@ def solve(self, time_limit=None, assumptions=None): if lit in sol: cpm_var._value = bool(sol[lit]) else: - cpm_var._value = None # not specified... + cpm_var._value = cpm_var.get_bounds()[0] # dummy value - TODO: ensure Pysdd assigns an actual value + # cpm_var._value = None # not specified... return has_sol From 828d2cd304052e3e8501e36331374af8c43cca0c Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 10 May 2024 14:54:38 +0200 Subject: [PATCH 29/48] update tests to exclude inverse --- tests/test_constraints.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 2bed73ee7..4cb264d52 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -24,9 +24,12 @@ # Solvers not supporting arithmetic constraints SAT_SOLVERS = {"pysat", "pysdd"} -EXCLUDE_GLOBAL = {"minizinc": {"circuit"}, - "pysat": NUM_GLOBAL, +EXCLUDE_GLOBAL = {"pysat": NUM_GLOBAL, "pysdd": NUM_GLOBAL | {"Xor"}, + "z3": {"Inverse"}, + "choco": {"Inverse"}, + "ortools":{"Inverse"}, + "exact": {"Inverse"}, } # Exclude certain operators for solvers. @@ -173,7 +176,7 @@ def global_constraints(solver): if name == "Xor": expr = cls(BOOL_ARGS) elif name == "Inverse": - expr = cls(NUM_ARGS, [1,2,0]) + expr = cls(NUM_ARGS, [1,0,2]) elif name == "Table": expr = cls(NUM_ARGS, [[0,1,2],[1,2,0],[1,0,2]]) elif name == "IfThenElse": From 47fd9c55f87b81a61e720a6919f0f2800bdb0a8b Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 10 May 2024 14:57:54 +0200 Subject: [PATCH 30/48] add increasing and decreasing to numerical globals in testsuite --- tests/test_constraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 4cb264d52..e1b002428 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -16,7 +16,7 @@ # Exclude some global constraints for solvers NUM_GLOBAL = { - "AllEqual", "AllDifferent", "AllDifferentExcept0", "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", + "AllEqual", "AllDifferent", "AllDifferentExcept0", "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", "Increasing", "Decreasing" # also global functions "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", } From d461be87a82d34e91469d5891663963c7b7745dd Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 10 May 2024 15:44:09 +0200 Subject: [PATCH 31/48] add new global constraints as numeric --- tests/test_constraints.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index e1b002428..58c1c0d67 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -16,7 +16,8 @@ # Exclude some global constraints for solvers NUM_GLOBAL = { - "AllEqual", "AllDifferent", "AllDifferentExcept0", "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", "Increasing", "Decreasing" + "AllEqual", "AllDifferent", "AllDifferentExcept0", "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", + "Increasing", "IncreasingStrict", "Decreasing", "DecreasingStrict", # also global functions "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", } From fc8f5f0bff1b37f56c56a4348ecd6177f53bb9c1 Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 10 May 2024 15:51:48 +0200 Subject: [PATCH 32/48] fix test, we have relational semantics in value computation now --- tests/test_expressions.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_expressions.py b/tests/test_expressions.py index 8921aa5ea..b01cc1e23 100644 --- a/tests/test_expressions.py +++ b/tests/test_expressions.py @@ -436,7 +436,7 @@ def test_incomplete_func(self): m = cp.Model([p.implies(cons), a == b]) if cp.SolverLookup.lookup("z3").supported(): self.assertTrue(m.solve(solver="z3")) # ortools does not support divisor spanning 0 work here - self.assertRaises(IncompleteFunctionError, cons.value) + self.assertFalse(cons.value()) # mayhem cons = (arr[10 // (a - b)] == 1).implies(p) From 464e5550f7926bf3e4a2035dc5cc9cf86373037a Mon Sep 17 00:00:00 2001 From: wout4 Date: Fri, 10 May 2024 16:46:22 +0200 Subject: [PATCH 33/48] indexerror -> false --- cpmpy/expressions/globalconstraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 12d2458d6..4b73c568e 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -316,7 +316,7 @@ def value(self): try: return all(rev[x] == i for i, x in enumerate(fwd)) except IndexError: # partiality of Element constraint - raise IncompleteFunctionError + return False class Table(GlobalConstraint): From 970bbb0963b607508a5da20de8a57977d1a0c3c0 Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 17:50:55 +0200 Subject: [PATCH 34/48] Safe_value() on expressions, automatically handle incompletefunction errors in argval() functions --- cpmpy/expressions/core.py | 9 ++++ cpmpy/expressions/globalconstraints.py | 70 ++++++++------------------ cpmpy/expressions/utils.py | 10 ++-- cpmpy/solvers/choco.py | 6 +-- cpmpy/solvers/exact.py | 6 +-- cpmpy/solvers/gurobi.py | 5 +- cpmpy/solvers/minizinc.py | 6 +-- cpmpy/solvers/ortools.py | 6 +-- cpmpy/solvers/pysdd.py | 6 +-- 9 files changed, 52 insertions(+), 72 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index 12b3fbeb7..0223e455d 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -144,6 +144,15 @@ def is_bool(self): def value(self): return None # default + def safe_value(self): + try: + return self.value() + except IncompleteFunctionError as e: + if self.is_bool(): + return False + else: + raise e + def get_bounds(self): if self.is_bool(): return 0, 1 #default for boolean expressions diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 4b73c568e..64b030f9a 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -120,7 +120,7 @@ def my_circuit_decomp(self): from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl, _IntVarImpl -from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds +from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, argvals from .globalfunctions import * # XXX make this file backwards compatible @@ -178,11 +178,8 @@ def decompose(self): return [var1 != var2 for var1, var2 in all_pairs(self.args)], [] def value(self): - try: - values = [argval(a) for a in self.args] - return len(set(values)) == len(self.args) - except IncompleteFunctionError: - return False + values = argvals(self.args) + return len(set(values)) == len(self.args) class AllDifferentExcept0(GlobalConstraint): @@ -197,11 +194,8 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - try: - vals = [a.value() for a in self.args if a.value() != 0] - return len(set(vals)) == len(vals) - except IncompleteFunctionError: - return False + vals = [argval(a) for a in self.args if argval(a) != 0] + return len(set(vals)) == len(vals) def allequal(args): warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -221,11 +215,8 @@ def decompose(self): return [var1 == var2 for var1, var2 in zip(self.args[:-1], self.args[1:])], [] def value(self): - try: - values = [argval(a) for a in self.args] - return len(set(values)) == 1 - except IncompleteFunctionError: - return False + values = argvals(self.args) + return len(set(values)) == 1 def circuit(args): warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -268,10 +259,7 @@ def value(self): pathlen = 0 idx = 0 visited = set() - try: - arr = [argval(a) for a in self.args] - except IncompleteFunctionError: - return False + arr = argvals(self.args) while idx not in visited: if idx is None: @@ -307,11 +295,8 @@ def decompose(self): return [all(rev[x] == i for i, x in enumerate(fwd))], [] def value(self): - try: - fwd = [argval(a) for a in self.args[0]] - rev = [argval(a) for a in self.args[1]] - except IncompleteFunctionError: - return False + fwd = argvals(self.args[0]) + rev = argvals(self.args[1]) # args are fine, now evaluate actual inverse cons try: return all(rev[x] == i for i, x in enumerate(fwd)) @@ -335,11 +320,8 @@ def decompose(self): def value(self): arr, tab = self.args - try: - arrval = [argval(a) for a in arr] - return arrval in tab - except IncompleteFunctionError: - return False + arrval = argvals(arr) + return arrval in tab @@ -354,13 +336,10 @@ def __init__(self, condition, if_true, if_false): def value(self): condition, if_true, if_false = self.args - try: - if argval(condition): - return argval(if_true) - else: - return argval(if_false) - except IncompleteFunctionError: - return False + if argval(condition): + return argval(if_true) + else: + return argval(if_false) def decompose(self): condition, if_true, if_false = self.args @@ -406,10 +385,7 @@ def decompose(self): def value(self): - try: - return argval(self.args[0]) in argval(self.args[1]) - except IncompleteFunctionError: - return False + return argval(self.args[0]) in argvals(self.args[1]) def __repr__(self): return "{} in {}".format(self.args[0], self.args[1]) @@ -439,10 +415,7 @@ def decompose(self): return decomp, [] def value(self): - try: - return sum(argval(a) for a in self.args) % 2 == 1 - except IncompleteFunctionError: - return False + return sum(argvals(self.args)) % 2 == 1 def __repr__(self): if len(self.args) == 2: @@ -511,11 +484,8 @@ def decompose(self): return cons, [] def value(self): - try: - argvals = [np.array([argval(a) for a in arg]) if is_any_list(arg) - else argval(arg) for arg in self.args] - except IncompleteFunctionError: - return False + argvals = [np.array(argvals(arg)) if is_any_list(arg) + else argval(arg) for arg in self.args] if any(a is None for a in argvals): return None diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index a42e88c82..3cd3c63b3 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -121,11 +121,11 @@ def argval(a): We check with hasattr instead of isinstance to avoid circular dependency """ - try: - return a.value() if hasattr(a, "value") else a - except IncompleteFunctionError as e: - if a.is_bool(): return False - raise e + return a.safe_value() if hasattr(a, "safe_value") else a + + +def argvals(arr): + return [argval(a) for a in arr] def eval_comparison(str_op, lhs, rhs): diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index f17f0b375..a86b2751c 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -29,7 +29,7 @@ from ..expressions.globalconstraints import DirectConstraint from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar from ..expressions.globalconstraints import GlobalConstraint -from ..expressions.utils import is_num, is_int, is_boolexpr, is_any_list, get_bounds +from ..expressions.utils import is_num, is_int, is_boolexpr, is_any_list, get_bounds, argval, argvals from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, flatten_objective @@ -208,9 +208,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from cpm_var._value = value # print the desired display if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 2d1c37ffd..5f0598cfb 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -37,7 +37,7 @@ from ..transformations.normalize import toplevel_list from ..expressions.globalconstraints import DirectConstraint from ..exceptions import NotSupportedError -from ..expressions.utils import flatlist +from ..expressions.utils import flatlist, argvals import numpy as np import numbers @@ -263,9 +263,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from if display is not None: self._fillObjAndVars() if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback elif my_status == 2: # found inconsistency diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 0b6f6e9d8..2463383f2 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -28,6 +28,7 @@ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..expressions.core import * +from ..expressions.utils import argvals from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar from ..expressions.globalconstraints import DirectConstraint from ..transformations.comparison import only_numexpr_equality @@ -461,9 +462,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from if display is not None: if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 55c2d59f2..812cde975 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -36,7 +36,7 @@ from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar from ..expressions.globalconstraints import DirectConstraint -from ..expressions.utils import is_num, is_any_list, eval_comparison +from ..expressions.utils import is_num, is_any_list, eval_comparison, argvals, argval from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..exceptions import MinizincPathException, NotSupportedError @@ -323,9 +323,9 @@ async def _solveAll(self, display=None, time_limit=None, solution_limit=None, ** # and the actual displaying if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index 175440770..c70dcbe8f 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -32,7 +32,7 @@ from ..expressions.globalconstraints import DirectConstraint from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, boolvar from ..expressions.globalconstraints import GlobalConstraint -from ..expressions.utils import is_num, is_any_list, eval_comparison, flatlist +from ..expressions.utils import is_num, is_any_list, eval_comparison, flatlist, argval, argvals from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, flatten_objective @@ -689,10 +689,10 @@ def on_solution_callback(self): cpm_var._value = self.Value(self._varmap[cpm_var]) if isinstance(self._display, Expression): - print(self._display.value()) + print(argval(self._display)) elif isinstance(self._display, list): # explicit list of expressions to display - print([v.value() for v in self._display]) + print(argvals(self._display)) else: # callable self._display() diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index fddae5911..a00800121 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -26,7 +26,7 @@ from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.variables import _BoolVarImpl, NegBoolView, boolvar from ..expressions.globalconstraints import DirectConstraint -from ..expressions.utils import is_any_list, is_bool +from ..expressions.utils import is_any_list, is_bool, argval, argvals from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.normalize import toplevel_list, simplify_boolean @@ -178,9 +178,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from # display is not None: if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback return solution_count From c013ee80dad1bb3c8f5651ca58884c65cd754db6 Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 17:55:11 +0200 Subject: [PATCH 35/48] use helper function argvals() --- cpmpy/expressions/core.py | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index 0223e455d..b93173b5c 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -72,7 +72,7 @@ import numpy as np -from .utils import is_num, is_any_list, flatlist, argval, get_bounds, is_boolexpr, is_true_cst, is_false_cst +from .utils import is_num, is_any_list, flatlist, argval, get_bounds, is_boolexpr, is_true_cst, is_false_cst, argvals from ..exceptions import IncompleteFunctionError, TypeError @@ -409,10 +409,7 @@ def __repr__(self): # return the value of the expression # optional, default: None def value(self): - try: - arg_vals = [argval(a) for a in self.args] - except IncompleteFunctionError: - return False + arg_vals = argvals(self.args) if any(a is None for a in arg_vals): return None if self.name == "==": return arg_vals[0] == arg_vals[1] @@ -542,13 +539,9 @@ def value(self): if self.name == "wsum": # wsum: arg0 is list of constants, no .value() use as is - arg_vals = [self.args[0], [argval(arg) for arg in self.args[1]]] + arg_vals = [self.args[0], argvals(self.args[1])] else: - try: - arg_vals = [argval(arg) for arg in self.args] - except IncompleteFunctionError as e: - if self.is_bool(): return False - raise e + arg_vals = argvals(self.args) if any(a is None for a in arg_vals): return None From 8d7a165a2a97deb579872a44abb9b1f17757ac26 Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 17:58:45 +0200 Subject: [PATCH 36/48] uncomment gurobi supported function --- cpmpy/solvers/gurobi.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 2463383f2..dbe3618bf 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -84,9 +84,9 @@ def __init__(self, cpm_model=None, subsolver=None): Arguments: - cpm_model: a CPMpy Model() """ - # if not self.supported(): - # raise Exception( - # "CPM_gurobi: Install the python package 'gurobipy' and make sure your licence is activated!") + if not self.supported(): + raise Exception( + "CPM_gurobi: Install the python package 'gurobipy' and make sure your licence is activated!") import gurobipy as gp # TODO: subsolver could be a GRB_ENV if a user would want to hand one over From 01c53f50faa6a294f5477e0f33d21c12cdbc01ff Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 18:01:58 +0200 Subject: [PATCH 37/48] fix test, .value() raises but argval() does not --- tests/test_expressions.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/test_expressions.py b/tests/test_expressions.py index b01cc1e23..7ff22e88e 100644 --- a/tests/test_expressions.py +++ b/tests/test_expressions.py @@ -6,7 +6,7 @@ from cpmpy.expressions import * from cpmpy.expressions.variables import NDVarArray from cpmpy.expressions.core import Operator, Expression -from cpmpy.expressions.utils import get_bounds +from cpmpy.expressions.utils import get_bounds, argval class TestComparison(unittest.TestCase): def test_comps(self): @@ -436,7 +436,8 @@ def test_incomplete_func(self): m = cp.Model([p.implies(cons), a == b]) if cp.SolverLookup.lookup("z3").supported(): self.assertTrue(m.solve(solver="z3")) # ortools does not support divisor spanning 0 work here - self.assertFalse(cons.value()) + self.assertRaises(IncompleteFunctionError, cons.value) + self.assertFalse(argval(cons)) # mayhem cons = (arr[10 // (a - b)] == 1).implies(p) From 6870a91384a5803dc59dd54867b32b26cb326123 Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 18:03:37 +0200 Subject: [PATCH 38/48] remove unnecessary aux vars in value calculation --- cpmpy/expressions/globalconstraints.py | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 64b030f9a..d6748c931 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -178,8 +178,7 @@ def decompose(self): return [var1 != var2 for var1, var2 in all_pairs(self.args)], [] def value(self): - values = argvals(self.args) - return len(set(values)) == len(self.args) + return len(set(argvals(self.args))) == len(self.args) class AllDifferentExcept0(GlobalConstraint): @@ -194,8 +193,7 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - vals = [argval(a) for a in self.args if argval(a) != 0] - return len(set(vals)) == len(vals) + return len(set([argval(a) for a in self.args if argval(a) != 0])) == len(vals) def allequal(args): warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -215,8 +213,7 @@ def decompose(self): return [var1 == var2 for var1, var2 in zip(self.args[:-1], self.args[1:])], [] def value(self): - values = argvals(self.args) - return len(set(values)) == 1 + return len(set(argvals(self.args))) == 1 def circuit(args): warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) From 3fee8d0861f4e3a7d910247d7f8ff08001f7f8dc Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 18:43:32 +0200 Subject: [PATCH 39/48] use argval in tests --- cpmpy/expressions/globalconstraints.py | 9 +++++---- tests/test_constraints.py | 9 +++++---- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index d6748c931..59cae7556 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -193,7 +193,8 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - return len(set([argval(a) for a in self.args if argval(a) != 0])) == len(vals) + vals = [argval(a) for a in self.args if argval(a) != 0] + return len(set(vals)) == len(vals) def allequal(args): warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -481,14 +482,14 @@ def decompose(self): return cons, [] def value(self): - argvals = [np.array(argvals(arg)) if is_any_list(arg) + arg_vals = [np.array(argvals(arg)) if is_any_list(arg) else argval(arg) for arg in self.args] - if any(a is None for a in argvals): + if any(a is None for a in arg_vals): return None # start, dur, end are np arrays - start, dur, end, demand, capacity = argvals + start, dur, end, demand, capacity = arg_vals # start and end seperated by duration if not (start + dur == end).all(): return False diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 58c1c0d67..9579b4dc1 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -11,6 +11,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'] ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint @@ -222,7 +223,7 @@ def reify_imply_exprs(solver): def verify(cons): - assert cons.value() + assert argval(cons) @pytest.mark.parametrize(("solver","constraint"),_generate_inputs(bool_exprs), ids=str) @@ -235,7 +236,7 @@ def test_bool_constaints(solver, constraint): assert n_sols >= 1 else: assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + assert argval(constraint) @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) @@ -248,7 +249,7 @@ def test_comparison_constraints(solver, constraint): assert n_sols >= 1 else: assert SolverLookup.get(solver,Model(constraint)).solve() - assert constraint.value() + assert argval(constraint) @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) @@ -261,4 +262,4 @@ def test_reify_imply_constraints(solver, constraint): assert n_sols >= 1 else: assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + assert argval(constraint) From db8efd768e6898e022c54d787d4df86945e002a7 Mon Sep 17 00:00:00 2001 From: wout4 Date: Mon, 13 May 2024 18:45:54 +0200 Subject: [PATCH 40/48] use argval in tests --- tests/test_constraints.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 9579b4dc1..39fda893c 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -11,7 +11,6 @@ # 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'] ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint From 429daf9ca754fa3ccf587521165eedf4bfa1cf18 Mon Sep 17 00:00:00 2001 From: wout4 Date: Tue, 14 May 2024 22:37:20 +0200 Subject: [PATCH 41/48] use argval and .value() in test constraints --- tests/test_constraints.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 39fda893c..7e47de2c6 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -223,6 +223,7 @@ def reify_imply_exprs(solver): def verify(cons): assert argval(cons) + assert cons.value() @pytest.mark.parametrize(("solver","constraint"),_generate_inputs(bool_exprs), ids=str) @@ -236,6 +237,7 @@ def test_bool_constaints(solver, constraint): else: assert SolverLookup.get(solver, Model(constraint)).solve() assert argval(constraint) + assert constraint.value() @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) @@ -249,6 +251,7 @@ def test_comparison_constraints(solver, constraint): else: assert SolverLookup.get(solver,Model(constraint)).solve() assert argval(constraint) + assert constraint.value() @pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) @@ -262,3 +265,4 @@ def test_reify_imply_constraints(solver, constraint): else: assert SolverLookup.get(solver, Model(constraint)).solve() assert argval(constraint) + assert constraint.value() From 2b049673be477929747e973911ff5895b7570818 Mon Sep 17 00:00:00 2001 From: wout4 Date: Tue, 14 May 2024 23:34:20 +0200 Subject: [PATCH 42/48] reference .safe_value when incompletefunctionerror is thrown. --- cpmpy/expressions/core.py | 3 ++- cpmpy/expressions/globalfunctions.py | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index b93173b5c..71fd68175 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -557,7 +557,8 @@ def value(self): try: return arg_vals[0] // arg_vals[1] except ZeroDivisionError: - raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}") + raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}" + + "\n Use .safe_value() if you want to use relational semantics.") # boolean elif self.name == "and": return all(arg_vals) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 8c1eeecca..752c836ec 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -257,7 +257,8 @@ def value(self): if idxval is not None: if idxval >= 0 and idxval < len(arr): return argval(arr[idxval]) - raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}") + raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}" + + "\n Use .safe_value() if you want to use relational semantics.") return None # default def decompose_comparison(self, cpm_op, cpm_rhs): From 72cbc496ae2d209a8132f726ad5929a87acf599d Mon Sep 17 00:00:00 2001 From: wout4 Date: Wed, 15 May 2024 23:09:36 +0200 Subject: [PATCH 43/48] remove safe_value, only need argval --- cpmpy/expressions/core.py | 10 +--------- cpmpy/expressions/globalfunctions.py | 2 +- cpmpy/expressions/utils.py | 10 +++++++++- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index 71fd68175..b2a01ba62 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -144,14 +144,6 @@ def is_bool(self): def value(self): return None # default - def safe_value(self): - try: - return self.value() - except IncompleteFunctionError as e: - if self.is_bool(): - return False - else: - raise e def get_bounds(self): if self.is_bool(): @@ -558,7 +550,7 @@ def value(self): return arg_vals[0] // arg_vals[1] except ZeroDivisionError: raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}" - + "\n Use .safe_value() if you want to use relational semantics.") + + "\n Use argval(expr) to get the value of expr with relational semantics.") # boolean elif self.name == "and": return all(arg_vals) diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 752c836ec..0479b0ad9 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -258,7 +258,7 @@ def value(self): if idxval >= 0 and idxval < len(arr): return argval(arr[idxval]) raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}" - + "\n Use .safe_value() if you want to use relational semantics.") + + "\n Use argval(expr) to get the value of expr with relational semantics.") return None # default def decompose_comparison(self, cpm_op, cpm_rhs): diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 3cd3c63b3..e5a78ed95 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -121,7 +121,15 @@ def argval(a): We check with hasattr instead of isinstance to avoid circular dependency """ - return a.safe_value() if hasattr(a, "safe_value") else a + if hasattr(a, "value"): + try: + return a.value() + except IncompleteFunctionError as e: + if a.is_bool(): + return False + else: + raise e + return a def argvals(arr): From 4dc7e503ebf7db8560278f82b8e44111eb671a45 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Fri, 17 May 2024 15:07:00 +0200 Subject: [PATCH 44/48] nvalueexcept constructor fixed in test_constraints --- tests/test_constraints.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 0788ac7d8..59d490d23 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -11,7 +11,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"] ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint # Exclude some global constraints for solvers @@ -93,12 +93,15 @@ def numexprs(solver): classes = [(name, cls) for name, cls in classes if name not in EXCLUDE_GLOBAL.get(solver, {})] for name, cls in classes: + print(name, cls) if name == "Abs": expr = cls(NUM_ARGS[0]) elif name == "Count": expr = cls(NUM_ARGS, NUM_VAR) elif name == "Element": expr = cls(NUM_ARGS, POS_VAR) + elif name == "NValueExcept": + expr = cls(NUM_ARGS, 3) else: expr = cls(NUM_ARGS) From e5debe434422e626beaf06076dfdc8aaddfaee16 Mon Sep 17 00:00:00 2001 From: wout4 Date: Fri, 17 May 2024 15:54:45 +0200 Subject: [PATCH 45/48] test all solvers in test_constraints --- tests/test_constraints.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 59d490d23..7e087d689 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -11,7 +11,6 @@ # 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"] ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint # Exclude some global constraints for solvers From 32c85355a83234138444354ce1360b7e705c7d87 Mon Sep 17 00:00:00 2001 From: wout4 Date: Fri, 17 May 2024 15:55:43 +0200 Subject: [PATCH 46/48] remove print --- tests/test_constraints.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 7e087d689..bba822782 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -92,7 +92,6 @@ def numexprs(solver): classes = [(name, cls) for name, cls in classes if name not in EXCLUDE_GLOBAL.get(solver, {})] for name, cls in classes: - print(name, cls) if name == "Abs": expr = cls(NUM_ARGS[0]) elif name == "Count": From d34a971ab388a6806e327f2da5d16be5965bc6f3 Mon Sep 17 00:00:00 2001 From: wout4 Date: Fri, 17 May 2024 16:25:23 +0200 Subject: [PATCH 47/48] add nvalueexcept to num_globals in test constraints --- tests/test_constraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index bba822782..c14fde9a0 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -19,7 +19,7 @@ "AllEqual", "AllDifferent", "AllDifferentExcept0", "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", "Table", "Circuit", "Increasing", "IncreasingStrict", "Decreasing", "DecreasingStrict", # also global functions - "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", + "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", "NValueExcept" } # Solvers not supporting arithmetic constraints From 3376000cc1809457446effccfaceda40e67e3953 Mon Sep 17 00:00:00 2001 From: Ignace Bleukx Date: Tue, 21 May 2024 11:07:36 +0200 Subject: [PATCH 48/48] exclude strictly_increasing from mzn tests --- tests/test_constraints.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/test_constraints.py b/tests/test_constraints.py index c14fde9a0..b777ce4e7 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -31,6 +31,7 @@ "choco": {"Inverse"}, "ortools":{"Inverse"}, "exact": {"Inverse"}, + "minizinc": {"IncreasingStrict"} # bug #813 reported on libminizinc } # Exclude certain operators for solvers. @@ -228,7 +229,7 @@ def verify(cons): assert cons.value() -@pytest.mark.parametrize(("solver","constraint"),_generate_inputs(bool_exprs), ids=str) +@pytest.mark.parametrize(("solver","constraint"),list(_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. @@ -242,7 +243,7 @@ def test_bool_constaints(solver, constraint): assert constraint.value() -@pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) +@pytest.mark.parametrize(("solver","constraint"), list(_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. @@ -256,7 +257,7 @@ def test_comparison_constraints(solver, constraint): assert constraint.value() -@pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) +@pytest.mark.parametrize(("solver","constraint"), list(_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.