From f34676f13da76fbd7e5b15ec53a0e5247f0c7eec Mon Sep 17 00:00:00 2001 From: ThomSerg Date: Mon, 3 Nov 2025 14:26:01 +0100 Subject: [PATCH] Negate maximisation objective --- cpmpy/solvers/z3.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index fa549b694..3451583d3 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -249,7 +249,9 @@ def solve(self, time_limit=None, assumptions=[], **kwargs): # translate objective, for optimisation problems only if self.has_objective(): obj = self.z3_solver.objectives()[0] - self.objective_value_ = sol.evaluate(obj).as_long() + self.objective_value_ = sol.evaluate(obj).as_long() + if not self._minimize: + self.objective_value_ = -1*self.objective_value_ # Z3 negates the objective function to turn a maximisation problem into a minimisation one, undoing negation here else: # clear values of variables for cpm_var in self.user_vars: @@ -318,8 +320,10 @@ def objective(self, expr, minimize=True): obj = self._z3_expr(expr) if minimize: self.obj_handle = self.z3_solver.minimize(obj) + self._minimize = True # record direction of optimisation else: self.obj_handle = self.z3_solver.maximize(obj) + self._minimize = False # record direction of optimisation def transform(self, cpm_expr):