From e65629787623f780b4d072c5655f4d3c145f520d Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 16:07:48 +0100 Subject: [PATCH 01/13] feat(pumpkin-solver-py): Add incrementality to python interface We have to annotate `Model` as `unsendable`, which means the python script will crash if the interpreter moves the object between threads. It remains to be seen whether this happens in practice, and if so, we will need to engineer our way around it. --- pumpkin-crates/core/src/api/solver.rs | 13 + .../src/constraints/arguments.rs | 17 +- pumpkin-solver-py/src/constraints/globals.rs | 6 +- pumpkin-solver-py/src/constraints/mod.rs | 6 +- pumpkin-solver-py/src/model.rs | 398 ++++-------------- pumpkin-solver-py/src/result.rs | 22 +- pumpkin-solver-py/src/variables.rs | 152 +------ 7 files changed, 137 insertions(+), 477 deletions(-) diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index f05cb13a6..457350d3e 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -211,6 +211,19 @@ impl Solver { .create_new_literal_for_predicate(predicate, None, constraint_tag) } + pub fn new_named_literal_for_predicate( + &mut self, + predicate: Predicate, + constraint_tag: ConstraintTag, + name: impl Into, + ) -> Literal { + self.satisfaction_solver.create_new_literal_for_predicate( + predicate, + Some(name.into()), + constraint_tag, + ) + } + /// Create a fresh propositional variable with a given name and return the literal with positive /// polarity. /// diff --git a/pumpkin-solver-py/src/constraints/arguments.rs b/pumpkin-solver-py/src/constraints/arguments.rs index 468bef3fb..a56047e47 100644 --- a/pumpkin-solver-py/src/constraints/arguments.rs +++ b/pumpkin-solver-py/src/constraints/arguments.rs @@ -4,35 +4,34 @@ use pumpkin_solver::variables::Literal; use crate::variables::BoolExpression; use crate::variables::IntExpression; -use crate::variables::VariableMap; /// Trait which helps to convert Python API types to the solver types when creating constraints. pub trait PythonConstraintArg { type Output; - fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output; + fn to_solver_constraint_argument(self) -> Self::Output; } impl PythonConstraintArg for IntExpression { type Output = AffineView; - fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output { - self.to_affine_view(variable_map) + fn to_solver_constraint_argument(self) -> Self::Output { + self.0 } } impl PythonConstraintArg for BoolExpression { type Output = Literal; - fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output { - self.to_literal(variable_map) + fn to_solver_constraint_argument(self) -> Self::Output { + self.0 } } impl PythonConstraintArg for i32 { type Output = i32; - fn to_solver_constraint_argument(self, _: &VariableMap) -> Self::Output { + fn to_solver_constraint_argument(self) -> Self::Output { self } } @@ -40,9 +39,9 @@ impl PythonConstraintArg for i32 { impl PythonConstraintArg for Vec { type Output = Vec; - fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output { + fn to_solver_constraint_argument(self) -> Self::Output { self.into_iter() - .map(|arg| arg.to_solver_constraint_argument(variable_map)) + .map(|arg| arg.to_solver_constraint_argument()) .collect() } } diff --git a/pumpkin-solver-py/src/constraints/globals.rs b/pumpkin-solver-py/src/constraints/globals.rs index ab553579a..5ef8e34b7 100644 --- a/pumpkin-solver-py/src/constraints/globals.rs +++ b/pumpkin-solver-py/src/constraints/globals.rs @@ -30,10 +30,9 @@ macro_rules! python_constraint { pub fn post( self, solver: &mut pumpkin_solver::Solver, - variable_map: &VariableMap, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { constraints::$constraint_func( - $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field, variable_map)),+ , + $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ , self.constraint_tag.0, ).post(solver) } @@ -42,10 +41,9 @@ macro_rules! python_constraint { self, solver: &mut pumpkin_solver::Solver, reification_literal: pumpkin_solver::variables::Literal, - variable_map: &VariableMap, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { constraints::$constraint_func( - $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field, variable_map)),+ , + $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ , self.constraint_tag.0, ).implied_by(solver, reification_literal) } diff --git a/pumpkin-solver-py/src/constraints/mod.rs b/pumpkin-solver-py/src/constraints/mod.rs index ec8080366..7dd1242e1 100644 --- a/pumpkin-solver-py/src/constraints/mod.rs +++ b/pumpkin-solver-py/src/constraints/mod.rs @@ -15,10 +15,9 @@ macro_rules! declare_constraints { pub fn post( self, solver: &mut pumpkin_solver::Solver, - variable_map: &$crate::variables::VariableMap, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { match self { - $($name::$constraint(cns) => cns.post(solver, variable_map)),+ + $($name::$constraint(cns) => cns.post(solver)),+ } } @@ -26,10 +25,9 @@ macro_rules! declare_constraints { self, solver: &mut pumpkin_solver::Solver, reification_literal: pumpkin_solver::variables::Literal, - variable_map: &$crate::variables::VariableMap, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { match self { - $($name::$constraint(cns) => cns.implied_by(solver, reification_literal, variable_map)),+ + $($name::$constraint(cns) => cns.implied_by(solver, reification_literal)),+ } } } diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 0173cf222..c6bad702a 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -3,11 +3,8 @@ use std::path::PathBuf; use std::time::Duration; use std::time::Instant; -use pumpkin_solver::ConstraintOperationError; use pumpkin_solver::DefaultBrancher; use pumpkin_solver::Solver; -use pumpkin_solver::containers::KeyGenerator; -use pumpkin_solver::containers::KeyedVec; use pumpkin_solver::containers::StorageKey; use pumpkin_solver::optimisation::OptimisationDirection; use pumpkin_solver::optimisation::linear_sat_unsat::LinearSatUnsat; @@ -20,8 +17,7 @@ use pumpkin_solver::results::SolutionReference; use pumpkin_solver::termination::Indefinite; use pumpkin_solver::termination::TerminationCondition; use pumpkin_solver::termination::TimeBudget; -use pumpkin_solver::variables::DomainId; -use pumpkin_solver::variables::Literal; +use pyo3::exceptions::PyRuntimeError; use pyo3::prelude::*; use crate::constraints::Constraint; @@ -32,19 +28,13 @@ use crate::result::SatisfactionResult; use crate::result::SatisfactionUnderAssumptionsResult; use crate::result::Solution; use crate::variables::BoolExpression; -use crate::variables::BoolVariable; use crate::variables::IntExpression; -use crate::variables::IntVariable; use crate::variables::Predicate; -use crate::variables::VariableMap; -#[pyclass] -#[derive(Default)] +#[pyclass(unsendable)] pub struct Model { - integer_variables: KeyedVec, - boolean_variables: KeyedVec, - constraints: Vec, - tags: KeyGenerator, + solver: Solver, + brancher: DefaultBrancher, } #[pyclass] @@ -72,8 +62,22 @@ impl StorageKey for Tag { #[pymethods] impl Model { #[new] - fn new() -> Model { - Model::default() + #[pyo3(signature = (proof=None))] + fn new(proof: Option) -> PyResult { + let proof_log = proof + .map(|path| ProofLog::cp(&path, true)) + .transpose() + .map(|proof| proof.unwrap_or_default())?; + + let options = SolverOptions { + proof_log, + ..Default::default() + }; + + let solver = Solver::with_options(options); + let brancher = solver.default_brancher(); + + Ok(Model { solver, brancher }) } /// Create a new integer variable. @@ -84,30 +88,30 @@ impl Model { upper_bound: i32, name: Option<&str>, ) -> IntExpression { - let variable = ModelIntVar { - lower_bound, - upper_bound, - name: name.map(|n| n.to_owned()), - }; - - self.integer_variables.push(variable).into() + if let Some(name) = name { + self.solver + .new_named_bounded_integer(lower_bound, upper_bound, name) + .into() + } else { + self.solver + .new_bounded_integer(lower_bound, upper_bound) + .into() + } } /// Create a new boolean variable. #[pyo3(signature = (name=None))] fn new_boolean_variable(&mut self, name: Option<&str>) -> BoolExpression { - self.boolean_variables - .push(ModelBoolVar { - name: name.map(|n| n.to_owned()), - integer_equivalent: None, - predicate: None, - }) - .into() + if let Some(name) = name { + self.solver.new_named_literal(name).into() + } else { + self.solver.new_literal().into() + } } /// Create a new constraint tag. fn new_constraint_tag(&mut self) -> Tag { - self.tags.next_key() + Tag(self.solver.new_constraint_tag()) } /// Get an integer variable for the given boolean. @@ -116,40 +120,17 @@ impl Model { /// /// A tag should be provided for this link to be identifiable in the proof. fn boolean_as_integer(&mut self, boolean: BoolExpression, tag: Tag) -> IntExpression { - let bool_variable = boolean.get_variable(); - - let int_variable = match self.boolean_variables[bool_variable] { - // If there is already an integer associated with the boolean variable, don't create a - // new one. - ModelBoolVar { - integer_equivalent: Some((existing_equivalent, _)), - .. - } => existing_equivalent, - - // Create a new integer variable which is equivalent to this boolean variable. - ModelBoolVar { - ref name, - integer_equivalent: None, - .. - } => self.integer_variables.push(ModelIntVar { - lower_bound: 0, - upper_bound: 1, - name: name.clone(), - }), - }; + let new_domain = self.solver.new_bounded_integer(0, 1); + let boolean_true = boolean.0.get_true_predicate(); - // Link the integer variable to the boolean variable. - self.boolean_variables[bool_variable].integer_equivalent = Some((int_variable, tag)); + self.solver + .add_clause([predicate![new_domain != 1], boolean_true], tag.0) + .expect("created a new domain so this should never cause an empty domain"); + self.solver + .add_clause([!boolean_true, predicate![new_domain == 1]], tag.0) + .expect("created a new domain so this should never cause an empty domain"); - // Convert the integer variable to an appropriate integer expression based on the polarity - // of the boolean expression. - let polarity = boolean.get_polarity(); - - IntExpression { - variable: int_variable, - offset: if polarity { 0 } else { 1 }, - scale: if polarity { 1 } else { -1 }, - } + IntExpression::from(new_domain) } /// Reify a predicate as an explicit boolean expression. @@ -162,52 +143,43 @@ impl Model { tag: Tag, name: Option<&str>, ) -> BoolExpression { - self.boolean_variables - .push(ModelBoolVar { - name: name.map(|n| n.to_owned()), - integer_equivalent: None, - predicate: Some((predicate, tag)), - }) - .into() + let solver_predicate = predicate.into_solver_predicate(); + let Tag(tag) = tag; + + if let Some(name) = name { + self.solver + .new_named_literal_for_predicate(solver_predicate, tag, name) + .into() + } else { + self.solver + .new_literal_for_predicate(solver_predicate, tag) + .into() + } } /// Add the given constraint to the model. #[pyo3(signature = (constraint))] - fn add_constraint(&mut self, constraint: Constraint) { - self.constraints.push(ModelConstraint { - constraint, - premise: None, - }); + fn add_constraint(&mut self, constraint: Constraint) -> PyResult<()> { + constraint + .post(&mut self.solver) + .map_err(|_| PyRuntimeError::new_err("inconsistency detected")) } /// Add `premise -> constraint` to the model. #[pyo3(signature = (constraint, premise))] - fn add_implication(&mut self, constraint: Constraint, premise: BoolExpression) { - self.constraints.push(ModelConstraint { - constraint, - premise: Some(premise), - }); + fn add_implication(&mut self, constraint: Constraint, premise: BoolExpression) -> PyResult<()> { + constraint + .implied_by(&mut self.solver, premise.0) + .map_err(|_| PyRuntimeError::new_err("inconsistency detected")) } - #[pyo3(signature = (timeout=None,proof=None))] - fn satisfy(&mut self, timeout: Option, proof: Option) -> SatisfactionResult { - let end_time = timeout.map(|secs| Instant::now() + Duration::from_secs_f32(secs)); + #[pyo3(signature = (timeout=None))] + fn satisfy(&mut self, timeout: Option) -> SatisfactionResult { + let mut termination = get_termination(timeout); - let solver_setup = self.create_solver(proof); - - let Ok((mut solver, variable_map)) = solver_setup else { - return SatisfactionResult::Unsatisfiable(); - }; - - let mut brancher = solver.default_brancher(); - let mut termination = get_termination(end_time); - - match solver.satisfy(&mut brancher, &mut termination) { + match self.solver.satisfy(&mut self.brancher, &mut termination) { pumpkin_solver::results::SatisfactionResult::Satisfiable(satisfiable) => { - SatisfactionResult::Satisfiable(Solution { - solver_solution: satisfiable.solution().into(), - variable_map, - }) + SatisfactionResult::Satisfiable(Solution::from(satisfiable.solution())) } pumpkin_solver::results::SatisfactionResult::Unsatisfiable(_, _) => { SatisfactionResult::Unsatisfiable() @@ -224,27 +196,16 @@ impl Model { assumptions: Vec, timeout: Option, ) -> SatisfactionUnderAssumptionsResult { - let end_time = timeout.map(|secs| Instant::now() + Duration::from_secs_f32(secs)); - let solver_setup = self.create_solver(None); - - let Ok((mut solver, variable_map)) = solver_setup else { - return SatisfactionUnderAssumptionsResult::Unsatisfiable(); - }; - - let mut brancher = solver.default_brancher(); - let mut termination = get_termination(end_time); + let mut termination = get_termination(timeout); let solver_assumptions = assumptions .iter() - .map(|pred| pred.to_solver_predicate(&variable_map)) + .map(|pred| pred.into_solver_predicate()) .collect::>(); - match solver.satisfy_under_assumptions(&mut brancher, &mut termination, &solver_assumptions) { + match self.solver.satisfy_under_assumptions(&mut self.brancher, &mut termination, &solver_assumptions) { pumpkin_solver::results::SatisfactionResultUnderAssumptions::Satisfiable(satisfiable) => { - SatisfactionUnderAssumptionsResult::Satisfiable(Solution { - solver_solution: satisfiable.solution().into(), - variable_map, - }) + SatisfactionUnderAssumptionsResult::Satisfiable(satisfiable.solution().into()) } pumpkin_solver::results::SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(mut result) => { // Maarten: For now we assume that the core _must_ consist of the predicates that @@ -261,7 +222,7 @@ impl Model { .iter() .map(|predicate| assumptions .iter() - .find(|pred| pred.to_solver_predicate(&variable_map) == *predicate) + .find(|pred| pred.into_solver_predicate() == *predicate) .copied() .expect("predicates in core must be part of the assumptions")) .collect(); @@ -277,42 +238,33 @@ impl Model { } } - #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, proof=None, timeout=None))] + #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None))] fn optimise( &mut self, objective: IntExpression, optimiser: Optimiser, direction: Direction, - proof: Option, timeout: Option, ) -> OptimisationResult { - let end_time = timeout.map(|secs| Instant::now() + Duration::from_secs_f32(secs)); - let solver_setup = self.create_solver(proof); - - let Ok((mut solver, variable_map)) = solver_setup else { - return OptimisationResult::Unsatisfiable(); - }; - - let mut brancher = solver.default_brancher(); - let mut termination = get_termination(end_time); + let mut termination = get_termination(timeout); let direction = match direction { Direction::Minimise => OptimisationDirection::Minimise, Direction::Maximise => OptimisationDirection::Maximise, }; - let objective = objective.to_affine_view(&variable_map); + let objective = objective.0; let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {}; let result = match optimiser { - Optimiser::LinearSatUnsat => solver.optimise( - &mut brancher, + Optimiser::LinearSatUnsat => self.solver.optimise( + &mut self.brancher, &mut termination, LinearSatUnsat::new(direction, objective, callback), ), - Optimiser::LinearUnsatSat => solver.optimise( - &mut brancher, + Optimiser::LinearUnsatSat => self.solver.optimise( + &mut self.brancher, &mut termination, LinearUnsatSat::new(direction, objective, callback), ), @@ -320,16 +272,10 @@ impl Model { match result { pumpkin_solver::results::OptimisationResult::Satisfiable(solution) => { - OptimisationResult::Satisfiable(Solution { - solver_solution: solution, - variable_map, - }) + OptimisationResult::Satisfiable(solution.into()) } pumpkin_solver::results::OptimisationResult::Optimal(solution) => { - OptimisationResult::Optimal(Solution { - solver_solution: solution, - variable_map, - }) + OptimisationResult::Optimal(solution.into()) } pumpkin_solver::results::OptimisationResult::Unsatisfiable => { OptimisationResult::Unsatisfiable() @@ -339,186 +285,12 @@ impl Model { } } -fn get_termination(end_time: Option) -> Box { +fn get_termination(end_time: Option) -> Box { end_time + .map(|secs| Instant::now() + Duration::from_secs_f32(secs)) .map(|end_time| end_time - Instant::now()) .map(|duration| { Box::new(TimeBudget::starting_now(duration)) as Box }) .unwrap_or(Box::new(Indefinite)) } - -impl Model { - fn create_variable_map( - &self, - solver: &mut Solver, - ) -> Result { - let mut map = VariableMap::default(); - - for model_int_var in self.integer_variables.iter() { - let _ = map - .integers - .push(model_int_var.create_domain(solver).into()); - } - - for model_bool_var in self.boolean_variables.iter() { - let _ = map - .booleans - .push(model_bool_var.create_literal(solver, &map)?); - } - - Ok(map) - } - - fn post_constraints( - &self, - solver: &mut Solver, - variable_map: &VariableMap, - ) -> Result<(), ConstraintOperationError> { - for constraint in self.constraints.iter() { - let ModelConstraint { - constraint, - premise, - } = constraint.clone(); - - if let Some(premise) = premise { - constraint.implied_by(solver, premise.to_literal(variable_map), variable_map)?; - } else { - constraint.post(solver, variable_map)?; - } - } - - Ok(()) - } - - fn create_solver( - &mut self, - proof: Option, - ) -> Result<(Solver, VariableMap), ConstraintOperationError> { - let is_logging_proof = proof.is_some(); - - let proof_log = proof - .map(|path| ProofLog::cp(&path, true)) - .transpose() - .map(|proof| proof.unwrap_or_default()) - .expect("failed to create proof file"); - - let options = SolverOptions { - proof_log, - ..Default::default() - }; - - let mut solver = Solver::with_options(options); - - let variable_map = self - .create_variable_map(&mut solver) - .and_then(|variable_map| { - self.post_constraints(&mut solver, &variable_map)?; - Ok(variable_map) - })?; - - if is_logging_proof { - // Reserve the constraint tags that have been allocated in the model. - let max_tag = self.new_constraint_tag(); - loop { - let next_solver_tag = solver.new_constraint_tag(); - if NonZero::from(next_solver_tag) >= NonZero::from(max_tag.0) { - break; - } - } - } - - Ok((solver, variable_map)) - } -} - -#[derive(Clone)] -struct ModelConstraint { - constraint: Constraint, - premise: Option, -} - -struct ModelIntVar { - lower_bound: i32, - upper_bound: i32, - name: Option, -} - -impl ModelIntVar { - fn create_domain(&self, solver: &mut Solver) -> DomainId { - match self.name { - Some(ref name) => { - solver.new_named_bounded_integer(self.lower_bound, self.upper_bound, name) - } - - None => solver.new_bounded_integer(self.lower_bound, self.upper_bound), - } - } -} - -struct ModelBoolVar { - name: Option, - /// If present, this is the 0-1 integer variable which is 1 if this boolean is `true`, and - /// 0 if this boolean is `false`. The `Tag` is the [`ConstraintTag`] which is used in the proof - /// log to maintain the consistency. - integer_equivalent: Option<(IntVariable, Tag)>, - /// If present, this boolean is true iff the predicate holds. The `Tag` is the - /// [`ConstraintTag`] which is used in the proof log to maintain the consistency between - /// the boolean and the predicate. - predicate: Option<(Predicate, Tag)>, -} - -impl ModelBoolVar { - /// Convert a boolean variable to a solver literal. - fn create_literal( - &self, - solver: &mut Solver, - variable_map: &VariableMap, - ) -> Result { - let literal = match self { - ModelBoolVar { - integer_equivalent: Some((int_var, tag_for_int)), - predicate: Some((predicate, tag_for_predicate)), - .. - } => { - // In case the boolean corresponds to both a predicate and a 0-1 integer, we have to - // enforce equality between the integer variable and the truth of the predicate. - - let affine_view = variable_map.get_integer(*int_var); - let int_eq_1 = predicate![affine_view == 1]; - - let predicate_literal = predicate.to_solver_predicate(variable_map); - - solver.add_clause([!predicate_literal, int_eq_1], tag_for_int.0)?; - solver.add_clause([predicate_literal, !int_eq_1], tag_for_int.0)?; - - solver.new_literal_for_predicate(int_eq_1, tag_for_predicate.0) - } - - ModelBoolVar { - integer_equivalent: Some((int_var, tag)), - predicate: None, - .. - } => { - let affine_view = variable_map.get_integer(*int_var); - solver.new_literal_for_predicate(predicate![affine_view == 1], tag.0) - } - - ModelBoolVar { - predicate: Some((predicate, tag)), - integer_equivalent: None, - .. - } => { - solver.new_literal_for_predicate(predicate.to_solver_predicate(variable_map), tag.0) - } - - ModelBoolVar { - name: Some(name), .. - } => solver.new_named_literal(name), - - ModelBoolVar { name: None, .. } => solver.new_literal(), - }; - - Ok(literal) - } -} diff --git a/pumpkin-solver-py/src/result.rs b/pumpkin-solver-py/src/result.rs index fc4653ae2..289985287 100644 --- a/pumpkin-solver-py/src/result.rs +++ b/pumpkin-solver-py/src/result.rs @@ -4,7 +4,6 @@ use pyo3::prelude::*; use crate::variables::BoolExpression; use crate::variables::IntExpression; use crate::variables::Predicate; -use crate::variables::VariableMap; #[pyclass] #[allow(clippy::large_enum_variant)] @@ -25,21 +24,28 @@ pub enum SatisfactionUnderAssumptionsResult { #[pyclass] #[derive(Clone)] -pub struct Solution { - pub solver_solution: pumpkin_solver::results::Solution, - pub variable_map: VariableMap, +pub struct Solution(pumpkin_solver::results::Solution); + +impl From for Solution { + fn from(value: pumpkin_solver::results::Solution) -> Self { + Solution(value) + } +} + +impl From> for Solution { + fn from(value: pumpkin_solver::results::SolutionReference<'_>) -> Self { + Solution(value.into()) + } } #[pymethods] impl Solution { fn int_value(&self, variable: IntExpression) -> i32 { - self.solver_solution - .get_integer_value(variable.to_affine_view(&self.variable_map)) + self.0.get_integer_value(variable.0) } fn bool_value(&self, variable: BoolExpression) -> bool { - self.solver_solution - .get_literal_value(variable.to_literal(&self.variable_map)) + self.0.get_literal_value(variable.0) } } diff --git a/pumpkin-solver-py/src/variables.rs b/pumpkin-solver-py/src/variables.rs index 77caa54f3..e9d5f2960 100644 --- a/pumpkin-solver-py/src/variables.rs +++ b/pumpkin-solver-py/src/variables.rs @@ -1,86 +1,26 @@ -use pumpkin_solver::containers::KeyedVec; -use pumpkin_solver::containers::StorageKey; use pumpkin_solver::predicate; use pumpkin_solver::variables::AffineView; use pumpkin_solver::variables::DomainId; use pumpkin_solver::variables::Literal; -use pumpkin_solver::variables::TransformableVariable; use pyo3::prelude::*; -#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)] -pub struct IntVariable(usize); - -impl StorageKey for IntVariable { - fn index(&self) -> usize { - self.0 - } - - fn create_from_index(index: usize) -> Self { - IntVariable(index) - } -} - #[pyclass(eq, hash, frozen)] -#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)] -pub struct IntExpression { - pub variable: IntVariable, - pub offset: i32, - pub scale: i32, -} - -impl From for IntExpression { - fn from(variable: IntVariable) -> Self { - IntExpression { - variable, - offset: 0, - scale: 1, - } - } -} - -impl IntExpression { - pub fn to_affine_view(self, variable_map: &VariableMap) -> AffineView { - let IntExpression { - variable, - offset, - scale, - } = self; +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct IntExpression(pub AffineView); - variable_map - .get_integer(variable) - .scaled(scale) - .offset(offset) +impl From for IntExpression { + fn from(domain_id: DomainId) -> IntExpression { + IntExpression(domain_id.into()) } } -#[pymethods] -impl IntExpression { - fn offset(&self, add_offset: i32) -> IntExpression { - let IntExpression { - variable, - offset, - scale, - } = *self; - - IntExpression { - variable, - offset: offset + add_offset, - scale, - } - } - - fn scaled(&self, scaling: i32) -> IntExpression { - let IntExpression { - variable, - offset, - scale, - } = *self; +#[pyclass(eq, hash, frozen)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct BoolExpression(pub Literal); - IntExpression { - variable, - offset: offset * scaling, - scale: scale * scaling, - } +impl From for BoolExpression { + fn from(literal: Literal) -> BoolExpression { + BoolExpression(literal) } } @@ -114,12 +54,8 @@ impl Predicate { } impl Predicate { - /// Convert the predicate in the model domain to a predicate in the solver domain. - pub(crate) fn to_solver_predicate( - self, - variable_map: &VariableMap, - ) -> pumpkin_solver::predicates::Predicate { - let affine_view = self.variable.to_affine_view(variable_map); + pub(crate) fn into_solver_predicate(self) -> pumpkin_solver::predicates::Predicate { + let affine_view = self.variable.0; match self.comparator { Comparator::NotEqual => predicate![affine_view != self.value], @@ -129,65 +65,3 @@ impl Predicate { } } } - -#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq)] -pub struct BoolVariable(usize); - -impl StorageKey for BoolVariable { - fn index(&self) -> usize { - self.0 - } - - fn create_from_index(index: usize) -> Self { - BoolVariable(index) - } -} - -#[pyclass(eq)] -#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq)] -pub struct BoolExpression(BoolVariable, bool); - -impl From for BoolExpression { - fn from(value: BoolVariable) -> Self { - BoolExpression(value, true) - } -} - -impl BoolExpression { - pub fn get_polarity(self) -> bool { - self.1 - } - - pub fn get_variable(self) -> BoolVariable { - self.0 - } - - pub fn to_literal(self, variable_map: &VariableMap) -> Literal { - let literal = variable_map.get_boolean(self.0); - - if self.1 { literal } else { !literal } - } -} - -#[pymethods] -impl BoolExpression { - pub fn negate(&self) -> Self { - BoolExpression(self.0, !self.1) - } -} - -#[derive(Clone, Default)] -pub struct VariableMap { - pub integers: KeyedVec>, - pub booleans: KeyedVec, -} - -impl VariableMap { - pub fn get_integer(&self, variable: IntVariable) -> AffineView { - self.integers[variable] - } - - pub fn get_boolean(&self, variable: BoolVariable) -> Literal { - self.booleans[variable] - } -} From 2b24b7589bd70b14b51da4f90f8297daf58e3882 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 16:13:49 +0100 Subject: [PATCH 02/13] fix: Re-add IntExpression::offset and IntExpression::scaled --- pumpkin-solver-py/src/variables.rs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/pumpkin-solver-py/src/variables.rs b/pumpkin-solver-py/src/variables.rs index e9d5f2960..5407a1df7 100644 --- a/pumpkin-solver-py/src/variables.rs +++ b/pumpkin-solver-py/src/variables.rs @@ -2,6 +2,7 @@ use pumpkin_solver::predicate; use pumpkin_solver::variables::AffineView; use pumpkin_solver::variables::DomainId; use pumpkin_solver::variables::Literal; +use pumpkin_solver::variables::TransformableVariable; use pyo3::prelude::*; #[pyclass(eq, hash, frozen)] @@ -14,6 +15,17 @@ impl From for IntExpression { } } +#[pymethods] +impl IntExpression { + fn offset(&self, add_offset: i32) -> IntExpression { + IntExpression(self.0.offset(add_offset)) + } + + fn scaled(&self, scaling: i32) -> IntExpression { + IntExpression(self.0.scaled(scaling)) + } +} + #[pyclass(eq, hash, frozen)] #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] pub struct BoolExpression(pub Literal); From 05ad4a2ace5cc5e07edcd39f304976417c9d5e0a Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 16:52:45 +0100 Subject: [PATCH 03/13] fix: Add new variables to the brancher --- .../branching/branchers/autonomous_search.rs | 4 +++ .../branching/variable_selection/random.rs | 5 ++++ pumpkin-solver-py/src/model.rs | 28 ++++++++++++------- 3 files changed, 27 insertions(+), 10 deletions(-) diff --git a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs index cb7628570..47a51f01a 100644 --- a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs +++ b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs @@ -135,6 +135,10 @@ impl DefaultBrancher { statistics: Default::default(), } } + + pub fn add_domain(&mut self, domain: DomainId) { + self.backup_brancher.variable_selector.add_domain(domain); + } } impl AutonomousSearch { diff --git a/pumpkin-crates/core/src/branching/variable_selection/random.rs b/pumpkin-crates/core/src/branching/variable_selection/random.rs index 703570cde..46a1c1627 100644 --- a/pumpkin-crates/core/src/branching/variable_selection/random.rs +++ b/pumpkin-crates/core/src/branching/variable_selection/random.rs @@ -20,6 +20,11 @@ impl RandomSelector { }), } } + + /// Add a domain to consideration in the variable selection. + pub fn add_domain(&mut self, domain: DomainId) { + self.variables.insert(domain); + } } impl VariableSelector for RandomSelector { diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index c6bad702a..31199bdc7 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -88,25 +88,31 @@ impl Model { upper_bound: i32, name: Option<&str>, ) -> IntExpression { - if let Some(name) = name { + let domain_id = if let Some(name) = name { self.solver .new_named_bounded_integer(lower_bound, upper_bound, name) - .into() } else { - self.solver - .new_bounded_integer(lower_bound, upper_bound) - .into() - } + self.solver.new_bounded_integer(lower_bound, upper_bound) + }; + + self.brancher.add_domain(domain_id); + + domain_id.into() } /// Create a new boolean variable. #[pyo3(signature = (name=None))] fn new_boolean_variable(&mut self, name: Option<&str>) -> BoolExpression { - if let Some(name) = name { - self.solver.new_named_literal(name).into() + let literal = if let Some(name) = name { + self.solver.new_named_literal(name) } else { - self.solver.new_literal().into() - } + self.solver.new_literal() + }; + + self.brancher + .add_domain(literal.get_true_predicate().get_domain()); + + literal.into() } /// Create a new constraint tag. @@ -121,6 +127,8 @@ impl Model { /// A tag should be provided for this link to be identifiable in the proof. fn boolean_as_integer(&mut self, boolean: BoolExpression, tag: Tag) -> IntExpression { let new_domain = self.solver.new_bounded_integer(0, 1); + self.brancher.add_domain(new_domain); + let boolean_true = boolean.0.get_true_predicate(); self.solver From 6e8d52046654508d9298d33a9f67f42c530681d1 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 17:28:26 +0100 Subject: [PATCH 04/13] Fix test constraints --- pumpkin-crates/core/src/api/solver.rs | 2 +- pumpkin-solver-py/tests/test_constraints.py | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index 457350d3e..d33dd991f 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -219,7 +219,7 @@ impl Solver { ) -> Literal { self.satisfaction_solver.create_new_literal_for_predicate( predicate, - Some(name.into()), + Some(name.into().into()), constraint_tag, ) } diff --git a/pumpkin-solver-py/tests/test_constraints.py b/pumpkin-solver-py/tests/test_constraints.py index 0901863a5..aee69e59f 100644 --- a/pumpkin-solver-py/tests/test_constraints.py +++ b/pumpkin-solver-py/tests/test_constraints.py @@ -182,7 +182,7 @@ def label(model, cons, name, scaled, bool): ) -LINEAR = list(generate_operators()) +LINEAR = list(generate_linear()) @pytest.mark.parametrize( @@ -222,9 +222,7 @@ def test_global(model, cons, name, scaled, bool): assert isinstance(res, pumpkin_solver.SatisfactionResult.Satisfiable) -ALL_EXPR = ( - list(generate_operators()) + list(generate_linear()) + list(generate_globals()) -) +ALL_EXPR = LINEAR + OPERATORS + GLOBALS @pytest.mark.parametrize( From 9def8f6570343ae5d5605e41139d565040363504 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 17:29:50 +0100 Subject: [PATCH 05/13] Re-add negation for booleans --- pumpkin-solver-py/src/variables.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/pumpkin-solver-py/src/variables.rs b/pumpkin-solver-py/src/variables.rs index 5407a1df7..d223d9650 100644 --- a/pumpkin-solver-py/src/variables.rs +++ b/pumpkin-solver-py/src/variables.rs @@ -30,6 +30,13 @@ impl IntExpression { #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] pub struct BoolExpression(pub Literal); +#[pymethods] +impl BoolExpression { + fn negate(&self) -> BoolExpression { + BoolExpression(!self.0) + } +} + impl From for BoolExpression { fn from(literal: Literal) -> BoolExpression { BoolExpression(literal) From be1d1d35cd71422922c49e1dc39e9a4c443a2768 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 16 Jan 2026 17:34:38 +0100 Subject: [PATCH 06/13] Force sendable in custom wrapper --- pumpkin-solver-py/src/model.rs | 64 +++++++++++++++++++++++++++++----- 1 file changed, 56 insertions(+), 8 deletions(-) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 31199bdc7..a107f999b 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -1,5 +1,8 @@ use std::num::NonZero; +use std::ops::Deref; +use std::ops::DerefMut; use std::path::PathBuf; +use std::thread::ThreadId; use std::time::Duration; use std::time::Instant; @@ -31,10 +34,10 @@ use crate::variables::BoolExpression; use crate::variables::IntExpression; use crate::variables::Predicate; -#[pyclass(unsendable)] +#[pyclass] pub struct Model { - solver: Solver, - brancher: DefaultBrancher, + solver: ThreadBound, + brancher: ThreadBound, } #[pyclass] @@ -77,7 +80,18 @@ impl Model { let solver = Solver::with_options(options); let brancher = solver.default_brancher(); - Ok(Model { solver, brancher }) + let owner = std::thread::current().id(); + + Ok(Model { + solver: ThreadBound { + value: solver, + owner, + }, + brancher: ThreadBound { + value: brancher, + owner, + }, + }) } /// Create a new integer variable. @@ -185,7 +199,10 @@ impl Model { fn satisfy(&mut self, timeout: Option) -> SatisfactionResult { let mut termination = get_termination(timeout); - match self.solver.satisfy(&mut self.brancher, &mut termination) { + match self + .solver + .satisfy(self.brancher.deref_mut(), &mut termination) + { pumpkin_solver::results::SatisfactionResult::Satisfiable(satisfiable) => { SatisfactionResult::Satisfiable(Solution::from(satisfiable.solution())) } @@ -211,7 +228,7 @@ impl Model { .map(|pred| pred.into_solver_predicate()) .collect::>(); - match self.solver.satisfy_under_assumptions(&mut self.brancher, &mut termination, &solver_assumptions) { + match self.solver.satisfy_under_assumptions(self.brancher.deref_mut(), &mut termination, &solver_assumptions) { pumpkin_solver::results::SatisfactionResultUnderAssumptions::Satisfiable(satisfiable) => { SatisfactionUnderAssumptionsResult::Satisfiable(satisfiable.solution().into()) } @@ -267,12 +284,12 @@ impl Model { let result = match optimiser { Optimiser::LinearSatUnsat => self.solver.optimise( - &mut self.brancher, + self.brancher.deref_mut(), &mut termination, LinearSatUnsat::new(direction, objective, callback), ), Optimiser::LinearUnsatSat => self.solver.optimise( - &mut self.brancher, + self.brancher.deref_mut(), &mut termination, LinearUnsatSat::new(direction, objective, callback), ), @@ -302,3 +319,34 @@ fn get_termination(end_time: Option) -> Box { }) .unwrap_or(Box::new(Indefinite)) } + +/// A wrapper around a type that is `!Send` that crashes if it is accessed by different threads. +struct ThreadBound { + value: T, + owner: ThreadId, +} + +unsafe impl Send for ThreadBound {} +unsafe impl Sync for ThreadBound {} + +impl Deref for ThreadBound { + type Target = T; + + fn deref(&self) -> &Self::Target { + if std::thread::current().id() != self.owner { + panic!("Accessing non-send value from multiple threads"); + } + + &self.value + } +} + +impl DerefMut for ThreadBound { + fn deref_mut(&mut self) -> &mut Self::Target { + if std::thread::current().id() != self.owner { + panic!("Accessing non-send value from multiple threads"); + } + + &mut self.value + } +} From 639fa8c82758cc3b87876f92f5213419aaeab759 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 17 Jan 2026 09:42:26 +0100 Subject: [PATCH 07/13] Remove custom threadbound wrapper --- pumpkin-solver-py/src/model.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 7eaa73901..f8e596372 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -1,8 +1,5 @@ use std::num::NonZero; -use std::ops::Deref; -use std::ops::DerefMut; use std::path::PathBuf; -use std::thread::ThreadId; use std::time::Duration; use std::time::Instant; From 4ed3c59e1da4a1d2c2f95e67573bc1cf5561613e Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 18 Jan 2026 10:29:27 +0100 Subject: [PATCH 08/13] feat(pumpkin-solver-py): Implement warm starting for optimisation problems --- pumpkin-solver-py/src/model.rs | 65 +++++++++++++++++++++++++++------- 1 file changed, 53 insertions(+), 12 deletions(-) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index f8e596372..3537da570 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -5,6 +5,9 @@ use std::time::Instant; use pumpkin_solver::DefaultBrancher; use pumpkin_solver::Solver; +use pumpkin_solver::branching::branchers::dynamic_brancher::DynamicBrancher; +use pumpkin_solver::branching::branchers::warm_start::WarmStart; +use pumpkin_solver::containers::HashMap; use pumpkin_solver::containers::StorageKey; use pumpkin_solver::optimisation::OptimisationDirection; use pumpkin_solver::optimisation::linear_sat_unsat::LinearSatUnsat; @@ -253,7 +256,17 @@ impl Model { } } - #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None, on_solution=None))] + /// Solve the model to optimality. + /// + /// Resets any incremental state in the stored brancher, but it is unlikely that the Model can + /// be used in an incremental fashion after this call. + #[pyo3(signature = ( + objective, + optimiser=Optimiser::LinearSatUnsat, + direction=Direction::Minimise, + timeout=None, + warm_start=HashMap::default(), + ))] fn optimise( &mut self, py: Python<'_>, @@ -261,7 +274,7 @@ impl Model { optimiser: Optimiser, direction: Direction, timeout: Option, - on_solution: Option>, + warm_start: HashMap, ) -> OptimisationResult { let mut termination = get_termination(timeout); @@ -272,24 +285,18 @@ impl Model { let objective = objective.0; - let callback = move |_: &Solver, solution: SolutionReference<'_>, _: &DefaultBrancher| { - let python_solution = crate::result::Solution::from(solution); + let callback: fn(&Solver, SolutionReference, &DynamicBrancher) = |_, _, _| {}; - if let Some(on_solution_callback) = on_solution.as_ref() { - let _ = on_solution_callback - .call(py, (python_solution,), None) - .expect("failed to call solution callback"); - } - }; + let mut brancher = self.create_warm_started_brancher(warm_start); let result = match optimiser { Optimiser::LinearSatUnsat => self.solver.optimise( - &mut self.brancher, + &mut brancher, &mut termination, LinearSatUnsat::new(direction, objective, callback), ), Optimiser::LinearUnsatSat => self.solver.optimise( - &mut self.brancher, + &mut brancher, &mut termination, LinearUnsatSat::new(direction, objective, callback), ), @@ -310,6 +317,40 @@ impl Model { } } +impl Model { + /// Create a brancher that is warm started with the given assignment. + /// + /// This resets the [`DefaultBrancher`] on self, so any knowledge on previous incremental + /// solves is lost. + fn create_warm_started_brancher( + &mut self, + warm_start: HashMap, + ) -> DynamicBrancher { + // First create the slice of variables to give to the WarmStart brancher. + let warm_start_variables: Vec<_> = warm_start.keys().map(|variable| variable.0).collect(); + + // For every variable collect the value into another slice. + let warm_start_values: Vec<_> = warm_start_variables + .iter() + .map(|variable| { + warm_start + .get(&IntExpression(*variable)) + .copied() + .expect("all elements are keys") + }) + .collect(); + + // Swap out the default brancher stored on self with a new default brancher. + let default_brancher = + std::mem::replace(&mut self.brancher, self.solver.default_brancher()); + + DynamicBrancher::new(vec![ + Box::new(WarmStart::new(&warm_start_variables, &warm_start_values)), + Box::new(default_brancher), + ]) + } +} + fn get_termination(end_time: Option) -> Box { end_time .map(|secs| Instant::now() + Duration::from_secs_f32(secs)) From e36424916acae92535b183abf323972e9c92b67e Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 19 Jan 2026 11:10:17 +0100 Subject: [PATCH 09/13] Re-implement warm start --- pumpkin-solver-py/src/model.rs | 83 ++++++++++++++++++++++------------ 1 file changed, 54 insertions(+), 29 deletions(-) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 3537da570..00a5a8638 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -5,7 +5,7 @@ use std::time::Instant; use pumpkin_solver::DefaultBrancher; use pumpkin_solver::Solver; -use pumpkin_solver::branching::branchers::dynamic_brancher::DynamicBrancher; +use pumpkin_solver::branching::Brancher; use pumpkin_solver::branching::branchers::warm_start::WarmStart; use pumpkin_solver::containers::HashMap; use pumpkin_solver::containers::StorageKey; @@ -22,6 +22,8 @@ use pumpkin_solver::results::SolutionReference; use pumpkin_solver::termination::Indefinite; use pumpkin_solver::termination::TerminationCondition; use pumpkin_solver::termination::TimeBudget; +use pumpkin_solver::variables::AffineView; +use pumpkin_solver::variables::DomainId; use pyo3::exceptions::PyRuntimeError; use pyo3::prelude::*; @@ -39,7 +41,7 @@ use crate::variables::Predicate; #[pyclass(unsendable)] pub struct Model { solver: Solver, - brancher: DefaultBrancher, + brancher: PythonBrancher, } #[pyclass] @@ -85,7 +87,10 @@ impl Model { }; let solver = Solver::with_options(options); - let brancher = solver.default_brancher(); + let brancher = PythonBrancher { + warm_start: WarmStart::new(&[], &[]), + default_brancher: solver.default_brancher(), + }; Ok(Model { solver, brancher }) } @@ -105,7 +110,7 @@ impl Model { self.solver.new_bounded_integer(lower_bound, upper_bound) }; - self.brancher.add_domain(domain_id); + self.brancher.default_brancher.add_domain(domain_id); domain_id.into() } @@ -120,6 +125,7 @@ impl Model { }; self.brancher + .default_brancher .add_domain(literal.get_true_predicate().get_domain()); literal.into() @@ -137,7 +143,7 @@ impl Model { /// A tag should be provided for this link to be identifiable in the proof. fn boolean_as_integer(&mut self, boolean: BoolExpression, tag: Tag) -> IntExpression { let new_domain = self.solver.new_bounded_integer(0, 1); - self.brancher.add_domain(new_domain); + self.brancher.default_brancher.add_domain(new_domain); let boolean_true = boolean.0.get_true_predicate(); @@ -256,15 +262,16 @@ impl Model { } } - /// Solve the model to optimality. - /// - /// Resets any incremental state in the stored brancher, but it is unlikely that the Model can - /// be used in an incremental fashion after this call. + #[allow( + clippy::too_many_arguments, + reason = "this is common in many Python APIs" + )] #[pyo3(signature = ( objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None, + on_solution=None, warm_start=HashMap::default(), ))] fn optimise( @@ -274,6 +281,7 @@ impl Model { optimiser: Optimiser, direction: Direction, timeout: Option, + on_solution: Option>, warm_start: HashMap, ) -> OptimisationResult { let mut termination = get_termination(timeout); @@ -285,18 +293,26 @@ impl Model { let objective = objective.0; - let callback: fn(&Solver, SolutionReference, &DynamicBrancher) = |_, _, _| {}; + let callback = move |_: &Solver, solution: SolutionReference<'_>, _: &PythonBrancher| { + let python_solution = crate::result::Solution::from(solution); + + if let Some(on_solution_callback) = on_solution.as_ref() { + let _ = on_solution_callback + .call(py, (python_solution,), None) + .expect("solution callback should be callable"); + } + }; - let mut brancher = self.create_warm_started_brancher(warm_start); + self.update_warm_start(warm_start); let result = match optimiser { Optimiser::LinearSatUnsat => self.solver.optimise( - &mut brancher, + &mut self.brancher, &mut termination, LinearSatUnsat::new(direction, objective, callback), ), Optimiser::LinearUnsatSat => self.solver.optimise( - &mut brancher, + &mut self.brancher, &mut termination, LinearUnsatSat::new(direction, objective, callback), ), @@ -318,14 +334,8 @@ impl Model { } impl Model { - /// Create a brancher that is warm started with the given assignment. - /// - /// This resets the [`DefaultBrancher`] on self, so any knowledge on previous incremental - /// solves is lost. - fn create_warm_started_brancher( - &mut self, - warm_start: HashMap, - ) -> DynamicBrancher { + /// Update the warm start in the [`PythonBrancher`]. + fn update_warm_start(&mut self, warm_start: HashMap) { // First create the slice of variables to give to the WarmStart brancher. let warm_start_variables: Vec<_> = warm_start.keys().map(|variable| variable.0).collect(); @@ -340,14 +350,7 @@ impl Model { }) .collect(); - // Swap out the default brancher stored on self with a new default brancher. - let default_brancher = - std::mem::replace(&mut self.brancher, self.solver.default_brancher()); - - DynamicBrancher::new(vec![ - Box::new(WarmStart::new(&warm_start_variables, &warm_start_values)), - Box::new(default_brancher), - ]) + self.brancher.warm_start = WarmStart::new(&warm_start_variables, &warm_start_values); } } @@ -360,3 +363,25 @@ fn get_termination(end_time: Option) -> Box { }) .unwrap_or(Box::new(Indefinite)) } + +struct PythonBrancher { + warm_start: WarmStart>, + default_brancher: DefaultBrancher, +} + +impl Brancher for PythonBrancher { + fn next_decision( + &mut self, + context: &mut pumpkin_solver::branching::SelectionContext, + ) -> Option { + if let Some(predicate) = self.warm_start.next_decision(context) { + return Some(predicate); + } + + self.default_brancher.next_decision(context) + } + + fn subscribe_to_events(&self) -> Vec { + self.default_brancher.subscribe_to_events() + } +} From b4cb0f84fe5626c2b1059491f50c4a5b1bfea76a Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 19 Jan 2026 11:32:59 +0100 Subject: [PATCH 10/13] Add ControlFlow to solution callback --- .../core/src/optimisation/linear_sat_unsat.rs | 6 +++- .../core/src/optimisation/linear_unsat_sat.rs | 9 +++-- .../src/optimisation/solution_callback.rs | 33 ++++++++++++++++--- pumpkin-solver-py/src/model.rs | 32 ++++++++++++------ pumpkin-solver-py/tests/test_optimisation.py | 25 ++++++++++++++ .../src/bin/pumpkin-solver/flatzinc/mod.rs | 3 ++ 6 files changed, 90 insertions(+), 18 deletions(-) diff --git a/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs b/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs index 7f61aea52..457ccbe03 100644 --- a/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs +++ b/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs @@ -60,12 +60,16 @@ where }; loop { - self.solution_callback.on_solution_callback( + let callback_result = self.solution_callback.on_solution_callback( solver, best_solution.as_reference(), brancher, ); + if callback_result.is_break() { + return OptimisationResult::Satisfiable(best_solution); + } + let best_objective_value = best_solution.get_integer_value(objective.clone()); let conclusion = { diff --git a/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs b/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs index 7b0d65324..102226ec8 100644 --- a/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs +++ b/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs @@ -62,12 +62,16 @@ where SatisfactionResult::Unknown(_, _) => return OptimisationResult::Unknown, }; - self.solution_callback.on_solution_callback( + let callback_result = self.solution_callback.on_solution_callback( solver, primal_solution.as_reference(), brancher, ); + if callback_result.is_break() { + return OptimisationResult::Satisfiable(primal_solution); + } + let primal_objective = primal_solution.get_integer_value(objective.clone()); // Then, we iterate from the lower bound of the objective until (excluding) the primal @@ -108,7 +112,8 @@ where match conclusion { Some(OptimisationResult::Optimal(solution)) => { - self.solution_callback.on_solution_callback( + // Optimisation will stop regardless of the result of the callback. + let _ = self.solution_callback.on_solution_callback( solver, primal_solution.as_reference(), brancher, diff --git a/pumpkin-crates/core/src/optimisation/solution_callback.rs b/pumpkin-crates/core/src/optimisation/solution_callback.rs index cb5b4f3a6..43ced6764 100644 --- a/pumpkin-crates/core/src/optimisation/solution_callback.rs +++ b/pumpkin-crates/core/src/optimisation/solution_callback.rs @@ -1,21 +1,44 @@ +use std::ops::ControlFlow; + use crate::Solver; use crate::branching::Brancher; use crate::results::SolutionReference; pub trait SolutionCallback { - fn on_solution_callback(&self, solver: &Solver, solution: SolutionReference, brancher: &B); + fn on_solution_callback( + &mut self, + solver: &Solver, + solution: SolutionReference, + brancher: &B, + ) -> ControlFlow<(), ()>; } -impl SolutionCallback for T { - fn on_solution_callback(&self, solver: &Solver, solution: SolutionReference, brancher: &B) { +impl SolutionCallback for T +where + T: FnMut(&Solver, SolutionReference, &B) -> ControlFlow<(), ()>, + B: Brancher, +{ + fn on_solution_callback( + &mut self, + solver: &Solver, + solution: SolutionReference, + brancher: &B, + ) -> ControlFlow<(), ()> { (self)(solver, solution, brancher) } } impl, B: Brancher> SolutionCallback for Option { - fn on_solution_callback(&self, solver: &Solver, solution: SolutionReference, brancher: &B) { + fn on_solution_callback( + &mut self, + solver: &Solver, + solution: SolutionReference, + brancher: &B, + ) -> ControlFlow<(), ()> { if let Some(callback) = self { - callback.on_solution_callback(solver, solution, brancher) + return callback.on_solution_callback(solver, solution, brancher); } + + ControlFlow::Continue(()) } } diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 00a5a8638..ae2246178 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -1,4 +1,5 @@ use std::num::NonZero; +use std::ops::ControlFlow; use std::path::PathBuf; use std::time::Duration; use std::time::Instant; @@ -283,7 +284,7 @@ impl Model { timeout: Option, on_solution: Option>, warm_start: HashMap, - ) -> OptimisationResult { + ) -> PyResult { let mut termination = get_termination(timeout); let direction = match direction { @@ -293,14 +294,19 @@ impl Model { let objective = objective.0; - let callback = move |_: &Solver, solution: SolutionReference<'_>, _: &PythonBrancher| { + let mut error_in_callback = None; + + let callback = |_: &Solver, solution: SolutionReference<'_>, _: &PythonBrancher| { let python_solution = crate::result::Solution::from(solution); - if let Some(on_solution_callback) = on_solution.as_ref() { - let _ = on_solution_callback - .call(py, (python_solution,), None) - .expect("solution callback should be callable"); + if let Some(on_solution_callback) = on_solution.as_ref() + && let Err(err) = on_solution_callback.call(py, (python_solution,), None) + { + error_in_callback = Some(err); + return ControlFlow::Break(()); } + + ControlFlow::Continue(()) }; self.update_warm_start(warm_start); @@ -318,17 +324,23 @@ impl Model { ), }; + if let Some(err) = error_in_callback { + return Err(err); + } + match result { pumpkin_solver::results::OptimisationResult::Satisfiable(solution) => { - OptimisationResult::Satisfiable(solution.into()) + Ok(OptimisationResult::Satisfiable(solution.into())) } pumpkin_solver::results::OptimisationResult::Optimal(solution) => { - OptimisationResult::Optimal(solution.into()) + Ok(OptimisationResult::Optimal(solution.into())) } pumpkin_solver::results::OptimisationResult::Unsatisfiable => { - OptimisationResult::Unsatisfiable() + Ok(OptimisationResult::Unsatisfiable()) + } + pumpkin_solver::results::OptimisationResult::Unknown => { + Ok(OptimisationResult::Unknown()) } - pumpkin_solver::results::OptimisationResult::Unknown => OptimisationResult::Unknown(), } } } diff --git a/pumpkin-solver-py/tests/test_optimisation.py b/pumpkin-solver-py/tests/test_optimisation.py index 20af4588e..d56bcb859 100644 --- a/pumpkin-solver-py/tests/test_optimisation.py +++ b/pumpkin-solver-py/tests/test_optimisation.py @@ -26,3 +26,28 @@ def test_linear_sat_unsat_maximisation(): solution = result._0 assert solution.int_value(objective) == 5 + + +def test_warm_start_with_callback(): + model = Model() + + objective = model.new_integer_variable(1, 5, name="objective") + + first_value = None + + def on_solution(solution): + nonlocal first_value + + if first_value is None: + first_value = solution.int_value(objective) + + result = model.optimise( + objective, + direction=Direction.Maximise, + warm_start={objective: 3}, + on_solution=on_solution, + ) + + assert isinstance(result, OptimisationResult.Optimal) + + assert first_value == 3 diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs index 41d92fb92..c07318b1d 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs @@ -6,6 +6,7 @@ mod parser; use std::fs::File; use std::io::Read; +use std::ops::ControlFlow; use std::path::Path; use std::time::Duration; use std::time::Instant; @@ -188,6 +189,8 @@ pub(crate) fn solve( options.verbose, init_time, ); + + ControlFlow::Continue(()) }; let result = match options.optimisation_strategy { From 816bb4b04aa3f547136c61e1c82a28cca6eec4aa Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 19 Jan 2026 12:05:15 +0100 Subject: [PATCH 11/13] Implement propagating values from solution callback to caller --- pumpkin-crates/core/src/api/outputs/mod.rs | 4 ++- pumpkin-crates/core/src/api/solver.rs | 2 +- .../core/src/optimisation/linear_sat_unsat.rs | 8 +++-- .../core/src/optimisation/linear_unsat_sat.rs | 7 ++-- pumpkin-crates/core/src/optimisation/mod.rs | 2 +- .../src/optimisation/solution_callback.rs | 30 ++++++++++++---- pumpkin-solver-py/src/model.rs | 25 +++++++------ pumpkin-solver-py/tests/test_optimisation.py | 2 +- .../src/bin/pumpkin-solver/flatzinc/mod.rs | 35 +++++++++++-------- 9 files changed, 71 insertions(+), 44 deletions(-) diff --git a/pumpkin-crates/core/src/api/outputs/mod.rs b/pumpkin-crates/core/src/api/outputs/mod.rs index 413a59158..6db16f8b4 100644 --- a/pumpkin-crates/core/src/api/outputs/mod.rs +++ b/pumpkin-crates/core/src/api/outputs/mod.rs @@ -43,13 +43,15 @@ pub enum SatisfactionResultUnderAssumptions<'solver, 'brancher, B: Brancher> { /// The result of a call to [`Solver::optimise`]. #[derive(Debug)] -pub enum OptimisationResult { +pub enum OptimisationResult { /// Indicates that an optimal solution has been found and proven to be optimal. It provides an /// instance of [`Solution`] which contains the optimal solution. Optimal(Solution), /// Indicates that a solution was found and provides an instance of [`Solution`] which contains /// best known solution by the solver. Satisfiable(Solution), + /// The optimisation was stopped by the solution callback. + Stopped(Solution, Stop), /// Indicates that there is no solution to the problem. Unsatisfiable, /// Indicates that it is not known whether a solution exists. This is likely due to a diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index 6088df6ec..69599b6ca 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -437,7 +437,7 @@ impl Solver { brancher: &mut B, termination: &mut impl TerminationCondition, mut optimisation_procedure: impl OptimisationProcedure, - ) -> OptimisationResult + ) -> OptimisationResult where B: Brancher, Callback: SolutionCallback, diff --git a/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs b/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs index 457ccbe03..4c422cb9e 100644 --- a/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs +++ b/pumpkin-crates/core/src/optimisation/linear_sat_unsat.rs @@ -1,3 +1,5 @@ +use std::ops::ControlFlow; + use super::OptimisationProcedure; use super::solution_callback::SolutionCallback; use crate::Solver; @@ -46,7 +48,7 @@ where brancher: &mut B, termination: &mut impl TerminationCondition, solver: &mut Solver, - ) -> OptimisationResult { + ) -> OptimisationResult { let objective = match self.direction { OptimisationDirection::Maximise => self.objective.scaled(-1), OptimisationDirection::Minimise => self.objective.scaled(1), @@ -66,8 +68,8 @@ where brancher, ); - if callback_result.is_break() { - return OptimisationResult::Satisfiable(best_solution); + if let ControlFlow::Break(stop) = callback_result { + return OptimisationResult::Stopped(best_solution, stop); } let best_objective_value = best_solution.get_integer_value(objective.clone()); diff --git a/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs b/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs index 102226ec8..73f028dc7 100644 --- a/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs +++ b/pumpkin-crates/core/src/optimisation/linear_unsat_sat.rs @@ -1,4 +1,5 @@ use std::num::NonZero; +use std::ops::ControlFlow; use super::OptimisationProcedure; use super::solution_callback::SolutionCallback; @@ -49,7 +50,7 @@ where brancher: &mut B, termination: &mut impl TerminationCondition, solver: &mut Solver, - ) -> OptimisationResult { + ) -> OptimisationResult { let objective = match self.direction { OptimisationDirection::Maximise => self.objective.scaled(-1), OptimisationDirection::Minimise => self.objective.scaled(1), @@ -68,8 +69,8 @@ where brancher, ); - if callback_result.is_break() { - return OptimisationResult::Satisfiable(primal_solution); + if let ControlFlow::Break(stop) = callback_result { + return OptimisationResult::Stopped(primal_solution, stop); } let primal_objective = primal_solution.get_integer_value(objective.clone()); diff --git a/pumpkin-crates/core/src/optimisation/mod.rs b/pumpkin-crates/core/src/optimisation/mod.rs index 2e2ec0730..3a623aecb 100644 --- a/pumpkin-crates/core/src/optimisation/mod.rs +++ b/pumpkin-crates/core/src/optimisation/mod.rs @@ -17,7 +17,7 @@ pub trait OptimisationProcedure> { brancher: &mut B, termination: &mut impl TerminationCondition, solver: &mut Solver, - ) -> OptimisationResult; + ) -> OptimisationResult; } /// The type of search which is performed by the solver. diff --git a/pumpkin-crates/core/src/optimisation/solution_callback.rs b/pumpkin-crates/core/src/optimisation/solution_callback.rs index 43ced6764..073afb966 100644 --- a/pumpkin-crates/core/src/optimisation/solution_callback.rs +++ b/pumpkin-crates/core/src/optimisation/solution_callback.rs @@ -4,37 +4,55 @@ use crate::Solver; use crate::branching::Brancher; use crate::results::SolutionReference; +/// Called during optimisation with every encountered solution. +/// +/// The callback can determine whether to proceed optimising or whether to stop by returning a +/// [`ControlFlow`] value. When [`ControlFlow::Break`] is returned, a value of +/// [`SolutionCallback::Stop`] can be supplied that will be forwarded to the result of the +/// optimisation call. pub trait SolutionCallback { + /// The type of value to return if optimisation should stop. + type Stop; + + /// Called when a solution is encountered. fn on_solution_callback( &mut self, solver: &Solver, solution: SolutionReference, brancher: &B, - ) -> ControlFlow<(), ()>; + ) -> ControlFlow; } -impl SolutionCallback for T +impl SolutionCallback for T where - T: FnMut(&Solver, SolutionReference, &B) -> ControlFlow<(), ()>, + T: FnMut(&Solver, SolutionReference, &B) -> ControlFlow, B: Brancher, { + type Stop = R; + fn on_solution_callback( &mut self, solver: &Solver, solution: SolutionReference, brancher: &B, - ) -> ControlFlow<(), ()> { + ) -> ControlFlow { (self)(solver, solution, brancher) } } -impl, B: Brancher> SolutionCallback for Option { +impl SolutionCallback for Option +where + T: SolutionCallback, + B: Brancher, +{ + type Stop = R; + fn on_solution_callback( &mut self, solver: &Solver, solution: SolutionReference, brancher: &B, - ) -> ControlFlow<(), ()> { + ) -> ControlFlow { if let Some(callback) = self { return callback.on_solution_callback(solver, solution, brancher); } diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index ae2246178..89a938fb2 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -294,19 +294,21 @@ impl Model { let objective = objective.0; - let mut error_in_callback = None; - let callback = |_: &Solver, solution: SolutionReference<'_>, _: &PythonBrancher| { let python_solution = crate::result::Solution::from(solution); - if let Some(on_solution_callback) = on_solution.as_ref() - && let Err(err) = on_solution_callback.call(py, (python_solution,), None) - { - error_in_callback = Some(err); - return ControlFlow::Break(()); - } + // If there is a solution callback, unpack it. + let Some(on_solution_callback) = on_solution.as_ref() else { + return ControlFlow::Continue(()); + }; + + // Call the callback, and if there is an error, unpack it. + let Err(err) = on_solution_callback.call(py, (python_solution,), None) else { + return ControlFlow::Continue(()); + }; - ControlFlow::Continue(()) + // Stop optimising and return the error. + ControlFlow::Break(err) }; self.update_warm_start(warm_start); @@ -324,11 +326,8 @@ impl Model { ), }; - if let Some(err) = error_in_callback { - return Err(err); - } - match result { + pumpkin_solver::results::OptimisationResult::Stopped(_, err) => Err(err), pumpkin_solver::results::OptimisationResult::Satisfiable(solution) => { Ok(OptimisationResult::Satisfiable(solution.into())) } diff --git a/pumpkin-solver-py/tests/test_optimisation.py b/pumpkin-solver-py/tests/test_optimisation.py index d56bcb859..430aeb5ca 100644 --- a/pumpkin-solver-py/tests/test_optimisation.py +++ b/pumpkin-solver-py/tests/test_optimisation.py @@ -36,7 +36,7 @@ def test_warm_start_with_callback(): first_value = None def on_solution(solution): - nonlocal first_value + # nonlocal first_value if first_value is None: first_value = solution.int_value(objective) diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs index c07318b1d..ced53f939 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs @@ -177,21 +177,23 @@ pub(crate) fn solve( } }; - let callback = - |solver: &Solver, solution: SolutionReference<'_>, brancher: &DynamicBrancher| { - solution_callback( - brancher, - Some(objective), - options.all_solutions, - &outputs, - solver, - solution, - options.verbose, - init_time, - ); - - ControlFlow::Continue(()) - }; + let callback = |solver: &Solver, + solution: SolutionReference<'_>, + brancher: &DynamicBrancher| + -> ControlFlow<()> { + solution_callback( + brancher, + Some(objective), + options.all_solutions, + &outputs, + solver, + solution, + options.verbose, + init_time, + ); + + ControlFlow::Continue(()) + }; let result = match options.optimisation_strategy { OptimisationStrategy::LinearSatUnsat => solver.optimise( @@ -207,6 +209,9 @@ pub(crate) fn solve( }; match result { + OptimisationResult::Stopped(_, _) => { + unreachable!("the callback will never return ControlFlow::Break") + } OptimisationResult::Optimal(optimal_solution) => { let objective_value = optimal_solution.get_integer_value(objective) as i64; if !options.all_solutions { From 084139928da3dc3037085f7bb2fcf8b49dfac853 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 19 Jan 2026 12:06:28 +0100 Subject: [PATCH 12/13] Fix optimisation test --- pumpkin-solver-py/tests/test_optimisation.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pumpkin-solver-py/tests/test_optimisation.py b/pumpkin-solver-py/tests/test_optimisation.py index 430aeb5ca..d56bcb859 100644 --- a/pumpkin-solver-py/tests/test_optimisation.py +++ b/pumpkin-solver-py/tests/test_optimisation.py @@ -36,7 +36,7 @@ def test_warm_start_with_callback(): first_value = None def on_solution(solution): - # nonlocal first_value + nonlocal first_value if first_value is None: first_value = solution.int_value(objective) From 6e75a57cf5824eb7ee278cfa86c6071a16e16a21 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 19 Jan 2026 12:23:55 +0100 Subject: [PATCH 13/13] Fix doctest --- pumpkin-solver/src/lib.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/pumpkin-solver/src/lib.rs b/pumpkin-solver/src/lib.rs index 3c289cf85..86a2b0537 100644 --- a/pumpkin-solver/src/lib.rs +++ b/pumpkin-solver/src/lib.rs @@ -131,6 +131,8 @@ //! //! Then we can find the optimal solution using [`Solver::optimise`]: //! ```rust +//! # use std::cmp::max; +//! # use std::ops::ControlFlow; //! # use pumpkin_solver::Solver; //! # use pumpkin_solver::results::OptimisationResult; //! # use pumpkin_solver::termination::Indefinite; @@ -139,7 +141,6 @@ //! # use pumpkin_solver::constraints::Constraint; //! # use pumpkin_solver::optimisation::OptimisationDirection; //! # use pumpkin_solver::optimisation::linear_sat_unsat::LinearSatUnsat; -//! # use std::cmp::max; //! # use crate::pumpkin_solver::optimisation::OptimisationProcedure; //! # use pumpkin_solver::results::SolutionReference; //! # use pumpkin_solver::DefaultBrancher; @@ -153,8 +154,12 @@ //! # solver.add_constraint(pumpkin_constraints::maximum(vec![x, y, z], objective, c1)).post(); //! # let mut termination = Indefinite; //! # let mut brancher = solver.default_brancher(); +//! +//! let callback = |_: &Solver, _: SolutionReference, _: &DefaultBrancher| -> ControlFlow<()> { +//! return ControlFlow::Continue(()); +//! }; +//! //! // Then we solve to optimality -//! let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {}; //! let result = solver.optimise( //! &mut brancher, //! &mut termination,