diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index b2e9069fa..6088df6ec 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().into()), + constraint_tag, + ) + } + /// Create a fresh propositional variable with a given name and return the literal with positive /// polarity. /// diff --git a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs index 7db972e70..1b86cec4a 100644 --- a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs +++ b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs @@ -136,6 +136,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/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 + "+" 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 8d8d88c5a..83920800d 100644 --- a/pumpkin-solver-py/src/constraints/globals.rs +++ b/pumpkin-solver-py/src/constraints/globals.rs @@ -29,10 +29,9 @@ macro_rules! python_constraint { pub fn post( self, solver: &mut pumpkin_solver::Solver, - variable_map: &VariableMap, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { pumpkin_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) } @@ -41,10 +40,9 @@ macro_rules! python_constraint { self, solver: &mut pumpkin_solver::Solver, reification_literal: pumpkin_solver::variables::Literal, - variable_map: &VariableMap, ) -> Result<(), pumpkin_solver::ConstraintOperationError> { pumpkin_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..31199bdc7 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,36 @@ impl Model { upper_bound: i32, name: Option<&str>, ) -> IntExpression { - let variable = ModelIntVar { - lower_bound, - upper_bound, - name: name.map(|n| n.to_owned()), + let domain_id = if let Some(name) = name { + self.solver + .new_named_bounded_integer(lower_bound, upper_bound, name) + } else { + self.solver.new_bounded_integer(lower_bound, upper_bound) }; - self.integer_variables.push(variable).into() + 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 { - self.boolean_variables - .push(ModelBoolVar { - name: name.map(|n| n.to_owned()), - integer_equivalent: None, - predicate: None, - }) - .into() + let literal = if let Some(name) = name { + self.solver.new_named_literal(name) + } else { + self.solver.new_literal() + }; + + self.brancher + .add_domain(literal.get_true_predicate().get_domain()); + + 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 +126,19 @@ 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); + self.brancher.add_domain(new_domain); - // Link the integer variable to the boolean variable. - self.boolean_variables[bool_variable].integer_equivalent = Some((int_variable, tag)); + let boolean_true = boolean.0.get_true_predicate(); - // Convert the integer variable to an appropriate integer expression based on the polarity - // of the boolean expression. - let polarity = boolean.get_polarity(); + 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"); - 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 +151,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)); - - let solver_setup = self.create_solver(proof); - - let Ok((mut solver, variable_map)) = solver_setup else { - return SatisfactionResult::Unsatisfiable(); - }; + #[pyo3(signature = (timeout=None))] + fn satisfy(&mut self, timeout: Option) -> SatisfactionResult { + let mut termination = get_termination(timeout); - 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 +204,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 +230,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 +246,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 +280,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 +293,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..d223d9650 100644 --- a/pumpkin-solver-py/src/variables.rs +++ b/pumpkin-solver-py/src/variables.rs @@ -1,5 +1,3 @@ -use pumpkin_solver::containers::KeyedVec; -use pumpkin_solver::containers::StorageKey; use pumpkin_solver::predicate; use pumpkin_solver::variables::AffineView; use pumpkin_solver::variables::DomainId; @@ -7,80 +5,41 @@ 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, -} +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct IntExpression(pub AffineView); -impl From for IntExpression { - fn from(variable: IntVariable) -> Self { - IntExpression { - variable, - offset: 0, - scale: 1, - } +impl From for IntExpression { + fn from(domain_id: DomainId) -> IntExpression { + IntExpression(domain_id.into()) } } +#[pymethods] impl IntExpression { - pub fn to_affine_view(self, variable_map: &VariableMap) -> AffineView { - let IntExpression { - variable, - offset, - scale, - } = self; + fn offset(&self, add_offset: i32) -> IntExpression { + IntExpression(self.0.offset(add_offset)) + } - variable_map - .get_integer(variable) - .scaled(scale) - .offset(offset) + fn scaled(&self, scaling: i32) -> IntExpression { + IntExpression(self.0.scaled(scaling)) } } -#[pymethods] -impl IntExpression { - fn offset(&self, add_offset: 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 + add_offset, - scale, - } +#[pymethods] +impl BoolExpression { + fn negate(&self) -> BoolExpression { + BoolExpression(!self.0) } +} - fn scaled(&self, scaling: i32) -> IntExpression { - let IntExpression { - variable, - offset, - scale, - } = *self; - - IntExpression { - variable, - offset: offset * scaling, - scale: scale * scaling, - } +impl From for BoolExpression { + fn from(literal: Literal) -> BoolExpression { + BoolExpression(literal) } } @@ -114,12 +73,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 +84,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] - } -} diff --git a/pumpkin-solver-py/tests/test_constraints.py b/pumpkin-solver-py/tests/test_constraints.py index 0901863a5..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,188 +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_operators()) - - -@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 = ( - list(generate_operators()) + list(generate_linear()) + list(generate_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)