diff --git a/Cargo.lock b/Cargo.lock index f63dff99b..3fc1b090a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -129,6 +129,24 @@ version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" +[[package]] +name = "bit-set" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2f926cc3060f09db9ebc5b52823d85268d24bb917e472c0c4bea35780a7d" +dependencies = [ + "bit-vec", +] + +[[package]] +name = "bit-vec" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b71798fca2c1fe1086445a7258a4bc81e6e49dcd24c8d0dd9a1e57395b603f51" +dependencies = [ + "serde", +] + [[package]] name = "bitfield" version = "0.19.4" @@ -2110,6 +2128,7 @@ dependencies = [ name = "pumpkin-core" version = "0.3.0" dependencies = [ + "bit-set", "bitfield", "bitfield-struct", "clap", diff --git a/pumpkin-crates/constraints/src/constraints/arithmetic/equality.rs b/pumpkin-crates/constraints/src/constraints/arithmetic/equality.rs index 9660a541d..1224e14a7 100644 --- a/pumpkin-crates/constraints/src/constraints/arithmetic/equality.rs +++ b/pumpkin-crates/constraints/src/constraints/arithmetic/equality.rs @@ -3,9 +3,9 @@ use pumpkin_core::Solver; use pumpkin_core::constraints::Constraint; use pumpkin_core::constraints::NegatableConstraint; use pumpkin_core::options::ReifiedPropagatorArgs; +use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::variables::IntegerVariable; -use pumpkin_core::variables::Literal; use pumpkin_core::variables::TransformableVariable; use pumpkin_propagators::arithmetic::BinaryEqualsPropagatorArgs; use pumpkin_propagators::arithmetic::BinaryNotEqualsPropagatorArgs; @@ -109,7 +109,7 @@ where fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { if self.terms.len() == 2 && !solver.is_logging_proof() { let _ = solver.add_propagator(ReifiedPropagatorArgs { @@ -184,7 +184,7 @@ where fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { let NotEqualConstraint { terms, diff --git a/pumpkin-crates/constraints/src/constraints/arithmetic/inequality.rs b/pumpkin-crates/constraints/src/constraints/arithmetic/inequality.rs index 5f928e358..a37377c38 100644 --- a/pumpkin-crates/constraints/src/constraints/arithmetic/inequality.rs +++ b/pumpkin-crates/constraints/src/constraints/arithmetic/inequality.rs @@ -2,9 +2,9 @@ use pumpkin_core::ConstraintOperationError; use pumpkin_core::Solver; use pumpkin_core::constraints::Constraint; use pumpkin_core::constraints::NegatableConstraint; +use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::variables::IntegerVariable; -use pumpkin_core::variables::Literal; use pumpkin_propagators::arithmetic::LinearLessOrEqualPropagatorArgs; /// Create the [`NegatableConstraint`] `∑ terms_i <= rhs`. @@ -119,7 +119,7 @@ impl Constraint for Inequality { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { LinearLessOrEqualPropagatorArgs { x: self.terms, diff --git a/pumpkin-crates/constraints/src/constraints/boolean.rs b/pumpkin-crates/constraints/src/constraints/boolean.rs index 32539f39b..8622de24c 100644 --- a/pumpkin-crates/constraints/src/constraints/boolean.rs +++ b/pumpkin-crates/constraints/src/constraints/boolean.rs @@ -1,19 +1,20 @@ use pumpkin_core::ConstraintOperationError; use pumpkin_core::Solver; use pumpkin_core::constraints::Constraint; +use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::variables::AffineView; +use pumpkin_core::variables::AnyInteger; use pumpkin_core::variables::DomainId; -use pumpkin_core::variables::Literal; use pumpkin_core::variables::TransformableVariable; -use super::equals; use super::less_than_or_equals; +use crate::equals; /// Creates the [`Constraint`] `∑ weights_i * bools_i <= rhs`. pub fn boolean_less_than_or_equals( weights: impl Into>, - bools: impl Into>, + bools: impl Into>, rhs: i32, constraint_tag: ConstraintTag, ) -> impl Constraint { @@ -28,7 +29,7 @@ pub fn boolean_less_than_or_equals( /// Creates the [`Constraint`] `∑ weights_i * bools_i == rhs`. pub fn boolean_equals( weights: impl Into>, - bools: impl Into>, + bools: impl Into>, rhs: DomainId, constraint_tag: ConstraintTag, ) -> impl Constraint { @@ -42,7 +43,7 @@ pub fn boolean_equals( struct BooleanLessThanOrEqual { weights: Box<[i32]>, - bools: Box<[Literal]>, + bools: Box<[Predicate]>, rhs: i32, constraint_tag: ConstraintTag, } @@ -57,7 +58,7 @@ impl Constraint for BooleanLessThanOrEqual { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { let domains = self.create_domains(); @@ -67,18 +68,18 @@ impl Constraint for BooleanLessThanOrEqual { } impl BooleanLessThanOrEqual { - fn create_domains(&self) -> Vec> { + fn create_domains(&self) -> Vec> { self.bools .iter() .enumerate() - .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index])) + .map(|(index, bool)| bool.scaled(self.weights[index])) .collect() } } struct BooleanEqual { weights: Box<[i32]>, - bools: Box<[Literal]>, + bools: Box<[Predicate]>, rhs: DomainId, constraint_tag: ConstraintTag, } @@ -93,7 +94,7 @@ impl Constraint for BooleanEqual { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { let domains = self.create_domains(); @@ -102,12 +103,12 @@ impl Constraint for BooleanEqual { } impl BooleanEqual { - fn create_domains(&self) -> Vec> { + fn create_domains(&self) -> Vec> { self.bools .iter() .enumerate() - .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index])) - .chain(std::iter::once(self.rhs.scaled(-1))) + .map(|(index, bool)| bool.scaled(self.weights[index]).into()) + .chain(std::iter::once(self.rhs.scaled(-1).into())) .collect() } } diff --git a/pumpkin-crates/constraints/src/constraints/clause.rs b/pumpkin-crates/constraints/src/constraints/clause.rs index aadc282bb..961172df6 100644 --- a/pumpkin-crates/constraints/src/constraints/clause.rs +++ b/pumpkin-crates/constraints/src/constraints/clause.rs @@ -2,14 +2,14 @@ use pumpkin_core::ConstraintOperationError; use pumpkin_core::Solver; use pumpkin_core::constraints::Constraint; use pumpkin_core::constraints::NegatableConstraint; +use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; -use pumpkin_core::variables::Literal; /// Creates the [`NegatableConstraint`] `\/ literal` /// /// Its negation is `/\ !literal` pub fn clause( - literals: impl Into>, + literals: impl Into>, constraint_tag: ConstraintTag, ) -> impl NegatableConstraint { Clause(literals.into(), constraint_tag) @@ -19,36 +19,32 @@ pub fn clause( /// /// Its negation is `\/ !literal` pub fn conjunction( - literals: impl Into>, + literals: impl Into>, constraint_tag: ConstraintTag, ) -> impl NegatableConstraint { Conjunction(literals.into(), constraint_tag) } -struct Clause(Vec, ConstraintTag); +struct Clause(Vec, ConstraintTag); impl Constraint for Clause { fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> { let Clause(clause, constraint_tag) = self; - solver.add_clause( - clause.iter().map(|literal| literal.get_true_predicate()), - constraint_tag, - ) + solver.add_clause(clause.iter().copied(), constraint_tag) } fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { let Clause(clause, constraint_tag) = self; solver.add_clause( clause .into_iter() - .chain(std::iter::once(!reification_literal)) - .map(|literal| literal.get_true_predicate()), + .chain(std::iter::once(!reification_literal)), constraint_tag, ) } @@ -64,7 +60,7 @@ impl NegatableConstraint for Clause { } } -struct Conjunction(Vec, ConstraintTag); +struct Conjunction(Vec, ConstraintTag); impl Constraint for Conjunction { fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> { @@ -72,25 +68,19 @@ impl Constraint for Conjunction { conjunction .into_iter() - .try_for_each(|lit| solver.add_clause([lit.get_true_predicate()], constraint_tag)) + .try_for_each(|lit| solver.add_clause([lit], constraint_tag)) } fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { let Conjunction(conjunction, constraint_tag) = self; - conjunction.into_iter().try_for_each(|lit| { - solver.add_clause( - [ - (!(reification_literal)).get_true_predicate(), - lit.get_true_predicate(), - ], - constraint_tag, - ) - }) + conjunction + .into_iter() + .try_for_each(|lit| solver.add_clause([(!(reification_literal)), lit], constraint_tag)) } } diff --git a/pumpkin-crates/constraints/src/constraints/cumulative.rs b/pumpkin-crates/constraints/src/constraints/cumulative.rs index 95674d623..6b2c300b2 100644 --- a/pumpkin-crates/constraints/src/constraints/cumulative.rs +++ b/pumpkin-crates/constraints/src/constraints/cumulative.rs @@ -4,9 +4,9 @@ use pumpkin_core::ConstraintOperationError; use pumpkin_core::Solver; use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::constraints::Constraint; +use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::variables::IntegerVariable; -use pumpkin_core::variables::Literal; use pumpkin_propagators::cumulative::ArgTask; use pumpkin_propagators::cumulative::options::CumulativeOptions; use pumpkin_propagators::cumulative::options::CumulativePropagationMethod; @@ -235,7 +235,7 @@ impl Constraint for CumulativeConstraint fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { match self.options.propagation_method { CumulativePropagationMethod::TimeTablePerPoint => TimeTablePerPointPropagator::new( diff --git a/pumpkin-crates/constraints/src/constraints/disjunctive_strict.rs b/pumpkin-crates/constraints/src/constraints/disjunctive_strict.rs index c857d3456..76905b2e7 100644 --- a/pumpkin-crates/constraints/src/constraints/disjunctive_strict.rs +++ b/pumpkin-crates/constraints/src/constraints/disjunctive_strict.rs @@ -1,9 +1,9 @@ use pumpkin_core::ConstraintOperationError; use pumpkin_core::Solver; use pumpkin_core::constraints::Constraint; +use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::variables::IntegerVariable; -use pumpkin_core::variables::Literal; use pumpkin_core::variables::TransformableVariable; use pumpkin_propagators::disjunctive::ArgDisjunctiveTask; use pumpkin_propagators::disjunctive::DisjunctiveConstructor; @@ -58,7 +58,7 @@ impl Constraint for DisjunctiveConstraint { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { // We post both the propagator on the lower-bound and the propagator on the upper-bound. DisjunctiveConstructor::new(self.tasks.clone(), self.constraint_tag) diff --git a/pumpkin-crates/constraints/src/constraints/table.rs b/pumpkin-crates/constraints/src/constraints/table.rs index 5aabda02c..a9bdb29e0 100644 --- a/pumpkin-crates/constraints/src/constraints/table.rs +++ b/pumpkin-crates/constraints/src/constraints/table.rs @@ -5,9 +5,10 @@ use pumpkin_core::Solver; use pumpkin_core::constraints::Constraint; use pumpkin_core::constraints::NegatableConstraint; use pumpkin_core::predicate; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::predicates::PredicateConstructor; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::variables::IntegerVariable; -use pumpkin_core::variables::Literal; /// Create the [table](https://sofdem.github.io/gccat/gccat/Cin_relation.html#uid22830) [`NegatableConstraint`]. /// @@ -65,11 +66,11 @@ impl Table { fn encode( self, solver: &mut Solver, - reification_literal: Option, + reification_literal: Option, ) -> Result<(), ConstraintOperationError> { // 1. Create a variable `y_i` that selects the row from the table which is chosen. let ys: Vec<_> = (0..self.table.len()) - .map(|_| solver.new_literal()) + .map(|_| solver.new_bounded_integer(0, 1).lower_bound_predicate(1)) .collect(); // 2. Setup the implications between values and `ys`. @@ -92,20 +93,20 @@ impl Table { // For every `support in supports`: `support -> condition` for support in supports.iter() { - let mut clause = vec![support.get_false_predicate(), condition]; + let mut clause = vec![!*support, condition]; // Account for possible reification. // l -> clause - clause.extend(reification_literal.iter().map(|l| l.get_false_predicate())); + clause.extend(reification_literal.iter().map(|l| !*l)); solver.add_clause(clause, self.constraint_tag)?; } // `condition -> (\/ supports)` let mut clause = vec![!condition]; - clause.extend(supports.iter().map(|l| l.get_true_predicate())); + clause.extend(supports.iter()); // Account for possible reification. - clause.extend(reification_literal.iter().map(|l| l.get_false_predicate())); + clause.extend(reification_literal.iter().map(|l| !*l)); } } @@ -129,7 +130,7 @@ impl Constraint for Table { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { self.encode(solver, Some(reification_literal)) } @@ -176,7 +177,7 @@ impl Constraint for NegativeTable { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { for row in self.table { let clause: Vec<_> = self @@ -184,7 +185,7 @@ impl Constraint for NegativeTable { .iter() .zip(row) .map(|(x, value)| predicate![x != value]) - .chain(std::iter::once(reification_literal.get_false_predicate())) + .chain(std::iter::once(!reification_literal)) .collect(); solver.add_clause(clause, self.constraint_tag)?; diff --git a/pumpkin-crates/core/Cargo.toml b/pumpkin-crates/core/Cargo.toml index 9d7129e28..2a340d14c 100644 --- a/pumpkin-crates/core/Cargo.toml +++ b/pumpkin-crates/core/Cargo.toml @@ -30,6 +30,7 @@ clap = { version = "4.5.40", optional = true, features=["derive"] } indexmap = "2.10.0" dyn-clone = "1.0.20" flate2 = { version = "1.1.2" } +bit-set = "0.10.0" [target.'cfg(target_arch = "wasm32")'.dependencies] web-time = "1.1" diff --git a/pumpkin-crates/core/src/api/mod.rs b/pumpkin-crates/core/src/api/mod.rs index 22f3a90d7..b4941bbc7 100644 --- a/pumpkin-crates/core/src/api/mod.rs +++ b/pumpkin-crates/core/src/api/mod.rs @@ -37,23 +37,26 @@ pub mod variables { //! information unaltered, or apply transformations which can be performed without the need of //! constraints. //! - //! We define 2 types of variables: - //! - Integer Variables ([`IntegerVariable`]) - These are represented by [`DomainId`]s when - //! interacting with the [`Solver`]. These variables can be created using - //! [`Solver::new_bounded_integer`] when creating a variable with the domain between a - //! lower-bound and an upper-bound or using [`Solver::new_sparse_integer`] when creating a - //! variable with holes in the domain. These variables can be transformed (according to the - //! trait [`TransformableVariable`]) to create an [`AffineView`]. - //! - Literals ([`Literal`]) - These specify booleans that can be used when interacting with the - //! [`Solver`]. A [`Literal`] can be created using [`Solver::new_literal`]. + //! We define the following types of variables: + //! - Integer Variables ([`IntegerVariable`]) - These can be represented using two types: + //! - Represented by [`DomainId`]s when interacting with the [`Solver`]. These variables can be + //! created using [`Solver::new_bounded_integer`] when creating a variable with the domain + //! between a lower-bound and an upper-bound or using [`Solver::new_sparse_integer`] when + //! creating a variable with holes in the domain. These variables can be transformed + //! (according to the trait [`TransformableVariable`]) to create an [`AffineView`]. + //! - Represented by [`Predicate`]s when interacting with the [`Solver`]. These can be created + //! over [`DomainId`]s using the [`crate::predicate`] macro. [`Predicate`]s are also treated + //! as integer variables by the [`Solver`]. #[cfg(doc)] use crate::Solver; pub use crate::engine::Reason; pub use crate::engine::variables::AffineView; + pub use crate::engine::variables::AnyInteger; pub use crate::engine::variables::DomainId; pub use crate::engine::variables::IntegerVariable; - pub use crate::engine::variables::Literal; pub use crate::engine::variables::TransformableVariable; + #[cfg(doc)] + use crate::predicates::Predicate; } pub mod options { @@ -109,8 +112,6 @@ pub mod predicates { pub use crate::engine::predicates::predicate::Predicate; pub use crate::engine::predicates::predicate::PredicateType; pub use crate::engine::predicates::predicate_constructor::PredicateConstructor; - #[cfg(doc)] - use crate::variables::Literal; } pub mod state { diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index e5f866dd3..69f5851c2 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -24,7 +24,6 @@ use crate::engine::predicates::predicate::Predicate; use crate::engine::termination::TerminationCondition; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; -use crate::engine::variables::Literal; use crate::optimisation::OptimisationProcedure; #[cfg(doc)] use crate::optimisation::linear_sat_unsat::LinearSatUnsat; @@ -54,6 +53,7 @@ use crate::statistics::log_statistic_postfix; /// ```rust /// # use pumpkin_core::Solver; /// # use pumpkin_core::variables::TransformableVariable; +/// # use pumpkin_core::predicate; /// let mut solver = Solver::default(); /// /// // Integer Variables @@ -75,19 +75,15 @@ use crate::statistics::log_statistic_postfix; /// /// /// // Propositional Variable +/// // +/// // Propositional variables do not explicitly exist in Pumpkin, but atomic constraints can be +/// // treated as integer variable. /// -/// // We can create a literal -/// let literal = solver.new_literal(); +/// // We can create a new Boolean variable first. +/// let boolean = solver.new_bounded_integer(0, 1); /// -/// // We can also create such a variable with a name -/// let named_literal = solver.new_named_literal("z"); -/// -/// // We can also get the predicate from the literal -/// let true_predicate = literal.get_true_predicate(); -/// -/// // We can also create an iterator of new literals and get a number of them at once -/// let list_of_5_literals = solver.new_literals().take(5).collect::>(); -/// assert_eq!(list_of_5_literals.len(), 5); +/// // And then create a predicate over this boolean variable. +/// let predicate = predicate!(boolean >= 1); /// ``` /// /// # Using the Solver @@ -96,16 +92,13 @@ use crate::statistics::log_statistic_postfix; pub struct Solver { /// The internal [`ConstraintSatisfactionSolver`] which is used to solve the problems. pub(crate) satisfaction_solver: ConstraintSatisfactionSolver, - true_literal: Literal, } impl Default for Solver { fn default() -> Self { let satisfaction_solver = ConstraintSatisfactionSolver::default(); - let true_literal = Literal::new(Predicate::trivially_true().get_domain()); Self { satisfaction_solver, - true_literal, } } } @@ -114,10 +107,8 @@ impl Solver { /// Creates a solver with the provided [`SolverOptions`]. pub fn with_options(solver_options: SolverOptions) -> Self { let satisfaction_solver = ConstraintSatisfactionSolver::new(solver_options); - let true_literal = Literal::new(Predicate::trivially_true().get_domain()); Self { satisfaction_solver, - true_literal, } } @@ -159,12 +150,9 @@ impl Solver { /// Methods to retrieve information about variables impl Solver { - /// Get the value of the given [`Literal`] at the root level (after propagation), which could be - /// unassigned. - pub fn get_literal_value(&self, literal: Literal) -> Option { - self.satisfaction_solver.get_literal_value(literal) + pub fn get_predicate_value(&self, predicate: Predicate) -> Option { + self.satisfaction_solver.evaluate_predicate(predicate) } - /// Get the lower-bound of the given [`IntegerVariable`] at the root level (after propagation). pub fn lower_bound(&self, variable: &impl IntegerVariable) -> i32 { self.satisfaction_solver.get_lower_bound(variable) @@ -183,88 +171,6 @@ impl Solver { /// Functions to create and retrieve integer and propositional variables. impl Solver { - /// Returns an infinite iterator of positive literals of new variables. The new variables will - /// be unnamed. - /// - /// # Example - /// ``` - /// # use pumpkin_core::Solver; - /// # use pumpkin_core::variables::Literal; - /// let mut solver = Solver::default(); - /// let literals: Vec = solver.new_literals().take(5).collect(); - /// - /// // `literals` contains 5 positive literals of newly created propositional variables. - /// assert_eq!(literals.len(), 5); - /// ``` - /// - /// Note that this method captures the lifetime of the immutable reference to `self`. - pub fn new_literals(&mut self) -> impl Iterator + '_ { - std::iter::from_fn(|| Some(self.new_literal())) - } - - /// Create a fresh propositional variable and return the literal with positive polarity. - /// - /// # Example - /// ```rust - /// # use pumpkin_core::Solver; - /// let mut solver = Solver::default(); - /// - /// // We can create a literal - /// let literal = solver.new_literal(); - /// ``` - pub fn new_literal(&mut self) -> Literal { - self.satisfaction_solver.create_new_literal(None) - } - - pub fn new_literal_for_predicate( - &mut self, - predicate: Predicate, - constraint_tag: ConstraintTag, - ) -> Literal { - self.satisfaction_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. - /// - /// # Example - /// ```rust - /// # use pumpkin_core::Solver; - /// let mut solver = Solver::default(); - /// - /// // We can also create such a variable with a name - /// let named_literal = solver.new_named_literal("z"); - /// ``` - pub fn new_named_literal(&mut self, name: impl Into) -> Literal { - let name = name.into(); - self.satisfaction_solver - .create_new_literal(Some(name.into())) - } - - /// Get a literal which is always true. - pub fn get_true_literal(&self) -> Literal { - self.true_literal - } - - /// Get a literal which is always false. - pub fn get_false_literal(&self) -> Literal { - !self.true_literal - } - /// Create a new integer variable with the given bounds. /// /// # Example diff --git a/pumpkin-crates/core/src/basic_types/function.rs b/pumpkin-crates/core/src/basic_types/function.rs index c1b8b0f4d..57411c259 100644 --- a/pumpkin-crates/core/src/basic_types/function.rs +++ b/pumpkin-crates/core/src/basic_types/function.rs @@ -1,13 +1,13 @@ use super::solution::ProblemSolution; use crate::basic_types::SolutionReference; use crate::containers::HashMap; -use crate::variables::Literal; +use crate::predicates::Predicate; -/// A struct which represents a linear function over weighted [`Literal`]s, and a +/// A struct which represents a linear function over weighted [`Predicate`]s, and a /// constant term. #[derive(Clone, Default, Debug)] pub struct Function { - literals: HashMap, + literals: HashMap, constant_term: u64, } @@ -16,15 +16,15 @@ impl Function { self.literals.values().sum() } - pub fn add_weighted_literal(&mut self, literal: Literal, weight: u64) { - *self.literals.entry(!literal).or_insert(0) += weight; + pub fn add_weighted_literal(&mut self, predicate: Predicate, weight: u64) { + *self.literals.entry(!predicate).or_insert(0) += weight; } pub fn add_constant_term(&mut self, value: u64) { self.constant_term += value; } - pub fn get_literal_terms(&self) -> impl Iterator { + pub fn get_literal_terms(&self) -> impl Iterator { self.literals.iter() } @@ -35,7 +35,7 @@ impl Function { pub fn evaluate_solution(&self, solution: SolutionReference) -> u64 { let mut value: u64 = self.constant_term; for (literal, weight) in self.get_literal_terms() { - value += weight * (solution.get_literal_value(*literal)) as u64; + value += weight * (solution.get_predicate_value(*literal)) as u64; } value } @@ -43,7 +43,7 @@ impl Function { pub fn evaluate_assignment(&self, solution: SolutionReference) -> u64 { let mut value: u64 = self.constant_term; for (literal, weight) in self.get_literal_terms() { - value += weight * solution.get_literal_value(*literal) as u32 as u64; + value += weight * solution.get_predicate_value(*literal) as u32 as u64; } value } diff --git a/pumpkin-crates/core/src/basic_types/solution.rs b/pumpkin-crates/core/src/basic_types/solution.rs index 4dbdb583f..2262bd603 100644 --- a/pumpkin-crates/core/src/basic_types/solution.rs +++ b/pumpkin-crates/core/src/basic_types/solution.rs @@ -1,7 +1,7 @@ use crate::engine::Assignments; use crate::engine::variables::DomainGeneratorIterator; use crate::engine::variables::DomainId; -use crate::engine::variables::Literal; +use crate::predicates::Predicate; use crate::propagation::HasAssignments; use crate::variables::IntegerVariable; @@ -12,7 +12,7 @@ pub trait ProblemSolution { fn get_integer_value(&self, var: Var) -> i32; - fn get_literal_value(&self, literal: Literal) -> bool; + fn get_predicate_value(&self, predicate: Predicate) -> bool; } impl ProblemSolution for T { @@ -27,9 +27,9 @@ impl ProblemSolution for T { .expect("Expected retrieved integer variable from solution to be assigned") } - fn get_literal_value(&self, literal: Literal) -> bool { + fn get_predicate_value(&self, predicate: Predicate) -> bool { self.assignments() - .evaluate_predicate(literal.get_true_predicate()) + .evaluate_predicate(predicate) .expect("Expected to retrieve concrete truth value from solution to be assigned.") } } diff --git a/pumpkin-crates/core/src/branching/value_selection/in_domain_random.rs b/pumpkin-crates/core/src/branching/value_selection/in_domain_random.rs index f6c3a2d92..6c6750aa1 100644 --- a/pumpkin-crates/core/src/branching/value_selection/in_domain_random.rs +++ b/pumpkin-crates/core/src/branching/value_selection/in_domain_random.rs @@ -4,7 +4,6 @@ use crate::branching::value_selection::ValueSelector; use crate::engine::predicates::predicate::Predicate; use crate::engine::variables::DomainId; use crate::predicate; -use crate::variables::Literal; /// A [`ValueSelector`] which assigns to a random value in the domain. #[derive(Debug, Clone, Copy)] @@ -35,16 +34,16 @@ impl ValueSelector for InDomainRandom { } } -impl ValueSelector for InDomainRandom { +impl ValueSelector for InDomainRandom { fn select_value( &mut self, context: &mut SelectionContext, - decision_variable: Literal, + decision_variable: Predicate, ) -> Predicate { if context.random().generate_bool(0.5) { - decision_variable.get_true_predicate() + decision_variable } else { - (!decision_variable).get_true_predicate() + !decision_variable } } diff --git a/pumpkin-crates/core/src/branching/variable_selection/input_order.rs b/pumpkin-crates/core/src/branching/variable_selection/input_order.rs index 59928a46f..1b7c7613c 100644 --- a/pumpkin-crates/core/src/branching/variable_selection/input_order.rs +++ b/pumpkin-crates/core/src/branching/variable_selection/input_order.rs @@ -4,7 +4,7 @@ use crate::branching::SelectionContext; use crate::branching::brancher::BrancherEvent; use crate::branching::variable_selection::VariableSelector; use crate::engine::variables::DomainId; -use crate::variables::Literal; +use crate::predicates::Predicate; /// A [`VariableSelector`] which selects the first variable which is not fixed given the order in /// the provided list. @@ -37,11 +37,11 @@ impl VariableSelector for InputOrder { } } -impl VariableSelector for InputOrder { - fn select_variable(&mut self, context: &mut SelectionContext) -> Option { +impl VariableSelector for InputOrder { + fn select_variable(&mut self, context: &mut SelectionContext) -> Option { self.variables .iter() - .find(|&variable| !context.is_predicate_assigned(variable.get_true_predicate())) + .find(|&variable| !context.is_predicate_assigned(*variable)) .copied() } diff --git a/pumpkin-crates/core/src/constraints/constraint_poster.rs b/pumpkin-crates/core/src/constraints/constraint_poster.rs index fec640a16..69d1b2b58 100644 --- a/pumpkin-crates/core/src/constraints/constraint_poster.rs +++ b/pumpkin-crates/core/src/constraints/constraint_poster.rs @@ -4,7 +4,7 @@ use super::Constraint; use super::NegatableConstraint; use crate::ConstraintOperationError; use crate::Solver; -use crate::variables::Literal; +use crate::predicates::Predicate; /// A structure which is responsible for adding the created [`Constraint`]s to the /// [`Solver`]. For an example on how to use this, see [`crate::constraints`]. @@ -39,7 +39,7 @@ impl ConstraintPoster<'_, ConstraintImpl> { /// to a root-level conflict. pub fn implied_by( mut self, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { self.constraint .take() @@ -54,7 +54,7 @@ impl ConstraintPoster<'_, ConstraintImpl> { /// /// This method returns a [`ConstraintOperationError`] if the addition of the [`Constraint`] led /// to a root-level conflict. - pub fn reify(mut self, reification_literal: Literal) -> Result<(), ConstraintOperationError> { + pub fn reify(mut self, reification_literal: Predicate) -> Result<(), ConstraintOperationError> { self.constraint .take() .unwrap() diff --git a/pumpkin-crates/core/src/constraints/mod.rs b/pumpkin-crates/core/src/constraints/mod.rs index 1e7f34304..c951fc88f 100644 --- a/pumpkin-crates/core/src/constraints/mod.rs +++ b/pumpkin-crates/core/src/constraints/mod.rs @@ -1,9 +1,9 @@ //! Defines the main building blocks of constraints. use crate::ConstraintOperationError; use crate::Solver; +use crate::predicates::Predicate; use crate::propagation::PropagatorConstructor; use crate::propagators::reified_propagator::ReifiedPropagatorArgs; -use crate::variables::Literal; mod constraint_poster; pub use constraint_poster::ConstraintPoster; @@ -34,7 +34,7 @@ pub trait Constraint { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError>; } @@ -50,7 +50,7 @@ where fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { let _ = solver.add_propagator(ReifiedPropagatorArgs { propagator: self, @@ -68,7 +68,7 @@ impl Constraint for Vec { fn implied_by( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> { self.into_iter() .try_for_each(|c| c.implied_by(solver, reification_literal)) @@ -97,7 +97,7 @@ pub trait NegatableConstraint: Constraint { fn reify( self, solver: &mut Solver, - reification_literal: Literal, + reification_literal: Predicate, ) -> Result<(), ConstraintOperationError> where Self: Sized, diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 36e33a1aa..d0437cc51 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -15,7 +15,6 @@ use rand::rngs::SmallRng; use super::solver_statistics::SolverStatistics; use super::termination::TerminationCondition; use super::variables::IntegerVariable; -use super::variables::Literal; #[cfg(doc)] use crate::Solver; use crate::basic_types::CSPSolverExecutionFlag; @@ -326,37 +325,6 @@ impl ConstraintSatisfactionSolver { self.state.new_constraint_tag() } - pub fn create_new_literal(&mut self, name: Option>) -> Literal { - self.state.new_literal(name) - } - - pub fn create_new_literal_for_predicate( - &mut self, - predicate: Predicate, - name: Option>, - constraint_tag: ConstraintTag, - ) -> Literal { - let literal = self.state.new_literal(name); - - self.internal_parameters - .proof_log - .reify_predicate(literal, predicate); - - // If literal --> predicate - let _ = self.add_clause( - vec![!literal.get_true_predicate(), predicate], - constraint_tag, - ); - - // If !literal --> !predicate - let _ = self.add_clause( - vec![!literal.get_false_predicate(), !predicate], - constraint_tag, - ); - - literal - } - /// Create a new integer variable. Its domain will have the given lower and upper bounds. pub fn create_new_integer_variable( &mut self, @@ -452,8 +420,8 @@ impl ConstraintSatisfactionSolver { }) } - pub fn get_literal_value(&self, literal: Literal) -> Option { - self.state.get_literal_value(literal) + pub fn evaluate_predicate(&self, predicate: Predicate) -> Option { + self.state.truth_value(predicate) } /// Get the lower bound for the given variable. @@ -1247,8 +1215,12 @@ mod tests { let c1 = solver.new_constraint_tag(); let c2 = solver.new_constraint_tag(); let c3 = solver.new_constraint_tag(); - let lit1 = solver.create_new_literal(None).get_true_predicate(); - let lit2 = solver.create_new_literal(None).get_true_predicate(); + + let i_1 = solver.create_new_integer_variable(0, 1, None); + let lit1 = predicate!(i_1 == 1); + + let i_2 = solver.create_new_integer_variable(0, 1, None); + let lit2 = predicate!(i_2 == 1); let _ = solver.add_clause([lit1, lit2], c1); let _ = solver.add_clause([lit1, !lit2], c2); @@ -1260,7 +1232,10 @@ mod tests { fn core_extraction_unit_core() { let mut solver = ConstraintSatisfactionSolver::default(); let constraint_tag = solver.new_constraint_tag(); - let lit1 = solver.create_new_literal(None).get_true_predicate(); + + let i_1 = solver.create_new_integer_variable(0, 1, None); + let lit1 = predicate!(i_1 == 1); + let _ = solver.add_clause(vec![lit1], constraint_tag); run_test( @@ -1320,9 +1295,15 @@ mod tests { let mut solver = ConstraintSatisfactionSolver::default(); let c1 = solver.new_constraint_tag(); let c2 = solver.new_constraint_tag(); - let lit1 = solver.create_new_literal(None).get_true_predicate(); - let lit2 = solver.create_new_literal(None).get_true_predicate(); - let lit3 = solver.create_new_literal(None).get_true_predicate(); + + let i_1 = solver.create_new_integer_variable(0, 1, None); + let lit1 = predicate!(i_1 == 1); + + let i_2 = solver.create_new_integer_variable(0, 1, None); + let lit2 = predicate!(i_2 == 1); + + let i_3 = solver.create_new_integer_variable(0, 1, None); + let lit3 = predicate!(i_3 == 1); let _ = solver.add_clause([lit1, lit2, lit3], c1); let _ = solver.add_clause([lit1, !lit2, lit3], c2); @@ -1365,9 +1346,14 @@ mod tests { let mut solver = ConstraintSatisfactionSolver::default(); let constraint_tag = solver.new_constraint_tag(); - let lit1 = solver.create_new_literal(None).get_true_predicate(); - let lit2 = solver.create_new_literal(None).get_true_predicate(); - let lit3 = solver.create_new_literal(None).get_true_predicate(); + let i_1 = solver.create_new_integer_variable(0, 1, None); + let lit1 = predicate!(i_1 == 1); + + let i_2 = solver.create_new_integer_variable(0, 1, None); + let lit2 = predicate!(i_2 == 1); + + let i_3 = solver.create_new_integer_variable(0, 1, None); + let lit3 = predicate!(i_3 == 1); let _ = solver.add_clause([lit1, lit2, lit3], constraint_tag); (solver, vec![lit1, lit2, lit3]) diff --git a/pumpkin-crates/core/src/engine/cp/assignments.rs b/pumpkin-crates/core/src/engine/cp/assignments.rs index 5ccbbb455..5b24eabec 100644 --- a/pumpkin-crates/core/src/engine/cp/assignments.rs +++ b/pumpkin-crates/core/src/engine/cp/assignments.rs @@ -285,6 +285,15 @@ impl Assignments { self.is_domain_assigned(var).then(|| var.lower_bound(self)) } + pub(crate) fn get_assigned_value_at_trail_position( + &self, + var: &Var, + trail_position: usize, + ) -> Option { + self.is_domain_assigned_at_trail_position(var, trail_position) + .then(|| var.lower_bound(self)) + } + pub(crate) fn is_decision_predicate(&self, predicate: &Predicate) -> bool { let domain = predicate.get_domain(); if let Some(trail_position) = self.get_trail_position(predicate) @@ -365,6 +374,15 @@ impl Assignments { var.lower_bound(self) == var.upper_bound(self) } + pub(crate) fn is_domain_assigned_at_trail_position( + &self, + var: &Var, + trail_position: usize, + ) -> bool { + var.lower_bound_at_trail_position(self, trail_position) + == var.upper_bound_at_trail_position(self, trail_position) + } + /// Returns the index of the trail entry at which point the given predicate became true. /// In case the predicate is not true, then the function returns None. /// Note that it is not necessary for the predicate to be explicitly present on the trail, @@ -612,6 +630,66 @@ impl Assignments { Ok(update_took_place) } + /// Determines whether the provided [`Predicate`] holds at the provided trail position. In case + /// the predicate is not assigned yet (neither true nor false), returns None. + pub(crate) fn evaluate_predicate_at_trail_position( + &self, + predicate: Predicate, + trail_position: usize, + ) -> Option { + let domain_id = predicate.get_domain(); + let value = predicate.get_right_hand_side(); + + match predicate.get_predicate_type() { + PredicateType::LowerBound => { + if self.get_lower_bound_at_trail_position(domain_id, trail_position) >= value { + Some(true) + } else if self.get_upper_bound_at_trail_position(domain_id, trail_position) < value + { + Some(false) + } else { + None + } + } + PredicateType::UpperBound => { + if self.get_upper_bound_at_trail_position(domain_id, trail_position) <= value { + Some(true) + } else if self.get_lower_bound_at_trail_position(domain_id, trail_position) > value + { + Some(false) + } else { + None + } + } + PredicateType::NotEqual => { + if !self.is_value_in_domain_at_trail_position(domain_id, value, trail_position) { + Some(true) + } else if let Some(assigned_value) = + self.get_assigned_value_at_trail_position(&domain_id, trail_position) + { + // Previous branch concluded the value is not in the domain, so if the variable + // is assigned, then it is assigned to the not equals value. + pumpkin_assert_simple!(assigned_value == value); + Some(false) + } else { + None + } + } + PredicateType::Equal => { + if !self.is_value_in_domain_at_trail_position(domain_id, value, trail_position) { + Some(false) + } else if let Some(assigned_value) = + self.get_assigned_value_at_trail_position(&domain_id, trail_position) + { + pumpkin_assert_moderate!(assigned_value == value); + Some(true) + } else { + None + } + } + } + } + /// Determines whether the provided [`Predicate`] holds in the current state of the /// [`Assignments`]. In case the predicate is not assigned yet (neither true nor false), /// returns None. @@ -668,6 +746,15 @@ impl Assignments { .is_some_and(|truth_value| truth_value) } + pub(crate) fn is_predicate_satisfied_at_trail_position( + &self, + predicate: Predicate, + trail_position: usize, + ) -> bool { + self.evaluate_predicate_at_trail_position(predicate, trail_position) + .is_some_and(|truth_value| truth_value) + } + #[allow(unused, reason = "makes sense to have in this API")] pub(crate) fn is_predicate_falsified(&self, predicate: Predicate) -> bool { self.evaluate_predicate(predicate) diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 4bbcdf795..c7766a304 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -11,7 +11,6 @@ use crate::engine::State; use crate::engine::predicates::predicate::Predicate; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; -use crate::engine::variables::Literal; use crate::options::LearningOptions; use crate::predicate; use crate::predicates::PropositionalConjunction; @@ -84,11 +83,6 @@ impl TestSolver { self.state.new_sparse_variable(values, None) } - pub fn new_literal(&mut self) -> Literal { - let domain_id = self.new_variable(0, 1); - Literal::new(domain_id) - } - pub fn new_propagator( &mut self, constructor: Constructor, @@ -197,13 +191,6 @@ impl TestSolver { } } - pub fn is_literal_false(&self, literal: Literal) -> bool { - self.state - .assignments - .evaluate_predicate(literal.get_true_predicate()) - .is_some_and(|truth_value| !truth_value) - } - pub fn upper_bound(&self, var: DomainId) -> i32 { self.state.assignments.get_upper_bound(var) } @@ -214,21 +201,15 @@ impl TestSolver { Ok(()) } - pub fn set_literal(&mut self, literal: Literal, truth_value: bool) -> Result<(), EmptyDomain> { - let _ = match truth_value { - true => self.state.assignments.post_predicate( - literal.get_true_predicate(), - None, - &mut self.state.notification_engine, - )?, - false => self.state.assignments.post_predicate( - (!literal).get_true_predicate(), - None, - &mut self.state.notification_engine, - )?, - }; + pub fn set_predicate(&mut self, predicate: Predicate) -> Result<(), EmptyDomain> { + self.state + .assignments + .post_predicate(predicate, None, &mut self.state.notification_engine) + .map(|_| ()) + } - Ok(()) + pub fn evaluate_predicate(&self, predicate: Predicate) -> Option { + self.state.assignments.evaluate_predicate(predicate) } pub fn propagate(&mut self, propagator: PropagatorId) -> Result<(), Conflict> { @@ -305,18 +286,6 @@ impl TestSolver { PropositionalConjunction::from(predicates) } - pub fn get_reason_bool( - &mut self, - literal: Literal, - truth_value: bool, - ) -> PropositionalConjunction { - let predicate = match truth_value { - true => literal.get_true_predicate(), - false => (!literal).get_true_predicate(), - }; - self.get_reason_int(predicate) - } - pub fn assert_bounds(&self, var: DomainId, lb: i32, ub: i32) { let actual_lb = self.lower_bound(var); let actual_ub = self.upper_bound(var); diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs index 9d3220c2c..517dec2bc 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs @@ -4,8 +4,11 @@ use enumset::EnumSet; use enumset::EnumSetType; use crate::containers::KeyedVec; +use crate::engine::Assignments; +use crate::engine::TrailedValues; use crate::engine::notifications::NotificationEngine; use crate::engine::variables::DomainId; +use crate::predicates::Predicate; use crate::propagation::PropagatorVarId; #[derive(Default, Debug, Clone)] @@ -22,6 +25,40 @@ pub(crate) struct WatchListDomainEvents { pub struct Watchers<'a> { propagator_var: PropagatorVarId, notification_engine: &'a mut NotificationEngine, + trailed_values: &'a mut TrailedValues, + assignments: &'a Assignments, +} + +impl<'a> Watchers<'a> { + pub(crate) fn watch_predicate(&mut self, predicate: Predicate, events: EnumSet) { + self.notification_engine.watch_predicate_events( + predicate, + events, + self.propagator_var, + self.trailed_values, + self.assignments, + ) + } + + pub(crate) fn watch_predicate_backtrack( + &mut self, + predicate: Predicate, + events: EnumSet, + ) { + self.notification_engine.watch_predicate_events_backtrack( + predicate, + events, + self.propagator_var, + self.trailed_values, + self.assignments, + ) + } + + pub(crate) fn unwatch_predicate(&mut self, predicate: Predicate) { + let predicate_id = self.notification_engine.get_id(predicate); + self.notification_engine + .unwatch_predicate(predicate_id, self.propagator_var.propagator); + } } /// A description of the kinds of events that can happen on a domain variable. @@ -95,10 +132,14 @@ impl<'a> Watchers<'a> { pub(crate) fn new( propagator_var: PropagatorVarId, notification_engine: &'a mut NotificationEngine, + trailed_values: &'a mut TrailedValues, + assignments: &'a Assignments, ) -> Self { Watchers { propagator_var, notification_engine, + trailed_values, + assignments, } } diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/mod.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/mod.rs index ddf607046..baac4a23d 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/mod.rs @@ -6,3 +6,5 @@ pub use domain_event_watch_list::DomainEvent; pub(crate) use domain_event_watch_list::WatchListDomainEvents; pub(crate) use domain_event_watch_list::Watchers; pub(crate) use event_sink::*; +pub(crate) use watch_list_predicate_id::PredicateWatchList; +mod watch_list_predicate_id; diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/watch_list_predicate_id.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/watch_list_predicate_id.rs new file mode 100644 index 000000000..ad2f49d6c --- /dev/null +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/watch_list_predicate_id.rs @@ -0,0 +1,307 @@ +use enumset::EnumSet; + +use crate::basic_types::PredicateId; +use crate::containers::HashMap; +use crate::containers::KeyedVec; +use crate::engine::Assignments; +use crate::engine::TrailedValues; +use crate::engine::notifications::PredicateNotifier; +use crate::predicates::Predicate; +use crate::propagation::DomainEvent; +use crate::propagation::LocalId; +use crate::propagation::PropagatorVarId; +use crate::state::PropagatorId; + +#[derive(Debug, Default, Clone)] +pub(crate) struct PredicateWatchList { + /// The watch list from predicates to propagators. + pub(crate) watch_list_predicate_id: KeyedVec>, + pub(crate) watch_list_predicate_id_backtrack: HashMap>, +} + +#[derive(Debug, Clone, Copy)] +pub(crate) struct PredicateWatcher { + pub(crate) propagator_id: PropagatorId, + pub(crate) local_id: Option, + pub(crate) events: Option>, +} + +impl PredicateWatcher { + pub(crate) fn new_predicate_watcher(propagator_id: PropagatorId) -> Self { + PredicateWatcher { + propagator_id, + local_id: None, + events: None, + } + } + + pub(crate) fn new_literal_watcher( + propagator_id: PropagatorId, + local_id: LocalId, + events: EnumSet, + ) -> Self { + Self { + propagator_id, + local_id: Some(local_id), + events: Some(events), + } + } +} + +impl PredicateWatchList { + pub(crate) fn watch_predicate_id( + &mut self, + predicate_id: PredicateId, + propagator_id: PropagatorId, + assignments: &Assignments, + trailed_values: &mut TrailedValues, + predicate_notifier: &mut PredicateNotifier, + ) { + self.watch_list_predicate_id + .accomodate(predicate_id, vec![]); + self.watch_list_predicate_id[predicate_id] + .push(PredicateWatcher::new_predicate_watcher(propagator_id)); + + predicate_notifier.track_predicate(predicate_id, trailed_values, assignments); + } + + pub(crate) fn watch_predicate( + &mut self, + predicate: Predicate, + propagator_id: PropagatorId, + predicate_notifier: &mut PredicateNotifier, + assignments: &Assignments, + trailed_values: &mut TrailedValues, + ) -> PredicateId { + let predicate_id = predicate_notifier.predicate_to_id.get_id(predicate); + self.watch_predicate_id( + predicate_id, + propagator_id, + assignments, + trailed_values, + predicate_notifier, + ); + + predicate_id + } + + pub(crate) fn unwatch_predicate( + &mut self, + predicate_id: PredicateId, + propagator_to_unwatch: PropagatorId, + ) { + if let Some(watch_list) = self.watchers_predicate_id_mut(predicate_id) { + let index = watch_list + .iter() + .position(|&watched_propagator| { + watched_propagator.propagator_id == propagator_to_unwatch + }) + .expect("cannot unwatch a (predicate, propagator) pair if it was not watched"); + + let _ = watch_list.swap_remove(index); + } + + // TODO: Can we remove the predicate from being tracked if it does not have watchers? + } + + fn add_literal_watcher( + &mut self, + predicate: Predicate, + propagator_var: PropagatorVarId, + predicate_notifier: &mut PredicateNotifier, + trailed_values: &mut TrailedValues, + assignments: &Assignments, + events: EnumSet, + ) { + let predicate_id = predicate_notifier.predicate_to_id.get_id(predicate); + + self.watch_list_predicate_id + .accomodate(predicate_id, vec![]); + self.watch_list_predicate_id[predicate_id].push(PredicateWatcher::new_literal_watcher( + propagator_var.propagator, + propagator_var.variable, + events, + )); + predicate_notifier.track_predicate(predicate_id, trailed_values, assignments); + } + + pub(crate) fn watch_predicate_events( + &mut self, + predicate: Predicate, + propagator_var: PropagatorVarId, + events: EnumSet, + predicate_notifier: &mut PredicateNotifier, + assignments: &Assignments, + trailed_values: &mut TrailedValues, + ) { + for event in events { + match event { + DomainEvent::Assign => { + self.add_literal_watcher( + predicate, + propagator_var, + predicate_notifier, + trailed_values, + assignments, + events, + ); + self.add_literal_watcher( + !predicate, + propagator_var, + predicate_notifier, + trailed_values, + assignments, + events, + ); + } + DomainEvent::LowerBound => { + self.add_literal_watcher( + predicate, + propagator_var, + predicate_notifier, + trailed_values, + assignments, + events, + ); + } + DomainEvent::UpperBound => { + self.add_literal_watcher( + !predicate, + propagator_var, + predicate_notifier, + trailed_values, + assignments, + events, + ); + } + DomainEvent::Removal => { + self.add_literal_watcher( + predicate, + propagator_var, + predicate_notifier, + trailed_values, + assignments, + events, + ); + self.add_literal_watcher( + !predicate, + propagator_var, + predicate_notifier, + trailed_values, + assignments, + events, + ); + } + }; + } + } + + pub(crate) fn watchers_predicate_id_mut( + &mut self, + predicate_id: PredicateId, + ) -> Option<&mut Vec> { + self.watch_list_predicate_id.get_mut(predicate_id) + } + + pub(crate) fn watchers_predicate_id( + &self, + predicate_id: PredicateId, + ) -> Option<&Vec> { + self.watch_list_predicate_id.get(predicate_id) + } + + pub(crate) fn watch_predicate_events_backtrack( + &mut self, + predicate: Predicate, + propagator_var: PropagatorVarId, + events: EnumSet, + predicate_notifier: &mut PredicateNotifier, + assignments: &Assignments, + trailed_values: &mut TrailedValues, + ) { + let predicate_id = predicate_notifier.get_id(predicate); + self.watch_list_predicate_id_backtrack + .entry(predicate_id) + .or_default() + .push(PredicateWatcher::new_literal_watcher( + propagator_var.propagator, + propagator_var.variable, + events, + )); + for event in events { + match event { + DomainEvent::Assign => { + self.add_literal_watcher_backtrack( + predicate, + predicate_notifier, + trailed_values, + assignments, + ); + self.add_literal_watcher_backtrack( + !predicate, + predicate_notifier, + trailed_values, + assignments, + ); + } + DomainEvent::LowerBound => { + self.add_literal_watcher_backtrack( + predicate, + predicate_notifier, + trailed_values, + assignments, + ); + } + DomainEvent::UpperBound => { + self.add_literal_watcher_backtrack( + !predicate, + predicate_notifier, + trailed_values, + assignments, + ); + } + DomainEvent::Removal => { + self.add_literal_watcher_backtrack( + predicate, + predicate_notifier, + trailed_values, + assignments, + ); + self.add_literal_watcher_backtrack( + !predicate, + predicate_notifier, + trailed_values, + assignments, + ); + } + }; + } + } + + fn add_literal_watcher_backtrack( + &mut self, + predicate: Predicate, + predicate_notifier: &mut PredicateNotifier, + trailed_values: &mut TrailedValues, + assignments: &Assignments, + ) { + let predicate_id = predicate_notifier.predicate_to_id.get_id(predicate); + + predicate_notifier.track_predicate(predicate_id, trailed_values, assignments); + } + + pub(crate) fn backtrack_watcher_for_literal_and_propagator( + &self, + predicate_id: PredicateId, + propagator_id: PropagatorId, + ) -> Option { + self.watch_list_predicate_id_backtrack + .get(&predicate_id) + .and_then(|watch_list| { + watch_list + .iter() + .find(|watcher| watcher.propagator_id == propagator_id) + }) + .copied() + } +} diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index ba6a5e64e..8e929e243 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -1,6 +1,7 @@ mod domain_event_notification; mod predicate_notification; +use bit_set::BitSet; pub use domain_event_notification::DomainEvent; pub(crate) use domain_event_notification::EventSink; pub(crate) use domain_event_notification::WatchListDomainEvents; @@ -11,10 +12,12 @@ use enumset::EnumSet; pub(crate) use predicate_notification::PredicateNotifier; use crate::basic_types::PredicateId; -use crate::containers::KeyedVec; +use crate::basic_types::Trail; +use crate::containers::StorageKey; use crate::engine::Assignments; use crate::engine::PropagatorQueue; use crate::engine::TrailedValues; +use crate::engine::notifications::domain_event_notification::PredicateWatchList; use crate::predicates::Predicate; use crate::propagation::Domains; use crate::propagation::EnqueueDecision; @@ -36,24 +39,27 @@ pub(crate) struct NotificationEngine { /// Contains information on which propagator to notify upon /// integer events, e.g., lower or upper bound change of a variable. watch_list_domain_events: WatchListDomainEvents, - /// The watch list from predicates to propagators. - pub(crate) watch_list_predicate_id: KeyedVec>, + watch_list_predicate_ids: PredicateWatchList, /// Events which have occurred since the last round of notifications have taken place events: EventSink, /// Backtrack events which have occurred since the last of backtrack notifications have taken /// place backtrack_events: EventSink, + backtrack_events_literals: Trail<(PredicateId, PropagatorId)>, + notified_predicate_ids: BitSet, } impl Default for NotificationEngine { fn default() -> Self { let mut result = Self { watch_list_domain_events: Default::default(), - watch_list_predicate_id: Default::default(), + watch_list_predicate_ids: Default::default(), predicate_notifier: Default::default(), last_notified_trail_index: 0, events: Default::default(), backtrack_events: Default::default(), + backtrack_events_literals: Default::default(), + notified_predicate_ids: Default::default(), }; // Grow for the dummy predicate result.grow(); @@ -72,11 +78,13 @@ impl NotificationEngine { let mut result = Self { watch_list_domain_events, - watch_list_predicate_id: Default::default(), + watch_list_predicate_ids: Default::default(), predicate_notifier: Default::default(), last_notified_trail_index: usize::MAX, events: Default::default(), backtrack_events: Default::default(), + backtrack_events_literals: Default::default(), + notified_predicate_ids: Default::default(), }; // Grow for the dummy predicate result.grow(); @@ -156,42 +164,59 @@ impl NotificationEngine { trailed_values: &mut TrailedValues, assignments: &Assignments, ) -> PredicateId { - let predicate_id = self.get_id(predicate); - self.watch_predicate_id(predicate_id, propagator_id, trailed_values, assignments); - - predicate_id + self.watch_list_predicate_ids.watch_predicate( + predicate, + propagator_id, + &mut self.predicate_notifier, + assignments, + trailed_values, + ) } - pub(crate) fn watch_predicate_id( + pub(crate) fn unwatch_predicate( &mut self, predicate_id: PredicateId, - propagator_id: PropagatorId, + propagator_to_unwatch: PropagatorId, + ) { + self.watch_list_predicate_ids + .unwatch_predicate(predicate_id, propagator_to_unwatch) + } + + pub(crate) fn watch_predicate_events( + &mut self, + predicate: Predicate, + events: EnumSet, + propagator_var: PropagatorVarId, trailed_values: &mut TrailedValues, assignments: &Assignments, ) { - self.watch_list_predicate_id - .accomodate(predicate_id, vec![]); - self.watch_list_predicate_id[predicate_id].push(propagator_id); - - self.predicate_notifier - .track_predicate(predicate_id, trailed_values, assignments); + self.watch_list_predicate_ids.watch_predicate_events( + predicate, + propagator_var, + events, + &mut self.predicate_notifier, + assignments, + trailed_values, + ); } - pub(crate) fn unwatch_predicate( + pub(crate) fn watch_predicate_events_backtrack( &mut self, - predicate_id: PredicateId, - propagator_to_unwatch: PropagatorId, + predicate: Predicate, + events: EnumSet, + propagator_var: PropagatorVarId, + trailed_values: &mut TrailedValues, + assignments: &Assignments, ) { - let watch_list = &mut self.watch_list_predicate_id[predicate_id]; - - let index = watch_list - .iter() - .position(|&watched_propagator| watched_propagator == propagator_to_unwatch) - .expect("cannot unwatch a (predicate, propagator) pair if it was not watched"); - - let _ = watch_list.swap_remove(index); - - // TODO: Can we remove the predicate from being tracked if it does not have watchers? + self.watch_list_predicate_ids + .watch_predicate_events_backtrack( + predicate, + propagator_var, + events, + &mut self.predicate_notifier, + assignments, + trailed_values, + ); } pub(crate) fn watch_all_backtrack( @@ -351,6 +376,7 @@ impl NotificationEngine { pub(crate) fn process_backtrack_events( &mut self, + new_checkpoint: usize, assignments: &mut Assignments, trailed_values: &mut TrailedValues, propagators: &mut PropagatorStore, @@ -377,6 +403,23 @@ impl NotificationEngine { } } } + + for (literal, propagator_id) in self.backtrack_events_literals.synchronise(new_checkpoint) { + let _ = self.notified_predicate_ids.remove(literal.index()); + if let Some(watcher) = self + .watch_list_predicate_ids + .backtrack_watcher_for_literal_and_propagator(literal, propagator_id) + && let Some(events) = watcher.events + && let Some(local_id) = watcher.local_id + { + let propagator = &mut propagators[propagator_id]; + for event in events.iter() { + let mut context = NotificationContext::new(trailed_values, assignments); + + propagator.notify_backtrack(context.domains(), local_id, event.into()) + } + } + } true } @@ -389,21 +432,59 @@ impl NotificationEngine { assignments: &Assignments, ) { for predicate_id in self.predicate_notifier.drain_satisfied_predicates() { - if let Some(watch_list) = self.watch_list_predicate_id.get(predicate_id) { - let propagators_to_notify = watch_list.iter().copied(); + let Some(watchers) = self + .watch_list_predicate_ids + .watchers_predicate_id(predicate_id) + else { + continue; + }; + + for predicate_watcher in watchers { + if let Some(events) = predicate_watcher.events + && let Some(local_id) = predicate_watcher.local_id + { + if events.is_empty() + || self.notified_predicate_ids.contains(predicate_id.index()) + { + continue; + } - for propagator_id in propagators_to_notify { + self.backtrack_events_literals + .push((predicate_id, predicate_watcher.propagator_id)); + + let propagator = &mut propagators[predicate_watcher.propagator_id]; + for event in events.iter() { + let mut context = NotificationContext::new(trailed_values, assignments); + + let enqueue_decision = + propagator.notify(context.reborrow(), local_id, event.into()); + + if enqueue_decision == EnqueueDecision::Enqueue { + propagator_queue.enqueue_propagator( + predicate_watcher.propagator_id, + propagator.priority(), + ); + } + } + } else { let mut context = NotificationContext::new(trailed_values, assignments); - let propagator = &mut propagators[propagator_id]; + let propagator = &mut propagators[predicate_watcher.propagator_id]; let enqueue_decision = propagator.notify_predicate_id_satisfied(context.reborrow(), predicate_id); if enqueue_decision == EnqueueDecision::Enqueue { - propagator_queue.enqueue_propagator(propagator_id, propagator.priority()); + propagator_queue.enqueue_propagator( + predicate_watcher.propagator_id, + propagator.priority(), + ); } } } + + // NOTE: This assumes that there are no registration for predicates after it has become + // true. + let _ = self.notified_predicate_ids.insert(predicate_id.index()); } } @@ -504,6 +585,7 @@ impl NotificationEngine { self.predicate_notifier .predicate_id_assignments .new_checkpoint(); + self.backtrack_events_literals.new_checkpoint(); } pub(crate) fn debug_create_from_assignments(&mut self, assignments: &Assignments) { diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs index feefdc71b..c33568881 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs @@ -59,6 +59,11 @@ impl PredicateNotifier { self.predicate_to_id.get_predicate(predicate_id) } + /// Returns the [`PredicateId`] corresponding to a [`Predicate`]. + pub(crate) fn get_id(&mut self, predicate: Predicate) -> PredicateId { + self.predicate_to_id.get_id(predicate) + } + /// Method which is called when an update to a [`DomainId`] has taken place /// /// This method will pass it along to the correct [`PredicateNotifier::on_update`] diff --git a/pumpkin-crates/core/src/engine/predicates/predicate.rs b/pumpkin-crates/core/src/engine/predicates/predicate.rs index b62ae72e1..fd9afe6b9 100644 --- a/pumpkin-crates/core/src/engine/predicates/predicate.rs +++ b/pumpkin-crates/core/src/engine/predicates/predicate.rs @@ -1,10 +1,20 @@ +use enumset::EnumSet; use enumset::EnumSetType; use pumpkin_checking::AtomicConstraint; +use pumpkin_checking::CheckerVariable; +use pumpkin_checking::IntExt; +use pumpkin_checking::VariableState; use crate::engine::Assignments; +use crate::engine::notifications::Watchers; use crate::engine::variables::DomainId; use crate::predicate; +use crate::predicates::PredicateConstructor; use crate::propagation::DomainEvent; +use crate::propagation::OpaqueDomainEvent; +use crate::variables::AffineView; +use crate::variables::IntegerVariable; +use crate::variables::TransformableVariable; /// Representation of a domain operation, also known as an atomic constraint. It is a triple /// ([`DomainId`], [`PredicateType`], value). @@ -366,6 +376,293 @@ impl AtomicConstraint for Predicate { } } +impl CheckerVariable for Predicate { + fn does_atomic_constrain_self(&self, atomic: &Predicate) -> bool { + atomic.get_domain() == self.get_domain() + } + + fn atomic_less_than(&self, value: i32) -> Predicate { + if value == 0 { + self.negate() + } else if value >= 1 { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn atomic_greater_than(&self, value: i32) -> Predicate { + if value == 1 { + self.negate() + } else if value <= 0 { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn atomic_equal(&self, value: i32) -> Predicate { + if value == 1 { + *self + } else if value == 0 { + self.negate() + } else { + Predicate::trivially_false() + } + } + + fn atomic_not_equal(&self, value: i32) -> Predicate { + if value == 1 { + self.negate() + } else if value == 0 { + *self + } else { + Predicate::trivially_true() + } + } + + fn induced_lower_bound(&self, variable_state: &VariableState) -> IntExt { + IntExt::Int(if variable_state.is_true(self) { + 1 + } else { + Default::default() + }) + } + + fn induced_upper_bound(&self, variable_state: &VariableState) -> IntExt { + IntExt::Int(if variable_state.is_true(&self.negate()) { + 0 + } else { + 1 + }) + } + + fn induced_fixed_value(&self, variable_state: &VariableState) -> Option { + if variable_state.is_true(self) { + Some(1) + } else if variable_state.is_true(&self.negate()) { + Some(0) + } else { + None + } + } + + fn induced_domain_contains( + &self, + variable_state: &VariableState, + value: i32, + ) -> bool { + if value == 1 && !variable_state.is_true(&self.negate()) { + true + } else { + value == 0 && !variable_state.is_true(self) + } + } + + fn induced_holes<'this, 'state>( + &'this self, + _variable_state: &'state VariableState, + ) -> impl Iterator + 'state + where + 'this: 'state, + { + std::iter::empty() + } + + fn iter_induced_domain<'this, 'state>( + &'this self, + variable_state: &'state VariableState, + ) -> Option + 'state> + where + 'this: 'state, + { + Some((0..=1).filter(|&value| { + if value == 0 { + !variable_state.is_true(self) + } else if value == 1 { + !variable_state.is_true(&!*self) + } else { + unreachable!() + } + })) + } +} + +impl IntegerVariable for Predicate { + type AffineView = AffineView; + + /// Returns the lower bound represented as a 0-1 value. + /// Literals that evaluate to true have a lower bound of 1. + /// Literal that evaluate to false have a lower bound of 0. + /// Unassigned literals have a lower bound of 0. + fn lower_bound(&self, assignment: &Assignments) -> i32 { + if assignment.is_predicate_satisfied(*self) { + 1 + } else { + 0 + } + } + + fn lower_bound_at_trail_position( + &self, + assignment: &Assignments, + trail_position: usize, + ) -> i32 { + if assignment.is_predicate_satisfied_at_trail_position(*self, trail_position) { + 1 + } else { + 0 + } + } + + /// Returns the upper bound represented as a 0-1 value. + /// Literals that evaluate to true have an upper bound of 1. + /// Literal that evaluate to false have a upper bound of 0. + /// Unassigned literals have a upper bound of 1. + fn upper_bound(&self, assignment: &Assignments) -> i32 { + if assignment.is_predicate_satisfied(self.negate()) { + 0 + } else { + 1 + } + } + + fn upper_bound_at_trail_position( + &self, + assignment: &Assignments, + trail_position: usize, + ) -> i32 { + if assignment.is_predicate_satisfied_at_trail_position(self.negate(), trail_position) { + 0 + } else { + 1 + } + } + + /// Returns whether the input value, when interpreted as a bool, + /// can be considered for the literal. + /// Literals that evaluate to true only contain value 1. + /// Literals that evaluate to false only contain value 0. + /// Unassigned literals contain both values 0 and 1. + fn contains(&self, assignment: &Assignments, value: i32) -> bool { + if value == 0 { + !assignment.is_predicate_satisfied(*self) + } else if value == 1 { + !assignment.is_predicate_satisfied(self.negate()) + } else { + false + } + } + + fn contains_at_trail_position( + &self, + assignment: &Assignments, + value: i32, + trail_position: usize, + ) -> bool { + if value == 0 { + !assignment.is_predicate_satisfied_at_trail_position(*self, trail_position) + } else if value == 1 { + !assignment.is_predicate_satisfied_at_trail_position(self.negate(), trail_position) + } else { + false + } + } + + fn iterate_domain(&self, assignment: &Assignments) -> impl Iterator { + (0..=1).filter(|&value| { + if value == 0 { + !assignment.is_predicate_satisfied(*self) + } else if value == 1 { + !assignment.is_predicate_satisfied(!*self) + } else { + unreachable!() + } + }) + } + + fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet) { + watchers.watch_predicate(*self, events) + } + + fn unwatch_all(&self, watchers: &mut Watchers<'_>) { + watchers.unwatch_predicate(*self); + } + + fn unpack_event(&self, event: OpaqueDomainEvent) -> DomainEvent { + event.unwrap() + } + + fn watch_all_backtrack(&self, watchers: &mut Watchers<'_>, events: EnumSet) { + watchers.watch_predicate_backtrack(*self, events) + } + + fn get_holes_at_current_checkpoint( + &self, + _assignments: &Assignments, + ) -> impl Iterator { + std::iter::empty() + } + + fn get_holes(&self, _assignments: &Assignments) -> impl Iterator { + std::iter::empty() + } +} + +impl PredicateConstructor for Predicate { + type Value = i32; + + fn lower_bound_predicate(&self, bound: Self::Value) -> Predicate { + if bound == 1 { + *self + } else if bound < 1 { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn upper_bound_predicate(&self, bound: Self::Value) -> Predicate { + if bound == 0 { + self.negate() + } else if bound > 0 { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn equality_predicate(&self, bound: Self::Value) -> Predicate { + if bound == 0 { + self.negate() + } else if bound == 1 { + *self + } else { + Predicate::trivially_true() + } + } + + fn disequality_predicate(&self, bound: Self::Value) -> Predicate { + if bound == 0 { + *self + } else if bound == 1 { + self.negate() + } else { + Predicate::trivially_true() + } + } +} + +impl TransformableVariable> for Predicate { + fn scaled(&self, scale: i32) -> AffineView { + AffineView::new(*self, scale, 0) + } + + fn offset(&self, offset: i32) -> AffineView { + AffineView::new(*self, 1, offset) + } +} + #[cfg(test)] mod test { use super::Predicate; diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 9e358fab6..28ed4901a 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -49,7 +49,6 @@ use crate::statistics::StatisticLogger; use crate::statistics::log_statistic; use crate::variables::DomainId; use crate::variables::IntegerVariable; -use crate::variables::Literal; /// The [`State`] is the container of variables and propagators. /// @@ -157,20 +156,6 @@ impl State { self.constraint_tags.next_key() } - /// Creates a new Boolean (0-1) variable. - /// - /// The name is used in solver traces to identify individual domains. They are required to be - /// unique. If the state already contains a domain with the given name, then this function - /// will panic. - /// - /// Creation of new [`Literal`]s is not influenced by the current checkpoint of the state. - /// If a [`Literal`] is created at a non-zero checkpoint, then it will _not_ 'disappear' - /// when backtracking past the checkpoint where the domain was created. - pub fn new_literal(&mut self, name: Option>) -> Literal { - let domain_id = self.new_interval_variable(0, 1, name); - Literal::new(domain_id) - } - /// Creates a new interval variable with the given lower and upper bound. /// /// The name is used in solver traces to identify individual domains. They are required to be @@ -264,14 +249,6 @@ impl State { self.assignments.get_checkpoint_for_predicate(&predicate) } - /// Returns the truth value of the provided [`Literal`]. - /// - /// If the [`Literal`] is assigned in the current [`State`] then [`Some`] containing whether - /// the [`Literal`] is satisfied or falsified is returned. Otherwise, [`None`] is returned. - pub fn get_literal_value(&self, literal: Literal) -> Option { - self.truth_value(literal.get_true_predicate()) - } - /// Returns the number of created checkpoints. pub fn get_checkpoint(&self) -> usize { self.assignments.get_checkpoint() @@ -568,6 +545,7 @@ impl State { } let _ = self.notification_engine.process_backtrack_events( + checkpoint, &mut self.assignments, &mut self.trailed_values, &mut self.propagators, diff --git a/pumpkin-crates/core/src/engine/variables/any_integer.rs b/pumpkin-crates/core/src/engine/variables/any_integer.rs new file mode 100644 index 000000000..cd88fb9fd --- /dev/null +++ b/pumpkin-crates/core/src/engine/variables/any_integer.rs @@ -0,0 +1,364 @@ +use enumset::EnumSet; +use pumpkin_checking::CheckerVariable; + +use crate::engine::Assignments; +use crate::engine::notifications::Watchers; +use crate::predicates::Predicate; +use crate::predicates::PredicateConstructor; +use crate::propagation::DomainEvent; +use crate::propagation::OpaqueDomainEvent; +use crate::variables::AffineView; +use crate::variables::DomainId; +use crate::variables::IntegerVariable; +use crate::variables::TransformableVariable; + +/// An implementation of [`IntegerVariable`] which stores either a [`DomainId`] or [`Predicate`]. +/// +/// This enum can be used when you want to supply multiple [`IntegerVariable`]s, which should be of +/// the same type, but are not. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum AnyInteger { + DomainId(DomainId), + Predicate(Predicate), +} + +impl From> for AffineView { + fn from(value: AffineView) -> Self { + AffineView::new(AnyInteger::DomainId(value.inner), value.scale, value.offset) + } +} + +impl From for AffineView { + fn from(value: DomainId) -> Self { + AffineView::new(AnyInteger::DomainId(value), 1, 0) + } +} + +impl From for AnyInteger { + fn from(value: DomainId) -> Self { + AnyInteger::DomainId(value) + } +} + +impl From> for AffineView { + fn from(value: AffineView) -> Self { + AffineView::new( + AnyInteger::Predicate(value.inner), + value.scale, + value.offset, + ) + } +} + +impl From for AffineView { + fn from(value: Predicate) -> Self { + AffineView::new(AnyInteger::Predicate(value), 1, 0) + } +} + +impl From for AnyInteger { + fn from(value: Predicate) -> Self { + AnyInteger::Predicate(value) + } +} + +impl PredicateConstructor for AnyInteger { + type Value = i32; + + fn lower_bound_predicate(&self, bound: Self::Value) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.lower_bound_predicate(bound), + AnyInteger::Predicate(literal) => literal.lower_bound_predicate(bound), + } + } + + fn upper_bound_predicate(&self, bound: Self::Value) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.upper_bound_predicate(bound), + AnyInteger::Predicate(literal) => literal.upper_bound_predicate(bound), + } + } + + fn equality_predicate(&self, bound: Self::Value) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.equality_predicate(bound), + AnyInteger::Predicate(literal) => literal.equality_predicate(bound), + } + } + + fn disequality_predicate(&self, bound: Self::Value) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.disequality_predicate(bound), + AnyInteger::Predicate(literal) => literal.disequality_predicate(bound), + } + } +} + +impl TransformableVariable> for AnyInteger { + fn scaled(&self, scale: i32) -> AffineView { + AffineView::new(*self, scale, 0) + } + + fn offset(&self, offset: i32) -> AffineView { + AffineView::new(*self, 1, offset) + } +} + +impl IntegerVariable for AnyInteger { + type AffineView = AffineView; + + fn lower_bound(&self, assignment: &Assignments) -> i32 { + match self { + AnyInteger::DomainId(domain_id) => domain_id.lower_bound(assignment), + AnyInteger::Predicate(literal) => literal.lower_bound(assignment), + } + } + + fn lower_bound_at_trail_position( + &self, + assignment: &Assignments, + trail_position: usize, + ) -> i32 { + match self { + AnyInteger::DomainId(domain_id) => { + domain_id.lower_bound_at_trail_position(assignment, trail_position) + } + AnyInteger::Predicate(literal) => { + literal.lower_bound_at_trail_position(assignment, trail_position) + } + } + } + + fn upper_bound(&self, assignment: &Assignments) -> i32 { + match self { + AnyInteger::DomainId(domain_id) => domain_id.upper_bound(assignment), + AnyInteger::Predicate(literal) => literal.upper_bound(assignment), + } + } + + fn upper_bound_at_trail_position( + &self, + assignment: &Assignments, + trail_position: usize, + ) -> i32 { + match self { + AnyInteger::DomainId(domain_id) => { + domain_id.upper_bound_at_trail_position(assignment, trail_position) + } + AnyInteger::Predicate(literal) => { + literal.upper_bound_at_trail_position(assignment, trail_position) + } + } + } + + fn contains(&self, assignment: &Assignments, value: i32) -> bool { + match self { + AnyInteger::DomainId(domain_id) => domain_id.contains(assignment, value), + AnyInteger::Predicate(literal) => literal.contains(assignment, value), + } + } + + fn contains_at_trail_position( + &self, + assignment: &Assignments, + value: i32, + trail_position: usize, + ) -> bool { + match self { + AnyInteger::DomainId(domain_id) => { + domain_id.contains_at_trail_position(assignment, value, trail_position) + } + AnyInteger::Predicate(literal) => { + literal.contains_at_trail_position(assignment, value, trail_position) + } + } + } + + fn iterate_domain(&self, assignment: &Assignments) -> impl Iterator { + match self { + AnyInteger::DomainId(domain_id) => domain_id + .iterate_domain(assignment) + .collect::>() + .into_iter(), + AnyInteger::Predicate(literal) => literal + .iterate_domain(assignment) + .collect::>() + .into_iter(), + } + } + + fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet) { + match self { + AnyInteger::DomainId(domain_id) => domain_id.watch_all(watchers, events), + AnyInteger::Predicate(literal) => literal.watch_all(watchers, events), + } + } + + fn unwatch_all(&self, watchers: &mut Watchers<'_>) { + match self { + AnyInteger::DomainId(domain_id) => domain_id.unwatch_all(watchers), + AnyInteger::Predicate(literal) => literal.unwatch_all(watchers), + } + } + + fn watch_all_backtrack(&self, watchers: &mut Watchers<'_>, events: EnumSet) { + match self { + AnyInteger::DomainId(domain_id) => domain_id.watch_all_backtrack(watchers, events), + AnyInteger::Predicate(literal) => literal.watch_all_backtrack(watchers, events), + } + } + + fn unpack_event(&self, event: OpaqueDomainEvent) -> DomainEvent { + match self { + AnyInteger::DomainId(domain_id) => domain_id.unpack_event(event), + AnyInteger::Predicate(literal) => literal.unpack_event(event), + } + } + + fn get_holes_at_current_checkpoint( + &self, + assignments: &Assignments, + ) -> impl Iterator { + match self { + AnyInteger::DomainId(domain_id) => domain_id + .get_holes_at_current_checkpoint(assignments) + .collect::>() + .into_iter(), + AnyInteger::Predicate(literal) => literal + .get_holes_at_current_checkpoint(assignments) + .collect::>() + .into_iter(), + } + } + + fn get_holes(&self, assignments: &Assignments) -> impl Iterator { + match self { + AnyInteger::DomainId(domain_id) => domain_id + .get_holes(assignments) + .collect::>() + .into_iter(), + AnyInteger::Predicate(literal) => literal + .get_holes(assignments) + .collect::>() + .into_iter(), + } + } +} + +impl CheckerVariable for AnyInteger { + fn does_atomic_constrain_self(&self, atomic: &Predicate) -> bool { + match self { + AnyInteger::DomainId(domain_id) => domain_id.does_atomic_constrain_self(atomic), + AnyInteger::Predicate(literal) => literal.does_atomic_constrain_self(atomic), + } + } + + fn atomic_less_than(&self, value: i32) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.atomic_less_than(value), + AnyInteger::Predicate(literal) => literal.atomic_less_than(value), + } + } + + fn atomic_greater_than(&self, value: i32) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.atomic_greater_than(value), + AnyInteger::Predicate(literal) => literal.atomic_greater_than(value), + } + } + + fn atomic_equal(&self, value: i32) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.atomic_equal(value), + AnyInteger::Predicate(literal) => literal.atomic_equal(value), + } + } + + fn atomic_not_equal(&self, value: i32) -> Predicate { + match self { + AnyInteger::DomainId(domain_id) => domain_id.atomic_not_equal(value), + AnyInteger::Predicate(literal) => literal.atomic_not_equal(value), + } + } + + fn induced_lower_bound( + &self, + variable_state: &pumpkin_checking::VariableState, + ) -> pumpkin_checking::IntExt { + match self { + AnyInteger::DomainId(domain_id) => domain_id.induced_lower_bound(variable_state), + AnyInteger::Predicate(literal) => literal.induced_lower_bound(variable_state), + } + } + + fn induced_upper_bound( + &self, + variable_state: &pumpkin_checking::VariableState, + ) -> pumpkin_checking::IntExt { + match self { + AnyInteger::DomainId(domain_id) => domain_id.induced_upper_bound(variable_state), + AnyInteger::Predicate(literal) => literal.induced_upper_bound(variable_state), + } + } + + fn induced_fixed_value( + &self, + variable_state: &pumpkin_checking::VariableState, + ) -> Option { + match self { + AnyInteger::DomainId(domain_id) => domain_id.induced_fixed_value(variable_state), + AnyInteger::Predicate(literal) => literal.induced_fixed_value(variable_state), + } + } + + fn induced_domain_contains( + &self, + variable_state: &pumpkin_checking::VariableState, + value: i32, + ) -> bool { + match self { + AnyInteger::DomainId(domain_id) => { + domain_id.induced_domain_contains(variable_state, value) + } + AnyInteger::Predicate(literal) => { + literal.induced_domain_contains(variable_state, value) + } + } + } + + fn induced_holes<'this, 'state>( + &'this self, + variable_state: &'state pumpkin_checking::VariableState, + ) -> impl Iterator + 'state + where + 'this: 'state, + { + match self { + AnyInteger::DomainId(domain_id) => domain_id + .induced_holes(variable_state) + .collect::>() + .into_iter(), + AnyInteger::Predicate(literal) => literal + .induced_holes(variable_state) + .collect::>() + .into_iter(), + } + } + + fn iter_induced_domain<'this, 'state>( + &'this self, + variable_state: &'state pumpkin_checking::VariableState, + ) -> Option + 'state> + where + 'this: 'state, + { + match self { + AnyInteger::DomainId(domain_id) => domain_id + .iter_induced_domain(variable_state) + .map(|iter| iter.collect::>().into_iter()), + AnyInteger::Predicate(literal) => literal + .iter_induced_domain(variable_state) + .map(|iter| iter.collect::>().into_iter()), + } + } +} diff --git a/pumpkin-crates/core/src/engine/variables/literal.rs b/pumpkin-crates/core/src/engine/variables/literal.rs deleted file mode 100644 index 980ffa737..000000000 --- a/pumpkin-crates/core/src/engine/variables/literal.rs +++ /dev/null @@ -1,224 +0,0 @@ -use std::ops::Not; - -use enumset::EnumSet; -use pumpkin_checking::CheckerVariable; -use pumpkin_checking::IntExt; -use pumpkin_checking::VariableState; - -use super::DomainId; -use super::IntegerVariable; -use super::TransformableVariable; -use crate::engine::Assignments; -use crate::engine::notifications::DomainEvent; -use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::notifications::Watchers; -use crate::engine::predicates::predicate::Predicate; -use crate::engine::predicates::predicate_constructor::PredicateConstructor; -use crate::engine::variables::AffineView; - -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] -pub struct Literal { - integer_variable: AffineView, -} - -impl Literal { - /// Creates a new literal wrapping the provided [`DomainId`]. - /// - /// Note: the provided `domain_id` should have a domain between 0 and 1. - pub fn new(domain_id: DomainId) -> Literal { - Literal { - integer_variable: domain_id.scaled(1), - } - } - - pub fn get_integer_variable(&self) -> AffineView { - self.integer_variable - } - - pub fn get_true_predicate(&self) -> Predicate { - self.lower_bound_predicate(1) - } - - pub fn get_false_predicate(&self) -> Predicate { - self.upper_bound_predicate(0) - } -} - -impl Not for Literal { - type Output = Literal; - - fn not(self) -> Self::Output { - Literal { - integer_variable: self.integer_variable.scaled(-1).offset(1), - } - } -} - -/// Forwards a function implementation to the field on self. -macro_rules! forward { - ( - $field:ident, - fn $(<$($lt:lifetime),+>)? $name:ident( - & $($lt_self:lifetime)? self, - $($param_name:ident : $param_type:ty),* - ) -> $return_type:ty - $(where $($where_clause:tt)*)? - ) => { - fn $name$(<$($lt),+>)?( - & $($lt_self)? self, - $($param_name: $param_type),* - ) -> $return_type $(where $($where_clause)*)? { - self.$field.$name($($param_name),*) - } - } -} - -impl CheckerVariable for Literal { - forward!(integer_variable, fn does_atomic_constrain_self(&self, atomic: &Predicate) -> bool); - forward!(integer_variable, fn atomic_less_than(&self, value: i32) -> Predicate); - forward!(integer_variable, fn atomic_greater_than(&self, value: i32) -> Predicate); - forward!(integer_variable, fn atomic_not_equal(&self, value: i32) -> Predicate); - forward!(integer_variable, fn atomic_equal(&self, value: i32) -> Predicate); - - forward!(integer_variable, fn induced_lower_bound(&self, variable_state: &VariableState) -> IntExt); - forward!(integer_variable, fn induced_upper_bound(&self, variable_state: &VariableState) -> IntExt); - forward!(integer_variable, fn induced_fixed_value(&self, variable_state: &VariableState) -> Option); - forward!(integer_variable, fn induced_domain_contains(&self, variable_state: &VariableState, value: i32) -> bool); - forward!( - integer_variable, - fn <'this, 'state> induced_holes( - &'this self, - variable_state: &'state VariableState - ) -> impl Iterator + 'state - where - 'this: 'state, - ); - forward!( - integer_variable, - fn <'this, 'state> iter_induced_domain( - &'this self, - variable_state: &'state VariableState - ) -> Option + 'state> - where - 'this: 'state, - ); -} - -impl IntegerVariable for Literal { - type AffineView = AffineView; - - /// Returns the lower bound represented as a 0-1 value. - /// Literals that evaluate to true have a lower bound of 1. - /// Literal that evaluate to false have a lower bound of 0. - /// Unassigned literals have a lower bound of 0. - fn lower_bound(&self, assignment: &Assignments) -> i32 { - self.integer_variable.lower_bound(assignment) - } - - fn lower_bound_at_trail_position( - &self, - assignment: &Assignments, - trail_position: usize, - ) -> i32 { - self.integer_variable - .lower_bound_at_trail_position(assignment, trail_position) - } - - /// Returns the upper bound represented as a 0-1 value. - /// Literals that evaluate to true have an upper bound of 1. - /// Literal that evaluate to false have a upper bound of 0. - /// Unassigned literals have a upper bound of 1. - fn upper_bound(&self, assignment: &Assignments) -> i32 { - self.integer_variable.upper_bound(assignment) - } - - fn upper_bound_at_trail_position( - &self, - assignment: &Assignments, - trail_position: usize, - ) -> i32 { - self.integer_variable - .upper_bound_at_trail_position(assignment, trail_position) - } - - /// Returns whether the input value, when interpreted as a bool, - /// can be considered for the literal. - /// Literals that evaluate to true only contain value 1. - /// Literals that evaluate to false only contain value 0. - /// Unassigned literals contain both values 0 and 1. - fn contains(&self, assignment: &Assignments, value: i32) -> bool { - self.integer_variable.contains(assignment, value) - } - - fn contains_at_trail_position( - &self, - assignment: &Assignments, - value: i32, - trail_position: usize, - ) -> bool { - self.integer_variable - .contains_at_trail_position(assignment, value, trail_position) - } - - fn iterate_domain(&self, assignment: &Assignments) -> impl Iterator { - self.integer_variable.iterate_domain(assignment) - } - - fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet) { - self.integer_variable.watch_all(watchers, events) - } - - fn unwatch_all(&self, watchers: &mut Watchers<'_>) { - self.integer_variable.unwatch_all(watchers) - } - - fn unpack_event(&self, event: OpaqueDomainEvent) -> DomainEvent { - self.integer_variable.unpack_event(event) - } - - fn watch_all_backtrack(&self, watchers: &mut Watchers<'_>, events: EnumSet) { - self.integer_variable.watch_all_backtrack(watchers, events) - } - - fn get_holes_at_current_checkpoint( - &self, - assignments: &Assignments, - ) -> impl Iterator { - self.integer_variable - .get_holes_at_current_checkpoint(assignments) - } - - fn get_holes(&self, assignments: &Assignments) -> impl Iterator { - self.integer_variable.get_holes(assignments) - } -} - -impl PredicateConstructor for Literal { - type Value = i32; - - fn lower_bound_predicate(&self, bound: Self::Value) -> Predicate { - self.integer_variable.lower_bound_predicate(bound) - } - - fn upper_bound_predicate(&self, bound: Self::Value) -> Predicate { - self.integer_variable.upper_bound_predicate(bound) - } - - fn equality_predicate(&self, bound: Self::Value) -> Predicate { - self.integer_variable.equality_predicate(bound) - } - - fn disequality_predicate(&self, bound: Self::Value) -> Predicate { - self.integer_variable.disequality_predicate(bound) - } -} - -impl TransformableVariable> for Literal { - fn scaled(&self, scale: i32) -> AffineView { - AffineView::new(*self, scale, 0) - } - - fn offset(&self, offset: i32) -> AffineView { - AffineView::new(*self, 1, offset) - } -} diff --git a/pumpkin-crates/core/src/engine/variables/mod.rs b/pumpkin-crates/core/src/engine/variables/mod.rs index 42837e402..dc1e9116b 100644 --- a/pumpkin-crates/core/src/engine/variables/mod.rs +++ b/pumpkin-crates/core/src/engine/variables/mod.rs @@ -3,16 +3,16 @@ //! constraints. mod affine_view; +mod any_integer; mod constant; mod domain_generator_iterator; mod domain_id; mod integer_variable; -mod literal; mod transformable_variable; pub use affine_view::AffineView; +pub use any_integer::AnyInteger; pub(crate) use domain_generator_iterator::DomainGeneratorIterator; pub use domain_id::DomainId; pub use integer_variable::IntegerVariable; -pub use literal::Literal; pub use transformable_variable::TransformableVariable; diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 082f97e63..bf36f8637 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -31,7 +31,6 @@ use crate::containers::KeyGenerator; use crate::engine::Assignments; use crate::engine::variable_names::VariableNames; use crate::predicates::Predicate; -use crate::variables::Literal; /// A proof log which logs the proof steps necessary to prove unsatisfiability or optimality. We /// allow the following types of proofs: @@ -311,18 +310,6 @@ impl ProofLog { ) || cfg!(feature = "check-deductions") } - pub(crate) fn reify_predicate(&mut self, literal: Literal, predicate: Predicate) { - let Some(ProofImpl::CpProof { - ref mut proof_atomics, - .. - }) = self.internal_proof - else { - return; - }; - - proof_atomics.reify_predicate(literal, predicate); - } - pub(crate) fn is_logging_proof(&self) -> bool { self.internal_proof.is_some() } diff --git a/pumpkin-crates/core/src/proof/proof_atomics.rs b/pumpkin-crates/core/src/proof/proof_atomics.rs index 50c1ad30c..d744df989 100644 --- a/pumpkin-crates/core/src/proof/proof_atomics.rs +++ b/pumpkin-crates/core/src/proof/proof_atomics.rs @@ -6,7 +6,6 @@ use crate::engine::VariableNames; use crate::engine::predicates::predicate::PredicateType; use crate::predicates::Predicate; use crate::variables::DomainId; -use crate::variables::Literal; #[derive(Default, Debug)] pub(crate) struct ProofAtomics { @@ -42,18 +41,6 @@ impl ProofAtomics { IntAtomic::new(name, comparison, value) } - /// Given a literal, whenever it shows up in a proof step, substitute it with the provided - /// predicate. - pub(crate) fn reify_predicate(&mut self, literal: Literal, predicate: Predicate) { - // Note: This only works because we assume `literal` is a fresh literal and we are given - // the positive polarity. That assumption holds as the only place this can be called is - // transitively through `new_literal_for_predicate`. As soon as this assumption is - // violated, all hell will break loose. - let domain = literal.get_true_predicate().get_domain(); - - let _ = self.reification_domains.insert(domain, predicate); - } - /// The given predicate is a predicate over a literal. This function gets the associated /// predicate that was reified with [`Self::reify_predicate`] if it exists. fn get_underlying_predicate(&self, predicate: Predicate) -> Option { diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index 791627880..6427208c4 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -27,7 +27,6 @@ use crate::propagation::DomainEvent; use crate::propagation::DomainEvents; use crate::propagators::reified_propagator::ReifiedChecker; use crate::variables::IntegerVariable; -use crate::variables::Literal; /// A propagator constructor creates a fully initialized instance of a [`Propagator`]. /// @@ -55,7 +54,7 @@ pub trait PropagatorConstructor { #[derive(Debug)] pub struct InferenceCheckers<'state> { state: &'state mut State, - reification_literal: Option, + reification_literal: Option, } impl<'state> InferenceCheckers<'state> { @@ -87,7 +86,7 @@ impl InferenceCheckers<'_> { } } - pub fn with_reification_literal(&mut self, literal: Literal) { + pub fn with_reification_literal(&mut self, literal: Predicate) { self.reification_literal = Some(literal) } } @@ -164,7 +163,12 @@ impl PropagatorConstructorContext<'_> { self.update_next_local_id(local_id); - let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); + let mut watchers = Watchers::new( + propagator_var, + &mut self.state.notification_engine, + &mut self.state.trailed_values, + &self.state.assignments, + ); var.watch_all(&mut watchers, domain_events.events()); } @@ -207,7 +211,12 @@ impl PropagatorConstructorContext<'_> { self.update_next_local_id(local_id); - let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); + let mut watchers = Watchers::new( + propagator_var, + &mut self.state.notification_engine, + &mut self.state.trailed_values, + &self.state.assignments, + ); var.watch_all_backtrack(&mut watchers, domain_events.events()); } diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs index ab3218552..a1ec0ad16 100644 --- a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -9,7 +9,6 @@ use crate::engine::predicates::predicate::Predicate; use crate::engine::reason::Reason; use crate::engine::reason::ReasonStore; use crate::engine::reason::StoredReason; -use crate::engine::variables::Literal; use crate::propagation::DomainEvents; use crate::propagation::Domains; use crate::propagation::HasAssignments; @@ -83,7 +82,7 @@ pub struct PropagationContext<'a> { pub(crate) reason_store: &'a mut ReasonStore, pub(crate) propagator_id: PropagatorId, pub(crate) notification_engine: &'a mut NotificationEngine, - reification_literal: Option, + reification_literal: Option, } impl<'a> HasAssignments for PropagationContext<'a> { @@ -151,7 +150,12 @@ impl<'a> PropagationContext<'a> { variable: local_id, }; - let mut watchers = Watchers::new(propagator_var, self.notification_engine); + let mut watchers = Watchers::new( + propagator_var, + self.notification_engine, + self.trailed_values, + self.assignments, + ); var.watch_all(&mut watchers, domain_events.events()); } @@ -162,7 +166,12 @@ impl<'a> PropagationContext<'a> { variable: local_id, }; - let mut watchers = Watchers::new(propagator_var, self.notification_engine); + let mut watchers = Watchers::new( + propagator_var, + self.notification_engine, + self.trailed_values, + self.assignments, + ); var.unwatch_all(&mut watchers); } @@ -179,7 +188,7 @@ impl<'a> PropagationContext<'a> { } /// Apply a reification literal to all the explanations that are passed to the context. - pub(crate) fn with_reification(&mut self, reification_literal: Literal) { + pub(crate) fn with_reification(&mut self, reification_literal: Predicate) { pumpkin_assert_simple!( self.reification_literal.is_none(), "cannot reify an already reified propagation context" @@ -276,15 +285,11 @@ impl PropagationContext<'_> { pub(crate) fn build_reason( reason: impl Into, - reification_literal: Option, + reification_literal: Option, ) -> StoredReason { match reason.into() { Reason::Eager(mut conjunction, inference_code) => { - conjunction.extend( - reification_literal - .iter() - .map(|lit| lit.get_true_predicate()), - ); + conjunction.extend(reification_literal); StoredReason::Eager(conjunction, inference_code) } Reason::DynamicLazy(code) => StoredReason::DynamicLazy(code), diff --git a/pumpkin-crates/core/src/propagation/domains.rs b/pumpkin-crates/core/src/propagation/domains.rs index c79f0aed5..6bdd89caa 100644 --- a/pumpkin-crates/core/src/propagation/domains.rs +++ b/pumpkin-crates/core/src/propagation/domains.rs @@ -6,7 +6,6 @@ use crate::predicates::Predicate; use crate::propagation::ExplanationContext; use crate::variables::DomainId; use crate::variables::IntegerVariable; -use crate::variables::Literal; /// Provides access to domain information to propagators. /// @@ -58,10 +57,6 @@ pub trait ReadDomains { /// currently unassigned. fn evaluate_predicate(&self, predicate: Predicate) -> Option; - /// Returns whether the provided [`Literal`] is assigned (either true or false) or is - /// currently unassigned. - fn evaluate_literal(&self, literal: Literal) -> Option; - /// Returns the holes in the domain which were created on the current checkpoint. fn get_holes_at_current_checkpoint( &self, @@ -166,10 +161,6 @@ impl ReadDomains for T { self.assignments().evaluate_predicate(predicate) } - fn evaluate_literal(&self, literal: Literal) -> Option { - self.evaluate_predicate(literal.get_true_predicate()) - } - fn get_holes_at_current_checkpoint( &self, var: &Var, diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index 0bb782495..5661aa57a 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -22,13 +22,12 @@ use crate::propagation::PropagatorConstructorContext; use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; use crate::state::Conflict; -use crate::variables::Literal; /// A [`PropagatorConstructor`] for the reified propagator. #[derive(Clone, Debug)] pub struct ReifiedPropagatorArgs { pub propagator: WrappedArgs, - pub reification_literal: Literal, + pub reification_literal: Predicate, } impl PropagatorConstructor for ReifiedPropagatorArgs @@ -81,7 +80,7 @@ where #[derive(Clone, Debug)] pub struct ReifiedPropagator { propagator: WrappedPropagator, - reification_literal: Literal, + reification_literal: Predicate, /// The formatted name of the propagator. name: String, /// The `LocalId` of the reification literal. Is guaranteed to be a larger ID than any of the @@ -127,7 +126,7 @@ impl Propagator for ReifiedPropagator PropagationStatusCP { self.propagate_reification(&mut context)?; - if context.evaluate_literal(self.reification_literal) == Some(true) { + if context.evaluate_predicate(self.reification_literal) == Some(true) { context.with_reification(self.reification_literal); let result = self.propagator.propagate(context); @@ -145,7 +144,7 @@ impl Propagator for ReifiedPropagator PropagationStatusCP { self.propagate_reification(&mut context)?; - if context.evaluate_literal(self.reification_literal) == Some(true) { + if context.evaluate_predicate(self.reification_literal) == Some(true) { context.with_reification(self.reification_literal); let result = self.propagator.propagate_from_scratch(context); @@ -161,8 +160,7 @@ impl Propagator for ReifiedPropagator Propagator for ReifiedPropagator ReifiedPropagator { fn map_propagation_status(&self, mut status: PropagationStatusCP) -> PropagationStatusCP { if let Err(Conflict::Propagator(ref mut conflict)) = status { - conflict - .conjunction - .push(self.reification_literal.get_true_predicate()); + conflict.conjunction.push(self.reification_literal); } status } @@ -186,13 +182,13 @@ impl ReifiedPropagator { where Prop: Propagator, { - if context.evaluate_literal(self.reification_literal) == Some(true) { + if context.evaluate_predicate(self.reification_literal) == Some(true) { return Ok(()); } if let Some(conflict) = self.propagator.detect_inconsistency(context.domains()) { context.post( - self.reification_literal.get_false_predicate(), + !self.reification_literal, (conflict.conjunction, &conflict.inference_code), )?; } @@ -210,13 +206,13 @@ impl ReifiedPropagator { return EnqueueDecision::Skip; } - if context.evaluate_literal(self.reification_literal) == Some(true) { + if context.evaluate_predicate(self.reification_literal) == Some(true) { // If the propagator would have enqueued and the literal is true then the reified // propagator is also enqueued return EnqueueDecision::Enqueue; } - if context.evaluate_literal(self.reification_literal) != Some(false) + if context.evaluate_predicate(self.reification_literal) != Some(false) && self .propagator .detect_inconsistency(context.domains()) @@ -271,6 +267,7 @@ mod tests { use crate::engine::PropagatorConflict; use crate::engine::test_solver::TestSolver; use crate::predicate; + use crate::predicates::PredicateConstructor; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; @@ -280,7 +277,9 @@ mod tests { fn a_detected_inconsistency_is_given_as_reason_for_propagating_reification_literal_to_false() { let mut solver = TestSolver::default(); - let reification_literal = solver.new_literal(); + let i_1 = solver.new_variable(0, 1); + let reification_literal = predicate!(i_1 == 1); + let a = solver.new_variable(1, 1); let b = solver.new_variable(2, 2); @@ -314,9 +313,9 @@ mod tests { }) .expect("no conflict"); - assert!(solver.is_literal_false(reification_literal)); + assert_eq!(solver.evaluate_predicate(reification_literal), Some(false)); - let reason = solver.get_reason_bool(reification_literal, false); + let reason = solver.get_reason_int(!reification_literal); assert_eq!(reason, triggered_conflict); } @@ -324,7 +323,7 @@ mod tests { fn a_true_literal_is_added_to_reason_for_propagation() { let mut solver = TestSolver::default(); - let reification_literal = solver.new_literal(); + let reification_literal = solver.new_variable(0, 1).lower_bound_predicate(1); let var = solver.new_variable(1, 5); let propagator = solver @@ -348,23 +347,20 @@ mod tests { solver.assert_bounds(var, 1, 5); - let _ = solver.set_literal(reification_literal, true); + let _ = solver.set_predicate(reification_literal); solver.propagate(propagator).expect("no conflict"); solver.assert_bounds(var, 3, 5); let reason = solver.get_reason_int(predicate![var >= 3]); - assert_eq!( - reason, - PropositionalConjunction::from(reification_literal.get_true_predicate()) - ); + assert_eq!(reason, PropositionalConjunction::from(reification_literal)); } #[test] fn a_true_literal_is_added_to_a_conflict_conjunction() { let mut solver = TestSolver::default(); - let reification_literal = solver.new_literal(); - let _ = solver.set_literal(reification_literal, true); + let reification_literal = solver.new_variable(0, 1).lower_bound_predicate(1); + let _ = solver.set_predicate(reification_literal); let var = solver.new_variable(1, 1); let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); @@ -390,10 +386,7 @@ mod tests { Conflict::Propagator(conflict_nogood) => { assert_eq!( conflict_nogood.conjunction, - PropositionalConjunction::from(vec![ - reification_literal.get_true_predicate(), - predicate![var >= 1] - ]) + PropositionalConjunction::from(vec![reification_literal, predicate![var >= 1]]) ) } @@ -405,7 +398,7 @@ mod tests { fn notify_propagator_is_enqueued_if_inconsistency_can_be_detected() { let mut solver = TestSolver::default(); - let reification_literal = solver.new_literal(); + let reification_literal = solver.new_variable(0, 1).lower_bound_predicate(1); let var = solver.new_variable(1, 5); let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index 075af43d9..b355deebd 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -3,6 +3,7 @@ use pumpkin_checking::CheckerVariable; use pumpkin_checking::InferenceChecker; use pumpkin_checking::IntExt; use pumpkin_checking::VariableState; +use pumpkin_core::asserts::pumpkin_assert_extreme; use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; @@ -76,6 +77,13 @@ where current_bounds.push(context.new_trailed_integer(context.lower_bound(x_i) as i64)); } + pumpkin_assert_extreme!( + lower_bound_left_hand_side + == x.iter().map(|x| context.lower_bound(x) as i64).sum::(), + "Expected {lower_bound_left_hand_side} to be equal to {}", + x.iter().map(|x| context.lower_bound(x)).sum::() + ); + let lower_bound_left_hand_side = context.new_trailed_integer(lower_bound_left_hand_side); LinearLessOrEqualPropagator { @@ -145,10 +153,7 @@ where let old_bound = context.read_trailed_integer(self.current_bounds[index]); let new_bound = context.lower_bound(x_i) as i64; - pumpkin_assert_simple!( - old_bound < new_bound, - "propagator should only be triggered when lower bounds are tightened, old_bound={old_bound}, new_bound={new_bound}" - ); + pumpkin_assert_simple!(new_bound > old_bound); context.write_trailed_integer( self.lower_bound_left_hand_side, @@ -221,10 +226,19 @@ where return Ok(()); } }; + pumpkin_assert_extreme!( + lower_bound_left_hand_side + == self.x.iter().map(|x| context.lower_bound(x)).sum::(), + "Expected {lower_bound_left_hand_side} to be equal to {}\n{:?}", + self.x.iter().map(|x| context.lower_bound(x)).sum::(), + self.x + .iter() + .map(|x| (x, context.lower_bound(x))) + .collect::>() + ); for (i, x_i) in self.x.iter().enumerate() { let bound = self.c - (lower_bound_left_hand_side - context.lower_bound(x_i)); - if context.upper_bound(x_i) > bound { context.post(predicate![x_i <= bound], i)?; } diff --git a/pumpkin-solver-py/src/brancher.rs b/pumpkin-solver-py/src/brancher.rs index 88d2e0437..0e103c502 100644 --- a/pumpkin-solver-py/src/brancher.rs +++ b/pumpkin-solver-py/src/brancher.rs @@ -8,13 +8,14 @@ use pumpkin_solver::core::predicates::Predicate; use pumpkin_solver::core::results::SolutionReference; use pumpkin_solver::core::statistics::StatisticLogger; use pumpkin_solver::core::variables::AffineView; +use pumpkin_solver::core::variables::AnyInteger; use pumpkin_solver::core::variables::DomainId; use crate::variables::IntExpression; #[derive(Debug)] pub struct PythonBrancher { - warm_start: WarmStart>, + warm_start: WarmStart>, default_brancher: DefaultBrancher, } diff --git a/pumpkin-solver-py/src/constraints/arguments.rs b/pumpkin-solver-py/src/constraints/arguments.rs index ee2425fa8..4ce0b164e 100644 --- a/pumpkin-solver-py/src/constraints/arguments.rs +++ b/pumpkin-solver-py/src/constraints/arguments.rs @@ -1,6 +1,6 @@ +use pumpkin_solver::core::predicates::Predicate; use pumpkin_solver::core::variables::AffineView; -use pumpkin_solver::core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; +use pumpkin_solver::core::variables::AnyInteger; use crate::variables::BoolExpression; use crate::variables::IntExpression; @@ -13,7 +13,7 @@ pub trait PythonConstraintArg { } impl PythonConstraintArg for IntExpression { - type Output = AffineView; + type Output = AffineView; fn to_solver_constraint_argument(self) -> Self::Output { self.0 @@ -21,7 +21,7 @@ impl PythonConstraintArg for IntExpression { } impl PythonConstraintArg for BoolExpression { - type Output = Literal; + type Output = Predicate; fn to_solver_constraint_argument(self) -> Self::Output { self.0 diff --git a/pumpkin-solver-py/src/constraints/globals.rs b/pumpkin-solver-py/src/constraints/globals.rs index 75a3a9964..5369ad6c3 100644 --- a/pumpkin-solver-py/src/constraints/globals.rs +++ b/pumpkin-solver-py/src/constraints/globals.rs @@ -39,7 +39,7 @@ macro_rules! python_constraint { pub fn implied_by( self, solver: &mut pumpkin_solver::Solver, - reification_literal: pumpkin_solver::core::variables::Literal, + reification_literal: pumpkin_solver::core::predicates::Predicate, ) -> Result<(), pumpkin_solver::core::ConstraintOperationError> { pumpkin_constraints::$constraint_func( $(<$type as super::arguments::PythonConstraintArg>::to_solver_constraint_argument(self.$field)),+ , diff --git a/pumpkin-solver-py/src/constraints/mod.rs b/pumpkin-solver-py/src/constraints/mod.rs index e8e269153..680474267 100644 --- a/pumpkin-solver-py/src/constraints/mod.rs +++ b/pumpkin-solver-py/src/constraints/mod.rs @@ -24,7 +24,7 @@ macro_rules! declare_constraints { pub fn implied_by( self, solver: &mut pumpkin_solver::Solver, - reification_literal: pumpkin_solver::core::variables::Literal, + reification_literal: pumpkin_solver::core::predicates::Predicate, ) -> Result<(), pumpkin_solver::core::ConstraintOperationError> { match self { $($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 9137b3682..4f1c5d7f0 100644 --- a/pumpkin-solver-py/src/model.rs +++ b/pumpkin-solver-py/src/model.rs @@ -12,6 +12,7 @@ use pumpkin_solver::core::optimisation::OptimisationDirection; use pumpkin_solver::core::optimisation::linear_sat_unsat::LinearSatUnsat; use pumpkin_solver::core::optimisation::linear_unsat_sat::LinearUnsatSat; use pumpkin_solver::core::options::SolverOptions; +use pumpkin_solver::core::predicates::PredicateConstructor; use pumpkin_solver::core::proof::ConstraintTag; use pumpkin_solver::core::proof::ProofLog; use pumpkin_solver::core::rand::SeedableRng; @@ -127,13 +128,16 @@ impl Model { } let literal = if let Some(name) = name { - self.solver.new_named_literal(name) + self.solver + .new_named_bounded_integer(0, 1, name) + .lower_bound_predicate(1) } else { - self.solver.new_literal() + self.solver + .new_bounded_integer(0, 1) + .lower_bound_predicate(1) }; - self.brancher - .add_domain(literal.get_true_predicate().get_domain()); + self.brancher.add_domain(literal.get_domain()); Ok(literal.into()) } @@ -156,25 +160,9 @@ impl Model { self.solver.is_inconsistent() } - /// Get an integer variable for the given boolean. - /// - /// The integer is 1 if the boolean is `true`, and 0 if the boolean is `false`. - /// - /// This is deprecated as of 0.3.0. Prefer to use `BoolExpression.as_integer`. - fn boolean_as_integer(&mut self, boolean: BoolExpression) -> IntExpression { - boolean.as_integer() - } - /// Reify a predicate as an explicit boolean expression. - /// - /// A tag should be provided for this link to be identifiable in the proof. - #[pyo3(signature = (predicate, tag, name=None))] - fn predicate_as_boolean( - &mut self, - predicate: Predicate, - tag: Tag, - name: Option<&str>, - ) -> PyResult { + #[pyo3(signature = (predicate))] + fn predicate_as_boolean(&mut self, predicate: Predicate) -> PyResult { if self.solver.is_inconsistent() { return Err(PyValueError::new_err( "Cannot reify predicate: solver is in an infeasible state", @@ -182,19 +170,8 @@ impl Model { } let solver_predicate = predicate.into_solver_predicate(); - let Tag(tag) = tag; - - let literal = if let Some(name) = name { - self.solver - .new_named_literal_for_predicate(solver_predicate, tag, name) - } else { - self.solver.new_literal_for_predicate(solver_predicate, tag) - }; - self.brancher - .add_domain(*literal.get_integer_variable().inner()); - - Ok(literal.into()) + Ok(solver_predicate.into()) } /// Add the given constraint to the model. diff --git a/pumpkin-solver-py/src/result.rs b/pumpkin-solver-py/src/result.rs index b13c782a3..1ec715984 100644 --- a/pumpkin-solver-py/src/result.rs +++ b/pumpkin-solver-py/src/result.rs @@ -47,6 +47,6 @@ impl Solution { } fn bool_value(&self, variable: BoolExpression) -> bool { - self.0.get_literal_value(variable.0) + self.0.get_predicate_value(variable.0) } } diff --git a/pumpkin-solver-py/src/variables.rs b/pumpkin-solver-py/src/variables.rs index 05b15a4ab..30f73fa9e 100644 --- a/pumpkin-solver-py/src/variables.rs +++ b/pumpkin-solver-py/src/variables.rs @@ -1,13 +1,13 @@ use pumpkin_solver::core::predicate; use pumpkin_solver::core::variables::AffineView; +use pumpkin_solver::core::variables::AnyInteger; use pumpkin_solver::core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; use pumpkin_solver::core::variables::TransformableVariable; use pyo3::prelude::*; #[pyclass(eq, hash, frozen, from_py_object)] #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] -pub struct IntExpression(pub AffineView); +pub struct IntExpression(pub AffineView); impl From for IntExpression { fn from(domain_id: DomainId) -> IntExpression { @@ -15,6 +15,18 @@ impl From for IntExpression { } } +impl From for IntExpression { + fn from(value: pumpkin_solver::core::predicates::Predicate) -> Self { + IntExpression(value.into()) + } +} + +impl From for IntExpression { + fn from(value: BoolExpression) -> Self { + IntExpression(value.0.into()) + } +} + #[pymethods] impl IntExpression { fn offset(&self, add_offset: i32) -> IntExpression { @@ -28,21 +40,31 @@ impl IntExpression { #[pyclass(eq, hash, frozen, from_py_object)] #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] -pub struct BoolExpression(pub Literal); +pub struct BoolExpression(pub pumpkin_solver::core::predicates::Predicate); #[pymethods] impl BoolExpression { - pub fn as_integer(&self) -> IntExpression { - IntExpression(self.0.get_integer_variable()) + pub fn scaled(&self, scale: i32) -> IntExpression { + let int_expr: IntExpression = (*self).into(); + int_expr.scaled(scale) + } + + pub fn offset(&self, offset: i32) -> IntExpression { + let int_expr: IntExpression = (*self).into(); + int_expr.offset(offset) } pub fn negate(&self) -> BoolExpression { BoolExpression(!self.0) } + + pub fn as_integer(&self) -> IntExpression { + (*self).into() + } } -impl From for BoolExpression { - fn from(literal: Literal) -> BoolExpression { +impl From for BoolExpression { + fn from(literal: pumpkin_solver::core::predicates::Predicate) -> BoolExpression { BoolExpression(literal) } } diff --git a/pumpkin-solver-py/tests/test_constraints.py b/pumpkin-solver-py/tests/test_constraints.py index 8d26295a8..e80f00c68 100644 --- a/pumpkin-solver-py/tests/test_constraints.py +++ b/pumpkin-solver-py/tests/test_constraints.py @@ -1,15 +1,14 @@ -""" -Generate constraints and expressions based on the grammar supported by the API +"""Generate constraints and expressions based on the grammar supported by the API. -Generates linear constraints, special operators and global constraints. -Whenever possible, the script also generates 'boolean as integer' versions of the arguments +Generates linear constraints, special operators and global constraints. Whenever possible, the script also generates +'boolean as integer' versions of the arguments """ from random import randint +import pumpkin_solver import pytest from pumpkin_solver import constraints -import pumpkin_solver def chain(*iterables): @@ -68,15 +67,11 @@ def create_linear_model(request): model = pumpkin_solver.Model() if bool: - args = [ - model.new_boolean_variable(name=f"x[{i}]").as_integer() for i in range(3) - ] + args = [model.new_boolean_variable(name=f"x[{i}]").as_integer() 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 + args = [a.scaled(-2 * i + 1) for i, a in enumerate(args)] # TODO: div by zero when scale = 0, fixed with +1 rhs = 1 cons = None @@ -104,15 +99,11 @@ def create_operator_model(request): model = pumpkin_solver.Model() if bool: - args = [ - model.new_boolean_variable(name=f"x[{i}]").as_integer() for i in range(3) - ] + args = [model.new_boolean_variable(name=f"x[{i}]").as_integer() 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 + 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 @@ -128,9 +119,7 @@ def create_operator_model(request): 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 + 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: @@ -151,16 +140,11 @@ def create_global_model(request): if name == "alldiff": if bool: - args = [ - model.new_boolean_variable(name=f"x[{i}]").as_integer() - for i in range(3) - ] + args = [model.new_boolean_variable(name=f"x[{i}]").as_integer() 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 + 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()) @@ -182,9 +166,7 @@ def create_global_model(request): 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() - ) + cons = constraints.Cumulative(start, duration, demand, capacity, model.new_constraint_tag()) else: assert False, f"unknown global {name}" @@ -200,9 +182,7 @@ def global_model(request): def make_id(args): name, scaled, bool = args - return " ".join( - ["Scaled" if scaled else "Unscaled", "Boolean" if bool else "Integer", name] - ) + return " ".join(["Scaled" if scaled else "Unscaled", "Boolean" if bool else "Integer", name]) @pytest.mark.parametrize("linear_model", generate_linear(), indirect=True, ids=make_id) diff --git a/pumpkin-solver/examples/disjunctive_scheduling.rs b/pumpkin-solver/examples/disjunctive_scheduling.rs index 39a76ebb5..72274d451 100644 --- a/pumpkin-solver/examples/disjunctive_scheduling.rs +++ b/pumpkin-solver/examples/disjunctive_scheduling.rs @@ -11,6 +11,7 @@ use pumpkin_conflict_resolvers::resolvers::ResolutionResolver; use pumpkin_core::constraints::NegatableConstraint; +use pumpkin_core::predicates::PredicateConstructor; use pumpkin_solver::Solver; use pumpkin_solver::core::results::ProblemSolution; use pumpkin_solver::core::results::SatisfactionResult; @@ -53,7 +54,7 @@ fn main() { let precedence_literals = (0..n_tasks) .map(|_| { (0..n_tasks) - .map(|_| solver.new_literal()) + .map(|_| solver.new_bounded_integer(0, 1).lower_bound_predicate(1)) .collect::>() }) .collect::>(); @@ -77,13 +78,7 @@ fn main() { .reify(&mut solver, literal); // Either x starts before y or y start before x - let _ = solver.add_clause( - [ - literal.get_true_predicate(), - precedence_literals[y][x].get_true_predicate(), - ], - constraint_tag, - ); + let _ = solver.add_clause([literal, precedence_literals[y][x]], constraint_tag); } } diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/ast.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/ast.rs index b653e221b..224656ec6 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/ast.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/ast.rs @@ -1,4 +1,5 @@ use log::warn; +use pumpkin_core::predicates::Predicate; use pumpkin_solver::core::branching::value_selection::DynamicValueSelector; use pumpkin_solver::core::branching::value_selection::InDomainInterval; use pumpkin_solver::core::branching::value_selection::InDomainMax; @@ -23,7 +24,6 @@ use pumpkin_solver::core::branching::variable_selection::Smallest; use pumpkin_solver::core::pumpkin_assert_eq_simple; use pumpkin_solver::core::pumpkin_assert_simple; use pumpkin_solver::core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; use super::error::FlatZincError; #[derive(Debug)] @@ -43,8 +43,8 @@ pub(crate) enum VariableSelectionStrategy { impl VariableSelectionStrategy { pub(crate) fn create_from_literals( &self, - propositional_variables: &[Literal], - ) -> DynamicVariableSelector { + propositional_variables: &[Predicate], + ) -> DynamicVariableSelector { DynamicVariableSelector::new(match self { VariableSelectionStrategy::AntiFirstFail => { warn!( @@ -128,7 +128,7 @@ pub(crate) enum ValueSelectionStrategy { } impl ValueSelectionStrategy { - pub(crate) fn create_for_literals(&self) -> DynamicValueSelector { + pub(crate) fn create_for_literals(&self) -> DynamicValueSelector { DynamicValueSelector::new(match self { ValueSelectionStrategy::InDomain | ValueSelectionStrategy::InDomainInterval diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/collect_domains.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/collect_domains.rs index 46b2ac0f4..6a9f3080a 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/collect_domains.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/collect_domains.rs @@ -5,8 +5,8 @@ use std::rc::Rc; use flatzinc::Annotation; use pumpkin_core::Solver; use pumpkin_core::containers::HashMap; +use pumpkin_core::predicate; use pumpkin_core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; use super::context::CompilationContext; use super::context::Domain; @@ -39,7 +39,7 @@ pub(crate) fn run( ) }); - let literal = Literal::new(domain_id); + let literal = predicate!(domain_id >= 1); if is_output_variable(annos) { context.outputs.push(Output::bool(id, literal)); diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/context.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/context.rs index 8cc79b4a5..af6399218 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/context.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/context.rs @@ -4,12 +4,13 @@ use std::collections::BTreeSet; use std::rc::Rc; use log::warn; +use pumpkin_core::predicate; +use pumpkin_core::predicates::Predicate; use pumpkin_solver::Solver; use pumpkin_solver::core::containers::HashMap; use pumpkin_solver::core::containers::HashSet; use pumpkin_solver::core::proof::ConstraintTag; use pumpkin_solver::core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; use crate::flatzinc::FlatZincError; use crate::flatzinc::instance::Output; @@ -37,16 +38,12 @@ pub(crate) struct CompilationContext<'a> { /// is posted or an array is created). pub(crate) variable_map: HashMap, DomainId>, - /// Literal which is always true - pub(crate) true_literal: Literal, - /// Literal which is always false - pub(crate) false_literal: Literal, /// All boolean parameters. pub(crate) boolean_parameters: HashMap, bool>, /// All boolean array parameters. pub(crate) boolean_array_parameters: HashMap, Rc<[bool]>>, /// A mapping from boolean variable array identifiers to slices of literals. - pub(crate) boolean_variable_arrays: HashMap, Rc<[Literal]>>, + pub(crate) boolean_variable_arrays: HashMap, Rc<[Predicate]>>, /// All integer parameters. pub(crate) integer_parameters: HashMap, i32>, /// All integer array parameters. @@ -75,9 +72,6 @@ pub(crate) enum Set { impl CompilationContext<'_> { pub(crate) fn new(solver: &mut Solver) -> CompilationContext<'_> { - let true_literal = solver.get_true_literal(); - let false_literal = solver.get_false_literal(); - CompilationContext { solver, identifiers: Default::default(), @@ -85,8 +79,6 @@ impl CompilationContext<'_> { outputs: Default::default(), equivalences: Default::default(), - true_literal, - false_literal, boolean_parameters: Default::default(), boolean_array_parameters: Default::default(), boolean_variable_arrays: Default::default(), @@ -117,14 +109,14 @@ impl CompilationContext<'_> { pub(crate) fn resolve_bool_variable( &mut self, expr: &flatzinc::Expr, - ) -> Result { + ) -> Result { match expr { flatzinc::Expr::VarParIdentifier(id) => self.resolve_bool_variable_from_identifier(id), flatzinc::Expr::Bool(value) => { if *value { - Ok(self.solver.get_true_literal()) + Ok(Predicate::trivially_true()) } else { - Ok(self.solver.get_false_literal()) + Ok(!Predicate::trivially_true()) } } _ => Err(FlatZincError::UnexpectedExpr), @@ -134,20 +126,20 @@ impl CompilationContext<'_> { pub(crate) fn resolve_bool_variable_from_identifier( &self, identifier: &str, - ) -> Result { + ) -> Result { if let Some(domain_id) = self .variable_map .get(&self.equivalences.representative(identifier)) { - Ok(Literal::new(*domain_id)) + Ok(predicate!(domain_id >= 1)) } else { self.boolean_parameters .get(&self.equivalences.representative(identifier)) .map(|value| { if *value { - self.solver.get_true_literal() + Predicate::trivially_true() } else { - self.solver.get_false_literal() + !Predicate::trivially_true() } }) .ok_or_else(|| FlatZincError::InvalidIdentifier { @@ -160,7 +152,7 @@ impl CompilationContext<'_> { pub(crate) fn resolve_bool_variable_array( &self, expr: &flatzinc::Expr, - ) -> Result, FlatZincError> { + ) -> Result, FlatZincError> { match expr { flatzinc::Expr::VarParIdentifier(id) => { if let Some(literal) = self.boolean_variable_arrays.get(id.as_str()) { @@ -173,9 +165,9 @@ impl CompilationContext<'_> { .iter() .map(|value| { if *value { - self.solver.get_true_literal() + Predicate::trivially_true() } else { - self.solver.get_false_literal() + !Predicate::trivially_true() } }) .collect() @@ -192,8 +184,8 @@ impl CompilationContext<'_> { flatzinc::BoolExpr::VarParIdentifier(id) => { self.resolve_bool_variable_from_identifier(id) } - flatzinc::BoolExpr::Bool(true) => Ok(self.solver.get_true_literal()), - flatzinc::BoolExpr::Bool(false) => Ok(self.solver.get_false_literal()), + flatzinc::BoolExpr::Bool(true) => Ok(Predicate::trivially_true()), + flatzinc::BoolExpr::Bool(false) => Ok(!Predicate::trivially_true()), }) .collect(), flatzinc::Expr::ArrayOfInt(array) => array diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/create_search_strategy.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/create_search_strategy.rs index 52d1fc609..5dc8a2459 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/create_search_strategy.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/create_search_strategy.rs @@ -1,6 +1,7 @@ use std::rc::Rc; use flatzinc::AnnExpr; +use pumpkin_core::predicates::Predicate; use pumpkin_solver::core::branching::Brancher; use pumpkin_solver::core::branching::branchers::dynamic_brancher::DynamicBrancher; use pumpkin_solver::core::branching::branchers::independent_variable_value_brancher::IndependentVariableValueBrancher; @@ -9,7 +10,6 @@ use pumpkin_solver::core::branching::value_selection::InDomainMax; use pumpkin_solver::core::branching::value_selection::InDomainMin; use pumpkin_solver::core::branching::variable_selection::InputOrder; use pumpkin_solver::core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; use super::context::CompilationContext; use crate::flatzinc::ast::FlatZincAst; @@ -31,7 +31,7 @@ pub(crate) fn run( fn get_bool_variables( context: &mut CompilationContext, variables: &AnnExpr, -) -> Result, FlatZincError> { +) -> Result, FlatZincError> { Ok(match variables { AnnExpr::String(identifier) => { vec![context.resolve_bool_variable_from_identifier(identifier)?] @@ -146,10 +146,7 @@ fn create_from_search_strategy( } AnnExpr::Expr(expr) => { let bool_variable_array = context - .resolve_bool_variable_array(expr)? - .iter() - .map(|literal| literal.get_integer_variable()) - .collect::>(); + .resolve_bool_variable_array(expr)?; match values { AnnExpr::Expr(expr) => { @@ -228,7 +225,7 @@ fn create_search_over_domains( } fn create_search_over_propositional_variables( - search_variables: &[Literal], + search_variables: &[Predicate], variable_selection_strategy: &VariableSelectionStrategy, value_selection_strategy: &ValueSelectionStrategy, ) -> DynamicBrancher { diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/define_variable_arrays.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/define_variable_arrays.rs index 2b023d80d..f928eacdd 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/define_variable_arrays.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/define_variable_arrays.rs @@ -11,7 +11,8 @@ use flatzinc::Expr; use flatzinc::IntExpr; use flatzinc::SetExpr; use flatzinc::SetLiteralExpr; -use pumpkin_core::variables::Literal; +use pumpkin_core::predicate; +use pumpkin_core::predicates::Predicate; use super::context::CompilationContext; use crate::flatzinc::FlatZincError; @@ -36,8 +37,8 @@ pub(crate) fn run( ArrayOfBoolExpr::Array(array) => array .iter() .map(|expr| match expr { - BoolExpr::Bool(true) => context.true_literal, - BoolExpr::Bool(false) => context.false_literal, + BoolExpr::Bool(true) => Predicate::trivially_true(), + BoolExpr::Bool(false) => !Predicate::trivially_true(), BoolExpr::VarParIdentifier(identifier) => { let other_id = context.identifiers.get_interned(identifier); let representative = @@ -49,7 +50,7 @@ pub(crate) fn run( .copied() .expect("referencing undefined boolean variable"); - Literal::new(domain_id) + predicate!(domain_id >= 1) } }) .collect(), diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs index e72963c14..24cf33c21 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs @@ -2,6 +2,7 @@ use std::rc::Rc; +use pumpkin_core::variables::AnyInteger; use pumpkin_propagators::disjunctive::ArgDisjunctiveTask; use pumpkin_solver::core::constraints::Constraint; use pumpkin_solver::core::constraints::NegatableConstraint; @@ -473,21 +474,12 @@ fn compile_set_in_reif( // Decomposed to `reif -> x >= lb /\ reif -> x <= ub` let forward = context .solver - .add_clause( - [ - !reif.get_true_predicate(), - predicate![variable >= lower_bound], - ], - constraint_tag, - ) + .add_clause([!reif, predicate![variable >= lower_bound]], constraint_tag) .is_ok() && context .solver .add_clause( - [ - !reif.get_true_predicate(), - !predicate![variable >= upper_bound + 1], - ], + [!reif, !predicate![variable >= upper_bound + 1]], constraint_tag, ) .is_ok(); @@ -498,7 +490,7 @@ fn compile_set_in_reif( .solver .add_clause( [ - reif.get_true_predicate(), + reif, !predicate![variable >= lower_bound], predicate![variable >= upper_bound + 1], ], @@ -512,11 +504,7 @@ fn compile_set_in_reif( Set::Sparse { values } => { let clause = values .iter() - .map(|&value| { - context - .solver - .new_literal_for_predicate(predicate![variable == value], constraint_tag) - }) + .map(|&value| predicate!(variable == value)) .collect::>(); pumpkin_constraints::clause(clause, constraint_tag) @@ -612,7 +600,6 @@ fn compile_bool_clause( .iter() .cloned() .chain(clause_2.iter().map(|literal| !*literal)) - .map(|literal| literal.get_true_predicate()) .collect(); Ok(context.solver.add_clause(clause, constraint_tag).is_ok()) @@ -648,11 +635,13 @@ fn compile_bool2int( let a = context.resolve_bool_variable(&exprs[0])?; let b = context.resolve_integer_variable(&exprs[1])?; - Ok( - pumpkin_constraints::binary_equals(a.get_integer_variable(), b.scaled(1), constraint_tag) - .post(context.solver) - .is_ok(), + Ok(pumpkin_constraints::binary_equals( + AnyInteger::Predicate(a).scaled(1), + AnyInteger::DomainId(b).scaled(1), + constraint_tag, ) + .post(context.solver) + .is_ok()) } fn compile_bool_or( @@ -677,12 +666,8 @@ fn compile_bool_xor( ) -> Result { check_parameters!(exprs, 2, "pumpkin_bool_xor"); - let a = context - .resolve_bool_variable(&exprs[0])? - .get_true_predicate(); - let b = context - .resolve_bool_variable(&exprs[1])? - .get_true_predicate(); + let a = context.resolve_bool_variable(&exprs[0])?; + let b = context.resolve_bool_variable(&exprs[1])?; let c1 = context.solver.add_clause([!a, !b], constraint_tag).is_ok(); let c2 = context.solver.add_clause([b, a], constraint_tag).is_ok(); diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/instance.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/instance.rs index a3e6f3e17..8f4e0349d 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/instance.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/instance.rs @@ -2,10 +2,10 @@ use std::fmt::Display; use std::fmt::Write; use std::rc::Rc; +use pumpkin_core::predicates::Predicate; use pumpkin_solver::core::branching::branchers::dynamic_brancher::DynamicBrancher; use pumpkin_solver::core::optimisation::OptimisationDirection; use pumpkin_solver::core::variables::DomainId; -use pumpkin_solver::core::variables::Literal; /// The objective function of a FlatZinc model, /// consisting of the direction (e.g. maximization or minimization) and the integer variable which @@ -41,14 +41,14 @@ impl FlatZincInstance { #[derive(Clone, Debug, PartialEq, Eq)] pub(crate) enum Output { - Bool(VariableOutput), + Bool(VariableOutput), Int(VariableOutput), - ArrayOfBool(ArrayOutput), + ArrayOfBool(ArrayOutput), ArrayOfInt(ArrayOutput), } impl Output { - pub(crate) fn bool(id: Rc, boolean: Literal) -> Output { + pub(crate) fn bool(id: Rc, boolean: Predicate) -> Output { Output::Bool(VariableOutput { id, variable: boolean, @@ -58,7 +58,7 @@ impl Output { pub(crate) fn array_of_bool( id: Rc, shape: Box<[(i32, i32)]>, - contents: Rc<[Literal]>, + contents: Rc<[Predicate]>, ) -> Output { Output::ArrayOfBool(ArrayOutput { id, diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs index eae152942..75f43ff11 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs @@ -394,7 +394,7 @@ fn print_solution_from_solver(solution: SolutionReference, outputs: &[Output]) { for output_specification in outputs { match output_specification { Output::Bool(output) => { - output.print_value(|literal| solution.get_literal_value(*literal)) + output.print_value(|literal| solution.get_predicate_value(*literal)) } Output::Int(output) => { @@ -402,7 +402,7 @@ fn print_solution_from_solver(solution: SolutionReference, outputs: &[Output]) { } Output::ArrayOfBool(output) => { - output.print_value(|literal| solution.get_literal_value(*literal)) + output.print_value(|literal| solution.get_predicate_value(*literal)) } Output::ArrayOfInt(output) => { diff --git a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/cardinality_networks_encoder.rs b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/cardinality_networks_encoder.rs index 0c3df3c1d..195d49854 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/cardinality_networks_encoder.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/cardinality_networks_encoder.rs @@ -1,10 +1,11 @@ use std::time::Instant; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::predicates::PredicateConstructor; use pumpkin_solver::Solver; use pumpkin_solver::core::proof::ConstraintTag; use pumpkin_solver::core::pumpkin_assert_eq_simple; use pumpkin_solver::core::pumpkin_assert_simple; -use pumpkin_solver::core::variables::Literal; use super::PseudoBooleanConstraintEncoderInterface; use super::WeightedLiteral; @@ -20,8 +21,8 @@ use crate::maxsat::encoders::EncodingError::CannotStrengthen; /// Constraints, 2011, 16: 195-221. #[derive(Debug)] pub(crate) struct CardinalityNetworkEncoder { - literals: Vec, - output: Vec, + literals: Vec, + output: Vec, num_clauses_added: usize, /// Useless, since the encoder is only used when solving DIMACS problems, but required to add /// constraints. @@ -81,10 +82,7 @@ impl PseudoBooleanConstraintEncoderInterface for CardinalityNetworkEncoder { println!("c CNE k = {k}"); if solver - .add_clause( - [(!self.output[k as usize]).get_true_predicate()], - self.constraint_tag, - ) + .add_clause([(!self.output[k as usize])], self.constraint_tag) .is_err() { Err(CannotStrengthen) @@ -97,7 +95,7 @@ impl PseudoBooleanConstraintEncoderInterface for CardinalityNetworkEncoder { impl CardinalityNetworkEncoder { /// Create a new encoder from the given literals which form the left-hand side. pub(crate) fn new( - literals: Vec, + literals: Vec, p: u64, solver: &mut Solver, ) -> Result { @@ -136,10 +134,7 @@ impl CardinalityNetworkEncoder { if result.is_err() { println!("c encoding detected conflict at the root!"); } else if !self.output.is_empty() { - let r = solver.add_clause( - [(!self.output[p as usize]).get_true_predicate()], - self.constraint_tag, - ); + let r = solver.add_clause([(!self.output[p as usize])], self.constraint_tag); if r.is_err() { return Err(EncodingError::RootPropagationConflict); } @@ -159,14 +154,11 @@ impl CardinalityNetworkEncoder { let num_padding_literals = round_up_to_multiple(n, k) - n; let padding_lits = (0..num_padding_literals) - .map(|_| solver.new_literal()) + .map(|_| solver.new_bounded_integer(0, 1).lower_bound_predicate(1)) .collect::>(); for &lit in padding_lits.iter() { - if solver - .add_clause([(!lit).get_true_predicate()], self.constraint_tag) - .is_err() - { + if solver.add_clause([(!lit)], self.constraint_tag).is_err() { return Err(EncodingError::RootPropagationConflict); } } @@ -188,35 +180,23 @@ impl CardinalityNetworkEncoder { fn s_merge( &mut self, - a: &[Literal], - b: &[Literal], + a: &[Predicate], + b: &[Predicate], solver: &mut Solver, - ) -> Option> { + ) -> Option> { pumpkin_assert_eq_simple!(a.len(), b.len()); if a.len() == 1 { - let c = vec![solver.new_literal(), solver.new_literal()]; - let a = a[0].get_true_predicate(); - let b = b[0].get_true_predicate(); + let c = vec![ + solver.new_bounded_integer(0, 1).lower_bound_predicate(1), + solver.new_bounded_integer(0, 1).lower_bound_predicate(1), + ]; + let a = a[0]; + let b = b[0]; - try_add_clause!( - self, - solver, - vec![!a, !b, c[1].get_true_predicate()], - self.constraint_tag - ); - try_add_clause!( - self, - solver, - vec![!a, c[0].get_true_predicate()], - self.constraint_tag - ); - try_add_clause!( - self, - solver, - vec![!b, c[0].get_true_predicate()], - self.constraint_tag - ); + try_add_clause!(self, solver, vec![!a, !b, c[1]], self.constraint_tag); + try_add_clause!(self, solver, vec![!a, c[0]], self.constraint_tag); + try_add_clause!(self, solver, vec![!b, c[0]], self.constraint_tag); return Some(c); } @@ -234,7 +214,7 @@ impl CardinalityNetworkEncoder { pumpkin_assert_eq_simple!((a.len() >> 1) + 1, e.len()); let mut c = (0..a.len()) - .map(|_| solver.new_literal()) + .map(|_| solver.new_bounded_integer(0, 1).lower_bound_predicate(1)) .collect::>(); c.insert(0, d[0]); @@ -242,29 +222,19 @@ impl CardinalityNetworkEncoder { try_add_clause!( self, solver, - vec![ - (!d[i + 1]).get_true_predicate(), - (!e[i]).get_true_predicate(), - (c[2 * (i + 1)]).get_true_predicate() - ], + vec![(!d[i + 1]), (!e[i]), (c[2 * (i + 1)])], self.constraint_tag ); try_add_clause!( self, solver, - vec![ - (!d[i + 1]).get_true_predicate(), - (c[2 * (i + 1) - 1]).get_true_predicate() - ], + vec![(!d[i + 1]), (c[2 * (i + 1) - 1])], self.constraint_tag ); try_add_clause!( self, solver, - vec![ - (!e[i]).get_true_predicate(), - (c[2 * (i + 1) - 1]).get_true_predicate() - ], + vec![(!e[i]), (c[2 * (i + 1) - 1])], self.constraint_tag ); } @@ -272,7 +242,7 @@ impl CardinalityNetworkEncoder { Some(c) } - fn h_sort(&mut self, seq: &[Literal], solver: &mut Solver) -> Option> { + fn h_sort(&mut self, seq: &[Predicate], solver: &mut Solver) -> Option> { pumpkin_assert_simple!(seq.len() & 1 == 0); let n = seq.len() >> 1; @@ -289,10 +259,10 @@ impl CardinalityNetworkEncoder { fn h_merge( &mut self, - a: &[Literal], - b: &[Literal], + a: &[Predicate], + b: &[Predicate], solver: &mut Solver, - ) -> Option> { + ) -> Option> { pumpkin_assert_eq_simple!(a.len(), b.len()); let n = a.len(); @@ -310,7 +280,7 @@ impl CardinalityNetworkEncoder { let e = self.h_merge(&a_even, &b_even, solver)?; let mut c = (0..2 * n - 2) - .map(|_| solver.new_literal()) + .map(|_| solver.new_bounded_integer(0, 1).lower_bound_predicate(1)) .collect::>(); c.insert(0, d[0]); @@ -320,29 +290,19 @@ impl CardinalityNetworkEncoder { try_add_clause!( self, solver, - vec![ - (!d[i + 1]).get_true_predicate(), - (!e[i]).get_true_predicate(), - (c[2 * (i + 1)]).get_true_predicate() - ], + vec![(!d[i + 1]), (!e[i]), (c[2 * (i + 1)])], self.constraint_tag ); try_add_clause!( self, solver, - vec![ - (!d[i + 1]).get_true_predicate(), - (c[2 * (i + 1) - 1]).get_true_predicate() - ], + vec![(!d[i + 1]), (c[2 * (i + 1) - 1])], self.constraint_tag ); try_add_clause!( self, solver, - vec![ - (!e[i]).get_true_predicate(), - (c[2 * (i + 1) - 1]).get_true_predicate() - ], + vec![(!e[i]), (c[2 * (i + 1) - 1])], self.constraint_tag ); } @@ -350,7 +310,7 @@ impl CardinalityNetworkEncoder { Some(c) } - fn card(&mut self, a: &[Literal], k: u64, solver: &mut Solver) -> Option> { + fn card(&mut self, a: &[Predicate], k: u64, solver: &mut Solver) -> Option> { let n = a.len() as u64; let m = n / k; pumpkin_assert_eq_simple!(n, m * k); @@ -393,13 +353,13 @@ fn round_up_to_multiple(k: u64, multiple: u64) -> u64 { } } -fn odd_literals(lits: &[Literal]) -> Vec { +fn odd_literals(lits: &[Predicate]) -> Vec { // Note: in the literature, sequences start at 1, hence the odd literals // step by two but start at the first literal. lits.iter().copied().step_by(2).collect::>() } -fn even_literals(lits: &[Literal]) -> Vec { +fn even_literals(lits: &[Predicate]) -> Vec { // Note: in the literature, sequences start at 1, hence the even literals // skip the first and then step by two. lits.iter().copied().skip(1).step_by(2).collect::>() @@ -407,6 +367,9 @@ fn even_literals(lits: &[Literal]) -> Vec { #[cfg(test)] mod tests { + use pumpkin_core::predicates::Predicate; + use pumpkin_core::predicates::PredicateConstructor; + use super::*; #[test] @@ -427,16 +390,8 @@ mod tests { let _ = CardinalityNetworkEncoder::new(xs.clone(), 1, &mut solver); - assert!( - solver - .add_clause([xs[0].get_true_predicate()], constraint_tag) - .is_ok() - ); - assert!( - solver - .add_clause([xs[1].get_true_predicate()], constraint_tag) - .is_err() - ); + assert!(solver.add_clause([xs[0]], constraint_tag).is_ok()); + assert!(solver.add_clause([xs[1]], constraint_tag).is_err()); } #[test] @@ -447,25 +402,13 @@ mod tests { let _ = CardinalityNetworkEncoder::new(xs.clone(), 2, &mut solver).expect("valid encoding"); - assert!( - solver - .add_clause([xs[0].get_true_predicate()], constraint_tag) - .is_ok() - ); - assert!( - solver - .add_clause([xs[1].get_true_predicate()], constraint_tag) - .is_ok() - ); - assert!( - solver - .add_clause([xs[2].get_true_predicate()], constraint_tag) - .is_err() - ); + assert!(solver.add_clause([xs[0]], constraint_tag).is_ok()); + assert!(solver.add_clause([xs[1]], constraint_tag).is_ok()); + assert!(solver.add_clause([xs[2]], constraint_tag).is_err()); } - fn create_variables(solver: &mut Solver, n: usize) -> Vec { - std::iter::from_fn(|| Some(solver.new_literal())) + fn create_variables(solver: &mut Solver, n: usize) -> Vec { + std::iter::from_fn(|| Some(solver.new_bounded_integer(0, 1).lower_bound_predicate(1))) .take(n) .collect::>() } diff --git a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/generalised_totaliser_encoder.rs b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/generalised_totaliser_encoder.rs index 968b3d7bd..008254c78 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/generalised_totaliser_encoder.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/generalised_totaliser_encoder.rs @@ -1,9 +1,10 @@ use log::debug; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::predicates::PredicateConstructor; use pumpkin_solver::core::containers::HashMap; use pumpkin_solver::core::proof::ConstraintTag; use pumpkin_solver::core::pumpkin_assert_moderate; use pumpkin_solver::core::pumpkin_assert_simple; -use pumpkin_solver::core::variables::Literal; use super::WeightedLiteral; use super::pseudo_boolean_constraint_encoder::EncodingError; @@ -70,10 +71,7 @@ impl PseudoBooleanConstraintEncoderInterface for GeneralisedTotaliserEncoder { self.index_last_added_weighted_literal = i; if solver - .add_clause( - [(!weighted_literals[i].literal).get_true_predicate()], - self.constraint_tag, - ) + .add_clause([(!weighted_literals[i].literal)], self.constraint_tag) .is_err() { return Err(EncodingError::CannotStrengthen); @@ -127,7 +125,7 @@ impl GeneralisedTotaliserEncoder { // these are to be used in the loop below // will be reused to avoid allocating each iteration - let mut value_to_literal_map: HashMap = HashMap::default(); + let mut value_to_literal_map: HashMap = HashMap::default(); let mut partial_sums: Vec = Vec::new(); // in each iteration, the literals of the next_layer are created and appropriate clauses @@ -189,7 +187,7 @@ impl GeneralisedTotaliserEncoder { // then create the variables, one for each partial sum, and register the mapping // between the partial sum value and the corresponding literal for partial_sum in &partial_sums { - let literal = solver.new_literal(); + let literal = solver.new_bounded_integer(0, 1).lower_bound_predicate(1); let _ = value_to_literal_map.insert(*partial_sum, literal); next_layer_node.push(WeightedLiteral { literal, @@ -205,9 +203,8 @@ impl GeneralisedTotaliserEncoder { solver .add_clause( vec![ - (!weighted_literal.literal).get_true_predicate(), - (*value_to_literal_map.get(&weighted_literal.weight).unwrap()) - .get_true_predicate(), + (!weighted_literal.literal), + (*value_to_literal_map.get(&weighted_literal.weight).unwrap()), ], self.constraint_tag, ) @@ -220,9 +217,8 @@ impl GeneralisedTotaliserEncoder { solver .add_clause( vec![ - (!weighted_literal.literal).get_true_predicate(), - (*value_to_literal_map.get(&weighted_literal.weight).unwrap()) - .get_true_predicate(), + (!weighted_literal.literal), + (*value_to_literal_map.get(&weighted_literal.weight).unwrap()), ], self.constraint_tag, ) @@ -239,10 +235,9 @@ impl GeneralisedTotaliserEncoder { solver .add_clause( vec![ - (!wl1.literal).get_true_predicate(), - (!wl2.literal).get_true_predicate(), - (*value_to_literal_map.get(&combined_weight).unwrap()) - .get_true_predicate(), + (!wl1.literal), + (!wl2.literal), + (*value_to_literal_map.get(&combined_weight).unwrap()), ], self.constraint_tag, ) @@ -256,10 +251,7 @@ impl GeneralisedTotaliserEncoder { } else { solver .add_clause( - vec![ - (!wl1.literal).get_true_predicate(), - (!wl2.literal).get_true_predicate(), - ], + vec![(!wl1.literal), (!wl2.literal)], self.constraint_tag, ) .expect("Adding encoding clause should not lead to conflict"); diff --git a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs index 472fd900b..58b6b3463 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/pseudo_boolean_constraint_encoder.rs @@ -318,16 +318,15 @@ impl PseudoBooleanConstraintEncoder { for term in &weighted_literals { if term.weight > k - self.constant_term - && solver.get_literal_value(term.literal).is_none() + && solver.get_predicate_value(term.literal).is_none() { has_assigned = true; - let result = - solver.add_clause([(!term.literal).get_true_predicate()], constraint_tag); + let result = solver.add_clause([(!term.literal)], constraint_tag); if result.is_err() { return Err(EncodingError::RootPropagationConflict); } - } else if solver.get_literal_value(term.literal) == Some(true) { + } else if solver.get_predicate_value(term.literal) == Some(true) { self.constant_term += term.weight; } } @@ -340,7 +339,7 @@ impl PseudoBooleanConstraintEncoder { // collect terms that are not assigned at the root level let unassigned_weighted_literals: Vec = weighted_literals .iter() - .filter(|term| solver.get_literal_value(term.literal).is_none()) + .filter(|term| solver.get_predicate_value(term.literal).is_none()) .copied() .collect(); diff --git a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/weighted_literal.rs b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/weighted_literal.rs index 70efe5828..fdb97b050 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/weighted_literal.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/maxsat/encoders/weighted_literal.rs @@ -1,8 +1,8 @@ -use pumpkin_solver::core::variables::Literal; +use pumpkin_core::predicates::Predicate; #[derive(Copy, Clone, Debug)] /// A struct containing a literal, weight and (optionally) the bound which the literal represents pub(crate) struct WeightedLiteral { - pub(crate) literal: Literal, + pub(crate) literal: Predicate, pub(crate) weight: u64, } diff --git a/pumpkin-solver/src/bin/pumpkin-solver/parsers/dimacs.rs b/pumpkin-solver/src/bin/pumpkin-solver/parsers/dimacs.rs index be722af6b..8d78ae5ab 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/parsers/dimacs.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/parsers/dimacs.rs @@ -19,11 +19,12 @@ use std::num::NonZeroI32; use std::num::NonZeroU32; use std::str::FromStr; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::predicates::PredicateConstructor; use pumpkin_solver::Solver; use pumpkin_solver::core::Function; use pumpkin_solver::core::options::SolverOptions; use pumpkin_solver::core::proof::ConstraintTag; -use pumpkin_solver::core::variables::Literal; use thiserror::Error; /// A dimacs sink stores a set of clauses and allows for new variables to be created. @@ -434,7 +435,7 @@ fn next_header_component<'a, Num: FromStr>( pub(crate) struct SolverDimacsSink { pub(crate) solver: Solver, pub(crate) objective: Function, - pub(crate) variables: Vec, + pub(crate) variables: Vec, constraint_tag: ConstraintTag, } @@ -452,7 +453,7 @@ impl SolverArgs { } impl SolverDimacsSink { - fn mapped_clause(&self, clause: &[NonZeroI32]) -> Vec { + fn mapped_clause(&self, clause: &[NonZeroI32]) -> Vec { clause .iter() .map(|dimacs_code| { @@ -474,7 +475,11 @@ impl DimacsSink for SolverDimacsSink { let mut solver = Solver::with_options(solver_options); let variables = (0..num_variables) - .map(|code| solver.new_named_literal(format!("{}", code + 1))) + .map(|code| { + solver + .new_named_bounded_integer(0, 1, format!("{}", code + 1)) + .lower_bound_predicate(1) + }) .collect::>(); let constraint_tag = solver.new_constraint_tag(); @@ -488,10 +493,7 @@ impl DimacsSink for SolverDimacsSink { } fn add_hard_clause(&mut self, clause: &[NonZeroI32]) { - let mapped = self - .mapped_clause(clause) - .into_iter() - .map(|literal| literal.get_true_predicate()); + let mapped = self.mapped_clause(clause).into_iter(); let _ = self.solver.add_clause(mapped, self.constraint_tag); } @@ -500,7 +502,7 @@ impl DimacsSink for SolverDimacsSink { let is_clause_satisfied = clause .iter() - .any(|literal| self.solver.get_literal_value(*literal).unwrap_or(false)); + .any(|literal| self.solver.get_predicate_value(*literal).unwrap_or(false)); if clause.is_empty() { // The soft clause is violated at the root level. @@ -512,14 +514,12 @@ impl DimacsSink for SolverDimacsSink { .add_weighted_literal(clause[0], weight.get().into()); } else { // General case, a soft clause with more than one literal. - let soft_literal = self.solver.new_literal(); + let soft_literal = self + .solver + .new_bounded_integer(0, 1) + .lower_bound_predicate(1); clause.push(soft_literal); - let _ = self.solver.add_clause( - clause - .into_iter() - .map(|literal| literal.get_true_predicate()), - self.constraint_tag, - ); + let _ = self.solver.add_clause(clause, self.constraint_tag); self.objective .add_weighted_literal(!soft_literal, weight.get().into()); diff --git a/pumpkin-solver/tests/solver_test.rs b/pumpkin-solver/tests/solver_test.rs index e7b0d3171..6a5df2b2e 100644 --- a/pumpkin-solver/tests/solver_test.rs +++ b/pumpkin-solver/tests/solver_test.rs @@ -20,7 +20,7 @@ fn proof_with_reified_literals() { let constraint_tag = solver.new_constraint_tag(); let variable = solver.new_named_bounded_integer(1, 10, "var"); - let literal = solver.new_literal_for_predicate(predicate![variable == 5], constraint_tag); + let literal = predicate![variable == 5]; solver .add_constraint(pumpkin_constraints::clause(vec![literal], constraint_tag))