Docs on solver statistics (#440)

* save minizinc result in solver object

* format solver api, and add missing links in docs

* update version and copyright date

* uncomment assumption-based python code in docs

cpmpy/solvers/__init__.py

@@ -12,6 +12,7 @@
         :nosignatures:
 
         ortools
+        minizinc
         pysat
         gurobi
         pysdd
@@ -26,6 +27,7 @@
         :nosignatures:
 
         CPM_ortools
+        CPM_minizinc
         CPM_pysat
         CPM_gurobi
         CPM_pysdd

cpmpy/solvers/exact.py

@@ -51,12 +51,12 @@ class CPM_exact(SolverInterface):
     See https://pypi.org/project/exact for more information.
 
     Creates the following attributes (see parent constructor for more):
-    - xct_solver: the Exact instance used in solve() and solveAll()
-    - assumption_dict: maps Exact variables to (Exact value, CPM assumption expression)
+        - xct_solver: the Exact instance used in solve() and solveAll()
+        - assumption_dict: maps Exact variables to (Exact value, CPM assumption expression)
     to recover which expressions were in the core
-    - solver_is_initialized: whether xct_solver is initialized
-    - self.objective_given: whether an objective function is given to xct_solver
-    - self.objective_minimize: the direction of the optimization (if false then maximize)
+        - solver_is_initialized: whether xct_solver is initialized
+        - self.objective_given: whether an objective function is given to xct_solver
+        - self.objective_minimize: the direction of the optimization (if false then maximize)
     as Exact can only minimize
     """
 

cpmpy/solvers/gurobi.py

@@ -56,7 +56,7 @@ class CPM_gurobi(SolverInterface):
     https://support.gurobi.com/hc/en-us/articles/360044290292-How-do-I-install-Gurobi-for-Python-
 
     Creates the following attributes (see parent constructor for more):
-    - grb_model: object, TEMPLATE's model object
+        - grb_model: object, TEMPLATE's model object
 
     The `DirectConstraint`, when used, calls a function on the `grb_model` object.
     """

cpmpy/solvers/minizinc.py

@@ -63,9 +63,10 @@ class CPM_minizinc(SolverInterface):
 
 
     Creates the following attributes (see parent constructor for more):
-    mzn_model: object, the minizinc.Model instance
-    mzn_solve: object, the minizinc.Solver instance
-    mzn_txt_solve: str, the 'solve' item in text form, so it can be overwritten
+        - mzn_model: object, the minizinc.Model instance
+        - mzn_solver: object, the minizinc.Solver instance
+        - mzn_txt_solve: str, the 'solve' item in text form, so it can be overwritten
+        - mzn_result: object, containing solve results
 
     The `DirectConstraint`, when used, adds a constraint with that name and the given args to the MiniZinc model.
     """
@@ -135,6 +136,7 @@ def __init__(self, cpm_model=None, subsolver=None):
         self.mzn_model.add_string("% Generated by CPMpy\ninclude \"globals.mzn\";\n\n")
         # Prepare solve statement, so it can be overwritten on demand
         self.mzn_txt_solve = "solve satisfy;"
+        self.mzn_result = None
 
 
         # initialise everything else and post the constraints/objective
@@ -183,7 +185,7 @@ def solve(self, time_limit=None, **kwargs):
         # call the solver, with parameters
         import minizinc.error
         try:
-            mzn_result = mzn_inst.solve(**mzn_kwargs)
+            self.mzn_result = mzn_inst.solve(**mzn_kwargs)
         except minizinc.error.MiniZincError as e:
             if sys.platform == "win32" or sys.platform == "cygwin": #path error can occur in windows
                 path = os.environ.get("path")
@@ -195,15 +197,15 @@ def solve(self, time_limit=None, **kwargs):
             else:
                 raise e
         # new status, translate runtime
-        self.cpm_status = self._post_solve(mzn_result)
+        self.cpm_status = self._post_solve(self.mzn_result)
 
         # True/False depending on self.cpm_status
         has_sol = self._solve_return(self.cpm_status)
 
         # translate solution values (of user specified variables only)
         self.objective_value_ = None
         if has_sol: #mzn_result.status.has_solution():
-            mznsol = mzn_result.solution
+            mznsol = self.mzn_result.solution
             if is_any_list(mznsol):
                 print("Warning: multiple solutions found, only returning last one")
                 mznsol = mznsol[-1]
@@ -217,7 +219,7 @@ def solve(self, time_limit=None, **kwargs):
                     print("Warning, no value for ", sol_var)
 
             # translate objective, for optimisation problems only (otherwise None)
-            self.objective_value_ = mzn_result.objective
+            self.objective_value_ = self.mzn_result.objective
 
         return has_sol
 

cpmpy/solvers/ortools.py

@@ -51,8 +51,8 @@ class CPM_ortools(SolverInterface):
     https://developers.google.com/optimization/install
 
     Creates the following attributes (see parent constructor for more):
-    ort_model: the ortools.sat.python.cp_model.CpModel() created by _model()
-    ort_solver: the ortools cp_model.CpSolver() instance used in solve()
+        - ort_model: the ortools.sat.python.cp_model.CpModel() created by _model()
+        - ort_solver: the ortools cp_model.CpSolver() instance used in solve()
 
     The `DirectConstraint`, when used, calls a function on the `ort_model` object.
     """

cpmpy/solvers/pysat.py

@@ -53,8 +53,8 @@ class CPM_pysat(SolverInterface):
     https://pysathq.github.io/installation.html
 
     Creates the following attributes (see parent constructor for more):
-    pysat_vpool: a pysat.formula.IDPool for the variable mapping
-    pysat_solver: a pysat.solver.Solver() (default: glucose4)
+        - pysat_vpool: a pysat.formula.IDPool for the variable mapping
+        - pysat_solver: a pysat.solver.Solver() (default: glucose4)
 
     The `DirectConstraint`, when used, calls a function on the `pysat_solver` object.
     """

cpmpy/solvers/pysdd.py

@@ -42,9 +42,9 @@ class CPM_pysdd(SolverInterface):
     https://pysdd.readthedocs.io/en/latest/usage/installation.html
 
     Creates the following attributes (see parent constructor for more):
-    pysdd_vtree: a pysdd.sdd.Vtree
-    pysdd_manager: a pysdd.sdd.SddManager
-    pysdd_root: a pysdd.sdd.SddNode (changes whenever a formula is added)
+        - pysdd_vtree: a pysdd.sdd.Vtree
+        - pysdd_manager: a pysdd.sdd.SddManager
+        - pysdd_root: a pysdd.sdd.SddNode (changes whenever a formula is added)
 
     The `DirectConstraint`, when used, calls a function on the `pysdd_manager` object and replaces the root node with a conjunction of the previous root node and the result of this function call.
     """

cpmpy/solvers/z3.py

@@ -41,7 +41,7 @@ class CPM_z3(SolverInterface):
     https://github.com/Z3Prover/z3#python
 
     Creates the following attributes (see parent constructor for more):
-    z3_solver: object, z3's Solver() object
+        - z3_solver: object, z3's Solver() object
 
     The `DirectConstraint`, when used, calls a function in the `z3` namespace and `z3_solver.add()`'s the result.
     """

docs/api/solvers/exact.rst

@@ -0,0 +1,7 @@
+CPMpy exact interface (:mod:`cpmpy.solvers.exact`)
+=====================================================
+
+.. automodule:: cpmpy.solvers.exact
+    :members:
+    :undoc-members:
+    :inherited-members:

docs/api/solvers/pysdd.rst

@@ -0,0 +1,7 @@
+CPMpy pysdd interface (:mod:`cpmpy.solvers.pysdd`)
+=====================================================
+
+.. automodule:: cpmpy.solvers.pysdd
+    :members:
+    :undoc-members:
+    :inherited-members:

docs/api/solvers/z3.rst

@@ -0,0 +1,7 @@
+CPMpy z3 interface (:mod:`cpmpy.solvers.z3`)
+=====================================================
+
+.. automodule:: cpmpy.solvers.z3
+    :members:
+    :undoc-members:
+    :inherited-members:

docs/conf.py

@@ -20,11 +20,11 @@
 # -- Project information -----------------------------------------------------
 
 project = 'CPMpy'
-copyright = '2021, Tias Guns'
+copyright = '2024, Tias Guns'
 author = 'Tias Guns'
 
 # The full version, including alpha/beta/rc tags
-release = '0.5'
+release = '0.9.18'
 
 # variables to be accessed from html
 html_context = {

docs/index.rst

@@ -71,5 +71,4 @@ Are you a solver developer? We are keen to integrate solvers that have a python
    api/expressions
    api/model
    api/solvers
-   api/transformations
-
+   api/transformations

docs/modeling.md

@@ -538,8 +538,35 @@ s.solve(cp_model_probing_level = 2,
 
 See [the API documentation of the solvers](api/solvers.html) for information and links on the parameters supported. See our documentation page on [solver parameters](solver_parameters.html) if you want to tune your hyperparameters automatically. 
 
+## Accessing the underlying solver object
 
+After solving, we can access the underlying solver object to retrieve some information about the solve.
+For example in ortools we can find the number of search branches like this, expanding our previous example.
+```python
+import cpmpy as cp
+x = cp.intvar(0,10, shape=3) 
+s = cp.SolverLookup.get("ortools")
+# we are operating on the ortools interface here
+s += (cp.sum(x) <= 5)
+s.solve()
+print(s.ort_solver.NumBranches())
+```
+
+Other solvers, like Minizinc might have other native objects stored.
+You can see which solver native objects are initialized for each solver in [the API documentation](api/solvers.html) of the solver.
+We can access the solver statistics from the mzn_result object like this:
 
+```python
+import cpmpy as cp
+x = cp.intvar(0,10, shape=3) 
+s = cp.SolverLookup.get("minizinc")
+# we are operating on the minizinc interface here
+s += (cp.sum(x) <= 5)
+s.solve()
+print(s.mzn_result.statistics)
+print(s.mzn_result.statistics['nodes']) #if we are only interested in the nb of search nodes
+
+```
 ## Incremental solving
 It is important to realize that a CPMpy solver interface is _eager_. That means that when a CPMpy constraint is added to a solver object, CPMpy _immediately_ translates it and posts the constraints to the underlying solver. That is why the debugging trick of posting it one-by-one works.
 
@@ -568,7 +595,7 @@ Assumption variables are usefull for incremental solving when you want to activa
 By relying on the solver interface directly as in the previous section, the state of the solver is kept in between solve-calls.
 Many explanation-generation algorithms (see `cpmpy.tools.explain`) make use of this feature to speed up the solving.
 
-```pythonupdate tests
+```python
 import cpmpy as cp
 
 x = cp.intvar(1,5, shape=5, name="x")