From e65629787623f780b4d072c5655f4d3c145f520d Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 16:07:48 +0100 Subject: [PATCH 01/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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 109510ef61bbd6d8cb43993473d970eefff9d7b6 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 17 Jan 2026 08:37:34 +0100 Subject: [PATCH 07/10] Fix merge build errors --- pumpkin-solver-py/src/constraints/globals.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pumpkin-solver-py/src/constraints/globals.rs b/pumpkin-solver-py/src/constraints/globals.rs index acf5241fb..83920800d 100644 --- a/pumpkin-solver-py/src/constraints/globals.rs +++ b/pumpkin-solver-py/src/constraints/globals.rs @@ -30,7 +30,7 @@ macro_rules! python_constraint { self, solver: &mut pumpkin_solver::Solver, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { - constraints::$constraint_func( + pumpkin_constraints::$constraint_func( $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ , self.constraint_tag.0, ).post(solver) @@ -41,7 +41,7 @@ macro_rules! python_constraint { solver: &mut pumpkin_solver::Solver, reification_literal: pumpkin_solver::variables::Literal, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { - constraints::$constraint_func( + pumpkin_constraints::$constraint_func( $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ , self.constraint_tag.0, ).implied_by(solver, reification_literal) From 062984c1500cb4522db69c879f62959b9c794e89 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 17 Jan 2026 09:37:21 +0100 Subject: [PATCH 08/10] Refactor python tests to delay model creation --- pumpkin-solver-py/tests/test_constraints.py | 356 +++++++++++--------- 1 file changed, 201 insertions(+), 155 deletions(-) diff --git a/pumpkin-solver-py/tests/test_constraints.py b/pumpkin-solver-py/tests/test_constraints.py index aee69e59f..0a861c710 100644 --- a/pumpkin-solver-py/tests/test_constraints.py +++ b/pumpkin-solver-py/tests/test_constraints.py @@ -12,42 +12,19 @@ import pumpkin_solver +def chain(*iterables): + """Helper used to chain iterables/generators.""" + for it in iterables: + for element in it: + yield element + + # generate all linear sum-expressions def generate_linear(): for comp in "<=", "==", "!=": for scaled in (False, True): # to generate a weighted sum for bool in (False, True): # from bool-view? - model = pumpkin_solver.Model() - - if bool: - args = [ - model.boolean_as_integer( - model.new_boolean_variable(name=f"x[{i}]"), - model.new_constraint_tag(), - ) - for i in range(3) - ] - else: - args = [ - model.new_integer_variable(-3, 5, name=f"x[{i}]") - for i in range(3) - ] - if scaled: # do scaling (0, -2, 4,...) - args = [ - a.scaled(-2 * i + 1) for i, a in enumerate(args) - ] # TODO: div by zero when scale = 0, fixed with +1 - - rhs = 1 - if comp == "==": - cons = constraints.Equals(args, rhs, model.new_constraint_tag()) - if comp == "!=": - cons = constraints.NotEquals(args, rhs, model.new_constraint_tag()) - if comp == "<=": - cons = constraints.LessThanOrEquals( - args, rhs, model.new_constraint_tag() - ) - - yield model, cons, comp, scaled, bool + yield comp, scaled, bool # generate other operators @@ -55,186 +32,255 @@ def generate_operators(): for name in ["div", "mul", "abs", "min", "max", "element"]: for scaled in (False, True): for bool in (False, True): # from bool-view? - model = pumpkin_solver.Model() - - if bool: - args = [ - model.boolean_as_integer( - model.new_boolean_variable(name=f"x[{i}]"), - model.new_constraint_tag(), - ) - for i in range(3) - ] - else: - args = [ - model.new_integer_variable(-3, 5, name=f"x[{i}]") - for i in range(3) - ] - if scaled: # do scaling (0, -2, 4,...) - args = [ - a.scaled(-2 * i + 1) for i, a in enumerate(args) - ] # TODO: div by zero when scale = 0, fixed with +1 - - rhs = model.new_integer_variable(-3, 5, name="rhs") - if name == "div": - denom = model.new_integer_variable(1, 3, name="denom") - cons = constraints.Division( - args[0], denom, rhs, model.new_constraint_tag() - ) - if name == "mul": - cons = constraints.Times(*args[:2], rhs, model.new_constraint_tag()) - if name == "abs": - cons = constraints.Absolute( - args[0], rhs, model.new_constraint_tag() - ) - if name == "min": - cons = constraints.Minimum(args, rhs, model.new_constraint_tag()) - if name == "max": - cons = constraints.Maximum(args, rhs, model.new_constraint_tag()) - if name == "element": - idx = model.new_integer_variable( - -1, 5, name="idx" - ) # sneaky, idx can be out of bounds - cons = constraints.Element( - idx, args, rhs, model.new_constraint_tag() - ) - - yield model, cons, name, scaled, bool + yield name, scaled, bool # generate global constraints, separate functions for readability def generate_alldiff(): for scaled in (False, True): for bool in (False, True): # from bool-view? Unlikely constraint, but anyway - model = pumpkin_solver.Model() - if bool: - args = [ - model.boolean_as_integer( - model.new_boolean_variable(name=f"x[{i}]"), - model.new_constraint_tag(), - ) - for i in range(3) - ] - else: - args = [ - model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3) - ] - if scaled or bool: # do scaling (0, -2, 4,...) - args = [ - a.scaled(-2 * i + 1) for i, a in enumerate(args) - ] # TODO: div by zero when scale = 0, fixed with +1 - - cons = constraints.AllDifferent(args, model.new_constraint_tag()) - yield model, cons, "alldifferent", scaled or bool, bool + yield "alldiff", scaled, bool def generate_table(): - model = pumpkin_solver.Model() - variables = [model.new_integer_variable(1, 5, name=f"x[{i}]") for i in range(3)] + yield "table", False, False + + +def generate_negative_table(): + yield "negative_table", False, False - table = [[randint(1, 5) for _ in range(3)] for _ in range(3)] - cons = constraints.Table(variables, table, model.new_constraint_tag()) - yield model, cons, "table", bool, bool +def generate_cumulative(): + yield "cumulative", False, False + yield "cumulative", True, False -def generate_negative_table(): +def generate_globals(): + yield from generate_alldiff() + yield from generate_cumulative() + yield from generate_table() + yield from generate_negative_table() + + +def create_linear_model(request): + comp, scaled, bool = request.param + model = pumpkin_solver.Model() - variables = [model.new_integer_variable(1, 5, name=f"x[{i}]") for i in range(3)] - table = [[randint(1, 5) for _ in range(3)] for _ in range(3)] + if bool: + args = [ + model.boolean_as_integer( + model.new_boolean_variable(name=f"x[{i}]"), + model.new_constraint_tag(), + ) + for i in range(3) + ] + else: + args = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] + if scaled: # do scaling (0, -2, 4,...) + args = [ + a.scaled(-2 * i + 1) for i, a in enumerate(args) + ] # TODO: div by zero when scale = 0, fixed with +1 - cons = constraints.NegativeTable(variables, table, model.new_constraint_tag()) - yield model, cons, "negative_table", bool, bool + rhs = 1 + cons = None + if comp == "==": + cons = constraints.Equals(args, rhs, model.new_constraint_tag()) + if comp == "!=": + cons = constraints.NotEquals(args, rhs, model.new_constraint_tag()) + if comp == "<=": + cons = constraints.LessThanOrEquals(args, rhs, model.new_constraint_tag()) + if not cons: + assert False, f"unknown comp {comp}" + + return (model, cons) + + +@pytest.fixture +def linear_model(request): + return create_linear_model(request) -def generate_cumulative(): - duration = [2, 3, 4] - demand = [1, 2, 3] - capacity = 4 + +def create_operator_model(request): + name, scaled, bool = request.param model = pumpkin_solver.Model() - start = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] - cons = constraints.Cumulative( - start, duration, demand, capacity, model.new_constraint_tag() - ) - yield model, cons, "cumulative", False, False + + if bool: + args = [ + model.boolean_as_integer( + model.new_boolean_variable(name=f"x[{i}]"), + model.new_constraint_tag(), + ) + for i in range(3) + ] + else: + args = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] + if scaled: # do scaling (0, -2, 4,...) + args = [ + a.scaled(-2 * i + 1) for i, a in enumerate(args) + ] # TODO: div by zero when scale = 0, fixed with +1 + + rhs = model.new_integer_variable(-3, 5, name="rhs") + cons = None + if name == "div": + denom = model.new_integer_variable(1, 3, name="denom") + cons = constraints.Division(args[0], denom, rhs, model.new_constraint_tag()) + if name == "mul": + cons = constraints.Times(*args[:2], rhs, model.new_constraint_tag()) + if name == "abs": + cons = constraints.Absolute(args[0], rhs, model.new_constraint_tag()) + if name == "min": + cons = constraints.Minimum(args, rhs, model.new_constraint_tag()) + if name == "max": + cons = constraints.Maximum(args, rhs, model.new_constraint_tag()) + if name == "element": + idx = model.new_integer_variable( + -1, 5, name="idx" + ) # sneaky, idx can be out of bounds + cons = constraints.Element(idx, args, rhs, model.new_constraint_tag()) + + if not cons: + assert False, f"unknown constraint {name}" + + return (model, cons) + + +@pytest.fixture +def operator_model(request): + return create_operator_model(request) + + +def create_global_model(request): + name, scaled, bool = request.param model = pumpkin_solver.Model() - start = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] - start = [a.scaled(-2 * i) for i, a in enumerate(start)] - cons = constraints.Cumulative( - start, duration, demand, capacity, model.new_constraint_tag() - ) - yield model, cons, "cumulative", True, False + if name == "alldiff": + if bool: + args = [ + model.boolean_as_integer( + model.new_boolean_variable(name=f"x[{i}]"), + model.new_constraint_tag(), + ) + for i in range(3) + ] + else: + args = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] + if scaled or bool: # do scaling (0, -2, 4,...) + args = [ + a.scaled(-2 * i + 1) for i, a in enumerate(args) + ] # TODO: div by zero when scale = 0, fixed with +1 -def generate_globals(): - yield from generate_alldiff() - yield from generate_cumulative() - yield from generate_table() - yield from generate_negative_table() + cons = constraints.AllDifferent(args, model.new_constraint_tag()) + + elif name == "table": + variables = [model.new_integer_variable(1, 5, name=f"x[{i}]") for i in range(3)] + table = [[randint(1, 5) for _ in range(3)] for _ in range(3)] + cons = constraints.Table(variables, table, model.new_constraint_tag()) + + elif name == "negative_table": + variables = [model.new_integer_variable(1, 5, name=f"x[{i}]") for i in range(3)] + table = [[randint(1, 5) for _ in range(3)] for _ in range(3)] + cons = constraints.NegativeTable(variables, table, model.new_constraint_tag()) + + elif name == "cumulative": + duration = [2, 3, 4] + demand = [1, 2, 3] + capacity = 4 + start = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] + if scaled: + start = [a.scaled(-2 * i) for i, a in enumerate(start)] + cons = constraints.Cumulative( + start, duration, demand, capacity, model.new_constraint_tag() + ) + + else: + assert False, f"unknown global {name}" + + return (model, cons) + + +@pytest.fixture +def global_model(request): + return create_global_model(request) + + +def make_id(args): + name, scaled, bool = args -def label(model, cons, name, scaled, bool): return " ".join( ["Scaled" if scaled else "Unscaled", "Boolean" if bool else "Integer", name] ) -LINEAR = list(generate_linear()) - - -@pytest.mark.parametrize( - ("model", "cons", "name", "scaled", "bool"), LINEAR, ids=[label(*a) for a in LINEAR] -) -def test_linear(model, cons, name, scaled, bool): +@pytest.mark.parametrize("linear_model", generate_linear(), indirect=True, ids=make_id) +def test_linear(linear_model): + model, cons = linear_model model.add_constraint(cons) + res = model.satisfy() assert isinstance(res, pumpkin_solver.SatisfactionResult.Satisfiable) -OPERATORS = list(generate_operators()) - - @pytest.mark.parametrize( - ("model", "cons", "name", "scaled", "bool"), - OPERATORS, - ids=[label(*a) for a in OPERATORS], + "operator_model", + generate_operators(), + ids=make_id, + indirect=True, ) -def test_operators(model, cons, name, scaled, bool): +def test_operators(operator_model): + model, cons = operator_model model.add_constraint(cons) + res = model.satisfy() assert isinstance(res, pumpkin_solver.SatisfactionResult.Satisfiable) -GLOBALS = list(generate_globals()) - - @pytest.mark.parametrize( - ("model", "cons", "name", "scaled", "bool"), - GLOBALS, - ids=[label(*a) for a in GLOBALS], + "global_model", + generate_globals(), + ids=make_id, + indirect=True, ) -def test_global(model, cons, name, scaled, bool): +def test_globals(global_model): + model, cons = global_model model.add_constraint(cons) + res = model.satisfy() assert isinstance(res, pumpkin_solver.SatisfactionResult.Satisfiable) -ALL_EXPR = LINEAR + OPERATORS + GLOBALS +@pytest.fixture +def implication_model(request): + name, _, _ = request.param + + if name in ["<=", "==", "!="]: + model, cons = create_linear_model(request) + elif name in ["div", "mul", "abs", "min", "max", "element"]: + model, cons = create_operator_model(request) + elif name in ["alldiff", "element", "cumulative", "table", "negative_table"]: + model, cons = create_global_model(request) + + else: + assert False, f"unknown global {name}" + + return model, cons @pytest.mark.parametrize( - ("model", "cons", "name", "scaled", "bool"), - ALL_EXPR, - ids=["->" + label(*a) for a in ALL_EXPR], + "implication_model", + chain(generate_linear(), generate_operators(), generate_globals()), + ids=make_id, + indirect=True, ) -def test_implication(model, cons, name, scaled, bool): - if name == "element": - return # TODO: propagator not yet implemented? +def test_implication(implication_model): + model, cons = implication_model bv = model.new_boolean_variable("bv") model.add_implication(cons, bv) + res = model.satisfy() assert isinstance(res, pumpkin_solver.SatisfactionResult.Satisfiable) From cfa33efc0133b847384eed8d1da7d1e9453c7197 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 17 Jan 2026 09:42:26 +0100 Subject: [PATCH 09/10] Remove custom threadbound wrapper --- pumpkin-solver-py/src/model.rs | 64 +++++----------------------------- 1 file changed, 8 insertions(+), 56 deletions(-) diff --git a/pumpkin-solver-py/src/model.rs b/pumpkin-solver-py/src/model.rs index a107f999b..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; @@ -34,10 +31,10 @@ use crate::variables::BoolExpression; use crate::variables::IntExpression; use crate::variables::Predicate; -#[pyclass] +#[pyclass(unsendable)] pub struct Model { - solver: ThreadBound, - brancher: ThreadBound, + solver: Solver, + brancher: DefaultBrancher, } #[pyclass] @@ -80,18 +77,7 @@ impl Model { let solver = Solver::with_options(options); let brancher = solver.default_brancher(); - let owner = std::thread::current().id(); - - Ok(Model { - solver: ThreadBound { - value: solver, - owner, - }, - brancher: ThreadBound { - value: brancher, - owner, - }, - }) + Ok(Model { solver, brancher }) } /// Create a new integer variable. @@ -199,10 +185,7 @@ impl Model { fn satisfy(&mut self, timeout: Option) -> SatisfactionResult { let mut termination = get_termination(timeout); - match self - .solver - .satisfy(self.brancher.deref_mut(), &mut termination) - { + match self.solver.satisfy(&mut self.brancher, &mut termination) { pumpkin_solver::results::SatisfactionResult::Satisfiable(satisfiable) => { SatisfactionResult::Satisfiable(Solution::from(satisfiable.solution())) } @@ -228,7 +211,7 @@ impl Model { .map(|pred| pred.into_solver_predicate()) .collect::>(); - match self.solver.satisfy_under_assumptions(self.brancher.deref_mut(), &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(satisfiable.solution().into()) } @@ -284,12 +267,12 @@ impl Model { let result = match optimiser { Optimiser::LinearSatUnsat => self.solver.optimise( - self.brancher.deref_mut(), + &mut self.brancher, &mut termination, LinearSatUnsat::new(direction, objective, callback), ), Optimiser::LinearUnsatSat => self.solver.optimise( - self.brancher.deref_mut(), + &mut self.brancher, &mut termination, LinearUnsatSat::new(direction, objective, callback), ), @@ -319,34 +302,3 @@ 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 74da9f5897db21ef9970f1f009fa9a5ce74ea8b5 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 18 Jan 2026 08:32:30 +0100 Subject: [PATCH 10/10] Fix nqueens example --- pumpkin-solver-py/examples/nqueens.py | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/pumpkin-solver-py/examples/nqueens.py b/pumpkin-solver-py/examples/nqueens.py index f5d0091e1..778c5f69e 100644 --- a/pumpkin-solver-py/examples/nqueens.py +++ b/pumpkin-solver-py/examples/nqueens.py @@ -1,25 +1,27 @@ from argparse import ArgumentParser from pathlib import Path -from pumpkin_solver_py import constraints, SatisfactionResult, Model +from pumpkin_solver import constraints, SatisfactionResult, Model def main(n: int, proof: Path | None): assert n > 0, "Please provide a positive non-zero 'n'" - model = Model() + model = Model(proof=proof) variables = [model.new_integer_variable(0, n - 1, name=f"q{i}") for i in range(n)] - model.add_constraint(constraints.AllDifferent(variables), tag=1) + model.add_constraint( + constraints.AllDifferent(variables, model.new_constraint_tag()) + ) diag1 = [var.offset(i) for (i, var) in enumerate(variables)] diag2 = [var.offset(-i) for (i, var) in enumerate(variables)] - model.add_constraint(constraints.AllDifferent(diag1), tag=2) - model.add_constraint(constraints.AllDifferent(diag2), tag=3) + model.add_constraint(constraints.AllDifferent(diag1, model.new_constraint_tag())) + model.add_constraint(constraints.AllDifferent(diag2, model.new_constraint_tag())) - status = model.satisfy(proof=proof) + status = model.satisfy() match status: case SatisfactionResult.Satisfiable(solution): row_separator = "+---" * n + "+"