diff --git a/cpmpy/solvers/TEMPLATE.py b/cpmpy/solvers/TEMPLATE.py index 4656aa300..7fa658300 100644 --- a/cpmpy/solvers/TEMPLATE.py +++ b/cpmpy/solvers/TEMPLATE.py @@ -174,7 +174,7 @@ def native_model(self): """ return self.TPL_model - def solve(self, time_limit=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, **kwargs): """ Call the TEMPLATE solver @@ -469,7 +469,7 @@ def add(self, cpm_expr_orig): # Other functions from SolverInterface that you can overwrite: # solveAll, solution_hint, get_core - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ A shorthand to (efficiently) compute all (optimal) solutions, map them to CPMpy and optionally display the solutions. diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index 854cb12b6..37fbfe206 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -152,7 +152,7 @@ def native_model(self): """ return self.chc_model - def solve(self, time_limit=None, **kwargs): + def solve(self, time_limit: Optional[float]=None, **kwargs): """ Call the Choco solver @@ -230,7 +230,7 @@ def solve(self, time_limit=None, **kwargs): return has_sol - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all (optimal) solutions, map them to CPMpy and optionally display the solutions. diff --git a/cpmpy/solvers/cplex.py b/cpmpy/solvers/cplex.py index ddda58dea..60229ac1d 100644 --- a/cpmpy/solvers/cplex.py +++ b/cpmpy/solvers/cplex.py @@ -51,7 +51,7 @@ ============== """ import warnings -from typing import Optional +from typing import Optional, List from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError @@ -158,7 +158,7 @@ def native_model(self): """ return self.cplex_model - def solve(self, time_limit=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, **kwargs): """ Call the cplex solver @@ -473,7 +473,7 @@ def add(self, cpm_expr_orig): return self __add__ = add # avoid redirect in superclass - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): """ CPLEX supports warmstarting the solver with a (in)feasible solution. This is done using MIP starts which provide the solver with a starting point @@ -510,7 +510,7 @@ def solution_hint(self, cpm_vars, vals): self.cplex_model.add_mip_start(warmstart) - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit: Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all solutions and optionally display the solutions. diff --git a/cpmpy/solvers/cpo.py b/cpmpy/solvers/cpo.py index b6c0a2705..934f94a7d 100644 --- a/cpmpy/solvers/cpo.py +++ b/cpmpy/solvers/cpo.py @@ -151,7 +151,7 @@ def native_model(self): """ return self.cpo_model - def solve(self, time_limit=None, solution_callback=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, solution_callback=None, **kwargs): """ Call the CP Optimizer solver @@ -253,7 +253,7 @@ def solve(self, time_limit=None, solution_callback=None, **kwargs): return has_sol - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ A shorthand to (efficiently) compute all (optimal) solutions, map them to CPMpy and optionally display the solutions. diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index cb624a948..4a1e3231b 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -48,7 +48,7 @@ """ import sys # for stdout checking import time -from typing import Optional +from typing import Optional, List from packaging.version import Version @@ -170,7 +170,7 @@ def _fillVars(self): for cpm_var, val in zip(lst_vars,exact_vals): cpm_var._value = bool(val) if isinstance(cpm_var, _BoolVarImpl) else val # xct value is always an int - def solve(self, time_limit=None, assumptions=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, assumptions:Optional[List[_BoolVarImpl]]=None, **kwargs): """ Call Exact @@ -272,7 +272,7 @@ def _update_time(self, timelim, start, end): if timelim == 0: timelim = -1 return timelim - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all solutions and optionally, display the solutions. @@ -639,7 +639,7 @@ def get_core(self): return [self.assumption_dict[i][1] for i in self.xct_solver.getLastCore()] - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): """ Exact supports warmstarting the solver with a partial feasible assignment. diff --git a/cpmpy/solvers/gcs.py b/cpmpy/solvers/gcs.py index 3eee21e1a..b2b1b8831 100644 --- a/cpmpy/solvers/gcs.py +++ b/cpmpy/solvers/gcs.py @@ -50,8 +50,11 @@ CPM_gcs """ +import warnings from typing import Optional +from packaging.version import Version + from cpmpy.transformations.comparison import only_numexpr_equality from cpmpy.transformations.reification import reify_rewrite, only_bv_reifies from ..exceptions import NotSupportedError, GCSVerificationException @@ -95,6 +98,11 @@ def supported(): # try to import the package try: import gcspy + gcs_version = CPM_gcs.version() + if Version(gcs_version) < Version("0.1.8"): + warnings.warn(f"CPMpy requires GCS version >=0.1.8 but you have version " + f"{gcs_version}, beware exact>=2.1.0 requires Python 3.10 or higher.") + return False return True except ModuleNotFoundError: return False @@ -148,7 +156,7 @@ def native_model(self): def has_objective(self): return self.objective_var is not None - def solve(self, time_limit=None, prove=False, proof_name=None, proof_location=".", + def solve(self, time_limit:Optional[float]=None, prove=False, proof_name=None, proof_location=".", verify=False, verify_time_limit=None, veripb_args = [], display_verifier_output=True, **kwargs): """ Run the Glasgow Constraint Solver, get just one (optimal) solution. @@ -250,7 +258,7 @@ def solve(self, time_limit=None, prove=False, proof_name=None, proof_location=". return has_sol - def solveAll(self, time_limit=None, display=None, solution_limit=None, call_from_model=False, + def solveAll(self, time_limit:Optional[float]=None, display=None, solution_limit:Optional[int]=None, call_from_model=False, prove=False, proof_name=None, proof_location=".", verify=False, verify_time_limit=None, veripb_args = [], display_verifier_output=True, **kwargs): """ diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 8e3fd8ce7..53defc543 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -42,7 +42,7 @@ ============== """ -from typing import Optional +from typing import Optional, List from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError @@ -151,12 +151,13 @@ def native_model(self): return self.grb_model - def solve(self, time_limit=None, solution_callback=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, solution_callback=None, **kwargs): """ Call the gurobi solver Arguments: - time_limit (float, optional): maximum solve time in seconds + time_limit (float, optional): maximum solve time in seconds + solution_callback: Gurobi callback function **kwargs: any keyword argument, sets parameters of solver object Arguments that correspond to solver parameters: @@ -479,7 +480,7 @@ def add(self, cpm_expr_orig): return self __add__ = add # avoid redirect in superclass - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): """ Gurobi supports warmstarting the solver with a (in)feasible solution. The provided value will affect branching heurstics during solving, making it more likely the final solution will contain the provided assignment. @@ -499,7 +500,7 @@ def solution_hint(self, cpm_vars, vals): for cpm_var, val in zip(cpm_vars, vals): self.solver_var(cpm_var).setAttr("VarHintVal", val) - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all solutions and optionally display the solutions. diff --git a/cpmpy/solvers/hexaly.py b/cpmpy/solvers/hexaly.py index 74f693b3d..595f548d0 100644 --- a/cpmpy/solvers/hexaly.py +++ b/cpmpy/solvers/hexaly.py @@ -39,7 +39,7 @@ CPM_hexaly """ -from typing import Optional +from typing import Optional, List from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..expressions.core import Expression, Comparison, Operator, BoolVal @@ -113,7 +113,7 @@ def __init__(self, cpm_model=None, subsolver=None): def native_model(self): return self.hex_model - def solve(self, time_limit=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, **kwargs): """ Call the Hexaly solver @@ -396,7 +396,7 @@ def _hex_expr(self, cpm_expr): raise NotImplementedError(f"Unexpected expression {cpm_expr}") - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ A shorthand to (efficiently) compute all solutions, map them to CPMpy and optionally display the solutions. @@ -419,7 +419,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from return super(CPM_hexaly, self).solveAll(display, time_limit, solution_limit, call_from_model, **kwargs) - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): from hexaly.optimizer import HxObjectiveDirection if self.is_satisfaction: # set dummy objective, otherwise cannot close model self.hex_model.add_objective(0, HxObjectiveDirection.MINIMIZE) diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 6bed87386..efe6411fb 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -291,7 +291,7 @@ def native_model(self): return self.mzn_model - def _pre_solve(self, time_limit=None, **kwargs): + def _pre_solve(self, time_limit:Optional[float]=None, **kwargs): """ shared by solve() and solveAll() """ import minizinc @@ -308,7 +308,7 @@ def _pre_solve(self, time_limit=None, **kwargs): kwargs['output-time'] = True # required for time getting return (kwargs, mzn_inst) - def solve(self, time_limit=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, **kwargs): """ Call the MiniZinc solver @@ -441,7 +441,7 @@ def mzn_time_to_seconds(self, time): else: raise NotImplementedError # unexpected type for time - async def _solveAll(self, display=None, time_limit=None, solution_limit=None, **kwargs): + async def _solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, **kwargs): """ Special 'async' function because mzn.solutions() is async """ # ensure all vars are known to solver @@ -815,7 +815,7 @@ def zero_based(array): # default (incl name-compatible global constraints...) return "{}([{}])".format(expr.name, ",".join(args_str)) - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all solutions and optionally display the solutions. diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index abc284fec..ac8d422d8 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -44,7 +44,7 @@ ============== """ import sys -from typing import Optional # for stdout checking +from typing import Optional, List # for stdout checking import numpy as np from .solver_interface import SolverInterface, SolverStatus, ExitStatus @@ -142,7 +142,7 @@ def native_model(self): return self.ort_model - def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwargs): + def solve(self, time_limit:Optional[float]=None, assumptions:Optional[List[_BoolVarImpl]]=None, solution_callback=None, **kwargs): """ Call the CP-SAT solver @@ -277,7 +277,7 @@ def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwa cpm_var._value = None return has_sol - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ A shorthand to (efficiently) compute all solutions, map them to CPMpy and optionally display the solutions. @@ -626,7 +626,7 @@ def _post_constraint(self, cpm_expr, reifiable=False): raise NotImplementedError(cpm_expr) # if you reach this... please report on github - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): """ OR-Tools supports warmstarting the solver with a feasible solution. diff --git a/cpmpy/solvers/pindakaas.py b/cpmpy/solvers/pindakaas.py index f881cc8cc..41f3eda0f 100755 --- a/cpmpy/solvers/pindakaas.py +++ b/cpmpy/solvers/pindakaas.py @@ -39,7 +39,7 @@ import time from datetime import timedelta -from typing import Optional +from typing import Optional, List from ..exceptions import NotSupportedError from ..expressions.utils import eval_comparison @@ -121,7 +121,7 @@ def __init__(self, cpm_model=None, subsolver=None): def native_model(self): return self.pdk_solver - def solve(self, time_limit=None, assumptions=None): + def solve(self, time_limit:Optional[float]=None, assumptions:Optional[List[_BoolVarImpl]]=None): """ Solve the encoded CPMpy model given optional time limit and assumptions, returning whether a solution was found. diff --git a/cpmpy/solvers/pumpkin.py b/cpmpy/solvers/pumpkin.py index 9d36dc89b..d6e9d7fb2 100644 --- a/cpmpy/solvers/pumpkin.py +++ b/cpmpy/solvers/pumpkin.py @@ -38,8 +38,7 @@ ============== """ import warnings -from typing import Optional -from importlib.metadata import version, PackageNotFoundError +from typing import Optional, List from os.path import join import numpy as np @@ -134,7 +133,7 @@ def native_model(self): return self.pum_solver - def solve(self, time_limit=None, prove=False, proof_name="proof.drcp", proof_location=".", assumptions=None): + def solve(self, time_limit:Optional[float]=None, prove=False, proof_name="proof.drcp", proof_location=".", assumptions:Optional[List[_BoolVarImpl]]=None): """ Call the Pumpkin solver diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 0a157eaf1..742c7172c 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -52,7 +52,7 @@ ============== """ from threading import Timer -from typing import Optional +from typing import Optional, List import warnings from .solver_interface import SolverInterface, SolverStatus, ExitStatus @@ -212,7 +212,7 @@ def native_model(self): return self.pysat_solver - def solve(self, time_limit=None, assumptions=None): + def solve(self, time_limit:Optional[float]=None, assumptions:Optional[List[_BoolVarImpl]]=None): """ Call the PySAT solver @@ -478,12 +478,14 @@ def _post_constraint(self, cpm_expr): __add__ = add # avoid redirect in superclass - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_BoolVarImpl], vals:List[bool]): """ PySAT supports warmstarting the solver with a feasible solution In PySAT, this is called setting the 'phases' or the 'polarities' of literals + Note: our PySAT interface currently does not support solution hinting for integer variables + :param cpm_vars: list of CPMpy variables :param vals: list of (corresponding) values for the variables """ @@ -491,6 +493,7 @@ def solution_hint(self, cpm_vars, vals): cpm_vars = flatlist(cpm_vars) vals = flatlist(vals) assert (len(cpm_vars) == len(vals)), "Variables and values must have the same size for hinting" + assert all(var.is_bool() for var in cpm_vars), "PySAT interface currently only supports Boolean variables in solution hint" literals = [] for (cpm_var, val) in zip(cpm_vars, vals): diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index 496b3616b..1bd973b4a 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -44,7 +44,7 @@ ============== """ from functools import reduce -from typing import Optional +from typing import Optional, List from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError @@ -130,7 +130,7 @@ def native_model(self): """ return self.pysdd_root - def solve(self, time_limit=None, assumptions=None): + def solve(self, time_limit:Optional[float]=None, assumptions:Optional[List[_BoolVarImpl]]=None): """ See if an arbitrary model exists @@ -181,7 +181,7 @@ def solve(self, time_limit=None, assumptions=None): return has_sol - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all solutions and optionally display the solutions. diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index c41b43a20..7b97a09c8 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -19,13 +19,14 @@ ExitStatus """ -from typing import Optional +from typing import Optional, List import warnings import time from enum import Enum from ..exceptions import NotSupportedError from ..expressions.core import Expression +from ..expressions.variables import _NumVarImpl from ..transformations.get_variables import get_variables from ..expressions.utils import is_any_list from ..expressions.python_builtins import any @@ -138,18 +139,13 @@ def objective(self, expr, minimize): def status(self): return self.cpm_status - def solve(self, model, time_limit=None): + def solve(self,time_limit:Optional[float]=None): """ - Build the CPMpy model into solver-supported model ready for solving - and returns the answer (True/False/objective.value()) + Call the underlying solver. Overwrites self.cpm_status - :param model: CPMpy model to be parsed. - :type model: Model - :param time_limit: optional, time limit in seconds - :type time_limit: int or float :return: Bool: - True if a solution is found (not necessarily optimal, e.g. could be after timeout) @@ -236,7 +232,7 @@ def __add__(self, cpm_expr): # OPTIONAL functions - def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs): + def solveAll(self, display=None, time_limit:Optional[float]=None, solution_limit:Optional[int]=None, call_from_model=False, **kwargs): """ Compute all solutions and optionally display the solutions. @@ -304,7 +300,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from return solution_count - def solution_hint(self, cpm_vars, vals): + def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): """ For warmstarting the solver with a variable assignment diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 98fe99838..4d259dcf3 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -45,7 +45,7 @@ Module details ============== """ -from typing import Optional +from typing import Optional, List from cpmpy.transformations.get_variables import get_variables from .solver_interface import SolverInterface, SolverStatus, ExitStatus @@ -139,7 +139,7 @@ def native_model(self): return self.z3_solver - def solve(self, time_limit=None, assumptions=[], **kwargs): + def solve(self, time_limit:Optional[float]=None, assumptions:Optional[List[_BoolVarImpl]]=None, **kwargs): """ Call the z3 solver @@ -184,6 +184,9 @@ def solve(self, time_limit=None, assumptions=[], **kwargs): self.z3_solver.set(timeout=int(time_limit*1000)) + if assumptions is None: + assumptions = [] + z3_assum_vars = self.solver_vars(assumptions) self.assumption_dict = {z3_var : cpm_var for (cpm_var, z3_var) in zip(assumptions, z3_assum_vars)}