Merge remote-tracking branch 'refs/remotes/origin/master' into exact2

cpmpy/exceptions.py

@@ -32,6 +32,8 @@ class IncompleteFunctionError(CPMpyException):
 class TypeError(CPMpyException):
     pass
 
+class GCSVerificationException(CPMpyException):
+    pass
 
 class TransformationNotImplementedError(CPMpyException):
     pass

cpmpy/expressions/python_builtins.py

@@ -18,7 +18,6 @@
         min
         sum
 """
-import numpy as np
 import builtins  # to use the original Python-builtins
 
 from .utils import is_false_cst, is_true_cst
@@ -70,41 +69,59 @@ def any(iterable):
         elif isinstance(elem, Expression) and elem.is_bool():
             collect.append(elem)
         else:
-            raise Exception("Non-Boolean argument '{}' to 'all'".format(elem))
+            raise Exception("Non-Boolean argument '{}' to 'any'".format(elem))
     if len(collect) == 1:
         return collect[0]
     if len(collect) >= 2:
         return Operator("or", collect)
     return False
 
 
-def max(iterable):
+def max(*iterable, **kwargs):
     """
-        max() overwrites python built-in,
-        checks if all constants and computes np.max() in that case
+        max() overwrites the python built-in to support decision variables.
+
+        if iterable does not contain CPMpy expressions, the built-in is called
+        else a Maximum functional global constraint is constructed; no keyword
+          arguments are supported in that case
     """
+    if len(iterable) == 1:
+        iterable = tuple(iterable[0])
     if not builtins.any(isinstance(elem, Expression) for elem in iterable):
-        return np.max(iterable)
+        return builtins.max(*iterable, **kwargs)
+
+    assert len(kwargs)==0, "max over decision variables does not support keyword arguments"
     return Maximum(iterable)
 
 
-def min(iterable):
+def min(*iterable, **kwargs):
     """
-        min() overwrites python built-in,
-        checks if all constants and computes np.min() in that case
+        min() overwrites the python built-in to support decision variables.
+
+        if iterable does not contain CPMpy expressions, the built-in is called
+        else a Minimum functional global constraint is constructed; no keyword
+          arguments are supported in that case
     """
+    if len(iterable) == 1:
+        iterable = tuple(iterable[0])
     if not builtins.any(isinstance(elem, Expression) for elem in iterable):
-        return np.min(iterable)
+        return builtins.min(*iterable, **kwargs)
+
+    assert len(kwargs)==0, "min over decision variables does not support keyword arguments"
     return Minimum(iterable)
 
 
-def sum(iterable):
+def sum(*iterable, **kwargs):
     """
-        sum() overwrites python built-in,
-        checks if all constants and computes np.sum() in that case
-        otherwise, makes a sum Operator directly on `iterable`
+        sum() overwrites the python built-in to support decision variables.
+
+        if iterable does not contain CPMpy expressions, the built-in is called
+        checks if all constants and uses built-in sum() in that case
     """
-    iterable = list(iterable) # Fix generator polling
+    if len(iterable) == 1:
+        iterable = tuple(iterable[0]) # Fix generator polling
     if not builtins.any(isinstance(elem, Expression) for elem in iterable):
-        return np.sum(iterable)
+        return builtins.sum(iterable, **kwargs)
+
+    assert len(kwargs)==0, "sum over decision variables does not support keyword arguments"
     return Operator("sum", iterable)

cpmpy/model.py

@@ -136,7 +136,7 @@ def maximize(self, expr):
         self.objective(expr, minimize=False)
 
     # solver: name of supported solver or any SolverInterface object
-    def solve(self, solver=None, time_limit=None):
+    def solve(self, solver=None, time_limit=None, **kwargs):
         """ Send the model to a solver and get the result
 
         :param solver: name of a solver to use. Run SolverLookup.solvernames() to find out the valid solver names on your system. (default: None = first available solver)
@@ -156,7 +156,7 @@ def solve(self, solver=None, time_limit=None):
             s = SolverLookup.get(solver, self)
 
         # call solver
-        ret = s.solve(time_limit=time_limit)
+        ret = s.solve(time_limit=time_limit, **kwargs)
         # store CPMpy status (s object has no further use)
         self.cpm_status = s.status()
         return ret

cpmpy/solvers/__init__.py

@@ -19,6 +19,7 @@
         z3
         exact
         choco
+        gcs
         utils
 
     ===============
@@ -35,6 +36,7 @@
         CPM_z3
         CPM_exact
         CPM_choco
+        CPM_gcs
 
     =================
     List of functions
@@ -54,4 +56,5 @@
 from .z3 import CPM_z3
 from .exact import CPM_exact
 from .choco import CPM_choco
+from .gcs import CPM_gcs
 

cpmpy/solvers/choco.py

@@ -98,6 +98,13 @@ def __init__(self, cpm_model=None, subsolver=None):
         # initialise everything else and post the constraints/objective
         super().__init__(name="choco", cpm_model=cpm_model)
 
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.chc_model
+
     def solve(self, time_limit=None, **kwargs):
         """
             Call the Choco solver

cpmpy/solvers/exact.py

@@ -112,6 +112,12 @@ def __init__(self, cpm_model=None, subsolver=None, **kwargs):
 
         # initialise everything else and post the constraints/objective
         super().__init__(name="exact", cpm_model=cpm_model)
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.xct_solver
 
     def _fillObjAndVars(self):
         if not self.xct_solver.hasSolution():

cpmpy/solvers/gcs.py

@@ -18,7 +18,7 @@
 """
 from cpmpy.transformations.comparison import only_numexpr_equality
 from cpmpy.transformations.reification import reify_rewrite, only_bv_reifies, only_implies
-from ..exceptions import NotSupportedError
+from ..exceptions import NotSupportedError, GCSVerificationException
 from .solver_interface import SolverInterface, SolverStatus, ExitStatus
 from ..expressions.core import Expression, Comparison, Operator, BoolVal
 from ..expressions.variables import _BoolVarImpl, _IntVarImpl, _NumVarImpl, NegBoolView, boolvar
@@ -59,7 +59,7 @@ class CPM_gcs(SolverInterface):
     - objective_var: optional: the variable used as objective
     - proof_location: location of the last proof produced by the solver
     - proof_name: name of the last proof (means <proof_name>.opb and <proof_name>.pbp will be present at the proof location)
-    - proof_verification_failed: whether the last VeriPB check failed to verify the proof.
+    - veripb_return_code: return code from the last VeriPB check.
     - proof_check_timeout: whether the last VeriPB check timed out.
     """
 
@@ -92,7 +92,7 @@ def __init__(self, cpm_model=None, subsolver=None):
         self.proof_location = None
         self.proof_name = None
         self.proof_check_timeout = True
-        self.proof_verification_failed = False
+        self.veripb_return_code = False
 
         # initialise everything else and post the constraints/objective
         super().__init__(name="Glasgow Constraint Solver", cpm_model=cpm_model)
@@ -177,6 +177,10 @@ def solve(self, time_limit=None, prove=False, proof_name=None, proof_location=".
         if verify:
             self.verify(name=self.proof_name, location=proof_location, time_limit=verify_time_limit,
                         veripb_args=veripb_args, display_output=display_verifier_output)
+
+            if self.veripb_return_code > 0:
+                raise GCSVerificationException("Glasgow Constraint Solver: Proof failed to verify.")
+
         return has_sol
 
     def solveAll(self, time_limit=None, display=None, solution_limit=None, call_from_model=False, 
@@ -358,6 +362,8 @@ def verify(self, name=None, location=".", time_limit=None, display_output=False,
         """
         Verify a solver-produced proof using VeriPB.
 
+        Requires that the 'veripb' tool is installed and on system path. 
+        See `https://gitlab.com/MIAOresearch/software/VeriPB#installation` for installation instructions. 
         Arguments:
             - name:             name for the the proof files (default to self.proof_name)
             - location:         location for the proof files (default to current working directory).
@@ -366,27 +372,38 @@ def verify(self, name=None, location=".", time_limit=None, display_output=False,
             - display_output:   whether to print the output from VeriPB
         """
         if not which("veripb"):
-            raise Exception("Unable to run VeriPB: check it is installed and on system path")
+            raise Exception("Unable to run VeriPB: check it is installed and on system path - see https://gitlab.com/MIAOresearch/software/VeriPB#installation.")
 
         if name is None:
             name = self.proof_name
+
         if name is None: # Still None?
             raise ValueError("No proof to verify")
 
+        if not isinstance(veripb_args, list):
+            raise ValueError("veripb_args should be a list")
+
+        opb_file = path.join(location, name +".opb")
+        pbp_file = path.join(location, name +".pbp")
+
+        if not path.isfile(opb_file):
+            raise FileNotFoundError("Can't find " + opb_file)
+        if not path.isfile(pbp_file):
+            raise FileNotFoundError("Can't find " + pbp_file)
+
         try:
-            result = subprocess.run(["veripb", path.join(location, name +".opb"), path.join(location, name +".pbp")] + veripb_args, 
+            result = subprocess.run(["veripb"] + veripb_args + [opb_file, pbp_file], 
                                     capture_output=True, text=True, timeout=time_limit)
             self.proof_check_timeout = False
-            self.proof_verification_failed = result.returncode
+            self.veripb_return_code = result.returncode
+            if display_output:
+                print(result.stdout)
+                print(result.stderr)
         except subprocess.TimeoutExpired:
             self.proof_check_timeout = True
-            self.proof_verification_failed = False
+            self.veripb_return_code = 0
 
-        if display_output:
-            print(result.stdout)
-            print(result.stderr)
-
-        return self.proof_verification_failed
+        return self.veripb_return_code
 
     def __add__(self, cpm_cons):
         """
@@ -409,8 +426,6 @@ def __add__(self, cpm_cons):
             elif isinstance(cpm_expr, BoolVal):
                 if not cpm_expr:
                     self.gcs.post_or([])
-                else:
-                    return
             elif isinstance(cpm_expr, Operator) or \
                 (cpm_expr.name == '==' and isinstance(cpm_expr.args[0], _BoolVarImpl) \
                 and not isinstance(cpm_expr.args[1], _NumVarImpl)): 

cpmpy/solvers/gurobi.py

@@ -96,6 +96,13 @@ def __init__(self, cpm_model=None, subsolver=None):
         # it is sufficient to implement __add__() and minimize/maximize() below
         super().__init__(name="gurobi", cpm_model=cpm_model)
 
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.grb_model
+
 
     def solve(self, time_limit=None, solution_callback=None, **kwargs):
         """

cpmpy/solvers/minizinc.py

@@ -174,6 +174,14 @@ def __init__(self, cpm_model=None, subsolver=None):
         # initialise everything else and post the constraints/objective
         super().__init__(name="minizinc:"+subsolver, cpm_model=cpm_model)
 
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.mzn_model
+
+
     def _pre_solve(self, time_limit=None, **kwargs):
         """ shared by solve() and solveAll() """
         import minizinc
@@ -697,3 +705,19 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
             finally:
                 asyncio.events.set_event_loop(None)
                 loop.close()
+
+    def minizinc_string(self) -> str:
+        """
+            Returns the model as represented in the Minizinc language.
+        """
+        return "".join(self._pre_solve()[1]._code_fragments)
+
+    def flatzinc_string(self, **kwargs) -> str:
+        """
+            Returns the model as represented in the Flatzinc language.
+        """
+        with self._pre_solve()[1].flat(**kwargs) as (fzn, ozn, statistics):
+            with open(fzn.name) as f:
+                f.seek(0)
+                contents = f.readlines()
+        return "".join(contents)

cpmpy/solvers/ortools.py

@@ -98,6 +98,12 @@ def __init__(self, cpm_model=None, subsolver=None):
 
         # initialise everything else and post the constraints/objective
         super().__init__(name="ortools", cpm_model=cpm_model)
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.ort_model
 
 
     def solve(self, time_limit=None, assumptions=None, solution_callback=None, **kwargs):

cpmpy/solvers/pysat.py

@@ -50,7 +50,7 @@ class CPM_pysat(SolverInterface):
     $ pip install python-sat
 
     See detailed installation instructions at:
-    https://pysathq.github.io/installation.html
+    https://pysathq.github.io/installation
 
     Creates the following attributes (see parent constructor for more):
         - pysat_vpool: a pysat.formula.IDPool for the variable mapping
@@ -81,7 +81,8 @@ def solvernames():
         from pysat.solvers import SolverNames
         names = []
         for name, attr in vars(SolverNames).items():
-            if not name.startswith('__') and isinstance(attr, tuple):
+            # issue with cryptosat, so we don't include it in our https://github.com/msoos/cryptominisat/issues/765
+            if not name.startswith('__') and isinstance(attr, tuple) and not name == 'cryptosat':
                 if name not in attr:
                     name = attr[-1]
                 names.append(name)
@@ -124,6 +125,13 @@ def __init__(self, cpm_model=None, subsolver=None):
         # initialise everything else and post the constraints/objective
         super().__init__(name="pysat:"+subsolver, cpm_model=cpm_model)
 
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.pysat_solver
+
 
     def solve(self, time_limit=None, assumptions=None):
         """

cpmpy/solvers/solver_interface.py

@@ -88,6 +88,13 @@ def __init__(self, name="dummy", cpm_model=None, subsolver=None):
                 else:
                     self.maximize(cpm_model.objective_)
 
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        raise NotImplementedError("Solver does not support direct solver access. Look at the solver's API for alternative native objects to access directly.")
+
     # instead of overloading minimize/maximize, better just overload 'objective()'
     def minimize(self, expr):
         """

cpmpy/solvers/z3.py

@@ -82,6 +82,13 @@ def __init__(self, cpm_model=None, subsolver="sat"):
         # initialise everything else and post the constraints/objective
         super().__init__(name="z3", cpm_model=cpm_model)
 
+    @property
+    def native_model(self):
+        """
+            Returns the solver's underlying native model (for direct solver access).
+        """
+        return self.z3_solver
+
 
     def solve(self, time_limit=None, assumptions=[], **kwargs):
         """