Unified prooflogging

cpmpy/solvers/exact.py

@@ -115,7 +115,7 @@ def version() -> Optional[str]:
             return None
 
 
-    def __init__(self, cpm_model=None, subsolver=None, **kwargs):
+    def __init__(self, cpm_model=None, subsolver=None, proof=None, **kwargs):
         """
         Constructor of the native solver object
 
@@ -125,6 +125,7 @@ def __init__(self, cpm_model=None, subsolver=None, **kwargs):
         Arguments:
             cpm_model: Model(), a CPMpy Model() (optional)
             subsolver: None
+            proof: None, path to proof file when proof-logging (will be appended with .proof and .formula)
 
         Exact takes options at initialization instead of solving.
         The Exact solver parameters are defined by https://gitlab.com/nonfiction-software/exact/-/blob/main/src/Options.hpp
@@ -135,11 +136,14 @@ def __init__(self, cpm_model=None, subsolver=None, **kwargs):
             raise ModuleNotFoundError("CPM_exact: Install the python package 'cpmpy[exact]' to use this solver interface.")
 
         assert subsolver is None, "Exact does not allow subsolvers."
+        self._proof = proof
 
         from exact import Exact as xct
         # initialise the native solver object
         options = list(kwargs.items()) # options is a list of string-pairs, e.g. [("verbosity","1")]
         options = [(opt[0], str(opt[1])) for opt in options] # Ensure values are also strings
+        if proof is not None:
+            options += [('proof-log', proof)]
         self.xct_solver = xct(options)
 
         # can override encoding of variables
@@ -666,3 +670,12 @@ def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]):
         vals = flatlist(vals)
         assert (len(cpm_vars) == len(vals)), "Variables and values must have the same size for hinting"
         self.xct_solver.setSolutionHints(list(zip(self.solver_vars(cpm_vars), vals)))
+
+    def get_proof_files(self) -> tuple[str,str]:
+        """
+        Returns the list of VeriPb proof-files generated:
+        """
+        if self._proof is None:
+            raise ValueError("No proof name provided at construction time of the solver. Use cpmpy.SolverLookup.get('exact', model, proof=...)")
+
+        return (f"{self._proof}.formula", f"{self._proof}.proof")

cpmpy/solvers/gcs.py

@@ -124,7 +124,7 @@ def version() -> Optional[str]:
         except PackageNotFoundError:
             return None
 
-    def __init__(self, cpm_model=None, subsolver=None):
+    def __init__(self, cpm_model=None, subsolver=None, proof=None):
         """
         Constructor of the native solver object
 
@@ -142,8 +142,8 @@ def __init__(self, cpm_model=None, subsolver=None):
         # initialise the native solver object
         self.gcs = gcspy.GCS()
         self.objective_var = None
-        self.proof_location = None
-        self.proof_name = None
+        self._proof = proof
+
         self.proof_check_timeout = True
         self.veripb_return_code = False
 
@@ -179,33 +179,28 @@ def solve(self, time_limit:Optional[float]=None, prove=False, proof_name:Optiona
             Returns: 
                 whether a solution was found.
         """
+        if "proof" in kwargs or "prove" in kwargs or "prove_location" in kwargs or "proof_name" in kwargs:
+            raise ValueError("Proof-file should be supplied in the constructor, not as a keyword argument to solve."
+                             "`cpmpy.SolverLookup.get('gcs', model, proof='path/to/proof')`")
+
+        if verify is True and self._proof is None:
+            raise ValueError("Verify was set to True, but no proof name was supplied.")
+
         # ensure all user vars are known to solver
         self.solver_vars(list(self.user_vars))
 
-        # If we're verifying we must be proving
-        prove |= verify
-        # Set default proof name to name of file containing __main__
-        if prove and proof_name is None:
-            if hasattr(sys.modules['__main__'], "__file__"):
-                self.proof_name = path.splitext(path.basename(sys.modules['__main__'].__file__))[0]
-            else:
-                self.proof_name = "gcs_proof"
-        else:
-            self.proof_name = proof_name
-        self.proof_location = proof_location
-
         # set time limit
         if time_limit is not None and time_limit <= 0:
             raise ValueError("Time limit must be positive")
-                 
+
         # call the solver, with parameters    
         self.gcs_result = self.gcs.solve(
             all_solutions=self.has_objective(), 
             timeout=time_limit,
             callback=None,
-            prove=prove,
-            proof_name=self.proof_name,
-            proof_location=proof_location,
+            prove=self._proof is not None,
+            proof_name=self._proof,
+            proof_location=".",
             **kwargs)
 
         # new status, translate runtime
@@ -331,7 +326,7 @@ def display_callback(solution_map):
             solution_limit=solution_limit, 
             callback=sol_callback, 
             prove=prove, 
-            proof_name=proof_name, 
+            proof_name=self._proof,
             proof_location=proof_location, **kwargs)
 
         # new status, get runtime
@@ -702,5 +697,14 @@ def add(self, cpm_cons):
         return self
     __add__ = add  # avoid redirect in superclass
 
+    def get_proof_files(self) -> tuple[str,str,str]:
+        """
+        Returns a tuple with the proof files generated during the last solve call.
+        - opb file
+        - veripb proof file
+        - varmap linking Boolean variables to CP variables
+        """
+        return (f"{self._proof}.opb", f"{self._proof}.pbp", f"{self._proof}.varmap")
+
 
 

cpmpy/solvers/pumpkin.py

@@ -685,3 +685,9 @@ def solution_hint(self, cpm_vars: List[_NumVarImpl], vals: List[int]):
         """
         if self.pum_solver.is_inconsistent() is False: # otherwise, not guaranteed all variables are known
             self._solhint = {self.solver_var(v) : val for v, val in zip(cpm_vars, vals)} # store for later use in solve
+
+    def get_proof_files(self) -> tuple[str]:
+        """
+        Returns the path where the proof is stored.
+        """
+        return (self._proof,)

cpmpy/solvers/solver_interface.py

@@ -327,6 +327,14 @@ def get_core(self):
         """
         raise NotSupportedError("Solver does not support unsat core extraction")
 
+    def get_proof_files(self):
+        """
+        For use when solving using proof-logging.
+        Returns a list of filenames where the proof was stored.
+
+        Depending on the proof-format used, a solver may use multiple proof files for a single solve-call
+        """
+        raise NotSupportedError("Solver does not support proof logging")
 
     # shared helper functions
 

tests/test_solvers.py

@@ -1237,6 +1237,28 @@ def test_bug810(self, solver):
         assert model.solve(solver)
         assert model.solveAll(solver, **kwargs) == 2
 
+    def test_prooflogging(self, solver):
+
+        cls = cp.SolverLookup.lookup(solver)
+        args = inspect.signature(cls.__init__)
+        if "proof" not in args.parameters.keys():
+            pytest.skip(reason=f"{solver} does not support prooflogging")
+
+        x,y,z = cp.intvar(1,5,shape=3)
+        m = cp.Model(x < y, y < z, z < x)
+
+        prooffile = tempfile.NamedTemporaryFile(delete=False)
+        solver = cp.SolverLookup.get(solver, m, proof=f"{solver}_proof")
+        assert solver.solve() is False
+
+        for file in solver.get_proof_files():
+            with open(file, "r") as f:
+                print(f"Reading {file}")
+                proof = f.read()
+                print(proof)
+                assert len(proof) > 0, f"proof file {file} is empty"
+
+
 
 @pytest.mark.generate_constraints.with_args(numexprs)
 def test_objective_numexprs(solver, constraint):