diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 02999991d..e9d624cae 100644 --- a/cpmpy/solvers/exact.py +++ b/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) diff --git a/tests/test_solvers.py b/tests/test_solvers.py index 55108c91d..a7f8a4146 100644 --- a/tests/test_solvers.py +++ b/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) + + + + + +