Testing incrementality (#518)

* make tests and update exact.py

* fix test

* split test into objective/no objective

cpmpy/solvers/exact.py

@@ -112,6 +112,7 @@ def __init__(self, cpm_model=None, subsolver=None, **kwargs):
         # for solving with assumption variables,
         self.assumption_dict = None
         self.objective_ = None
+        self.objective_is_min_ = True
 
         # initialise everything else and post the constraints/objective
         super().__init__(name="exact", cpm_model=cpm_model)
@@ -122,7 +123,7 @@ def native_model(self):
         """
         return self.xct_solver
 
-    def _fillObjAndVars(self):
+    def _fillVars(self):
         if not self.xct_solver.hasSolution():
             self.objective_value_ = None
             for cpm_var in self.user_vars:
@@ -135,9 +136,6 @@ def _fillObjAndVars(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
 
-        # translate objective
-        self.objective_value_ = self.xct_solver.getBestSoFar() # last upper bound to the objective
-
     def solve(self, time_limit=None, assumptions=None, **kwargs):
         """
             Call Exact
@@ -177,8 +175,8 @@ def solve(self, time_limit=None, assumptions=None, **kwargs):
 
         # call the solver, with parameters
         start = time.time()
-        my_status = self.xct_solver.runFull(optimize=self.has_objective(),
-                                            timeout=time_limit if time_limit is not None else 0)
+        my_status, obj_val = self.xct_solver.toOptimum(timeout=time_limit if time_limit is not None else 0)
+        #                                     timeout=time_limit if time_limit is not None else 0)
         end = time.time()
 
         # new status, translate runtime
@@ -201,7 +199,13 @@ def solve(self, time_limit=None, assumptions=None, **kwargs):
         else:
             raise NotImplementedError(my_status)  # a new status type was introduced, please report on github
 
-        self._fillObjAndVars()
+        self._fillVars()
+        if self.has_objective():
+            if self.objective_is_min_:
+                self.objective_value_ = obj_val
+            else: # maximize, so actually negative value
+                self.objective_value_ = -obj_val
+
 
         # True/False depending on self.cpm_status
         return self._solve_return(self.cpm_status)
@@ -237,7 +241,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
 
             (my_status, objval) = self.xct_solver.toOptimum(timelim) # fix the solution to the optimal objective
             if my_status == "UNSAT": # found unsatisfiability
-                self._fillObjAndVars() # erases the solution
+                self._fillVars() # erases the solution
                 return 0
             elif my_status == "INCONSISTENT": # found inconsistency
                 raise ValueError("Error: inconsistency during solveAll should not happen, please warn the developers of this bug")
@@ -253,14 +257,14 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from
             my_status = self.xct_solver.runFull(optimize=False, timeout=timelim)
             assert my_status in ["UNSAT","SAT","INCONSISTENT","TIMEOUT"], "Unexpected status code for Exact: " + my_status
             if my_status == "UNSAT": # found unsatisfiability
-                self._fillObjAndVars() # erases the solution
+                self._fillVars() # erases the solution
                 return solsfound
             elif my_status == "SAT": # found solution, but not optimality proven
                 assert self.xct_solver.hasSolution()
                 solsfound += 1
                 self.xct_solver.invalidateLastSol() # TODO: pass user vars to this function
                 if display is not None:
-                    self._fillObjAndVars()
+                    self._fillVars()
                     if isinstance(display, Expression):
                         print(argval(display))
                     elif isinstance(display, list):
@@ -322,6 +326,7 @@ def objective(self, expr, minimize):
 
         """
         self.objective_ = expr
+        self.objective_is_min_ = minimize
 
         # make objective function non-nested
         (flat_obj, flat_cons) = flatten_objective(expr)

tests/test_solvers.py

@@ -11,7 +11,8 @@
 from cpmpy.solvers.choco import CPM_choco
 
 
-from cpmpy.exceptions import MinizincNameException
+from cpmpy.exceptions import MinizincNameException, NotSupportedError
+
 
 class TestSolvers(unittest.TestCase):
     def test_installed_solvers(self):
@@ -707,3 +708,53 @@ def test_count_mzn(self):
 
         m = cp.Model([x + y == 2, wsum == 9])
         self.assertTrue(m.solve(solver="minizinc"))
+
+    def test_incremental(self):
+
+        x,y,z = cp.boolvar(shape=3, name="x")
+        for solver, cls in cp.SolverLookup.base_solvers():
+            if cls.supported() is False:
+                continue
+            s = cp.SolverLookup.get(solver)
+            s += [x]
+            s += [y | z]
+            self.assertTrue(s.solve())
+            self.assertTrue(x.value(), (y | z).value())
+            s += ~y | ~z
+            self.assertTrue(s.solve())
+            self.assertTrue(x.value())
+            self.assertEqual(y.value() + z.value(), 1)
+
+    def test_incremental_objective(self):
+
+        x = cp.intvar(0,10,shape=3)
+        for solver, cls in cp.SolverLookup.base_solvers():
+            if solver == "choco":
+                """
+                Choco does not support first optimizing and then adding a constraint.
+                During optimization, additional constraints get added to the solver,
+                which removes feasible solutions.
+                No straightforward way to resolve this for now.
+                """
+                continue
+            if cls.supported() is False:
+                continue
+            s = cp.SolverLookup.get(solver)
+            try:
+                s.minimize(cp.sum(x))
+            except (NotSupportedError, NotImplementedError): # solver does not support optimization
+                continue
+            self.assertTrue(s.solve())
+            self.assertEqual(s.objective_value(), 0)
+            s += x[0] == 5
+            self.assertTrue(s.solve())
+            self.assertEqual(s.objective_value(), 5)
+            s.maximize(cp.sum(x))
+            self.assertTrue(s.solve())
+            self.assertEqual(s.objective_value(), 25)
+
+
+
+
+
+