From e65629787623f780b4d072c5655f4d3c145f520d Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 16:07:48 +0100 Subject: [PATCH 1/8] 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 2/8] 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 3/8] 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 4/8] 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 5/8] 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 6/8] 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 c4dea69a3300e96631670b2d9326af120e093a54 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 17 Jan 2026 09:42:26 +0100 Subject: [PATCH 7/8] 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 218b740cb..31199bdc7 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 04fd17de79710de9bda0fba2ef2355cf7fc3cdae Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 18 Jan 2026 09:51:17 +0100 Subject: [PATCH 8/8] feat(pumpkin-solver-py): Add a solution callback to Model::optimise --- pumpkin-solver-py/examples/optimisation.py | 41 ++++++++++++++++++++++ pumpkin-solver-py/src/model.rs | 14 ++++++-- 2 files changed, 53 insertions(+), 2 deletions(-) create mode 100644 pumpkin-solver-py/examples/optimisation.py diff --git a/pumpkin-solver-py/examples/optimisation.py b/pumpkin-solver-py/examples/optimisation.py new file mode 100644 index 000000000..2f80b0455 --- /dev/null +++ b/pumpkin-solver-py/examples/optimisation.py @@ -0,0 +1,41 @@ +from argparse import ArgumentParser +from pathlib import Path + +from pumpkin_solver import constraints, Model +from pumpkin_solver.optimisation import OptimisationResult + + +def main(proof: Path | None): + model = Model(proof=proof) + + objective = model.new_integer_variable(10, 20, name="objective") + + # .. build the model here + + def on_solution(solution): + objective_value = solution.int_value(objective) + print(f"objective_value={objective_value}") + + status = model.optimise(objective, on_solution=on_solution) + match status: + case OptimisationResult.Optimal(_solution): + print("OPTIMAL") + + case OptimisationResult.Satisfiable(_solution): + print("SATISFIABLE") + + case OptimisationResult.Unsatisfiable(): + print("UNSATISFIABLE") + + case OptimisationResult.Unknown(): + print("UNKNOWN") + + +if __name__ == "__main__": + arg_parser = ArgumentParser() + + arg_parser.add_argument("--proof", type=Path, help="The proof file.", default=None) + + args = arg_parser.parse_args() + + main(args.proof) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index 31199bdc7..1aa863a10 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -246,13 +246,15 @@ impl Model { } } - #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None))] + #[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None, on_solution=None))] fn optimise( &mut self, + py: Python<'_>, objective: IntExpression, optimiser: Optimiser, direction: Direction, timeout: Option, + on_solution: Option>, ) -> OptimisationResult { let mut termination = get_termination(timeout); @@ -263,7 +265,15 @@ impl Model { let objective = objective.0; - let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {}; + let callback = move |_: &Solver, solution: SolutionReference<'_>, _: &DefaultBrancher| { + 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("failed to call solution callback"); + } + }; let result = match optimiser { Optimiser::LinearSatUnsat => self.solver.optimise(