diff --git a/pumpkin-crates/core/src/api/mod.rs b/pumpkin-crates/core/src/api/mod.rs index eee7cf34c..9973e073b 100644 --- a/pumpkin-crates/core/src/api/mod.rs +++ b/pumpkin-crates/core/src/api/mod.rs @@ -128,8 +128,8 @@ pub mod state { pub use crate::engine::EmptyDomain; pub use crate::engine::EmptyDomainConflict; pub use crate::engine::State; - pub use crate::engine::propagation::CurrentNogood; - pub use crate::engine::propagation::PropagatorId; + pub use crate::propagation::CurrentNogood; + pub use crate::propagation::PropagatorId; } pub use crate::basic_types::Function; diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index f05cb13a6..9278963f9 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -19,8 +19,6 @@ use crate::constraints::ConstraintPoster; use crate::containers::HashSet; use crate::engine::ConstraintSatisfactionSolver; use crate::engine::predicates::predicate::Predicate; -use crate::engine::propagation::constructor::PropagatorConstructor; -pub use crate::engine::propagation::store::PropagatorHandle; use crate::engine::termination::TerminationCondition; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; @@ -35,6 +33,8 @@ use crate::options::SolverOptions; #[cfg(doc)] use crate::predicates; use crate::proof::ConstraintTag; +use crate::propagation::PropagatorConstructor; +pub use crate::propagation::store::PropagatorHandle; use crate::results::solution_iterator::SolutionIterator; use crate::results::unsatisfiable::UnsatisfiableUnderAssumptions; use crate::statistics::StatisticLogger; @@ -495,7 +495,7 @@ impl Solver { /// If the solver is already in a conflicting state, i.e. a previous call to this method /// already returned `false`, calling this again will not alter the solver in any way, and /// `false` will be returned again. - pub(crate) fn add_propagator( + pub fn add_propagator( &mut self, constructor: Constructor, ) -> Result, ConstraintOperationError> diff --git a/pumpkin-crates/core/src/basic_types/mod.rs b/pumpkin-crates/core/src/basic_types/mod.rs index 2cfe340ea..7635e9519 100644 --- a/pumpkin-crates/core/src/basic_types/mod.rs +++ b/pumpkin-crates/core/src/basic_types/mod.rs @@ -16,7 +16,7 @@ pub use constraint_operation_error::ConstraintOperationError; pub(crate) use csp_solver_execution_flag::CSPSolverExecutionFlag; pub use function::Function; pub(crate) use predicate_id_generators::DeletablePredicateIdGenerator; -pub(crate) use predicate_id_generators::PredicateId; +pub use predicate_id_generators::PredicateId; pub(crate) use predicate_id_generators::PredicateIdGenerator; pub use propagation_status_cp::*; pub use propositional_conjunction::PropositionalConjunction; diff --git a/pumpkin-crates/core/src/basic_types/predicate_id_generators/mod.rs b/pumpkin-crates/core/src/basic_types/predicate_id_generators/mod.rs index 674469ad6..535ce4d21 100644 --- a/pumpkin-crates/core/src/basic_types/predicate_id_generators/mod.rs +++ b/pumpkin-crates/core/src/basic_types/predicate_id_generators/mod.rs @@ -2,5 +2,5 @@ mod deletable_predicate_id_generator; mod predicate_id_generator; pub(crate) use deletable_predicate_id_generator::DeletablePredicateIdGenerator; -pub(crate) use predicate_id_generator::PredicateId; +pub use predicate_id_generator::PredicateId; pub(crate) use predicate_id_generator::PredicateIdGenerator; diff --git a/pumpkin-crates/core/src/basic_types/predicate_id_generators/predicate_id_generator.rs b/pumpkin-crates/core/src/basic_types/predicate_id_generators/predicate_id_generator.rs index cb4fd3b75..303452d95 100644 --- a/pumpkin-crates/core/src/basic_types/predicate_id_generators/predicate_id_generator.rs +++ b/pumpkin-crates/core/src/basic_types/predicate_id_generators/predicate_id_generator.rs @@ -104,8 +104,9 @@ impl Iterator for PredicateIdIterator { } } +/// An ID for a predicate which has its truth-value tracked by the solver. #[derive(Debug, Clone, Copy, Eq, PartialEq, Hash, Ord, PartialOrd)] -pub(crate) struct PredicateId { +pub struct PredicateId { pub(crate) id: u32, } diff --git a/pumpkin-crates/core/src/basic_types/solution.rs b/pumpkin-crates/core/src/basic_types/solution.rs index f6242b2f1..4dbdb583f 100644 --- a/pumpkin-crates/core/src/basic_types/solution.rs +++ b/pumpkin-crates/core/src/basic_types/solution.rs @@ -1,13 +1,21 @@ use crate::engine::Assignments; -use crate::engine::propagation::contexts::HasAssignments; 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; /// A trait which specifies the common behaviours of [`Solution`] and [`SolutionReference`]. -pub trait ProblemSolution: HasAssignments { +pub trait ProblemSolution { + /// Returns the number of defined [`DomainId`]s. + fn num_domains(&self) -> usize; + + fn get_integer_value(&self, var: Var) -> i32; + + fn get_literal_value(&self, literal: Literal) -> bool; +} + +impl ProblemSolution for T { /// Returns the number of defined [`DomainId`]s. fn num_domains(&self) -> usize { self.assignments().num_domains() as usize @@ -33,7 +41,7 @@ pub struct SolutionReference<'a> { } impl<'a> SolutionReference<'a> { - pub fn new(assignments: &'a Assignments) -> SolutionReference<'a> { + pub(crate) fn new(assignments: &'a Assignments) -> SolutionReference<'a> { SolutionReference { assignments } } @@ -43,19 +51,15 @@ impl<'a> SolutionReference<'a> { } } -impl ProblemSolution for SolutionReference<'_> {} - /// A solution which takes ownership of its inner structures. +/// +/// Implements [`ProblemSolution`]. #[derive(Clone, Debug, Default)] pub struct Solution { assignments: Assignments, } impl Solution { - pub fn new(assignments: Assignments) -> Self { - Self { assignments } - } - pub fn get_domains(&self) -> DomainGeneratorIterator { self.assignments.get_domains() // todo: Should we skip the first element as it could be the always true domain id? @@ -70,14 +74,14 @@ impl Solution { pub fn contains_domain_id(&self, domain_id: DomainId) -> bool { domain_id.id() < self.assignments.num_domains() } +} - pub fn is_predicate_satisfied(&self, predicate: Predicate) -> bool { - self.assignments.is_predicate_satisfied(predicate) +impl From for Solution { + fn from(value: Assignments) -> Self { + Self { assignments: value } } } -impl ProblemSolution for Solution {} - impl From> for Solution { fn from(value: SolutionReference) -> Self { Self { @@ -90,10 +94,26 @@ impl<'a> HasAssignments for SolutionReference<'a> { fn assignments(&self) -> &'a Assignments { self.assignments } + + fn trailed_values(&self) -> &crate::engine::TrailedValues { + unimplemented!("Currently, this information cannot be retrieved using this structure") + } + + fn trailed_values_mut(&mut self) -> &mut crate::engine::TrailedValues { + unimplemented!("Currently, this information cannot be retrieved using this structure") + } } impl HasAssignments for Solution { fn assignments(&self) -> &Assignments { &self.assignments } + + fn trailed_values(&self) -> &crate::engine::TrailedValues { + unimplemented!("Currently, this information cannot be retrieved using this structure") + } + + fn trailed_values_mut(&mut self) -> &mut crate::engine::TrailedValues { + unimplemented!("Currently, this information cannot be retrieved using this structure") + } } diff --git a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs index 4d38eeea5..c3fc3899e 100644 --- a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs +++ b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs @@ -3,10 +3,10 @@ use crate::ConstraintOperationError; #[cfg(doc)] use crate::engine::ConstraintSatisfactionSolver; use crate::engine::EmptyDomainConflict; -#[cfg(doc)] -use crate::engine::propagation::Propagator; use crate::engine::state::Conflict; use crate::predicates::Predicate; +#[cfg(doc)] +use crate::propagation::Propagator; /// a conflict info which can be stored in the solver. /// two (related) conflicts can happen: diff --git a/pumpkin-crates/core/src/branching/branchers/alternating/strategies/until_solution.rs b/pumpkin-crates/core/src/branching/branchers/alternating/strategies/until_solution.rs index c24d94b46..8abcbf904 100644 --- a/pumpkin-crates/core/src/branching/branchers/alternating/strategies/until_solution.rs +++ b/pumpkin-crates/core/src/branching/branchers/alternating/strategies/until_solution.rs @@ -143,7 +143,7 @@ mod tests { )); assert!(!brancher.is_using_default_brancher()); - brancher.on_solution(Solution::new(assignments.clone()).as_reference()); + brancher.on_solution(Solution::from(assignments.clone()).as_reference()); let _ = brancher.next_decision(&mut SelectionContext::new( &assignments, &mut TestRandom::default(), @@ -164,7 +164,7 @@ mod tests { )); assert!(brancher.is_using_default_brancher()); - brancher.on_solution(Solution::new(assignments.clone()).as_reference()); + brancher.on_solution(Solution::from(assignments.clone()).as_reference()); let _ = brancher.next_decision(&mut SelectionContext::new( &assignments, &mut TestRandom::default(), @@ -198,7 +198,7 @@ mod tests { )); assert!(!brancher.is_using_default_brancher()); - brancher.on_solution(Solution::new(assignments.clone()).as_reference()); + brancher.on_solution(Solution::from(assignments.clone()).as_reference()); let _ = brancher.next_decision(&mut SelectionContext::new( &assignments, &mut TestRandom::default(), @@ -219,7 +219,7 @@ mod tests { )); assert!(brancher.is_using_default_brancher()); - brancher.on_solution(Solution::new(assignments.clone()).as_reference()); + brancher.on_solution(Solution::from(assignments.clone()).as_reference()); let _ = brancher.next_decision(&mut SelectionContext::new( &assignments, &mut TestRandom::default(), diff --git a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs index cb7628570..7db972e70 100644 --- a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs +++ b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs @@ -15,6 +15,7 @@ use crate::containers::StorageKey; use crate::create_statistics_struct; use crate::engine::Assignments; use crate::engine::predicates::predicate::Predicate; +use crate::propagation::ReadDomains; use crate::results::Solution; use crate::statistics::Statistic; use crate::statistics::StatisticLogger; @@ -239,7 +240,7 @@ impl AutonomousSearch { return predicate; } // Match the truth value according to the best solution. - if solution.is_predicate_satisfied(predicate) { + if solution.evaluate_predicate(predicate) == Some(true) { predicate } else { !predicate diff --git a/pumpkin-crates/core/src/branching/selection_context.rs b/pumpkin-crates/core/src/branching/selection_context.rs index b37941d95..26c4fd86a 100644 --- a/pumpkin-crates/core/src/branching/selection_context.rs +++ b/pumpkin-crates/core/src/branching/selection_context.rs @@ -7,12 +7,12 @@ use crate::engine::Assignments; #[cfg(test)] use crate::engine::notifications::NotificationEngine; use crate::engine::predicates::predicate::Predicate; -#[cfg(doc)] -use crate::engine::propagation::PropagationContext; use crate::engine::variables::DomainGeneratorIterator; #[cfg(doc)] use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; +#[cfg(doc)] +use crate::propagation::Domains; /// The context provided to the [`Brancher`], /// it allows the retrieval of domain values of variables and access to methods from a [`Random`] diff --git a/pumpkin-crates/core/src/constraints/mod.rs b/pumpkin-crates/core/src/constraints/mod.rs index fe320abd3..a0b0f53b0 100644 --- a/pumpkin-crates/core/src/constraints/mod.rs +++ b/pumpkin-crates/core/src/constraints/mod.rs @@ -49,7 +49,7 @@ pub use table::*; use crate::ConstraintOperationError; use crate::Solver; -use crate::engine::propagation::constructor::PropagatorConstructor; +use crate::propagation::PropagatorConstructor; use crate::propagators::ReifiedPropagatorArgs; use crate::variables::Literal; diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 23d89d81c..a1ca33369 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -12,8 +12,6 @@ use crate::engine::State; use crate::engine::constraint_satisfaction_solver::CSPSolverState; use crate::engine::predicates::predicate::Predicate; use crate::engine::predicates::predicate::PredicateType; -use crate::engine::propagation::CurrentNogood; -use crate::engine::propagation::ExplanationContext; use crate::engine::solver_statistics::SolverStatistics; use crate::predicate; use crate::predicates::PropositionalConjunction; @@ -21,6 +19,8 @@ use crate::proof::InferenceCode; use crate::proof::ProofLog; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; +use crate::propagation::CurrentNogood; +use crate::propagation::ExplanationContext; use crate::propagators::nogoods::NogoodPropagator; use crate::pumpkin_assert_eq_simple; use crate::pumpkin_assert_simple; diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs index fb6e8439e..c8d38dc71 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -2,12 +2,12 @@ use crate::containers::HashMap; use crate::engine::Assignments; use crate::engine::SolverStatistics; use crate::engine::conflict_analysis::ConflictAnalysisContext; -#[cfg(doc)] -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::contexts::HasAssignments; use crate::predicates::Predicate; use crate::proof::InferenceCode; use crate::proof::ProofLog; +use crate::propagation::HasAssignments; +#[cfg(doc)] +use crate::propagation::ReadDomains; use crate::state::CurrentNogood; use crate::state::State; @@ -50,4 +50,12 @@ impl<'a> HasAssignments for MinimisationContext<'a> { fn assignments(&self) -> &Assignments { &self.state.assignments } + + fn trailed_values(&self) -> &crate::engine::TrailedValues { + &self.state.trailed_values + } + + fn trailed_values_mut(&mut self) -> &mut crate::engine::TrailedValues { + &mut self.state.trailed_values + } } diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs index 5bc023861..2056ac647 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs @@ -1,18 +1,18 @@ -use super::MinimisationContext; use crate::basic_types::moving_averages::MovingAverage; use crate::containers::HashMap; use crate::containers::HashSet; use crate::engine::Assignments; +use crate::engine::conflict_analysis::MinimisationContext; use crate::engine::conflict_analysis::NogoodMinimiser; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::contexts::HasAssignments; use crate::predicates::Predicate; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; +use crate::propagation::CurrentNogood; +use crate::propagation::HasAssignments; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_eq_moderate; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; -use crate::state::CurrentNogood; #[derive(Debug, Clone, Default)] pub(crate) struct RecursiveMinimiser { @@ -100,7 +100,7 @@ impl RecursiveMinimiser { // If the predicate is a decision predicate, it cannot be a predicate from the original // learned nogood since those are labelled as part of initialisation. // Therefore the decision literal is labelled as poison and then return. - if context.is_decision_predicate(&input_predicate) { + if context.is_decision_predicate(input_predicate) { self.assign_predicate_label(input_predicate, Label::Poison); self.current_depth -= 1; return; @@ -110,7 +110,7 @@ impl RecursiveMinimiser { // (levels from the original learned clause) cannot be removed. if !self.is_decision_level_allowed( context - .get_checkpoint_for_predicate(&input_predicate) + .get_checkpoint_for_predicate(input_predicate) .unwrap(), ) { self.assign_predicate_label(input_predicate, Label::Poison); @@ -130,7 +130,7 @@ impl RecursiveMinimiser { for antecedent_predicate in reason.iter().copied() { // Root assignments can be safely ignored. if context - .get_checkpoint_for_predicate(&antecedent_predicate) + .get_checkpoint_for_predicate(antecedent_predicate) .unwrap() == 0 { diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs index 225c59544..22288e285 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs @@ -1,14 +1,14 @@ use std::cmp; -use super::MinimisationContext; use crate::containers::HashSet; use crate::containers::KeyedVec; use crate::containers::SparseSet; +use crate::engine::conflict_analysis::MinimisationContext; use crate::engine::conflict_analysis::NogoodMinimiser; use crate::engine::predicates::predicate::PredicateType; -use crate::engine::propagation::contexts::HasAssignments; use crate::predicate; use crate::predicates::Predicate; +use crate::propagation::HasAssignments; use crate::variables::DomainId; #[derive(Clone, Debug)] diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs index d29031a71..2173bf98a 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs @@ -14,11 +14,11 @@ use crate::engine::conflict_analysis::Mode; use crate::engine::conflict_analysis::NogoodMinimiser; use crate::engine::conflict_analysis::RecursiveMinimiser; use crate::engine::constraint_satisfaction_solver::NogoodLabel; -use crate::engine::propagation::CurrentNogood; use crate::predicates::Predicate; use crate::proof::InferenceCode; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; +use crate::propagation::CurrentNogood; use crate::propagators::nogoods::NogoodPropagator; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_moderate; diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 1f2a0fe08..1e2d95603 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -17,7 +17,6 @@ use super::conflict_analysis::AnalysisMode; use super::conflict_analysis::ConflictAnalysisContext; use super::conflict_analysis::NoLearningResolver; use super::conflict_analysis::SemanticMinimiser; -use super::propagation::constructor::PropagatorConstructor; use super::solver_statistics::SolverStatistics; use super::termination::TerminationCondition; use super::variables::IntegerVariable; @@ -41,7 +40,6 @@ use crate::engine::RestartStrategy; use crate::engine::State; use crate::engine::conflict_analysis::ConflictResolver as Resolver; use crate::engine::predicates::predicate::Predicate; -use crate::engine::propagation::store::PropagatorHandle; use crate::options::LearningOptions; use crate::proof::ConstraintTag; use crate::proof::FinalizingContext; @@ -50,6 +48,8 @@ use crate::proof::ProofLog; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; use crate::proof::finalize_proof; +use crate::propagation::PropagatorConstructor; +use crate::propagation::store::PropagatorHandle; use crate::propagators::nogoods::NogoodPropagator; use crate::propagators::nogoods::NogoodPropagatorConstructor; use crate::pumpkin_assert_eq_simple; diff --git a/pumpkin-crates/core/src/engine/cp/mod.rs b/pumpkin-crates/core/src/engine/cp/mod.rs index e6dda5f9a..e987703a0 100644 --- a/pumpkin-crates/core/src/engine/cp/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/mod.rs @@ -1,5 +1,4 @@ mod assignments; -pub(crate) mod propagation; mod propagator_queue; pub(crate) mod reason; pub(crate) mod test_solver; @@ -9,7 +8,7 @@ pub(crate) use assignments::Assignments; pub(crate) use assignments::ConstraintProgrammingTrailEntry; pub use assignments::EmptyDomain; pub(crate) use propagator_queue::PropagatorQueue; -pub(crate) use trailed::*; +pub use trailed::*; #[cfg(test)] mod tests { @@ -20,11 +19,11 @@ mod tests { use crate::engine::TrailedValues; use crate::engine::cp::assignments; use crate::engine::notifications::NotificationEngine; - use crate::engine::propagation::PropagationContextMut; - use crate::engine::propagation::PropagatorId; use crate::engine::reason::ReasonStore; use crate::predicate; use crate::proof::InferenceCode; + use crate::propagation::PropagationContext; + use crate::propagation::PropagatorId; #[test] fn test_no_update_reason_store_if_no_update_lower_bound() { @@ -36,7 +35,7 @@ mod tests { assert_eq!(reason_store.len(), 0); { let mut notification_engine = NotificationEngine::default(); - let mut context = PropagationContextMut::new( + let mut context = PropagationContext::new( &mut trailed_values, &mut assignments, &mut reason_store, @@ -65,7 +64,7 @@ mod tests { assert_eq!(reason_store.len(), 0); { let mut notification_engine = NotificationEngine::default(); - let mut context = PropagationContextMut::new( + let mut context = PropagationContext::new( &mut trailed_values, &mut assignments, &mut reason_store, @@ -94,7 +93,7 @@ mod tests { assert_eq!(reason_store.len(), 0); { let mut notification_engine = NotificationEngine::default(); - let mut context = PropagationContextMut::new( + let mut context = PropagationContext::new( &mut trailed_values, &mut assignments, &mut reason_store, diff --git a/pumpkin-crates/core/src/engine/cp/propagation/contexts/mod.rs b/pumpkin-crates/core/src/engine/cp/propagation/contexts/mod.rs deleted file mode 100644 index 1c4a1eb5e..000000000 --- a/pumpkin-crates/core/src/engine/cp/propagation/contexts/mod.rs +++ /dev/null @@ -1,4 +0,0 @@ -pub(crate) mod explanation_context; -pub(crate) mod propagation_context; - -pub(crate) use propagation_context::*; diff --git a/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs deleted file mode 100644 index e9835e8b1..000000000 --- a/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs +++ /dev/null @@ -1,406 +0,0 @@ -use crate::basic_types::PredicateId; -use crate::engine::Assignments; -use crate::engine::EmptyDomain; -use crate::engine::EmptyDomainConflict; -use crate::engine::TrailedInteger; -use crate::engine::TrailedValues; -use crate::engine::notifications::NotificationEngine; -use crate::engine::notifications::PredicateIdAssignments; -use crate::engine::predicates::predicate::Predicate; -#[cfg(doc)] -use crate::engine::propagation::Propagator; -use crate::engine::propagation::PropagatorId; -use crate::engine::reason::Reason; -use crate::engine::reason::ReasonStore; -use crate::engine::reason::StoredReason; -use crate::engine::variables::IntegerVariable; -use crate::engine::variables::Literal; -use crate::proof::InferenceCode; -use crate::pumpkin_assert_simple; - -pub(crate) struct PropagationContextWithTrailedValues<'a> { - pub(crate) trailed_values: &'a mut TrailedValues, - pub(crate) assignments: &'a Assignments, - pub(crate) predicate_id_assignments: &'a PredicateIdAssignments, -} - -impl<'a> PropagationContextWithTrailedValues<'a> { - pub(crate) fn new( - trailed_values: &'a mut TrailedValues, - assignments: &'a Assignments, - predicate_id_assignments: &'a PredicateIdAssignments, - ) -> Self { - Self { - trailed_values, - assignments, - predicate_id_assignments, - } - } - - pub(crate) fn as_readonly(&self) -> PropagationContext<'_> { - PropagationContext { - assignments: self.assignments, - } - } -} - -/// [`PropagationContext`] is passed to propagators during propagation. -/// It may be queried to retrieve information about the current variable domains such as the -/// lower-bound of a particular variable, or used to apply changes to the domain of a variable -/// e.g. set `[x >= 5]`. -/// -/// -/// Note that the [`PropagationContext`] is the only point of communication beween -/// the propagations and the solver during propagation. -#[derive(Clone, Copy, Debug)] -pub(crate) struct PropagationContext<'a> { - pub assignments: &'a Assignments, -} - -impl<'a> PropagationContext<'a> { - pub(crate) fn new(assignments: &'a Assignments) -> Self { - PropagationContext { assignments } - } -} - -#[derive(Debug)] -pub(crate) struct PropagationContextMut<'a> { - pub(crate) trailed_values: &'a mut TrailedValues, - pub(crate) assignments: &'a mut Assignments, - pub(crate) reason_store: &'a mut ReasonStore, - pub(crate) propagator_id: PropagatorId, - pub(crate) notification_engine: &'a mut NotificationEngine, - reification_literal: Option, -} - -impl<'a> PropagationContextMut<'a> { - pub(crate) fn new( - trailed_values: &'a mut TrailedValues, - assignments: &'a mut Assignments, - reason_store: &'a mut ReasonStore, - notification_engine: &'a mut NotificationEngine, - propagator_id: PropagatorId, - ) -> Self { - PropagationContextMut { - trailed_values, - assignments, - reason_store, - propagator_id, - notification_engine, - reification_literal: None, - } - } - - pub(crate) fn get_predicate(&mut self, predicate_id: PredicateId) -> Predicate { - self.notification_engine.get_predicate(predicate_id) - } - - pub(crate) fn get_id(&mut self, predicate: Predicate) -> PredicateId { - self.notification_engine.get_id(predicate) - } - - /// Register the propagator to be enqueued when the provided [`Predicate`] becomes true. - /// - /// Returns the [`PredicateId`] assigned to the provided predicate, which will be provided - /// to [`Propagator::notify_predicate_satisfied`]. - pub(crate) fn register_predicate(&mut self, predicate: Predicate) -> PredicateId { - self.notification_engine.watch_predicate( - predicate, - self.propagator_id, - self.trailed_values, - self.assignments, - ) - } - - /// Apply a reification literal to all the explanations that are passed to the context. - pub(crate) fn with_reification(&mut self, reification_literal: Literal) { - pumpkin_assert_simple!( - self.reification_literal.is_none(), - "cannot reify an already reified propagation context" - ); - - self.reification_literal = Some(reification_literal); - } - - pub(crate) fn as_trailed_readonly(&mut self) -> PropagationContextWithTrailedValues<'_> { - PropagationContextWithTrailedValues { - trailed_values: self.trailed_values, - assignments: self.assignments, - predicate_id_assignments: self.notification_engine.predicate_id_assignments(), - } - } - - pub(crate) fn as_readonly(&self) -> PropagationContext<'_> { - PropagationContext { - assignments: self.assignments, - } - } - - pub(crate) fn get_checkpoint(&self) -> usize { - self.assignments.get_checkpoint() - } - - /// Returns whether the [`Predicate`] corresponding to the provided [`PredicateId`] is - /// satisfied. - pub(crate) fn is_predicate_id_falsified(&mut self, predicate_id: PredicateId) -> bool { - self.notification_engine - .is_predicate_id_falsified(predicate_id, self.assignments) - } - - /// Returns whether the [`Predicate`] corresponding to the provided [`PredicateId`] is - /// satisfied. - pub(crate) fn is_predicate_id_satisfied(&mut self, predicate_id: PredicateId) -> bool { - self.notification_engine - .is_predicate_id_satisfied(predicate_id, self.assignments) - } - - /// Returns the number of [`PredicateId`]s. - pub(crate) fn num_predicate_ids(&self) -> usize { - self.notification_engine.num_predicate_ids() - } -} - -/// A trait which defines common methods for retrieving the [`Assignments`] and -/// [`AssignmentsPropositional`] from the structure which implements this trait. -pub trait HasAssignments { - /// Returns the stored [`Assignments`]. - fn assignments(&self) -> &Assignments; -} - -pub(crate) trait HasTrailedValues { - fn trailed_values(&self) -> &TrailedValues; - fn trailed_values_mut(&mut self) -> &mut TrailedValues; -} - -mod private { - use super::*; - - impl HasTrailedValues for PropagationContextWithTrailedValues<'_> { - fn trailed_values(&self) -> &TrailedValues { - self.trailed_values - } - - fn trailed_values_mut(&mut self) -> &mut TrailedValues { - self.trailed_values - } - } - - impl HasTrailedValues for PropagationContextMut<'_> { - fn trailed_values(&self) -> &TrailedValues { - self.trailed_values - } - - fn trailed_values_mut(&mut self) -> &mut TrailedValues { - self.trailed_values - } - } - - impl HasAssignments for PropagationContext<'_> { - fn assignments(&self) -> &Assignments { - self.assignments - } - } - - impl HasAssignments for PropagationContextMut<'_> { - fn assignments(&self) -> &Assignments { - self.assignments - } - } - - impl HasAssignments for PropagationContextWithTrailedValues<'_> { - fn assignments(&self) -> &Assignments { - self.assignments - } - } -} - -pub(crate) trait ManipulateTrailedValues: HasTrailedValues { - fn new_trailed_integer(&mut self, initial_value: i64) -> TrailedInteger { - self.trailed_values_mut().grow(initial_value) - } - - fn value(&self, trailed_integer: TrailedInteger) -> i64 { - self.trailed_values().read(trailed_integer) - } - - fn add_assign(&mut self, trailed_integer: TrailedInteger, addition: i64) { - self.trailed_values_mut() - .add_assign(trailed_integer, addition); - } - - fn assign(&mut self, trailed_integer: TrailedInteger, value: i64) { - self.trailed_values_mut().assign(trailed_integer, value); - } -} - -impl ManipulateTrailedValues for T {} - -pub(crate) trait ReadDomains: HasAssignments { - fn is_predicate_satisfied(&self, predicate: Predicate) -> bool { - self.assignments() - .evaluate_predicate(predicate) - .is_some_and(|truth_value| truth_value) - } - - fn is_predicate_falsified(&self, predicate: Predicate) -> bool { - self.assignments() - .evaluate_predicate(predicate) - .is_some_and(|truth_value| !truth_value) - } - - fn is_decision_predicate(&self, predicate: &Predicate) -> bool { - self.assignments().is_decision_predicate(predicate) - } - - fn get_checkpoint_for_predicate(&self, predicate: &Predicate) -> Option { - self.assignments().get_checkpoint_for_predicate(predicate) - } - - fn is_literal_true(&self, literal: &Literal) -> bool { - literal - .get_integer_variable() - .lower_bound(self.assignments()) - == 1 - } - - fn is_literal_false(&self, literal: &Literal) -> bool { - literal - .get_integer_variable() - .upper_bound(self.assignments()) - == 0 - } - - fn is_literal_fixed(&self, literal: &Literal) -> bool { - self.is_fixed(literal) - } - - /// Returns the holes which were created on the current decision level. - fn get_holes_at_current_checkpoint( - &self, - var: &Var, - ) -> impl Iterator { - var.get_holes_at_current_checkpoint(self.assignments()) - } - - /// Returns all of the holes (currently) in the domain of `var` (including ones which were - /// created at previous decision levels). - fn get_holes(&self, var: &Var) -> impl Iterator { - var.get_holes(self.assignments()) - } - - /// Returns `true` if the domain of the given variable is singleton. - fn is_fixed(&self, var: &Var) -> bool { - self.lower_bound(var) == self.upper_bound(var) - } - - fn lower_bound(&self, var: &Var) -> i32 { - var.lower_bound(self.assignments()) - } - - #[allow(unused, reason = "Will be part of the API")] - fn lower_bound_at_trail_position( - &self, - var: &Var, - trail_position: usize, - ) -> i32 { - var.lower_bound_at_trail_position(self.assignments(), trail_position) - } - - fn upper_bound(&self, var: &Var) -> i32 { - var.upper_bound(self.assignments()) - } - - #[allow(unused, reason = "Will be part of the API")] - fn upper_bound_at_trail_position( - &self, - var: &Var, - trail_position: usize, - ) -> i32 { - var.upper_bound_at_trail_position(self.assignments(), trail_position) - } - - fn contains(&self, var: &Var, value: i32) -> bool { - var.contains(self.assignments(), value) - } - - fn contains_at_trail_position( - &self, - var: &Var, - value: i32, - trail_position: usize, - ) -> bool { - var.contains_at_trail_position(self.assignments(), value, trail_position) - } - - fn iterate_domain(&self, var: &Var) -> impl Iterator { - var.iterate_domain(self.assignments()) - } -} - -impl ReadDomains for T {} - -impl PropagationContextMut<'_> { - pub(crate) fn evaluate_predicate(&self, predicate: Predicate) -> Option { - self.assignments.evaluate_predicate(predicate) - } - - /// Assign the truth-value of the given [`Predicate`] to `true` in the current partial - /// assignment. - /// - /// If the truth-value is already `true`, then this is a no-op. Alternatively, if the - /// truth-value is `false`, then a conflict is triggered and the [`EmptyDomain`] error is - /// returned. At that point, no-more propagation should happen. - pub(crate) fn post( - &mut self, - predicate: Predicate, - reason: impl Into, - inference_code: InferenceCode, - ) -> Result<(), EmptyDomainConflict> { - let slot = self.reason_store.new_slot(); - - let modification_result = self.assignments.post_predicate( - predicate, - Some((slot.reason_ref(), inference_code)), - self.notification_engine, - ); - - match modification_result { - Ok(false) => Ok(()), - Ok(true) => { - let _ = slot.populate( - self.propagator_id, - build_reason(reason, self.reification_literal), - ); - Ok(()) - } - Err(EmptyDomain) => { - let _ = slot.populate( - self.propagator_id, - build_reason(reason, self.reification_literal), - ); - let (trigger_predicate, trigger_reason, trigger_inference_code) = - self.assignments.remove_last_trail_element(); - - Err(EmptyDomainConflict { - trigger_predicate, - trigger_reason, - trigger_inference_code, - }) - } - } - } -} - -fn build_reason(reason: impl Into, reification_literal: Option) -> StoredReason { - match reason.into() { - Reason::Eager(mut conjunction) => { - conjunction.extend( - reification_literal - .iter() - .map(|lit| lit.get_true_predicate()), - ); - StoredReason::Eager(conjunction) - } - Reason::DynamicLazy(code) => StoredReason::DynamicLazy(code), - } -} diff --git a/pumpkin-crates/core/src/engine/cp/propagation/mod.rs b/pumpkin-crates/core/src/engine/cp/propagation/mod.rs deleted file mode 100644 index 84470c3ea..000000000 --- a/pumpkin-crates/core/src/engine/cp/propagation/mod.rs +++ /dev/null @@ -1,107 +0,0 @@ -//! Contains the main building blocks for propagators. -//! -//! # Background -//! -//! A propagator takes as input a set of variables (xi ∈ X) and for each -//! variable a corresponding domain (Di ∈ D); it can then be seen as a -//! function which maps `D ↦ D'` such that D'i ⊆ Di for all -//! variables (i.e. the domain of a variable either remains the same after applying the propagator -//! or it becomes a subset of the domain before applying the propagator). -//! -//! An example of a propagator can be the simple not equal (`!=`) propagator, suppose that -//! we have two variables `x ∈ {0}` and `y ∈ {0, 1}` and the constraint `x != y`. The not equal -//! propagator will then take as input the variables `x` and `y` and their respective domains -//! D = {Dx = {0}, Dy = {0, 1} and produce a new domain D' -//! = {D'x = {0}, D'y = {1}} for which we can see that D_x = -//! D'x and D'y ⊆ Dy. -//! -//! A propagator is said to be at fix-point if Dx = D'x meaning -//! that no further propagations can take place when applying the propagator. A propagator is said -//! to be "idempotent" if a single call to it will result in it being at fix-point. -//! -//! For more information about the construction of these types of propagation-based solvers, we -//! refer to [\[1\]](https://dl.acm.org/doi/pdf/10.1145/1452044.1452046). -//! -//! # Practical -//! -//! Each concrete propagator is associated with one trait: [`Propagator`]. The main function to -//! implement for this trait is [`Proagator::propagate`], which performs the domain reduction. -//! -//! A propagator is created by a [`PropagatorConstructor`]. The constructor is responsible for -//! registering to domain events, and setting up the state of the propagator. The constructor is -//! provided a [`PropagatorConstructorContext`], which has all the available functions allowing the -//! propagator to hook into the solver state. -//! -//! We do not require propagators to be idempotent (see the previous section for a -//! definition) and it can be assumed that if a propagator is not at fix-point after propagating -//! that it will be called again by the solver until no further propagations happen. -//! -//! See the [`propagators`] folder for concrete propagator implementations. -//! -//! # How to implement a new propagator? -//! -//! We recommend the following workflow: -//! 1. Implement a propagator struct that implements the [`Propagator`] trait. For now only -//! implement the required functions, i.e., [`Propagator::debug_propagate_from_scratch`] and -//! [`Propagator::name`]. -//! 2. Implement the [`Propagator::initialise_at_root`] function which detects root-level -//! inconsistencies and is also responsible for registering the variables and corresponding -//! [`DomainEvents`] with the solver, so that the solver can notify the propagator once an event -//! happens that relates to one of the variables of the propagator. -//! 2. Create an implementation of the [`PropagatorConstructor`] trait, to register for domain -//! events and set up the propagator state. -//! 3. Following the procedure above gives an initial version of the propagator that is likely not -//! efficient, but has an important role for testing. Now is a good time to write tests which use -//! the [`TestSolver`]. **We strongly discourage skipping this step**. -//! * For example, see the tests in [`crate::propagators::arithmetic::absolute_value`]. -//! 4. Implement [`Propagator::notify`]. Depending on the concrete propagator, this may only make -//! sense when done together with the next step. -//! 5. Implement the remaining functions, i.e., [`Propagator::propagate`], -//! [`Propagator::synchronise`], and [`Propagator::initialise_at_root`]. These are all -//! interdependent. -//! 6. Decide on the priortiy of the propagator, i.e., implement [`Propagator::priority`]. -//! 7. Make sure to write new tests and run all tests throughout the process. -//! 8. The propagator implementation is now done! -//! -//! The propagator is added to the solver through [`ConstraintSatisfactionSolver::add_propagator`]. -//! -//! # Bibliography -//! -//! \[1\] C. Schulte and P. J. Stuckey, ‘Efficient constraint propagation engines’, ACM Transactions -//! on Programming Languages and Systems (TOPLAS), vol. 31, no. 1, pp. 1–43, 2008. -//! -//! \[2\] C. Schulte and G. Tack, ‘Views and iterators for generic constraint implementations’, in -//! International Workshop on Constraint Solving and Constraint Logic Programming, 2005, pp. -//! 118–132. - -pub(crate) mod constructor; -pub(crate) mod contexts; -pub(crate) mod local_id; -pub(crate) mod propagator; -pub(crate) mod propagator_id; -pub(crate) mod propagator_var_id; -pub(crate) mod store; - -pub use contexts::explanation_context::CurrentNogood; -pub(crate) use contexts::explanation_context::ExplanationContext; -pub(crate) use contexts::propagation_context::PropagationContext; -pub(crate) use contexts::propagation_context::PropagationContextMut; -pub(crate) use contexts::propagation_context::ReadDomains; -pub(crate) use local_id::LocalId; -pub(crate) use propagator::EnqueueDecision; -pub(crate) use propagator::Propagator; -pub use propagator_id::PropagatorId; -pub(crate) use propagator_var_id::PropagatorVarId; - -#[cfg(doc)] -use crate::engine::ConstraintSatisfactionSolver; -#[cfg(doc)] -use crate::engine::DomainEvents; -#[cfg(doc)] -use crate::engine::test_solver::TestSolver; -#[cfg(doc)] -use crate::engine::variables::IntegerVariable; -#[cfg(doc)] -use crate::propagators; -#[cfg(doc)] -use crate::propagators::linear_less_or_equal::LinearLessOrEqualPropagator; diff --git a/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs b/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs deleted file mode 100644 index 4dc13d8d8..000000000 --- a/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs +++ /dev/null @@ -1,196 +0,0 @@ -use downcast_rs::Downcast; -use downcast_rs::impl_downcast; -use dyn_clone::DynClone; -use dyn_clone::clone_trait_object; - -use super::ExplanationContext; -use super::PropagationContext; -use super::PropagationContextMut; -use super::contexts::PropagationContextWithTrailedValues; -use crate::basic_types::PredicateId; -use crate::basic_types::PropagationStatusCP; -use crate::basic_types::PropagatorConflict; -#[cfg(doc)] -use crate::create_statistics_struct; -#[cfg(doc)] -use crate::engine::ConstraintSatisfactionSolver; -use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::local_id::LocalId; -use crate::predicates::Predicate; -#[cfg(doc)] -use crate::pumpkin_asserts::PUMPKIN_ASSERT_ADVANCED; -#[cfg(doc)] -use crate::pumpkin_asserts::PUMPKIN_ASSERT_EXTREME; -#[cfg(doc)] -use crate::state::Conflict; -use crate::statistics::statistic_logger::StatisticLogger; - -// We need to use this to cast from `Box` to `NogoodPropagator`; rust inherently -// does not allow downcasting from the trait definition to its concrete type. -impl_downcast!(Propagator); - -// To allow the State object to be cloneable, we need to allow `Box` to be cloned. -clone_trait_object!(Propagator); - -/// All propagators implement the [`Propagator`] trait, which defines the main propagator logic with -/// regards to propagation, detecting conflicts, and providing explanations. -/// -/// The only required functions are [`Propagator::name`], -/// [`Propagator::initialise_at_root`], and [`Propagator::debug_propagate_from_scratch`]; all other -/// functions have default implementations. For initial development, the required functions are -/// enough, but a more mature implementation considers all functions in most cases. -/// -/// See the [`crate::engine::cp::propagation`] documentation for more details. -pub(crate) trait Propagator: Downcast + DynClone { - /// Return the name of the propagator, this is a convenience method that is used for printing. - fn name(&self) -> &str; - - /// A propagation method that is used to help debugging. - /// - /// This method propagates without relying on internal data structures, hence the immutable - /// &self parameter. It is usually best to implement this propagation method in the simplest - /// but correct way. When the assert level is set to [`PUMPKIN_ASSERT_ADVANCED`] or - /// [`PUMPKIN_ASSERT_EXTREME`] (see [`crate::pumpkin_asserts`]) this method will be called - /// to double check the reasons for failures and propagations that have been reported by - /// this propagator. - /// - /// Propagators are not required to propagate until a fixed point. It will be called again by - /// the solver until no further propagations happen. - fn debug_propagate_from_scratch(&self, context: PropagationContextMut) -> PropagationStatusCP; - - /// Propagate method that will be called during search (e.g. in - /// [`ConstraintSatisfactionSolver::solve`]). - /// - /// This method extends the current partial - /// assignments with inferred domain changes found by the - /// [`Propagator`]. In case no conflict has been detected it should return - /// [`Result::Ok`], otherwise it should return a [`Result::Err`] with an [`Conflict`] which - /// contains the reason for the failure; either because a propagation caused an - /// an empty domain ([`Conflict::EmptyDomain`]) or because the logic of the propagator - /// found the current state to be inconsistent ([`Conflict::Propagator`]). - /// - /// Note that the failure (explanation) is given as a conjunction of predicates that lead to the - /// failure - /// - /// Propagators are not required to propagate until a fixed point. It will be called - /// again by the solver until no further propagations happen. - /// - /// By default, this function calls [`Propagator::debug_propagate_from_scratch`]. - fn propagate(&mut self, context: PropagationContextMut) -> PropagationStatusCP { - self.debug_propagate_from_scratch(context) - } - - /// Called when an event happens to one of the variables the propagator is subscribed to. It - /// indicates whether the provided event should cause the propagator to be enqueued. - /// - /// This can be used to incrementally maintain data structures or perform propagations, and - /// should only be used for computationally cheap logic. Expensive computation should be - /// performed in the [`Propagator::propagate()`] method. - /// - /// By default the propagator is always enqueued for every event. Not all propagators will - /// benefit from implementing this, so it is not required to do so. - /// - /// Note that the variables and events to which the propagator is subscribed to are determined - /// upon propagator initialisation via [`Propagator::initialise_at_root`] by calling - /// [`PropagatorInitialisationContext::register()`]. - fn notify( - &mut self, - _context: PropagationContextWithTrailedValues, - _local_id: LocalId, - _event: OpaqueDomainEvent, - ) -> EnqueueDecision { - EnqueueDecision::Enqueue - } - - /// Called when an event happens to one of the variables the propagator is subscribed to. This - /// method is called during backtrack when the domain of a variable has been undone. - /// - /// This can be used to incrementally maintain data structures or perform propagations, and - /// should only be used for computationally cheap logic. Expensive computation should be - /// performed in the [`Propagator::propagate`] method. - /// - /// By default the propagator does nothing when this method is called. Not all propagators will - /// benefit from implementing this, so it is not required to do so. - /// - /// Note that the variables and events to which the propagator is subscribed to are determined - /// upon propagator initialisation via [`Propagator::initialise_at_root`] by calling - /// [`PropagatorInitialisationContext::register()`]. - fn notify_backtrack( - &mut self, - _context: PropagationContext, - _local_id: LocalId, - _event: OpaqueDomainEvent, - ) { - } - - /// Called when a [`PredicateId`] has been satisfied. - /// - /// By default, the propagator will be enqueued. - fn notify_predicate_id_satisfied(&mut self, _predicate_id: PredicateId) -> EnqueueDecision { - EnqueueDecision::Enqueue - } - - /// Called each time the [`ConstraintSatisfactionSolver`] backtracks, the propagator can then - /// update its internal data structures given the new variable domains. - /// - /// By default this function does nothing. - fn synchronise(&mut self, _context: PropagationContext) {} - - /// Returns the priority of the propagator represented as an integer. Lower values mean higher - /// priority and the priority determines the order in which propagators will be asked to - /// propagate. It is custom for simpler propagators to have lower priority values. - /// - /// By default the priority is set to 3. It is expected that propagator implementations would - /// set this value to some appropriate value. - fn priority(&self) -> u32 { - // setting an arbitrary priority by default - 3 - } - - /// A check whether this propagator can detect an inconsistency. - /// - /// By implementing this function, if the propagator is reified, it can propagate the - /// reification literal based on the detected inconsistency. Yet, an implementation is not - /// needed for correctness, as [`Propagator::propagate`] should still check for - /// inconsistency as well. - fn detect_inconsistency( - &self, - _context: PropagationContextWithTrailedValues, - ) -> Option { - None - } - - /// Hook which is called when a propagated [`Predicate`] should be explained using a lazy - /// reason. - /// - /// The code which was attached to the propagation through [`Reason::DynamicLazy`] is given, as - /// well as a context object which defines what can be inspected from the solver to build the - /// explanation. - /// - /// *Note:* The context which is provided contains the _current_ state (i.e. the state when the - /// explanation is generated); the bounds at the time of the propagation can be retrieved using - /// methods such as [`ExplanationContext::get_lower_bound_at_trail_position`] in combination - /// with [`ExplanationContext::get_trail_position`]. - fn lazy_explanation(&mut self, _code: u64, _context: ExplanationContext) -> &[Predicate] { - panic!( - "{}", - format!( - "Propagator {} does not support lazy explanations.", - self.name() - ) - ); - } - /// Logs statistics of the propagator using the provided [`StatisticLogger`]. - /// - /// It is recommended to create a struct through the [`create_statistics_struct!`] macro! - fn log_statistics(&self, _statistic_logger: StatisticLogger) {} -} - -/// Indicator of what to do when a propagator is notified. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub(crate) enum EnqueueDecision { - /// The propagator should be enqueued. - Enqueue, - /// The propagator should not be enqueued. - Skip, -} diff --git a/pumpkin-crates/core/src/engine/cp/propagator_queue.rs b/pumpkin-crates/core/src/engine/cp/propagator_queue.rs index 0625348c5..f11456dfe 100644 --- a/pumpkin-crates/core/src/engine/cp/propagator_queue.rs +++ b/pumpkin-crates/core/src/engine/cp/propagator_queue.rs @@ -3,7 +3,8 @@ use std::collections::BinaryHeap; use std::collections::VecDeque; use crate::containers::KeyedVec; -use crate::engine::cp::propagation::PropagatorId; +use crate::propagation::Priority; +use crate::propagation::PropagatorId; use crate::pumpkin_assert_moderate; #[derive(Debug, Clone)] @@ -34,7 +35,7 @@ impl PropagatorQueue { self.num_enqueued == 0 } - pub(crate) fn enqueue_propagator(&mut self, propagator_id: PropagatorId, priority: u32) { + pub(crate) fn enqueue_propagator(&mut self, propagator_id: PropagatorId, priority: Priority) { pumpkin_assert_moderate!((priority as usize) < self.queues.len()); if !self.is_propagator_enqueued(propagator_id) { @@ -43,7 +44,7 @@ impl PropagatorQueue { self.num_enqueued += 1; if self.queues[priority as usize].is_empty() { - self.present_priorities.push(Reverse(priority)); + self.present_priorities.push(Reverse(priority as u32)); } self.queues[priority as usize].push_back(propagator_id); } @@ -94,3 +95,26 @@ impl PropagatorQueue { .unwrap_or_default() } } + +#[cfg(test)] +mod tests { + use crate::engine::PropagatorQueue; + use crate::propagation::Priority; + use crate::state::PropagatorId; + + #[test] + fn test_ordering() { + let mut queue = PropagatorQueue::default(); + + queue.enqueue_propagator(PropagatorId(1), Priority::High); + queue.enqueue_propagator(PropagatorId(0), Priority::Medium); + queue.enqueue_propagator(PropagatorId(3), Priority::VeryLow); + queue.enqueue_propagator(PropagatorId(4), Priority::Low); + + assert_eq!(PropagatorId(1), queue.pop().unwrap()); + assert_eq!(PropagatorId(0), queue.pop().unwrap()); + assert_eq!(PropagatorId(4), queue.pop().unwrap()); + assert_eq!(PropagatorId(3), queue.pop().unwrap()); + assert_eq!(None, queue.pop()); + } +} diff --git a/pumpkin-crates/core/src/engine/cp/reason.rs b/pumpkin-crates/core/src/engine/cp/reason.rs index 05203a7e6..fb1e8525c 100644 --- a/pumpkin-crates/core/src/engine/cp/reason.rs +++ b/pumpkin-crates/core/src/engine/cp/reason.rs @@ -1,13 +1,13 @@ use std::fmt::Debug; -use super::propagation::ExplanationContext; -use super::propagation::PropagatorId; -use super::propagation::store::PropagatorStore; use crate::basic_types::PropositionalConjunction; use crate::basic_types::Trail; #[cfg(doc)] use crate::containers::KeyedVec; use crate::predicates::Predicate; +use crate::propagation::ExplanationContext; +use crate::propagation::PropagatorId; +use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_simple; /// The reason store holds a reason for each change made by a CP propagator on a trail. @@ -88,7 +88,7 @@ pub(crate) struct ReasonRef(pub(crate) u32); /// A reason for CP propagator to make a change #[derive(Debug)] -pub(crate) enum Reason { +pub enum Reason { /// An eager reason contains the propositional conjunction with the reason, without the /// propagated predicate. Eager(PropositionalConjunction), diff --git a/pumpkin-crates/core/src/engine/cp/test_helper.rs b/pumpkin-crates/core/src/engine/cp/test_helper.rs index 79e0df707..989480d46 100644 --- a/pumpkin-crates/core/src/engine/cp/test_helper.rs +++ b/pumpkin-crates/core/src/engine/cp/test_helper.rs @@ -4,19 +4,19 @@ use std::fmt::Debug; use std::fmt::Formatter; -use super::propagation::EnqueueDecision; +use crate::propagation::EnqueueDecision; use super::WatchListPropositional; use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropositionalConjunction; use crate::engine::opaque_domain_event::OpaqueDomainEvent; use crate::engine::predicates::integer_predicate::IntegerPredicate; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::PropagatorId; -use crate::engine::propagation::PropagatorInitialisationContext; +use crate::propagation::LocalId; +use crate::propagation::PropagationContext; +use crate::propagation::PropagationContextMut; +use crate::propagation::Propagator; +use crate::propagation::PropagatorId; +use crate::propagation::PropagatorInitialisationContext; use crate::engine::reason::ReasonStore; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; @@ -24,7 +24,7 @@ use crate::engine::variables::Literal; use crate::engine::variables::PropositionalVariable; use crate::engine::AssignmentsInteger; use crate::engine::AssignmentsPropositional; -use crate::engine::DomainEvents; +use crate::propagation::DomainEvents; use crate::engine::EmptyDomain; use crate::engine::WatchListCP; diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 4184f721a..f683543c2 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -5,16 +5,10 @@ use std::fmt::Debug; use std::num::NonZero; use super::PropagatorQueue; -use super::propagation::EnqueueDecision; -use super::propagation::ExplanationContext; -use super::propagation::constructor::PropagatorConstructor; use crate::containers::KeyGenerator; use crate::engine::EmptyDomain; use crate::engine::State; use crate::engine::predicates::predicate::Predicate; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::PropagatorId; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; use crate::engine::variables::Literal; @@ -23,6 +17,12 @@ use crate::predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::ExplanationContext; +use crate::propagation::PropagationContext; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorId; use crate::propagators::nogoods::NogoodPropagator; use crate::propagators::nogoods::NogoodPropagatorConstructor; use crate::state::Conflict; @@ -212,7 +212,7 @@ impl TestSolver { } pub(crate) fn propagate(&mut self, propagator: PropagatorId) -> Result<(), Conflict> { - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut self.state.trailed_values, &mut self.state.assignments, &mut self.state.reason_store, @@ -231,7 +231,7 @@ impl TestSolver { loop { { // Specify the life-times to be able to retrieve the trail entries - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut self.state.trailed_values, &mut self.state.assignments, &mut self.state.reason_store, @@ -339,7 +339,10 @@ impl TestSolver { .propagators .iter_propagators_mut() .for_each(|propagator| { - propagator.synchronise(PropagationContext::new(&self.state.assignments)) + propagator.synchronise(Domains::new( + &self.state.assignments, + &mut self.state.trailed_values, + )) }) } } diff --git a/pumpkin-crates/core/src/engine/cp/trailed/mod.rs b/pumpkin-crates/core/src/engine/cp/trailed/mod.rs index 6b322b555..3ce409b29 100644 --- a/pumpkin-crates/core/src/engine/cp/trailed/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/trailed/mod.rs @@ -2,5 +2,5 @@ mod trailed_change; mod trailed_integer; mod trailed_values; pub(crate) use trailed_change::TrailedChange; -pub(crate) use trailed_integer::TrailedInteger; +pub use trailed_integer::TrailedInteger; pub(crate) use trailed_values::TrailedValues; diff --git a/pumpkin-crates/core/src/engine/cp/trailed/trailed_integer.rs b/pumpkin-crates/core/src/engine/cp/trailed/trailed_integer.rs index 3ceeef972..397f783d2 100644 --- a/pumpkin-crates/core/src/engine/cp/trailed/trailed_integer.rs +++ b/pumpkin-crates/core/src/engine/cp/trailed/trailed_integer.rs @@ -1,7 +1,9 @@ use crate::containers::StorageKey; +/// An integer whose value is automatically restored upon backtracking to its previous value at the +/// checkpoint to which backtracking occurred. #[derive(Debug, Clone, Copy)] -pub(crate) struct TrailedInteger { +pub struct TrailedInteger { id: u32, } diff --git a/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs b/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs index 665719ca5..e2695b522 100644 --- a/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs +++ b/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs @@ -41,6 +41,7 @@ impl TrailedValues { self.values[trailed_integer] = value; } + #[cfg(test)] pub(crate) fn add_assign(&mut self, trailed_integer: TrailedInteger, addition: i64) { self.write(trailed_integer, self.values[trailed_integer] + addition); } diff --git a/pumpkin-crates/core/src/engine/debug_helper.rs b/pumpkin-crates/core/src/engine/debug_helper.rs index fa81125fc..d3eae77ec 100644 --- a/pumpkin-crates/core/src/engine/debug_helper.rs +++ b/pumpkin-crates/core/src/engine/debug_helper.rs @@ -7,14 +7,14 @@ use log::debug; use super::TrailedValues; use super::notifications::NotificationEngine; use super::predicates::predicate::Predicate; -use super::propagation::ExplanationContext; -use super::propagation::store::PropagatorStore; use super::reason::ReasonStore; use crate::basic_types::PropositionalConjunction; use crate::engine::cp::Assignments; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::PropagatorId; +use crate::propagation::ExplanationContext; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorId; +use crate::propagation::store::PropagatorStore; use crate::propagators::nogoods::NogoodPropagator; use crate::state::Conflict; @@ -77,14 +77,14 @@ impl DebugHelper { let num_entries_on_trail_before_propagation = assignments_clone.num_trail_entries(); let mut reason_store = Default::default(); - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, &mut notification_engine_clone, PropagatorId(propagator_id as u32), ); - let propagation_status_cp = propagator.debug_propagate_from_scratch(context); + let propagation_status_cp = propagator.propagate_from_scratch(context); if let Err(ref failure_reason) = propagation_status_cp { panic!( @@ -255,14 +255,14 @@ impl DebugHelper { if adding_predicates_was_successful { // Now propagate using the debug propagation method. let mut reason_store = Default::default(); - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, &mut notification_engine_clone, propagator_id, ); - let debug_propagation_status_cp = propagator.debug_propagate_from_scratch(context); + let debug_propagation_status_cp = propagator.propagate_from_scratch(context); // Note that it could be the case that the propagation leads to conflict, in this // case it should be the result of a propagation (i.e. an EmptyDomain) @@ -370,15 +370,14 @@ impl DebugHelper { loop { let num_predicates_before = assignments_clone.num_trail_entries(); - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, &mut notification_engine_clone, propagator_id, ); - let debug_propagation_status_cp = - propagator.debug_propagate_from_scratch(context); + let debug_propagation_status_cp = propagator.propagate_from_scratch(context); // We break if an error was found or if there were no more propagations (i.e. // fixpoint was reached) @@ -437,14 +436,14 @@ impl DebugHelper { if adding_predicates_was_successful { // now propagate using the debug propagation method let mut reason_store = Default::default(); - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, &mut notification_engine_clone, propagator_id, ); - let debug_propagation_status_cp = propagator.debug_propagate_from_scratch(context); + let debug_propagation_status_cp = propagator.propagate_from_scratch(context); assert!( debug_propagation_status_cp.is_err(), "Debug propagation could not reproduce the conflict reported diff --git a/pumpkin-crates/core/src/engine/mod.rs b/pumpkin-crates/core/src/engine/mod.rs index 684c3570d..5760b910e 100644 --- a/pumpkin-crates/core/src/engine/mod.rs +++ b/pumpkin-crates/core/src/engine/mod.rs @@ -27,5 +27,3 @@ pub(crate) use restart_strategy::RestartStrategy; pub(crate) use solver_statistics::SolverStatistics; pub use state::*; pub(crate) use variable_names::VariableNames; - -pub(crate) use crate::engine::notifications::DomainEvents; 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 a71b6fc44..4b0e69e5f 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 @@ -5,8 +5,8 @@ use enumset::EnumSetType; use crate::containers::KeyedVec; use crate::engine::notifications::NotificationEngine; -use crate::engine::propagation::PropagatorVarId; use crate::engine::variables::DomainId; +use crate::propagation::PropagatorVarId; #[derive(Default, Debug, Clone)] pub(crate) struct WatchListDomainEvents { diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_events.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_events.rs index da8d9ed35..2b428f7bc 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_events.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_events.rs @@ -3,46 +3,42 @@ use enumset::enum_set; use super::DomainEvent; +/// A set of [`DomainEvent`]s. #[derive(Debug, Copy, Clone)] -pub(crate) struct DomainEvents { - int_events: Option>, +pub struct DomainEvents { + events: Option>, } impl DomainEvents { /// DomainEvents with both lower and upper bound tightening (but not other value removal). - pub(crate) const BOUNDS: DomainEvents = DomainEvents::create_with_int_events(enum_set!( - DomainEvent::LowerBound | DomainEvent::UpperBound - )); + pub const BOUNDS: DomainEvents = + DomainEvents::new(enum_set!(DomainEvent::LowerBound | DomainEvent::UpperBound)); // this is all options right now, but won't be once we add variables of other types /// DomainEvents with lower and upper bound tightening, assigning to a single value, and /// single value removal. - pub(crate) const ANY_INT: DomainEvents = DomainEvents::create_with_int_events(enum_set!( + pub const ANY_INT: DomainEvents = DomainEvents::new(enum_set!( DomainEvent::Assign | DomainEvent::LowerBound | DomainEvent::UpperBound | DomainEvent::Removal )); /// DomainEvents with only lower bound tightening. - pub(crate) const LOWER_BOUND: DomainEvents = - DomainEvents::create_with_int_events(enum_set!(DomainEvent::LowerBound)); + pub const LOWER_BOUND: DomainEvents = DomainEvents::new(enum_set!(DomainEvent::LowerBound)); /// DomainEvents with only upper bound tightening. - #[allow(unused, reason = "will be part of public API at some point")] - pub(crate) const UPPER_BOUND: DomainEvents = - DomainEvents::create_with_int_events(enum_set!(DomainEvent::UpperBound)); + pub const UPPER_BOUND: DomainEvents = DomainEvents::new(enum_set!(DomainEvent::UpperBound)); /// DomainEvents with only assigning to a single value. - pub(crate) const ASSIGN: DomainEvents = - DomainEvents::create_with_int_events(enum_set!(DomainEvent::Assign)); + pub const ASSIGN: DomainEvents = DomainEvents::new(enum_set!(DomainEvent::Assign)); } impl DomainEvents { - pub(crate) const fn create_with_int_events(int_events: EnumSet) -> DomainEvents { + pub(crate) const fn new(int_events: EnumSet) -> DomainEvents { DomainEvents { - int_events: Some(int_events), + events: Some(int_events), } } - pub(crate) fn get_int_events(&self) -> EnumSet { - self.int_events + pub(crate) fn events(&self) -> EnumSet { + self.events .expect("Tried to retrieve int_events when it was not initialized") } } diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/event_sink.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/event_sink.rs index 3dee6bd2d..f1a618c1f 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/event_sink.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/event_sink.rs @@ -2,10 +2,10 @@ use enumset::EnumSet; use super::DomainEvent; use crate::containers::KeyedVec; -#[cfg(doc)] -use crate::engine::DomainEvents; use crate::engine::variables::DomainId; #[cfg(doc)] +use crate::propagation::DomainEvents; +#[cfg(doc)] use crate::propagators; use crate::pumpkin_assert_advanced; 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 a56c38c14..ddf607046 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 @@ -2,7 +2,7 @@ mod domain_event_watch_list; pub(crate) mod domain_events; mod event_sink; pub(crate) mod opaque_domain_event; -pub(crate) use domain_event_watch_list::DomainEvent; +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::*; diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/opaque_domain_event.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/opaque_domain_event.rs index f83bb5fe3..1b44f3539 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/opaque_domain_event.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/opaque_domain_event.rs @@ -1,7 +1,10 @@ use super::DomainEvent; +#[cfg(doc)] +use crate::engine::variables::IntegerVariable; -/// A wrapper for a domain event, which forces the propagator implementation to map the event -/// through the variable view. +/// A [`DomainEvent`] that happened in the solver. +/// +/// Obtain the event from the perspective of a variable through [`IntegerVariable::unpack_event`]. #[derive(Clone, Debug, Copy)] pub struct OpaqueDomainEvent(DomainEvent); diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index bd3521d0e..5e92af65c 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -1,29 +1,29 @@ mod domain_event_notification; mod predicate_notification; -pub(crate) use domain_event_notification::DomainEvent; +pub use domain_event_notification::DomainEvent; pub(crate) use domain_event_notification::EventSink; pub(crate) use domain_event_notification::WatchListDomainEvents; pub(crate) use domain_event_notification::Watchers; -pub(crate) use domain_event_notification::domain_events::DomainEvents; -pub(crate) use domain_event_notification::opaque_domain_event::OpaqueDomainEvent; +pub use domain_event_notification::domain_events::DomainEvents; +pub use domain_event_notification::opaque_domain_event::OpaqueDomainEvent; use enumset::EnumSet; pub(crate) use predicate_notification::PredicateIdAssignments; pub(crate) use predicate_notification::PredicateNotifier; -use super::propagation::PropagationContext; -use super::propagation::PropagatorVarId; use crate::basic_types::PredicateId; use crate::containers::KeyedVec; use crate::engine::Assignments; use crate::engine::PropagatorQueue; use crate::engine::TrailedValues; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagatorId; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; -use crate::engine::propagation::store::PropagatorStore; use crate::predicates::Predicate; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::PropagatorId; +use crate::propagation::PropagatorVarId; +use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_simple; use crate::variables::DomainId; @@ -309,6 +309,7 @@ impl NotificationEngine { pub(crate) fn process_backtrack_events( &mut self, assignments: &mut Assignments, + trailed_values: &mut TrailedValues, propagators: &mut PropagatorStore, ) -> bool { // If there are no variables being watched then there is no reason to perform these @@ -327,7 +328,7 @@ impl NotificationEngine { .get_backtrack_affected_propagators(event, domain) { let propagator = &mut propagators[propagator_var.propagator]; - let context = PropagationContext::new(assignments); + let context = Domains::new(assignments, trailed_values); propagator.notify_backtrack(context, propagator_var.variable, event.into()) } @@ -369,11 +370,8 @@ impl NotificationEngine { assignments: &mut Assignments, trailed_values: &mut TrailedValues, ) { - let context = PropagationContextWithTrailedValues::new( - trailed_values, - assignments, - predicate_id_assignments, - ); + let context = + NotificationContext::new(trailed_values, assignments, predicate_id_assignments); let enqueue_decision = propagators[propagator_id].notify(context, local_id, event.into()); @@ -517,10 +515,6 @@ impl NotificationEngine { result } - pub(crate) fn predicate_id_assignments(&self) -> &PredicateIdAssignments { - &self.predicate_notifier.predicate_id_assignments - } - pub(crate) fn synchronise( &mut self, backtrack_level: usize, diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index ca478c73b..808420a70 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -11,15 +11,6 @@ use crate::engine::PropagatorQueue; use crate::engine::TrailedValues; use crate::engine::VariableNames; use crate::engine::notifications::NotificationEngine; -use crate::engine::propagation::CurrentNogood; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::PropagatorId; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::store::PropagatorStore; use crate::engine::reason::ReasonRef; use crate::engine::reason::ReasonStore; use crate::predicate; @@ -30,6 +21,15 @@ use crate::proof::InferenceCode; use crate::proof::InferenceLabel; #[cfg(doc)] use crate::proof::ProofLog; +use crate::propagation::CurrentNogood; +use crate::propagation::Domains; +use crate::propagation::ExplanationContext; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::PropagatorId; +use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_eq_simple; use crate::pumpkin_assert_extreme; @@ -345,8 +345,6 @@ impl State { /// While the propagator is added to the queue for propagation, this function does _not_ /// trigger a round of propagation. An explicit call to [`State::propagate_to_fixed_point`] is /// necessary to run the new propagator for the first time. - #[allow(private_bounds, reason = "Propagator will be part of public API")] - #[allow(private_interfaces, reason = "Constructor will be part of public API")] pub fn add_propagator( &mut self, constructor: Constructor, @@ -362,7 +360,7 @@ impl State { let propagator = constructor.create(constructor_context); pumpkin_assert_simple!( - propagator.priority() <= 3, + propagator.priority() as u8 <= 3, "The propagator priority exceeds 3. Currently we only support values up to 3, but this can easily be changed if there is a good reason." @@ -385,19 +383,11 @@ impl State { /// Get a reference to the propagator identified by the given handle. /// /// For an exclusive reference, use [`State::get_propagator_mut`]. - #[allow( - private_bounds, - reason = "Propagator will be part of public interface in the future" - )] pub fn get_propagator(&self, handle: PropagatorHandle

) -> Option<&P> { self.propagators.get_propagator(handle) } /// Get an exclusive reference to the propagator identified by the given handle. - #[allow( - private_bounds, - reason = "Propagator will be part of public interface in the future" - )] pub fn get_propagator_mut( &mut self, handle: PropagatorHandle

, @@ -410,10 +400,10 @@ impl State { pub(crate) fn get_propagator_mut_with_context( &mut self, handle: PropagatorHandle

, - ) -> (Option<&mut P>, PropagationContextMut<'_>) { + ) -> (Option<&mut P>, PropagationContext<'_>) { ( self.propagators.get_propagator_mut(handle), - PropagationContextMut::new( + PropagationContext::new( &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, @@ -515,13 +505,15 @@ impl State { // + allow incremental synchronisation // + only call the subset of propagators that were notified since last backtrack for propagator in self.propagators.iter_propagators_mut() { - let context = PropagationContext::new(&self.assignments); + let context = Domains::new(&self.assignments, &mut self.trailed_values); propagator.synchronise(context); } - let _ = self - .notification_engine - .process_backtrack_events(&mut self.assignments, &mut self.propagators); + let _ = self.notification_engine.process_backtrack_events( + &mut self.assignments, + &mut self.trailed_values, + &mut self.propagators, + ); self.notification_engine.clear_event_drain(); self.notification_engine @@ -555,7 +547,7 @@ impl State { let propagation_status = { let propagator = &mut self.propagators[propagator_id]; - let context = PropagationContextMut::new( + let context = PropagationContext::new( &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, diff --git a/pumpkin-crates/core/src/lib.rs b/pumpkin-crates/core/src/lib.rs index 1e0107a3d..af2544699 100644 --- a/pumpkin-crates/core/src/lib.rs +++ b/pumpkin-crates/core/src/lib.rs @@ -4,7 +4,6 @@ pub(crate) mod basic_types; pub mod containers; pub(crate) mod engine; pub(crate) mod math; -pub(crate) mod propagators; pub(crate) mod pumpkin_asserts; #[cfg(doc)] @@ -16,6 +15,8 @@ pub mod branching; pub mod constraints; pub mod optimisation; pub mod proof; +pub mod propagation; +pub mod propagators; pub mod statistics; pub use convert_case; diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index 7115c90f8..432ce530d 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -7,9 +7,9 @@ use super::ProofLog; use crate::containers::HashMap; use crate::engine::State; use crate::engine::conflict_analysis::ConflictAnalysisContext; -use crate::engine::propagation::CurrentNogood; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; +use crate::propagation::CurrentNogood; pub(crate) struct FinalizingContext<'a> { pub(crate) conflict: PropositionalConjunction, diff --git a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs similarity index 86% rename from pumpkin-crates/core/src/engine/cp/propagation/constructor.rs rename to pumpkin-crates/core/src/propagation/constructor.rs index ba25d0714..290f625fc 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -1,29 +1,38 @@ use std::ops::Deref; use std::ops::DerefMut; +use super::Domains; use super::LocalId; -use super::PropagationContext; use super::Propagator; use super::PropagatorId; use super::PropagatorVarId; +#[cfg(doc)] +use crate::Solver; use crate::basic_types::PredicateId; use crate::engine::Assignments; -use crate::engine::DomainEvents; use crate::engine::State; use crate::engine::TrailedValues; use crate::engine::notifications::Watchers; +#[cfg(doc)] +use crate::engine::variables::AffineView; +#[cfg(doc)] +use crate::engine::variables::DomainId; use crate::predicates::Predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::proof::InferenceLabel; +#[cfg(doc)] +use crate::propagation::DomainEvent; +use crate::propagation::DomainEvents; use crate::variables::IntegerVariable; /// A propagator constructor creates a fully initialized instance of a [`Propagator`]. /// -/// The constructor is responsible for indicating on which events the propagator should be -/// enqueued. Additionally, the propagator can be initialized with values that come from the state -/// of the solver. -pub(crate) trait PropagatorConstructor { +/// The constructor is responsible for: +/// 1) Indicating on which [`DomainEvent`]s the propagator should be enqueued (via the +/// [`PropagatorConstructorContext`]). +/// 2) Initialising the [`PropagatorConstructor::PropagatorImpl`] and its structures. +pub trait PropagatorConstructor { /// The propagator that is produced by this constructor. type PropagatorImpl: Propagator + Clone; @@ -37,7 +46,7 @@ pub(crate) trait PropagatorConstructor { /// Propagators use the [`PropagatorConstructorContext`] to register to domain changes /// of variables and to retrieve the current bounds of variables. #[derive(Debug)] -pub(crate) struct PropagatorConstructorContext<'a> { +pub struct PropagatorConstructorContext<'a> { state: &'a mut State, pub(crate) propagator_id: PropagatorId, @@ -59,10 +68,9 @@ impl PropagatorConstructorContext<'_> { } } - pub(crate) fn as_readonly(&self) -> PropagationContext<'_> { - PropagationContext { - assignments: &self.state.assignments, - } + /// Get domain information. + pub fn domains(&mut self) -> Domains<'_> { + Domains::new(&self.state.assignments, &mut self.state.trailed_values) } /// Subscribes the propagator to the given [`DomainEvents`]. @@ -73,10 +81,7 @@ impl PropagatorConstructorContext<'_> { /// /// Each variable *must* have a unique [`LocalId`]. Most often this would be its index of the /// variable in the internal array of variables. - /// - /// Note that the [`LocalId`] is used to differentiate between [`DomainId`]s and - /// [`AffineView`]s. - pub(crate) fn register( + pub fn register( &mut self, var: impl IntegerVariable, domain_events: DomainEvents, @@ -90,13 +95,12 @@ impl PropagatorConstructorContext<'_> { self.update_next_local_id(local_id); let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); - var.watch_all(&mut watchers, domain_events.get_int_events()); + var.watch_all(&mut watchers, domain_events.events()); } /// Register the propagator to be enqueued when the given [`Predicate`] becomes true. /// Returns the [`PredicateId`] used by the solver to track the predicate. - #[allow(unused, reason = "will become public API")] - pub(crate) fn register_predicate(&mut self, predicate: Predicate) -> PredicateId { + pub fn register_predicate(&mut self, predicate: Predicate) -> PredicateId { self.state.notification_engine.watch_predicate( predicate, self.propagator_id, @@ -118,7 +122,7 @@ impl PropagatorConstructorContext<'_> { /// /// Note that the [`LocalId`] is used to differentiate between [`DomainId`]s and /// [`AffineView`]s. - pub(crate) fn register_for_backtrack_events( + pub fn register_backtrack( &mut self, var: Var, domain_events: DomainEvents, @@ -132,7 +136,7 @@ impl PropagatorConstructorContext<'_> { self.update_next_local_id(local_id); let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); - var.watch_all_backtrack(&mut watchers, domain_events.get_int_events()); + var.watch_all_backtrack(&mut watchers, domain_events.events()); } /// Create a new [`InferenceCode`]. These codes are required to identify specific propagations @@ -207,16 +211,13 @@ impl DerefMut for RefOrOwned<'_, T> { mod private { use super::*; - use crate::engine::propagation::contexts::HasAssignments; - use crate::engine::propagation::contexts::HasTrailedValues; + use crate::propagation::HasAssignments; impl HasAssignments for PropagatorConstructorContext<'_> { fn assignments(&self) -> &Assignments { &self.state.assignments } - } - impl HasTrailedValues for PropagatorConstructorContext<'_> { fn trailed_values(&self) -> &TrailedValues { &self.state.trailed_values } diff --git a/pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs b/pumpkin-crates/core/src/propagation/contexts/explanation_context.rs similarity index 81% rename from pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs rename to pumpkin-crates/core/src/propagation/contexts/explanation_context.rs index 030483f6b..e69fb5409 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/explanation_context.rs @@ -1,17 +1,21 @@ use std::sync::LazyLock; -use super::HasAssignments; use crate::basic_types::PredicateId; use crate::basic_types::PredicateIdGenerator; use crate::containers::KeyValueHeap; use crate::engine::Assignments; +use crate::engine::TrailedValues; use crate::engine::notifications::NotificationEngine; use crate::predicates::Predicate; +use crate::propagation::HasAssignments; +#[cfg(doc)] +use crate::propagation::Propagator; /// The context that is available when lazily explaining propagations. /// -/// See [`pumpkin_solver::engine::propagation::Propagator`] for more information. -pub(crate) struct ExplanationContext<'a> { +/// See [`Propagator`] for more information. +#[derive(Debug)] +pub struct ExplanationContext<'a> { assignments: &'a Assignments, pub(crate) notification_engine: &'a mut NotificationEngine, current_nogood: CurrentNogood<'a>, @@ -46,10 +50,6 @@ impl<'a> ExplanationContext<'a> { } } - pub(crate) fn get_predicate(&mut self, predicate_id: PredicateId) -> Predicate { - self.notification_engine.get_predicate(predicate_id) - } - pub(crate) fn without_working_nogood( assignments: &'a Assignments, trail_position: usize, @@ -63,13 +63,16 @@ impl<'a> ExplanationContext<'a> { } } + pub fn get_predicate(&mut self, predicate_id: PredicateId) -> Predicate { + self.notification_engine.get_predicate(predicate_id) + } + /// Get the current working nogood. /// /// The working nogood does not necessarily contain the predicate that is being explained. /// However, the explanation will be used to either resolve with the working nogood or minimize /// it some other way. - #[allow(unused, reason = "it will be part of the public API at some point")] - pub(crate) fn working_nogood(&self) -> impl Iterator + '_ { + pub fn working_nogood(&self) -> impl Iterator + '_ { self.current_nogood.iter() } @@ -77,7 +80,7 @@ impl<'a> ExplanationContext<'a> { /// /// For example, if the context is created for explaining a predicate `[x >= v]` at trail /// position i, then this method will return `i - 1` - pub(crate) fn get_trail_position(&self) -> usize { + pub fn get_trail_position(&self) -> usize { self.trail_position - 1 } } @@ -86,6 +89,14 @@ impl HasAssignments for ExplanationContext<'_> { fn assignments(&self) -> &Assignments { self.assignments } + + fn trailed_values(&self) -> &TrailedValues { + unimplemented!("Currently, this information cannot be retrieved using this structure") + } + + fn trailed_values_mut(&mut self) -> &mut TrailedValues { + unimplemented!("Currently, this information cannot be retrieved using this structure") + } } static EMPTY_HEAP: KeyValueHeap = KeyValueHeap::new(); @@ -95,6 +106,9 @@ static EMPTY_PREDICATE_IDS: LazyLock = static EMPTY_PREDICATES: [Predicate; 0] = []; +/// The current nogood that is being analyzed. +/// +/// Can be used by propagators to guide how they explain their propagations. #[derive(Debug)] pub struct CurrentNogood<'a> { heap: &'a KeyValueHeap, diff --git a/pumpkin-crates/core/src/propagation/contexts/mod.rs b/pumpkin-crates/core/src/propagation/contexts/mod.rs new file mode 100644 index 000000000..5e365abd0 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/contexts/mod.rs @@ -0,0 +1,5 @@ +mod explanation_context; +mod propagation_context; + +pub use explanation_context::*; +pub use propagation_context::*; diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs new file mode 100644 index 000000000..dc9d6571a --- /dev/null +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -0,0 +1,239 @@ +use crate::basic_types::PredicateId; +use crate::engine::Assignments; +use crate::engine::EmptyDomain; +use crate::engine::EmptyDomainConflict; +use crate::engine::TrailedValues; +use crate::engine::notifications::NotificationEngine; +use crate::engine::notifications::PredicateIdAssignments; +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::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::HasAssignments; +#[cfg(doc)] +use crate::propagation::Propagator; +use crate::propagation::PropagatorId; +#[cfg(doc)] +use crate::propagation::ReadDomains; +use crate::pumpkin_assert_simple; + +/// Provided to the propagator when it is notified of a domain event. +/// +/// Domains can be read through the implementation of [`ReadDomains`]. +/// +/// The difference with [`PropagationContext`] is that it is not possible to perform a propagation +/// in the notify callback. +#[derive(Debug)] +pub struct NotificationContext<'a> { + pub(crate) trailed_values: &'a mut TrailedValues, + pub(crate) assignments: &'a Assignments, + pub(crate) predicate_id_assignments: &'a PredicateIdAssignments, +} + +impl<'a> NotificationContext<'a> { + pub(crate) fn new( + trailed_values: &'a mut TrailedValues, + assignments: &'a Assignments, + predicate_id_assignments: &'a PredicateIdAssignments, + ) -> Self { + Self { + trailed_values, + assignments, + predicate_id_assignments, + } + } + + /// Get the current domains. + pub fn domains(&mut self) -> Domains<'_> { + Domains::new(self.assignments, self.trailed_values) + } +} + +impl<'a> HasAssignments for NotificationContext<'a> { + fn assignments(&self) -> &Assignments { + self.assignments + } + + fn trailed_values(&self) -> &TrailedValues { + self.trailed_values + } + + fn trailed_values_mut(&mut self) -> &mut TrailedValues { + self.trailed_values + } +} + +/// Provides information about the state of the solver to a propagator. +/// +/// Domains can be read through the implementation of [`ReadDomains`], and changes to the state can +/// be made via [`Self::post`]. +#[derive(Debug)] +pub struct PropagationContext<'a> { + pub(crate) trailed_values: &'a mut TrailedValues, + pub(crate) assignments: &'a mut Assignments, + pub(crate) reason_store: &'a mut ReasonStore, + pub(crate) propagator_id: PropagatorId, + pub(crate) notification_engine: &'a mut NotificationEngine, + reification_literal: Option, +} + +impl<'a> HasAssignments for PropagationContext<'a> { + fn assignments(&self) -> &Assignments { + self.assignments + } + + fn trailed_values(&self) -> &TrailedValues { + self.trailed_values + } + + fn trailed_values_mut(&mut self) -> &mut TrailedValues { + self.trailed_values + } +} + +impl<'a> PropagationContext<'a> { + pub(crate) fn new( + trailed_values: &'a mut TrailedValues, + assignments: &'a mut Assignments, + reason_store: &'a mut ReasonStore, + notification_engine: &'a mut NotificationEngine, + propagator_id: PropagatorId, + ) -> Self { + PropagationContext { + trailed_values, + assignments, + reason_store, + propagator_id, + notification_engine, + reification_literal: None, + } + } + + /// Register the propagator to be enqueued when the provided [`Predicate`] becomes true. + /// + /// Returns the [`PredicateId`] assigned to the provided predicate, which will be provided + /// to [`Propagator::notify_predicate_id_satisfied`]. + pub fn register_predicate(&mut self, predicate: Predicate) -> PredicateId { + self.notification_engine.watch_predicate( + predicate, + self.propagator_id, + self.trailed_values, + self.assignments, + ) + } + + /// Get the [`Predicate`] for a given [`PredicateId`]. + pub fn get_predicate(&mut self, predicate_id: PredicateId) -> Predicate { + self.notification_engine.get_predicate(predicate_id) + } + + /// Get a [`PredicateId`] for the given [`Predicate`]. + /// + /// If no ID exists, one will be created. + pub fn get_id(&mut self, predicate: Predicate) -> PredicateId { + self.notification_engine.get_id(predicate) + } + + /// Apply a reification literal to all the explanations that are passed to the context. + pub(crate) fn with_reification(&mut self, reification_literal: Literal) { + pumpkin_assert_simple!( + self.reification_literal.is_none(), + "cannot reify an already reified propagation context" + ); + + self.reification_literal = Some(reification_literal); + } + + /// Get the current domain information. + pub fn domains(&mut self) -> Domains<'_> { + Domains::new(self.assignments, self.trailed_values) + } + + pub(crate) fn get_checkpoint(&self) -> usize { + self.assignments.get_checkpoint() + } + + /// Returns whether the [`Predicate`] corresponding to the provided [`PredicateId`] is + /// satisfied. + pub(crate) fn is_predicate_id_falsified(&mut self, predicate_id: PredicateId) -> bool { + self.notification_engine + .is_predicate_id_falsified(predicate_id, self.assignments) + } + + /// Returns whether the [`Predicate`] corresponding to the provided [`PredicateId`] is + /// satisfied. + pub(crate) fn is_predicate_id_satisfied(&mut self, predicate_id: PredicateId) -> bool { + self.notification_engine + .is_predicate_id_satisfied(predicate_id, self.assignments) + } + + /// Returns the number of [`PredicateId`]s. + pub(crate) fn num_predicate_ids(&self) -> usize { + self.notification_engine.num_predicate_ids() + } +} + +impl PropagationContext<'_> { + /// Assign the truth-value of the given [`Predicate`] to `true` in the current partial + /// assignment. + /// + /// If the truth-value is already `true`, then this is a no-op. Alternatively, if the + /// truth-value is `false`, then a conflict is triggered and the [`EmptyDomain`] error is + /// returned. At that point, no-more propagation should happen. + pub fn post( + &mut self, + predicate: Predicate, + reason: impl Into, + inference_code: InferenceCode, + ) -> Result<(), EmptyDomainConflict> { + let slot = self.reason_store.new_slot(); + + let modification_result = self.assignments.post_predicate( + predicate, + Some((slot.reason_ref(), inference_code)), + self.notification_engine, + ); + + match modification_result { + Ok(false) => Ok(()), + Ok(true) => { + let _ = slot.populate( + self.propagator_id, + build_reason(reason, self.reification_literal), + ); + Ok(()) + } + Err(EmptyDomain) => { + let _ = slot.populate( + self.propagator_id, + build_reason(reason, self.reification_literal), + ); + let (trigger_predicate, trigger_reason, trigger_inference_code) = + self.assignments.remove_last_trail_element(); + + Err(EmptyDomainConflict { + trigger_predicate, + trigger_reason, + trigger_inference_code, + }) + } + } + } +} + +fn build_reason(reason: impl Into, reification_literal: Option) -> StoredReason { + match reason.into() { + Reason::Eager(mut conjunction) => { + conjunction.extend( + reification_literal + .iter() + .map(|lit| lit.get_true_predicate()), + ); + StoredReason::Eager(conjunction) + } + Reason::DynamicLazy(code) => StoredReason::DynamicLazy(code), + } +} diff --git a/pumpkin-crates/core/src/propagation/domains.rs b/pumpkin-crates/core/src/propagation/domains.rs new file mode 100644 index 000000000..1f67c341d --- /dev/null +++ b/pumpkin-crates/core/src/propagation/domains.rs @@ -0,0 +1,225 @@ +use crate::engine::Assignments; +use crate::engine::TrailedInteger; +use crate::engine::TrailedValues; +use crate::predicates::Predicate; +#[cfg(doc)] +use crate::propagation::ExplanationContext; +use crate::variables::IntegerVariable; +use crate::variables::Literal; + +/// Provides access to domain information to propagators. +/// +/// Implements [`ReadDomains`] to expose information about the current variable domains such as the +/// lower-bound of a particular variable. +#[derive(Debug)] +pub struct Domains<'a> { + pub(crate) assignments: &'a Assignments, + trailed_values: &'a mut TrailedValues, +} + +impl<'a> Domains<'a> { + pub(crate) fn new(assignments: &'a Assignments, trailed_values: &'a mut TrailedValues) -> Self { + Domains { + assignments, + trailed_values, + } + } + + pub fn reborrow(&mut self) -> Domains<'_> { + Domains::new(self.assignments, self.trailed_values) + } +} + +/// A helper-trait for implementing [`ReadDomains`], which exposes the assignment. +pub(crate) trait HasAssignments { + fn assignments(&self) -> &Assignments; + fn trailed_values(&self) -> &TrailedValues; + fn trailed_values_mut(&mut self) -> &mut TrailedValues; +} + +impl HasAssignments for Domains<'_> { + fn assignments(&self) -> &Assignments { + self.assignments + } + + fn trailed_values(&self) -> &TrailedValues { + self.trailed_values + } + + fn trailed_values_mut(&mut self) -> &mut TrailedValues { + self.trailed_values + } +} + +/// A trait defining functions for retrieving information about the current domains. +pub trait ReadDomains { + /// Returns whether the provided [`Predicate`] is assigned (either true or false) or is + /// 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, + var: &Var, + ) -> impl Iterator; + + /// Returns all of the holes (currently) in the domain of `var` (including ones which were + /// created at previous decision levels). + fn get_holes(&self, var: &Var) -> impl Iterator; + + /// Returns `true` if the domain of the given variable is singleton (i.e., the variable is + /// fixed). + fn is_fixed(&self, var: &Var) -> bool; + + /// Returns the lowest value in the domain of `var`. + fn lower_bound(&self, var: &Var) -> i32; + + /// Returns the lowest value in the domain of `var` at the given `trail_position`. + /// + /// The trail position can be retrieved when generating lazy explanations using + /// [`ExplanationContext::get_trail_position`]. + fn lower_bound_at_trail_position( + &self, + var: &Var, + trail_position: usize, + ) -> i32; + + /// Returns the highest value in the domain of `var`. + fn upper_bound(&self, var: &Var) -> i32; + + /// Returns the highest value in the domain of `var` at the given `trail_position`. + /// + /// The trail position can be retrieved when generating lazy explanations using + /// [`ExplanationContext::get_trail_position`]. + fn upper_bound_at_trail_position( + &self, + var: &Var, + trail_position: usize, + ) -> i32; + + /// Returns whether the provided `value` is in the domain of `var`. + fn contains(&self, var: &Var, value: i32) -> bool; + + /// Returns whether the provided `value` is in the domain of `var` at the given + /// `trail_position`. + /// + /// The trail position can be retrieved when generating lazy explanations using + /// [`ExplanationContext::get_trail_position`]. + fn contains_at_trail_position( + &self, + var: &Var, + value: i32, + trail_position: usize, + ) -> bool; + + /// Returns an [`Iterator`] over the values in the domain of the provided `var` (including the + /// lower-bound and upper-bound values). + fn iterate_domain(&self, var: &Var) -> impl Iterator; + + /// Returns whether the provided [`Predicate`] was posted as a decision (i.e., it was posted as + /// a [`Predicate`] without a reason). + fn is_decision_predicate(&self, predicate: Predicate) -> bool; + + /// If the provided [`Predicate`] is true, then this method returns the checkpoint at which it + /// first become true; otherwise, it returns [`None`]. + fn get_checkpoint_for_predicate(&self, predicate: Predicate) -> Option; + + /// Returns the current value of the provided [`TrailedInteger`]. + fn read_trailed_integer(&self, trailed_integer: TrailedInteger) -> i64; + + /// Creates a new [`TrailedInteger`] assigned to the provided `initial_value`. + fn new_trailed_integer(&mut self, initial_value: i64) -> TrailedInteger; + + /// Assigns the provided [`TrailedInteger`] to the provided `value`. + fn write_trailed_integer(&mut self, trailed_integer: TrailedInteger, value: i64); +} + +impl ReadDomains for T { + fn evaluate_predicate(&self, predicate: Predicate) -> Option { + 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, + ) -> impl Iterator { + var.get_holes_at_current_checkpoint(self.assignments()) + } + + fn get_holes(&self, var: &Var) -> impl Iterator { + var.get_holes(self.assignments()) + } + + fn is_fixed(&self, var: &Var) -> bool { + self.lower_bound(var) == self.upper_bound(var) + } + + fn lower_bound(&self, var: &Var) -> i32 { + var.lower_bound(self.assignments()) + } + + fn lower_bound_at_trail_position( + &self, + var: &Var, + trail_position: usize, + ) -> i32 { + var.lower_bound_at_trail_position(self.assignments(), trail_position) + } + + fn upper_bound(&self, var: &Var) -> i32 { + var.upper_bound(self.assignments()) + } + + fn upper_bound_at_trail_position( + &self, + var: &Var, + trail_position: usize, + ) -> i32 { + var.upper_bound_at_trail_position(self.assignments(), trail_position) + } + + fn contains(&self, var: &Var, value: i32) -> bool { + var.contains(self.assignments(), value) + } + + fn contains_at_trail_position( + &self, + var: &Var, + value: i32, + trail_position: usize, + ) -> bool { + var.contains_at_trail_position(self.assignments(), value, trail_position) + } + + fn iterate_domain(&self, var: &Var) -> impl Iterator { + var.iterate_domain(self.assignments()) + } + + fn is_decision_predicate(&self, predicate: Predicate) -> bool { + self.assignments().is_decision_predicate(&predicate) + } + + fn get_checkpoint_for_predicate(&self, predicate: Predicate) -> Option { + self.assignments().get_checkpoint_for_predicate(&predicate) + } + + fn read_trailed_integer(&self, trailed_integer: TrailedInteger) -> i64 { + self.trailed_values().read(trailed_integer) + } + + fn new_trailed_integer(&mut self, initial_value: i64) -> TrailedInteger { + self.trailed_values_mut().grow(initial_value) + } + + fn write_trailed_integer(&mut self, trailed_integer: TrailedInteger, value: i64) { + self.trailed_values_mut().assign(trailed_integer, value); + } +} diff --git a/pumpkin-crates/core/src/engine/cp/propagation/local_id.rs b/pumpkin-crates/core/src/propagation/local_id.rs similarity index 84% rename from pumpkin-crates/core/src/engine/cp/propagation/local_id.rs rename to pumpkin-crates/core/src/propagation/local_id.rs index f343474fb..b3a3334df 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/local_id.rs +++ b/pumpkin-crates/core/src/propagation/local_id.rs @@ -3,14 +3,14 @@ use crate::containers::StorageKey; /// A local id uniquely identifies a variable within a specific propagator. A local id can be /// thought of as the index of the variable in the propagator. #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub(crate) struct LocalId(u32); +pub struct LocalId(u32); impl LocalId { - pub(crate) const fn from(value: u32) -> Self { + pub const fn from(value: u32) -> Self { LocalId(value) } - pub(crate) fn unpack(self) -> u32 { + pub fn unpack(self) -> u32 { self.0 } } diff --git a/pumpkin-crates/core/src/propagation/mod.rs b/pumpkin-crates/core/src/propagation/mod.rs new file mode 100644 index 000000000..68b3d6113 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/mod.rs @@ -0,0 +1,111 @@ +//! Contains the main building blocks for propagators. +//! +//! # Background +//! +//! A propagator takes as input a set of variables (xi ∈ X) and for each +//! variable a corresponding domain (Di ∈ D); it then removes values from +//! the domains of variables which are impossible under its reasoning. +//! Thus, it can be seen as a function which maps `D ↦ D'` such that +//! D'i ⊆ Di for all variables (i.e. the domain of a variable +//! either remains the same after applying the propagator or it becomes a subset of the domain +//! before applying the propagator). +//! +//! An example of a simple propagator is that of the binary not equals (`!=`) constraint: suppose +//! that we have two variables `x ∈ {0}` and `y ∈ {0, 1}` and the constraint `x != y`. The not equal +//! propagator will then take as input the variables `x` and `y` and their respective domains +//! D = {Dx = {0}, Dy = {0, 1}} and produce a new domain +//! D' = {D'x = {0}, D'y = {1}} for which we can see that +//! Dx = D'x and D'y ⊆ Dy. +//! +//! A propagator is said to be at fixed-point if Dx = D'x meaning +//! that no further propagations can take place when applying the propagator. A propagator is said +//! to be "idempotent" if a single call to it will result in it being at fix-point. +//! +//! For more information about the construction of these types of propagation-based solvers, we +//! refer to [\[1\]](https://dl.acm.org/doi/pdf/10.1145/1452044.1452046). +//! +//! # Practical +//! +//! Each concrete propagator is associated with one trait: [`Propagator`]. The main function to +//! implement for this trait is [`Propagator::propagate`], which performs the domain reduction. +//! +//! A propagator is created by a [`PropagatorConstructor`]. The constructor is responsible for +//! registering to [`DomainEvents`] (using [`PropagatorConstructorContext::register`]), and setting +//! up the state of the propagator. The constructor is provided a [`PropagatorConstructorContext`], +//! which has all the available functions allowing the propagator to hook into the solver state. +//! +//! We do not require propagators to be idempotent (see the previous section for a +//! definition) and it can be assumed that if a propagator is not at fix-point after propagating, +//! that it will be called again by the solver until no further propagations happen. +//! +//! See the [`propagators`] folder for concrete propagator implementations. +//! +//! # How to implement a new propagator? +//! +//! We recommend the following workflow: +//! 1. Implement a propagator struct that implements the [`Propagator`] trait. For now only +//! implement the required functions, i.e., [`Propagator::propagate_from_scratch`] and +//! [`Propagator::name`]. +//! 2. Create an implementation of the [`PropagatorConstructor`] trait, to register for domain +//! events and set up the propagator state. +//! 3. Following the procedure above gives an initial version of the propagator that is likely not +//! efficient, but has an important role for testing. Now is a good time to write tests using the +//! [`State`] API. **We strongly discourage skipping this step**. +//! 4. Implement [`Propagator::notify`] and/or [`Propagator::notify_predicate_id_satisfied`] to +//! control when the propagator is enqueued. Depending on the concrete propagator, this may only +//! make sense when done together with the next step. +//! 5. Implement the remaining hooks, i.e., [`Propagator::propagate`], and +//! [`Propagator::synchronise`] to exploit incrementality. These functions are all +//! interdependent. +//! 6. Decide on the priortiy of the propagator, i.e., implement [`Propagator::priority`]. +//! 7. Make sure to write new tests and run all tests throughout the process. +//! 8. The propagator implementation is now done! +//! +//! The propagator is added to the solver through [`Solver::add_propagator`]. +//! +//! # Bibliography +//! +//! \[1\] C. Schulte and P. J. Stuckey, ‘Efficient constraint propagation engines’, ACM Transactions +//! on Programming Languages and Systems (TOPLAS), vol. 31, no. 1, pp. 1–43, 2008. + +mod constructor; +mod contexts; +mod domains; +mod local_id; +mod propagator; + +pub(crate) mod propagator_id; +pub(crate) mod propagator_var_id; +pub(crate) mod store; + +mod reexports { + // Re-exports of types not in this module according to the file tree. + // These will probably be be moved at some point, but for now they are simply re-exported here + // to make the propagator API public. + pub use crate::basic_types::PredicateId; + pub use crate::engine::cp::TrailedInteger; + pub use crate::engine::notifications::DomainEvent; + pub use crate::engine::notifications::DomainEvents; + pub use crate::engine::notifications::OpaqueDomainEvent; +} +pub use constructor::*; +pub use contexts::*; +pub use domains::*; +pub use local_id::*; +pub use propagator::*; +pub use propagator_id::PropagatorId; +pub(crate) use propagator_var_id::PropagatorVarId; +pub use reexports::*; + +#[cfg(doc)] +use crate::Solver; +#[cfg(doc)] +use crate::engine::test_solver::TestSolver; +#[cfg(doc)] +use crate::engine::variables::IntegerVariable; +#[cfg(doc)] +use crate::propagators; +#[cfg(doc)] +use crate::propagators::linear_less_or_equal::LinearLessOrEqualPropagator; +#[cfg(doc)] +use crate::state::State; diff --git a/pumpkin-crates/core/src/propagation/propagator.rs b/pumpkin-crates/core/src/propagation/propagator.rs new file mode 100644 index 000000000..85f2ed389 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/propagator.rs @@ -0,0 +1,241 @@ +use downcast_rs::Downcast; +use downcast_rs::impl_downcast; +use dyn_clone::DynClone; +use dyn_clone::clone_trait_object; + +use super::Domains; +use super::ExplanationContext; +use super::PropagationContext; +use super::contexts::NotificationContext; +use crate::basic_types::PredicateId; +use crate::basic_types::PropagationStatusCP; +use crate::basic_types::PropagatorConflict; +#[cfg(doc)] +use crate::create_statistics_struct; +#[cfg(doc)] +use crate::engine::ConstraintSatisfactionSolver; +use crate::engine::notifications::OpaqueDomainEvent; +use crate::predicates::Predicate; +#[cfg(doc)] +use crate::propagation::DomainEvent; +#[cfg(doc)] +use crate::propagation::PropagatorConstructor; +#[cfg(doc)] +use crate::propagation::PropagatorConstructorContext; +#[cfg(doc)] +use crate::propagation::ReadDomains; +use crate::propagation::local_id::LocalId; +#[cfg(doc)] +use crate::pumpkin_asserts::PUMPKIN_ASSERT_ADVANCED; +#[cfg(doc)] +use crate::pumpkin_asserts::PUMPKIN_ASSERT_EXTREME; +#[cfg(doc)] +use crate::state::Conflict; +use crate::statistics::statistic_logger::StatisticLogger; + +// We need to use this to cast from `Box` to `NogoodPropagator`; rust inherently +// does not allow downcasting from the trait definition to its concrete type. +impl_downcast!(Propagator); + +// To allow the State object to be cloneable, we need to allow `Box` to be cloned. +clone_trait_object!(Propagator); + +/// A propagator removes values from domains which will never be in any solution, or raises +/// explicit conflicts. +/// +/// The only required functions are [`Propagator::name`], +/// and [`Propagator::propagate_from_scratch`]; all other +/// functions have default implementations. For initial development, the required functions are +/// enough, but a more mature implementation considers all functions in most cases. +/// +/// See the [`crate::propagation`] documentation for more details. +pub trait Propagator: Downcast + DynClone { + /// Return the name of the propagator. + /// + /// This is a convenience method that is used for printing. + fn name(&self) -> &str; + + /// Performs propagation from scratch (i.e., without relying on updating + /// internal data structures, as opposed to [`Propagator::propagate`]). + /// + /// The main aims of this method are to remove values from the domains of variables (using + /// [`PropagationContext::post`]) which cannot be part of any solution given the current + /// domains and to detect conflicts. + /// + /// In case no conflict has been detected this function should + /// return [`Result::Ok`], otherwise it should return a [`Result::Err`] with a [`Conflict`] + /// which contains the reason for the failure; either because a propagation caused an + /// an empty domain ([`Conflict::EmptyDomain`] as a result of [`PropagationContext::post`]) or + /// because the logic of the propagator found the current state to be inconsistent + /// ([`Conflict::Propagator`] ). + /// + /// It is usually best to implement this propagation method in the simplest + /// but correct way. When this crate is compiled with the `debug-checks` feature, this method + /// will be called to double check the reasons for failures and propagations that have been + /// reported by this propagator. + /// + /// Propagators are not required to propagate until a fixed point. It will be called again by + /// the solver until no further propagations happen. + fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP; + + /// Performs propagation with state (i.e., with being able to mutate internal data structures, + /// as opposed to [`Propagator::propagate_from_scratch`]). + /// + /// The main aims of this method are to remove values from the domains of variables (using + /// [`PropagationContext::post`]) which cannot be part of any solution given the current + /// domains and to detect conflicts. + /// + /// In case no conflict has been detected this function should + /// return [`Result::Ok`], otherwise it should return a [`Result::Err`] with a [`Conflict`] + /// which contains the reason for the failure; either because a propagation caused an + /// an empty domain ([`Conflict::EmptyDomain`] as a result of [`PropagationContext::post`]) or + /// because the logic of the propagator found the current state to be inconsistent + /// ([`Conflict::Propagator`] ). + /// + /// Propagators are not required to propagate until a fixed point. It will be called + /// again by the solver until no further propagations happen. + /// + /// By default, this function calls [`Propagator::propagate_from_scratch`]. + fn propagate(&mut self, context: PropagationContext) -> PropagationStatusCP { + self.propagate_from_scratch(context) + } + + /// Returns whether the propagator should be enqueued for propagation when a [`DomainEvent`] + /// happens to one of the variables the propagator is subscribed to (as registered during + /// creation with [`PropagatorConstructor`] using [`PropagatorConstructorContext::register`]). + /// + /// This can be used to incrementally maintain data structures or perform propagations, and + /// should only be used for computationally cheap logic. Expensive computation should be + /// performed in the [`Propagator::propagate`] method. + /// + /// By default the propagator is always enqueued for every event it is subscribed to. Not all + /// propagators will benefit from implementing this, so it is not required to do so. + fn notify( + &mut self, + _context: NotificationContext, + _local_id: LocalId, + _event: OpaqueDomainEvent, + ) -> EnqueueDecision { + EnqueueDecision::Enqueue + } + + /// This function is called when the effect of a [`DomainEvent`] is undone during backtracking + /// of one of the variables the propagator is subscribed to (as registered during creation with + /// [`PropagatorConstructor`] using [`PropagatorConstructorContext::register_backtrack`]). + /// + /// This can be used to incrementally maintain data structures or perform propagations, and + /// should only be used for computationally cheap logic. Expensive computation should be + /// performed in the [`Propagator::propagate`] method. + /// + /// *Note*: This method is only called for [`DomainEvent`]s for which [`Propagator::notify`] + /// was called. This means that if the propagator itself made a change, but was not notified of + /// it (e.g., due to a conflict being detected), then this method will also not be called for + /// that [`DomainEvent`]. + /// + /// By default the propagator does nothing when this method is called. Not all propagators will + /// benefit from implementing this, so it is not required to do so. + fn notify_backtrack( + &mut self, + _context: Domains, + _local_id: LocalId, + _event: OpaqueDomainEvent, + ) { + } + + /// Returns whether the propagator should be enqueued for propagation when a [`Predicate`] (with + /// corresponding [`PredicateId`]) which the propagator is subscribed to (as registered either + /// during using [`PropagationContext::register_predicate`] or during creation with + /// [`PropagatorConstructor`] using [`PropagatorConstructorContext::register_predicate`]). + /// + /// By default, the propagator will be enqueued. + fn notify_predicate_id_satisfied(&mut self, _predicate_id: PredicateId) -> EnqueueDecision { + EnqueueDecision::Enqueue + } + + /// Called after backtracking, allowing the propagator to + /// update its internal data structures given the new variable domains. + /// + /// By default this function does nothing. + fn synchronise(&mut self, _domains: Domains) {} + + /// Returns the [`Priority`] of the propagator, used for determining the order in which + /// propagators are called. + /// + /// See [`Priority`] documentation for more explanation. + /// + /// By default the priority is set to [`Priority::VeryLow`]. It is expected that + /// propagator implementations would set this value to some appropriate value. + fn priority(&self) -> Priority { + Priority::VeryLow + } + + /// A function which returns [`Some`] with a [`PropagatorConflict`] when this propagator can + /// detect an inconsistency (and [`None`] otherwise). + /// + /// By implementing this function, if the propagator is reified, it can propagate the + /// reification literal based on the detected inconsistency. Yet, an implementation is not + /// needed for correctness, as [`Propagator::propagate`] should still check for + /// inconsistency as well. + fn detect_inconsistency(&self, _domains: Domains) -> Option { + None + } + + /// Hook which is called when a propagated [`Predicate`] should be explained using a lazy + /// reason. + /// + /// The code which was attached to the propagation is given, as + /// well as a context object which defines what can be inspected from the solver to build the + /// explanation. + /// + /// *Note:* The context which is provided contains the _current_ state (i.e. the state when the + /// explanation is generated); the bounds at the time of the propagation can be retrieved using + /// methods such as [`ReadDomains::lower_bound_at_trail_position`] in combination + /// with [`ExplanationContext::get_trail_position`]. + fn lazy_explanation(&mut self, _code: u64, _context: ExplanationContext) -> &[Predicate] { + panic!( + "{}", + format!( + "Propagator {} does not support lazy explanations.", + self.name() + ) + ); + } + + /// Logs statistics of the propagator using the provided [`StatisticLogger`]. + /// + /// It is recommended to create a struct through the [`create_statistics_struct!`] macro! + fn log_statistics(&self, _statistic_logger: StatisticLogger) {} +} + +/// Indicator of what to do when a propagator is notified. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum EnqueueDecision { + /// The propagator should be enqueued. + Enqueue, + /// The propagator should not be enqueued. + Skip, +} + +/// The priority of a propagator, used for determining the order in which propagators will be +/// called. +/// +/// Propagators with high priority are propagated before propagators with low(er) priority. If two +/// propagators have the same priority, then the order in which they are propagated is unspecified. +/// +/// Typically, propagators with low computational complexity should be assigned a high +/// priority (i.e., should be propagated before computationally expensive propagators). +#[derive(Default, Debug, Clone, Copy, Hash, PartialEq, Eq)] +#[repr(u8)] +pub enum Priority { + High = 0, + Medium = 1, + Low = 2, + #[default] + VeryLow = 3, +} + +impl PartialOrd for Priority { + fn partial_cmp(&self, other: &Self) -> Option { + ((*self) as u8).partial_cmp(&((*other) as u8)) + } +} diff --git a/pumpkin-crates/core/src/engine/cp/propagation/propagator_id.rs b/pumpkin-crates/core/src/propagation/propagator_id.rs similarity index 100% rename from pumpkin-crates/core/src/engine/cp/propagation/propagator_id.rs rename to pumpkin-crates/core/src/propagation/propagator_id.rs diff --git a/pumpkin-crates/core/src/engine/cp/propagation/propagator_var_id.rs b/pumpkin-crates/core/src/propagation/propagator_var_id.rs similarity index 71% rename from pumpkin-crates/core/src/engine/cp/propagation/propagator_var_id.rs rename to pumpkin-crates/core/src/propagation/propagator_var_id.rs index d7dae9573..7d40d16e1 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/propagator_var_id.rs +++ b/pumpkin-crates/core/src/propagation/propagator_var_id.rs @@ -1,5 +1,5 @@ -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagatorId; +use crate::propagation::LocalId; +use crate::propagation::PropagatorId; /// A handle to a variable registered to a propagator. #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)] diff --git a/pumpkin-crates/core/src/engine/cp/propagation/store.rs b/pumpkin-crates/core/src/propagation/store.rs similarity index 100% rename from pumpkin-crates/core/src/engine/cp/propagation/store.rs rename to pumpkin-crates/core/src/propagation/store.rs diff --git a/pumpkin-crates/core/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/core/src/propagators/arithmetic/absolute_value.rs index f4af6856f..f7cb232cf 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/absolute_value.rs @@ -1,17 +1,18 @@ use crate::basic_types::PropagationStatusCP; use crate::conjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::LocalId; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; declare_inference_label!(AbsoluteValue); @@ -65,18 +66,15 @@ where VA: IntegerVariable + 'static, VB: IntegerVariable + 'static, { - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { "IntAbs" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { // The bound of absolute may be tightened further during propagation, but it is at least // zero at the root. context.post( diff --git a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs index eb977d8d2..e2e1b867a 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs @@ -9,20 +9,9 @@ use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::containers::HashSet; use crate::declare_inference_label; -use crate::engine::DomainEvents; use crate::engine::EmptyDomainConflict; -use crate::engine::cp::propagation::ReadDomains; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::predicates::Predicate; @@ -30,6 +19,18 @@ use crate::predicates::PredicateConstructor; use crate::predicates::PredicateType; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::ExplanationContext; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_advanced; declare_inference_label!(BinaryEquals); @@ -116,7 +117,7 @@ where { fn post( &self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, variable: Variable, predicate_type: PredicateType, value: i32, @@ -152,15 +153,12 @@ where AVar: IntegerVariable + 'static, BVar: IntegerVariable + 'static, { - fn detect_inconsistency( - &self, - context: PropagationContextWithTrailedValues, - ) -> Option { - let a_lb = context.lower_bound(&self.a); - let a_ub = context.upper_bound(&self.a); + fn detect_inconsistency(&self, domains: Domains) -> Option { + let a_lb = domains.lower_bound(&self.a); + let a_ub = domains.upper_bound(&self.a); - let b_lb = context.lower_bound(&self.b); - let b_ub = context.upper_bound(&self.b); + let b_lb = domains.lower_bound(&self.b); + let b_ub = domains.upper_bound(&self.b); if a_ub < b_lb { // If `a` is fully before `b` then we report a conflict @@ -185,7 +183,7 @@ where fn notify( &mut self, - context: PropagationContextWithTrailedValues, + context: NotificationContext, local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { @@ -212,27 +210,27 @@ where EnqueueDecision::Enqueue } - fn synchronise(&mut self, _context: PropagationContext) { + fn synchronise(&mut self, _context: Domains) { // Recall that we need to ensure that the stored removed values could now be inaccurate self.has_backtracked = true; } - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { "BinaryEq" } - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { if self.first_propagation_loop { // If it is the first propagation loop then we do full propagation self.first_propagation_loop = false; - return self.debug_propagate_from_scratch(context); + return self.propagate_from_scratch(context); } - if let Some(conflict) = self.detect_inconsistency(context.as_trailed_readonly()) { + if let Some(conflict) = self.detect_inconsistency(context.domains()) { return Err(conflict.into()); } @@ -252,17 +250,19 @@ where // re-evaluate the values which have been removed if self.has_backtracked { self.has_backtracked = false; - self.a_removed_values - .retain(|element| context.is_predicate_satisfied(predicate!(self.a != *element))); - self.b_removed_values - .retain(|element| context.is_predicate_satisfied(predicate!(self.b != *element))); + self.a_removed_values.retain(|element| { + context.evaluate_predicate(predicate!(self.a != *element)) == Some(true) + }); + self.b_removed_values.retain(|element| { + context.evaluate_predicate(predicate!(self.b != *element)) == Some(true) + }); } // Then we remove all of the values which have been removed from `a` from `b` let mut a_removed_values = std::mem::take(&mut self.a_removed_values); for removed_value_a in a_removed_values.drain() { pumpkin_assert_advanced!( - context.is_predicate_satisfied(predicate!(self.a != removed_value_a)) + context.evaluate_predicate(predicate!(self.a != removed_value_a)) == Some(true) ); self.post( &mut context, @@ -277,7 +277,7 @@ where let mut b_removed_values = std::mem::take(&mut self.b_removed_values); for removed_value_b in b_removed_values.drain() { pumpkin_assert_advanced!( - context.is_predicate_satisfied(predicate!(self.b != removed_value_b)) + context.evaluate_predicate(predicate!(self.b != removed_value_b)) == Some(true) ); self.post( &mut context, @@ -314,10 +314,7 @@ where slice::from_ref(&self.reason) } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { let a_lb = context.lower_bound(&self.a); let a_ub = context.upper_bound(&self.a); @@ -390,8 +387,8 @@ struct BinaryEqualsPropagation { #[cfg(test)] mod tests { - use crate::engine::propagation::EnqueueDecision; use crate::engine::test_solver::TestSolver; + use crate::propagation::EnqueueDecision; use crate::propagators::binary::BinaryEqualsPropagatorArgs; #[test] diff --git a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs index ed28c28b8..43298ea1e 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -2,18 +2,19 @@ use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::Domains; +use crate::propagation::LocalId; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; declare_inference_label!(BinaryNotEquals); @@ -66,14 +67,11 @@ where AVar: IntegerVariable + 'static, BVar: IntegerVariable + 'static, { - fn detect_inconsistency( - &self, - context: PropagationContextWithTrailedValues, - ) -> Option { + fn detect_inconsistency(&self, domains: Domains) -> Option { // We first check whether they are both fixed - if context.is_fixed(&self.a) && context.is_fixed(&self.b) { - let lb_a = context.lower_bound(&self.a); - let lb_b = context.lower_bound(&self.b); + if domains.is_fixed(&self.a) && domains.is_fixed(&self.b) { + let lb_a = domains.lower_bound(&self.a); + let lb_b = domains.lower_bound(&self.b); // If they are, then we check whether they are assigned to the same value if lb_a == lb_b { @@ -90,16 +88,16 @@ where } } - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { "BinaryNotEq" } - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { - if let Some(conflict) = self.detect_inconsistency(context.as_trailed_readonly()) { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { + if let Some(conflict) = self.detect_inconsistency(context.domains()) { return Err(conflict.into()); } @@ -135,11 +133,8 @@ where Ok(()) } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { - if let Some(conflict) = self.detect_inconsistency(context.as_trailed_readonly()) { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { + if let Some(conflict) = self.detect_inconsistency(context.domains()) { return Err(conflict.into()); } @@ -175,8 +170,8 @@ where #[cfg(test)] mod tests { - use crate::engine::propagation::EnqueueDecision; use crate::engine::test_solver::TestSolver; + use crate::propagation::EnqueueDecision; use crate::propagators::binary::BinaryNotEqualsPropagatorArgs; #[test] diff --git a/pumpkin-crates/core/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/core/src/propagators/arithmetic/integer_division.rs index 33563381a..33e308e71 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/integer_division.rs @@ -1,17 +1,18 @@ use crate::basic_types::PropagationStatusCP; use crate::conjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::LocalId; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; /// The [`PropagatorConstructor`] for the [`DivisionPropagator`]. @@ -85,15 +86,15 @@ where VB: IntegerVariable, VC: IntegerVariable, { - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { "Division" } - fn debug_propagate_from_scratch(&self, context: PropagationContextMut) -> PropagationStatusCP { + fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP { perform_propagation( context, &self.numerator, @@ -105,7 +106,7 @@ where } fn perform_propagation( - mut context: PropagationContextMut, + mut context: PropagationContext, numerator: &VA, denominator: &VB, rhs: &VC, @@ -189,7 +190,7 @@ fn perform_propagation( - context: &mut PropagationContextMut, + context: &mut PropagationContext, numerator: &VA, denominator: &VB, rhs: &VC, @@ -279,7 +280,7 @@ fn propagate_positive_domains( - context: &mut PropagationContextMut, + context: &mut PropagationContext, numerator: &VA, denominator: &VB, rhs: &VC, @@ -325,7 +326,7 @@ fn propagate_upper_bounds( - context: &mut PropagationContextMut, + context: &mut PropagationContext, numerator: &VA, denominator: &VB, rhs: &VC, diff --git a/pumpkin-crates/core/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/core/src/propagators/arithmetic/integer_multiplication.rs index 199d8812f..1bacc65b7 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/integer_multiplication.rs @@ -2,17 +2,18 @@ use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::LocalId; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; declare_inference_label!(IntegerMultiplication); @@ -77,21 +78,21 @@ where VB: IntegerVariable, VC: IntegerVariable, { - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { "IntTimes" } - fn debug_propagate_from_scratch(&self, context: PropagationContextMut) -> PropagationStatusCP { + fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP { perform_propagation(context, &self.a, &self.b, &self.c, self.inference_code) } } fn perform_propagation( - mut context: PropagationContextMut, + mut context: PropagationContext, a: &VA, b: &VB, c: &VC, @@ -214,7 +215,7 @@ fn perform_propagation( - context: &mut PropagationContextMut, + context: &mut PropagationContext, a: &VA, b: &VB, c: &VC, diff --git a/pumpkin-crates/core/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/core/src/propagators/arithmetic/linear_less_or_equal.rs index 3ae22f673..5eefca4ee 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/linear_less_or_equal.rs @@ -2,25 +2,25 @@ use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::basic_types::PropositionalConjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; use crate::engine::TrailedInteger; -use crate::engine::cp::propagation::ReadDomains; use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::ManipulateTrailedValues; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::predicates::Predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::ExplanationContext; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; declare_inference_label!(LinearBounds); @@ -92,7 +92,7 @@ impl LinearLessOrEqualPropagator where Var: IntegerVariable, { - fn create_conflict(&self, context: PropagationContext) -> PropagatorConflict { + fn create_conflict(&self, context: Domains) -> PropagatorConflict { PropagatorConflict { conjunction: self .x @@ -108,12 +108,9 @@ impl Propagator for LinearLessOrEqualPropagator where Var: IntegerVariable, { - fn detect_inconsistency( - &self, - context: PropagationContextWithTrailedValues, - ) -> Option { - if (self.c as i64) < context.value(self.lower_bound_left_hand_side) { - Some(self.create_conflict(context.as_readonly())) + fn detect_inconsistency(&self, domains: Domains) -> Option { + if (self.c as i64) < domains.read_trailed_integer(self.lower_bound_left_hand_side) { + Some(self.create_conflict(domains)) } else { None } @@ -121,14 +118,14 @@ where fn notify( &mut self, - mut context: PropagationContextWithTrailedValues, + mut context: NotificationContext, local_id: LocalId, _event: OpaqueDomainEvent, ) -> EnqueueDecision { let index = local_id.unpack() as usize; let x_i = &self.x[index]; - let old_bound = context.value(self.current_bounds[index]); + let old_bound = context.read_trailed_integer(self.current_bounds[index]); let new_bound = context.lower_bound(x_i) as i64; pumpkin_assert_simple!( @@ -136,14 +133,17 @@ where "propagator should only be triggered when lower bounds are tightened, old_bound={old_bound}, new_bound={new_bound}" ); - context.add_assign(self.lower_bound_left_hand_side, new_bound - old_bound); - context.assign(self.current_bounds[index], new_bound); + context.write_trailed_integer( + self.lower_bound_left_hand_side, + context.read_trailed_integer(self.lower_bound_left_hand_side) + (new_bound - old_bound), + ); + context.write_trailed_integer(self.current_bounds[index], new_bound); EnqueueDecision::Enqueue } - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { @@ -170,32 +170,37 @@ where &self.reason_buffer } - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { - if let Some(conflict) = self.detect_inconsistency(context.as_trailed_readonly()) { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { + if let Some(conflict) = self.detect_inconsistency(context.domains()) { return Err(conflict.into()); } - let lower_bound_left_hand_side = - match TryInto::::try_into(context.value(self.lower_bound_left_hand_side)) { - Ok(bound) => bound, - Err(_) if context.value(self.lower_bound_left_hand_side).is_positive() => { - // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an - // overflow (hence the check that the lower-bound on the left-hand side is - // positive) - // - // This means that the lower-bounds of the current variables will always be - // higher than the right-hand side (with a maximum value of i32). We thus - // return a conflict - return Err(self.create_conflict(context.as_readonly()).into()); - } - Err(_) => { - // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an - // underflow - // - // This means that the constraint is always satisfied - return Ok(()); - } - }; + let lower_bound_left_hand_side = match TryInto::::try_into( + context.read_trailed_integer(self.lower_bound_left_hand_side), + ) { + Ok(bound) => bound, + Err(_) + if context + .read_trailed_integer(self.lower_bound_left_hand_side) + .is_positive() => + { + // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an + // overflow (hence the check that the lower-bound on the left-hand side is + // positive) + // + // This means that the lower-bounds of the current variables will always be + // higher than the right-hand side (with a maximum value of i32). We thus + // return a conflict + return Err(self.create_conflict(context.domains()).into()); + } + Err(_) => { + // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an + // underflow + // + // This means that the constraint is always satisfied + return Ok(()); + } + }; for (i, x_i) in self.x.iter().enumerate() { let bound = self.c - (lower_bound_left_hand_side - context.lower_bound(x_i)); @@ -208,10 +213,7 @@ where Ok(()) } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { let lower_bound_left_hand_side = self .x .iter() @@ -221,7 +223,11 @@ where let lower_bound_left_hand_side = match TryInto::::try_into(lower_bound_left_hand_side) { Ok(bound) => bound, - Err(_) if context.value(self.lower_bound_left_hand_side).is_positive() => { + Err(_) + if context + .read_trailed_integer(self.lower_bound_left_hand_side) + .is_positive() => + { // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an // overflow (hence the check that the lower-bound on the left-hand side is // positive) @@ -229,7 +235,7 @@ where // This means that the lower-bounds of the current variables will always be // higher than the right-hand side (with a maximum value of i32). We thus // return a conflict - return Err(self.create_conflict(context.as_readonly()).into()); + return Err(self.create_conflict(context.domains()).into()); } Err(_) => { // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an diff --git a/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs index a63908f3c..9e3f26abb 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs @@ -6,22 +6,23 @@ use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::basic_types::PropositionalConjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; @@ -54,11 +55,9 @@ where for (i, x_i) in terms.iter().enumerate() { context.register(x_i.clone(), DomainEvents::ASSIGN, LocalId::from(i as u32)); - context.register_for_backtrack_events( + context.register_backtrack( x_i.clone(), - DomainEvents::create_with_int_events(enum_set!( - DomainEvent::Assign | DomainEvent::Removal - )), + DomainEvents::new(enum_set!(DomainEvent::Assign | DomainEvent::Removal)), LocalId::from(i as u32), ); } @@ -73,7 +72,7 @@ where inference_code: context.create_inference_code(constraint_tag, LinearNotEquals), }; - propagator.recalculate_fixed_variables(context.as_readonly()); + propagator.recalculate_fixed_variables(context.domains()); propagator } @@ -108,8 +107,8 @@ impl Propagator for LinearNotEqualPropagator where Var: IntegerVariable + 'static, { - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { @@ -118,7 +117,7 @@ where fn notify( &mut self, - context: PropagationContextWithTrailedValues, + context: NotificationContext, local_id: LocalId, _event: OpaqueDomainEvent, ) -> EnqueueDecision { @@ -145,12 +144,7 @@ where } } - fn notify_backtrack( - &mut self, - _context: PropagationContext, - local_id: LocalId, - event: OpaqueDomainEvent, - ) { + fn notify_backtrack(&mut self, _context: Domains, local_id: LocalId, event: OpaqueDomainEvent) { if matches!( self.terms[local_id.unpack() as usize].unpack_event(event), DomainEvent::Assign @@ -178,14 +172,14 @@ where } } - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { // If the left-hand side is out of date then we simply recalculate from scratch; we only do // this when we can propagate or check for a conflict if self.should_recalculate_lhs && self.number_of_fixed_terms >= self.terms.len() - 1 { - self.recalculate_fixed_variables(context.as_readonly()); + self.recalculate_fixed_variables(context.domains()); self.should_recalculate_lhs = false; } - pumpkin_assert_extreme!(self.is_propagator_state_consistent(context.as_readonly())); + pumpkin_assert_extreme!(self.is_propagator_state_consistent(context.domains())); // If there is only 1 unfixed variable, then we can propagate if self.number_of_fixed_terms == self.terms.len() - 1 { @@ -222,16 +216,13 @@ where } else if self.number_of_fixed_terms == self.terms.len() { pumpkin_assert_simple!(!self.should_recalculate_lhs); // Otherwise we check for a conflict - self.check_for_conflict(context.as_readonly())?; + self.check_for_conflict(context.domains())?; } Ok(()) } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { let num_fixed = self .terms .iter() @@ -304,7 +295,7 @@ impl LinearNotEqualPropagator { /// Note that this method always sets the `unfixed_variable_has_been_updated` to true; this /// might be too lenient as it could be the case that synchronisation does not lead to the /// re-adding of the removed value. - fn recalculate_fixed_variables(&mut self, context: PropagationContext) { + fn recalculate_fixed_variables(&mut self, context: Domains) { self.unfixed_variable_has_been_updated = false; (self.fixed_lhs, self.number_of_fixed_terms) = self.terms @@ -322,7 +313,7 @@ impl LinearNotEqualPropagator { } /// Determines whether a conflict has occurred and calculate the reason for the conflict - fn check_for_conflict(&self, context: PropagationContext) -> Result<(), PropagatorConflict> { + fn check_for_conflict(&self, context: Domains) -> Result<(), PropagatorConflict> { pumpkin_assert_simple!(!self.should_recalculate_lhs); if self.number_of_fixed_terms == self.terms.len() && self.fixed_lhs == self.rhs { let conjunction = self @@ -342,7 +333,7 @@ impl LinearNotEqualPropagator { /// Checks whether the number of fixed terms is equal to the number of fixed terms in the /// provided [`PropagationContext`] and whether the value of the fixed lhs is the same as in the /// provided [`PropagationContext`]. - fn is_propagator_state_consistent(&self, context: PropagationContext) -> bool { + fn is_propagator_state_consistent(&self, context: Domains) -> bool { let expected_number_of_fixed_terms = self .terms .iter() diff --git a/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs index 13c65efed..ad71bb01a 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs @@ -2,17 +2,18 @@ use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropositionalConjunction; use crate::conjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::LocalId; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; #[derive(Clone, Debug)] pub(crate) struct MaximumArgs { @@ -69,18 +70,15 @@ pub(crate) struct MaximumPropagator { impl Propagator for MaximumPropagator { - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn name(&self) -> &str { "Maximum" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { // This is the constraint that is being propagated: // max(a_0, a_1, ..., a_{n-1}) = rhs diff --git a/pumpkin-crates/core/src/propagators/cumulative/options.rs b/pumpkin-crates/core/src/propagators/cumulative/options.rs index 82c6a572c..1b7d4f2bc 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/options.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/options.rs @@ -1,4 +1,6 @@ use super::CumulativeExplanationType; +#[cfg(doc)] +use crate::constraints; #[derive(Debug, Default, Clone, Copy)] pub(crate) struct CumulativePropagatorOptions { @@ -15,6 +17,7 @@ pub(crate) struct CumulativePropagatorOptions { pub(crate) incremental_backtracking: bool, } +/// The options provided to the [`constraints::cumulative`] constraints. #[derive(Debug, Copy, Clone, Default)] pub struct CumulativeOptions { /// The propagation method which is used for the cumulative constraints; currently all of them @@ -45,6 +48,7 @@ impl CumulativeOptions { } } +/// The approach used for propagating the [`constraints::cumulative`] constraint. #[derive(Debug, Default, Clone, Copy)] #[cfg_attr(feature = "clap", derive(clap::ValueEnum))] pub enum CumulativePropagationMethod { diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs index 33b04df36..45b150cd0 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs @@ -1,11 +1,11 @@ use std::cmp::max; use std::rc::Rc; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::ReadDomains; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::variables::IntegerVariable; @@ -62,7 +62,7 @@ where pub(crate) fn create_big_step_predicate_propagating_task_upper_bound_propagation( task: &Rc>, profile: &ResourceProfile, - context: PropagationContext, + context: Domains, ) -> Predicate where Var: IntegerVariable + 'static, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs index 902beb439..cc96aae27 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs @@ -11,9 +11,9 @@ use naive::create_naive_predicate_propagating_task_upper_bound_propagation; use pointwise::create_pointwise_predicate_propagating_task_lower_bound_propagation; use pointwise::create_pointwise_predicate_propagating_task_upper_bound_propagation; -use crate::engine::propagation::PropagationContext; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; +use crate::propagation::Domains; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::variables::IntegerVariable; @@ -73,7 +73,7 @@ pub(crate) fn create_predicate_propagating_task_lower_bound_propagation< Var: IntegerVariable + 'static, >( explanation_type: CumulativeExplanationType, - context: PropagationContext, + context: Domains, task: &Rc>, profile: &ResourceProfile, time_point: Option, @@ -95,7 +95,7 @@ pub(crate) fn create_predicate_propagating_task_lower_bound_propagation< pub(crate) fn add_propagating_task_predicate_lower_bound( mut explanation: PropositionalConjunction, explanation_type: CumulativeExplanationType, - context: PropagationContext, + context: Domains, task: &Rc>, profile: &ResourceProfile, time_point: Option, @@ -115,7 +115,7 @@ pub(crate) fn create_predicate_propagating_task_upper_bound_propagation< Var: IntegerVariable + 'static, >( explanation_type: CumulativeExplanationType, - context: PropagationContext, + context: Domains, task: &Rc>, profile: &ResourceProfile, time_point: Option, @@ -139,7 +139,7 @@ pub(crate) fn create_predicate_propagating_task_upper_bound_propagation< pub(crate) fn add_propagating_task_predicate_upper_bound( mut explanation: PropositionalConjunction, explanation_type: CumulativeExplanationType, - context: PropagationContext, + context: Domains, task: &Rc>, profile: &ResourceProfile, time_point: Option, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs index 4c1f1270b..c92f6b2b0 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs @@ -1,10 +1,10 @@ use std::rc::Rc; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::ReadDomains; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::variables::IntegerVariable; @@ -13,7 +13,7 @@ use crate::variables::IntegerVariable; /// [`CumulativeExplanationType::Naive`]) pub(crate) fn create_naive_propagation_explanation( profile: &ResourceProfile, - context: PropagationContext, + context: Domains, ) -> PropositionalConjunction { profile .profile_tasks @@ -35,7 +35,7 @@ pub(crate) fn create_naive_propagation_explanation( +pub(crate) fn create_naive_conflict_explanation( conflict_profile: &ResourceProfile, context: Context, ) -> PropositionalConjunction @@ -61,7 +61,7 @@ where } pub(crate) fn create_naive_predicate_propagating_task_lower_bound_propagation( - context: PropagationContext, + context: Domains, task: &Rc>, ) -> Predicate where @@ -71,7 +71,7 @@ where } pub(crate) fn create_naive_predicate_propagating_task_upper_bound_propagation( - context: PropagationContext, + context: Domains, task: &Rc>, ) -> Predicate where diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs index 0b728c1bd..e6cf85914 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs @@ -2,13 +2,12 @@ use std::rc::Rc; use crate::constraint_arguments::CumulativeExplanationType; use crate::engine::EmptyDomainConflict; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::contexts::propagation_context::HasAssignments; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; use crate::proof::InferenceCode; +use crate::propagation::PropagationContext; +use crate::propagation::ReadDomains; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::propagators::cumulative::time_table::explanations::add_propagating_task_predicate_lower_bound; @@ -18,7 +17,7 @@ use crate::pumpkin_assert_simple; use crate::variables::IntegerVariable; pub(crate) fn propagate_lower_bounds_with_pointwise_explanations( - context: &mut PropagationContextMut, + context: &mut PropagationContext, profiles: &[&ResourceProfile], propagating_task: &Rc>, inference_code: InferenceCode, @@ -64,7 +63,7 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations( - context: &mut PropagationContextMut, + context: &mut PropagationContext, profiles: &[&ResourceProfile], propagating_task: &Rc>, inference_code: InferenceCode, @@ -173,7 +172,7 @@ pub(crate) fn propagate_upper_bounds_with_pointwise_explanations( - context: PropagationContext, + mut context: Domains, inference_code: InferenceCode, time_table: &OverIntervalTimeTableType, parameters: &CumulativeParameters, ) -> bool { - let time_table_scratch = - create_time_table_over_interval_from_scratch(context, parameters, inference_code) - .expect("Expected no error"); + let time_table_scratch = create_time_table_over_interval_from_scratch( + context.reborrow(), + parameters, + inference_code, + ) + .expect("Expected no error"); if time_table.is_empty() { return time_table_scratch.is_empty(); diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs index 1da409f59..2decdf04c 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs @@ -3,9 +3,9 @@ use std::rc::Rc; use super::debug::are_mergeable; use super::debug::merge_profiles; use crate::basic_types::PropagationStatusCP; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::ReadDomains; use crate::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; use crate::propagators::CumulativeParameters; use crate::propagators::OverIntervalTimeTableType; use crate::propagators::ResourceProfile; @@ -57,7 +57,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_over_interval< Var: IntegerVariable + 'static, >( synchronised_conflict_explanation: &PropagationStatusCP, - context: PropagationContext, + context: Domains, parameters: &CumulativeParameters, inference_code: InferenceCode, ) -> bool { @@ -81,7 +81,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_over_interval< /// been reported by [`TimeTableOverIntervalPropagator`] by finding the tasks which should be /// included in the profile and sorting them in the same order. pub(crate) fn create_synchronised_conflict_explanation( - context: PropagationContext, + mut context: Domains, inference_code: InferenceCode, conflicting_profile: &mut ResourceProfile, parameters: &CumulativeParameters, @@ -93,7 +93,7 @@ pub(crate) fn create_synchronised_conflict_explanation( time_table: &mut OverIntervalTimeTableType, - context: PropagationContext, + mut context: Domains, ) { if !time_table.is_empty() { // If the time-table is not empty then we merge all the profiles in the range @@ -138,14 +138,14 @@ pub(crate) fn synchronise_time_table( // And then we sort each profile according to upper-bound and then ID time_table .iter_mut() - .for_each(|profile| sort_profile_based_on_upper_bound_and_id(profile, context)) + .for_each(|profile| sort_profile_based_on_upper_bound_and_id(profile, context.reborrow())) } /// Sorts the provided `profile` on non-decreasing order of upper-bound while tie-breaking in /// non-decreasing order of ID fn sort_profile_based_on_upper_bound_and_id( profile: &mut ResourceProfile, - context: PropagationContext, + context: Domains, ) { profile.profile_tasks.sort_by(|a, b| { // First match on the upper-bound of the variable diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index 372708cd0..522c04179 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -9,14 +9,15 @@ use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::engine::notifications::OpaqueDomainEvent; use crate::engine::notifications::DomainEvent; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; +use crate::propagation::Priority; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::NotificationContext; +use crate::propagation::PropagatorConstructor; +use crate::propagation::EnqueueDecision; +use crate::propagation::LocalId; +use crate::propagation::Domains; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; use crate::engine::variables::IntegerVariable; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; @@ -33,7 +34,7 @@ use crate::propagators::cumulative::time_table::time_table_util::insert_update; use crate::propagators::cumulative::time_table::time_table_util::propagate_based_on_timetable; use crate::propagators::cumulative::time_table::time_table_util::should_enqueue; use crate::propagators::cumulative::time_table::TimeTable; -use crate::propagators::debug_propagate_from_scratch_time_table_interval; +use crate::propagators::propagate_from_scratch_time_table_interval; use crate::propagators::util::check_bounds_equal_at_propagation; use crate::propagators::util::create_tasks; use crate::propagators::util::register_tasks; @@ -117,7 +118,7 @@ impl PropagatorConstruc // First we store the bounds in the parameters self.updatable_structures - .reset_all_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); self.is_time_table_outdated = true; @@ -155,7 +156,7 @@ impl /// that all of the adjustments are applied even if a conflict is found. fn add_to_time_table( &mut self, - context: PropagationContext, + mut context: Domains, mandatory_part_adjustments: &MandatoryPartAdjustments, task: &Rc>, ) -> PropagationStatusCP { @@ -179,7 +180,7 @@ impl && conflict.is_none() { conflict = Some(Err(create_conflict_explanation( - context, + context.reborrow(), self.inference_code.unwrap(), &conflict_tasks, self.parameters.options.explanation_type, @@ -235,11 +236,11 @@ impl /// [`TimeTableOverIntervalIncrementalPropagator::is_time_table_outdated`] is true. /// /// An error is returned if an overflow of the resource occurs while updating the time-table. - fn update_time_table(&mut self, context: &mut PropagationContextMut) -> PropagationStatusCP { + fn update_time_table(&mut self, context: &mut PropagationContext) -> PropagationStatusCP { if self.is_time_table_outdated { // We create the time-table from scratch (and return an error if it overflows) self.time_table = create_time_table_over_interval_from_scratch( - context.as_readonly(), + context.domains(), &self.parameters, self.inference_code.unwrap(), )?; @@ -249,7 +250,7 @@ impl // And we clear all of the updates since they have now necessarily been processed self.updatable_structures - .reset_all_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); return Ok(()); } @@ -275,7 +276,7 @@ impl // Note that the inconsistency returned here does not necessarily hold since other // updates could remove from the profile let result = self.add_to_time_table( - context.as_readonly(), + context.domains(), &mandatory_part_adjustments, &updated_task, ); @@ -301,7 +302,7 @@ impl if let Some(mut conflicting_profile) = conflicting_profile { let synchronised_conflict_explanation = create_synchronised_conflict_explanation( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &mut conflicting_profile, &self.parameters, @@ -309,7 +310,7 @@ impl pumpkin_assert_extreme!( check_synchronisation_conflict_explanation_over_interval( &synchronised_conflict_explanation, - context.as_readonly(), + context.domains(), &self.parameters, self.inference_code.unwrap(), ), @@ -331,7 +332,7 @@ impl if let Some(conflicting_profile) = conflicting_profile { pumpkin_assert_extreme!( create_time_table_over_interval_from_scratch( - context.as_readonly(), + context.domains(), &self.parameters, self.inference_code.unwrap(), ) @@ -342,7 +343,7 @@ impl self.found_previous_conflict = true; return Err(create_conflict_explanation( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), conflicting_profile, self.parameters.options.explanation_type, @@ -358,7 +359,7 @@ impl // We have not found a conflict; we need to ensure that the time-tables are the same by // ensuring that the profiles are maximal and the profile tasks are sorted in the same // order - synchronise_time_table(&mut self.time_table, context.as_readonly()) + synchronise_time_table(&mut self.time_table, context.domains()) } // We check whether there are no non-conflicting profiles in the time-table if we do not @@ -375,10 +376,10 @@ impl impl Propagator for TimeTableOverIntervalIncrementalPropagator { - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { pumpkin_assert_advanced!( check_bounds_equal_at_propagation( - context.as_readonly(), + context.domains(), &self.parameters.tasks, self.updatable_structures.get_stored_bounds(), ), @@ -396,7 +397,7 @@ impl Propagator pumpkin_assert_extreme!( debug::time_tables_are_the_same_interval::( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &self.time_table, &self.parameters, @@ -419,7 +420,7 @@ impl Propagator fn notify( &mut self, - context: PropagationContextWithTrailedValues, + mut context: NotificationContext, local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { @@ -435,7 +436,7 @@ impl Propagator &self.parameters, &self.updatable_structures, &updated_task, - context.as_readonly(), + context.domains(), self.time_table.is_empty(), ); @@ -444,7 +445,7 @@ impl Propagator insert_update(&updated_task, &mut self.updatable_structures, result.update); update_bounds_task( - context.as_readonly(), + context.domains(), self.updatable_structures.get_stored_bounds_mut(), &updated_task, ); @@ -461,7 +462,7 @@ impl Propagator fn notify_backtrack( &mut self, - context: PropagationContext, + mut context: Domains, local_id: LocalId, event: OpaqueDomainEvent, ) { @@ -469,7 +470,11 @@ impl Propagator let updated_task = Rc::clone(&self.parameters.tasks[local_id.unpack() as usize]); - backtrack_update(context, &mut self.updatable_structures, &updated_task); + backtrack_update( + context.reborrow(), + &mut self.updatable_structures, + &updated_task, + ); update_bounds_task( context, @@ -486,7 +491,7 @@ impl Propagator } } - fn synchronise(&mut self, context: PropagationContext) { + fn synchronise(&mut self, context: Domains) { // We now recalculate the time-table from scratch if necessary and reset all of the bounds // *if* incremental backtracking is disabled if !self.parameters.options.incremental_backtracking { @@ -503,20 +508,17 @@ impl Propagator } } - fn priority(&self) -> u32 { - 3 + fn priority(&self) -> Priority { + Priority::VeryLow } fn name(&self) -> &str { "CumulativeTimeTableOverIntervalIncremental" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { // Use the same debug propagator from `TimeTableOverInterval` - debug_propagate_from_scratch_time_table_interval( + propagate_from_scratch_time_table_interval( &mut context, &self.parameters, &self.updatable_structures, @@ -626,9 +628,9 @@ fn find_overlapping_profile( mod tests { use crate::conjunction; use crate::engine::predicates::predicate::Predicate; - use crate::engine::propagation::EnqueueDecision; use crate::engine::test_solver::TestSolver; use crate::predicate; + use crate::propagation::EnqueueDecision; use crate::propagators::ArgTask; use crate::propagators::CumulativeExplanationType; use crate::propagators::CumulativePropagatorOptions; diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs index 048ef6533..c5a0fec47 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs @@ -1,8 +1,8 @@ use std::rc::Rc; use crate::basic_types::PropagationStatusCP; -use crate::engine::propagation::PropagationContext; use crate::proof::InferenceCode; +use crate::propagation::Domains; use crate::propagators::CumulativeParameters; use crate::propagators::PerPointTimeTableType; use crate::propagators::ResourceProfile; @@ -20,7 +20,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_per_point< Var: IntegerVariable + 'static, >( synchronised_conflict_explanation: &PropagationStatusCP, - context: PropagationContext, + context: Domains, inference_code: InferenceCode, parameters: &CumulativeParameters, ) -> bool { @@ -110,7 +110,7 @@ fn get_minimum_set_of_tasks_which_overflow_capacity<'a, Var: IntegerVariable + ' /// reported by [`TimeTablePerPointPropagator`] by finding the tasks which should be included in the /// profile and sorting them in the same order. pub(crate) fn create_synchronised_conflict_explanation( - context: PropagationContext, + context: Domains, inference_code: InferenceCode, conflicting_profile: &mut ResourceProfile, parameters: &CumulativeParameters, @@ -165,8 +165,8 @@ mod tests { use std::rc::Rc; use super::find_synchronised_conflict; - use crate::engine::propagation::LocalId; use crate::engine::test_solver::TestSolver; + use crate::propagation::LocalId; use crate::propagators::CumulativeParameters; use crate::propagators::CumulativePropagatorOptions; use crate::propagators::PerPointTimeTableType; diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index a98ae5839..b717db86f 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -8,17 +8,18 @@ use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; use crate::propagators::ArgTask; use crate::propagators::CumulativeParameters; use crate::propagators::CumulativePropagatorOptions; @@ -40,7 +41,7 @@ use crate::propagators::cumulative::time_table::time_table_util::backtrack_updat use crate::propagators::cumulative::time_table::time_table_util::insert_update; use crate::propagators::cumulative::time_table::time_table_util::propagate_based_on_timetable; use crate::propagators::cumulative::time_table::time_table_util::should_enqueue; -use crate::propagators::debug_propagate_from_scratch_time_table_point; +use crate::propagators::propagate_from_scratch_time_table_point; use crate::propagators::util::check_bounds_equal_at_propagation; use crate::propagators::util::create_tasks; use crate::propagators::util::register_tasks; @@ -106,7 +107,7 @@ impl Propagator fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { register_tasks(&self.parameters.tasks, context.reborrow(), true); self.updatable_structures - .reset_all_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); // Then we do normal propagation self.is_time_table_outdated = true; @@ -144,7 +145,7 @@ impl /// that all of the adjustments are applied even if a conflict is found. fn add_to_time_table( &mut self, - context: PropagationContext, + mut context: Domains, mandatory_part_adjustments: &MandatoryPartAdjustments, task: &Rc>, ) -> PropagationStatusCP { @@ -180,7 +181,7 @@ impl if current_profile.height > self.parameters.capacity && conflict.is_none() { // The newly introduced mandatory part(s) caused an overflow of the resource conflict = Some(Err(create_conflict_explanation( - context, + context.reborrow(), self.inference_code.unwrap(), current_profile, self.parameters.options.explanation_type, @@ -253,11 +254,11 @@ impl /// [`DynamicStructures::updated`]. /// /// An error is returned if an overflow of the resource occurs while updating the time-table. - fn update_time_table(&mut self, context: &mut PropagationContextMut) -> PropagationStatusCP { + fn update_time_table(&mut self, context: &mut PropagationContext) -> PropagationStatusCP { if self.is_time_table_outdated { // We create the time-table from scratch (and return an error if it overflows) self.time_table = create_time_table_per_point_from_scratch( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &self.parameters, )?; @@ -267,7 +268,7 @@ impl // And we clear all of the updates since they have now necessarily been processed self.updatable_structures - .reset_all_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); return Ok(()); } @@ -293,7 +294,7 @@ impl // Note that the inconsistency returned here does not necessarily hold since other // updates could remove from the profile let result = self.add_to_time_table( - context.as_readonly(), + context.domains(), &mandatory_part_adjustments, &updated_task, ); @@ -325,7 +326,7 @@ impl .expect("Expected to find a conflicting profile"); let synchronised_conflict_explanation = create_synchronised_conflict_explanation( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), conflicting_profile, &self.parameters, @@ -334,7 +335,7 @@ impl pumpkin_assert_extreme!( check_synchronisation_conflict_explanation_per_point( &synchronised_conflict_explanation, - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &self.parameters, ), @@ -360,7 +361,7 @@ impl if let Some(conflicting_profile) = conflicting_profile { pumpkin_assert_extreme!( create_time_table_per_point_from_scratch( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &self.parameters ) @@ -371,7 +372,7 @@ impl self.found_previous_conflict = true; return Err(create_conflict_explanation( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), conflicting_profile, self.parameters.options.explanation_type, @@ -404,10 +405,10 @@ impl impl Propagator for TimeTablePerPointIncrementalPropagator { - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { pumpkin_assert_advanced!( check_bounds_equal_at_propagation( - context.as_readonly(), + context.domains(), &self.parameters.tasks, self.updatable_structures.get_stored_bounds(), ), @@ -425,7 +426,7 @@ impl Propagator self.update_time_table(&mut context)?; pumpkin_assert_extreme!(debug::time_tables_are_the_same_point::( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &self.time_table, &self.parameters @@ -446,7 +447,7 @@ impl Propagator fn notify( &mut self, - context: PropagationContextWithTrailedValues, + mut context: NotificationContext, local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { @@ -462,7 +463,7 @@ impl Propagator &self.parameters, &self.updatable_structures, &updated_task, - context.as_readonly(), + context.domains(), self.time_table.is_empty(), ); @@ -471,7 +472,7 @@ impl Propagator insert_update(&updated_task, &mut self.updatable_structures, result.update); update_bounds_task( - context.as_readonly(), + context.domains(), self.updatable_structures.get_stored_bounds_mut(), &updated_task, ); @@ -488,13 +489,17 @@ impl Propagator fn notify_backtrack( &mut self, - context: PropagationContext, + mut context: Domains, local_id: LocalId, event: OpaqueDomainEvent, ) { let updated_task = Rc::clone(&self.parameters.tasks[local_id.unpack() as usize]); - backtrack_update(context, &mut self.updatable_structures, &updated_task); + backtrack_update( + context.reborrow(), + &mut self.updatable_structures, + &updated_task, + ); update_bounds_task( context, @@ -511,7 +516,7 @@ impl Propagator } } - fn synchronise(&mut self, context: PropagationContext) { + fn synchronise(&mut self, context: Domains) { // We now recalculate the time-table from scratch if necessary and reset all of the bounds // *if* incremental backtracking is disabled if !self.parameters.options.incremental_backtracking { @@ -528,20 +533,17 @@ impl Propagator } } - fn priority(&self) -> u32 { - 3 + fn priority(&self) -> Priority { + Priority::VeryLow } fn name(&self) -> &str { "CumulativeTimeTablePerPointIncremental" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { // Use the same debug propagator from `TimeTablePerPoint` - debug_propagate_from_scratch_time_table_point( + propagate_from_scratch_time_table_point( &mut context, self.inference_code.unwrap(), &self.parameters, @@ -553,8 +555,8 @@ impl Propagator /// Contains functions related to debugging mod debug { - use crate::engine::propagation::PropagationContext; use crate::proof::InferenceCode; + use crate::propagation::Domains; use crate::propagators::CumulativeParameters; use crate::propagators::PerPointTimeTableType; use crate::propagators::create_time_table_per_point_from_scratch; @@ -573,7 +575,7 @@ mod debug { Var: IntegerVariable + 'static, const SYNCHRONISE: bool, >( - context: PropagationContext, + context: Domains, inference_code: InferenceCode, time_table: &PerPointTimeTableType, parameters: &CumulativeParameters, @@ -623,10 +625,10 @@ mod debug { mod tests { use crate::conjunction; use crate::engine::predicates::predicate::Predicate; - use crate::engine::propagation::EnqueueDecision; use crate::engine::test_solver::TestSolver; use crate::predicate; use crate::predicates::PredicateConstructor; + use crate::propagation::EnqueueDecision; use crate::propagators::ArgTask; use crate::propagators::CumulativeExplanationType; use crate::propagators::CumulativePropagatorOptions; diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs index f378c2c29..882dc3b07 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs @@ -16,14 +16,14 @@ use super::explanations::pointwise::create_pointwise_conflict_explanation; use super::explanations::pointwise::create_pointwise_propagation_explanation; use crate::basic_types::PropagatorConflict; use crate::engine::EmptyDomainConflict; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::contexts::HasAssignments; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; use crate::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::HasAssignments; +use crate::propagation::PropagationContext; +use crate::propagation::ReadDomains; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::propagators::cumulative::time_table::explanations::pointwise; @@ -46,7 +46,7 @@ pub(crate) struct CumulativePropagationHandler { fn check_explanation( explained_predicate: Predicate, explanation: &PropositionalConjunction, - context: PropagationContext, + context: Domains, ) -> bool { let all_predicates_hold = explanation .iter() @@ -86,7 +86,7 @@ impl CumulativePropagationHandler { /// `profiles` anymore. pub(crate) fn propagate_chain_of_lower_bounds_with_explanations( &mut self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, profiles: &[&ResourceProfile], propagating_task: &Rc>, ) -> Result<(), EmptyDomainConflict> @@ -101,7 +101,7 @@ impl CumulativePropagationHandler { for profile in profiles { let explanation = match self.explanation_type { CumulativeExplanationType::Naive => { - create_naive_propagation_explanation(profile, context.as_readonly()) + create_naive_propagation_explanation(profile, context.domains()) } CumulativeExplanationType::BigStep => { create_big_step_propagation_explanation(profile) @@ -120,7 +120,7 @@ impl CumulativePropagationHandler { let full_explanation = add_propagating_task_predicate_lower_bound( full_explanation, self.explanation_type, - context.as_readonly(), + context.domains(), propagating_task, profiles[0], None, @@ -132,7 +132,7 @@ impl CumulativePropagationHandler { pumpkin_assert_extreme!(check_explanation( predicate, &full_explanation, - context.as_readonly() + context.domains() )); context.post(predicate, full_explanation, self.inference_code) } @@ -151,7 +151,7 @@ impl CumulativePropagationHandler { /// `profiles` anymore. pub(crate) fn propagate_chain_of_upper_bounds_with_explanations( &mut self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, profiles: &[&ResourceProfile], propagating_task: &Rc>, ) -> Result<(), EmptyDomainConflict> @@ -167,7 +167,7 @@ impl CumulativePropagationHandler { for profile in profiles { let explanation = match self.explanation_type { CumulativeExplanationType::Naive => { - create_naive_propagation_explanation(profile, context.as_readonly()) + create_naive_propagation_explanation(profile, context.domains()) } CumulativeExplanationType::BigStep => { create_big_step_propagation_explanation(profile) @@ -186,7 +186,7 @@ impl CumulativePropagationHandler { let full_explanation = add_propagating_task_predicate_upper_bound( full_explanation, self.explanation_type, - context.as_readonly(), + context.domains(), propagating_task, profiles[profiles.len() - 1], None, @@ -198,7 +198,7 @@ impl CumulativePropagationHandler { pumpkin_assert_extreme!(check_explanation( predicate, &full_explanation, - context.as_readonly() + context.domains() )); context.post(predicate, full_explanation, self.inference_code) } @@ -216,7 +216,7 @@ impl CumulativePropagationHandler { /// Propagates the lower-bound of the `propagating_task` to not conflict with `profile` anymore. pub(crate) fn propagate_lower_bound_with_explanations( &mut self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, profile: &ResourceProfile, propagating_task: &Rc>, ) -> Result<(), EmptyDomainConflict> @@ -237,7 +237,7 @@ impl CumulativePropagationHandler { let lower_bound_predicate_propagating_task = create_predicate_propagating_task_lower_bound_propagation( self.explanation_type, - context.as_readonly(), + context.domains(), propagating_task, profile, None, @@ -246,7 +246,7 @@ impl CumulativePropagationHandler { pumpkin_assert_extreme!(check_explanation( predicate, &explanation, - context.as_readonly() + context.domains() )); let mut reason = (*explanation).clone(); @@ -267,7 +267,7 @@ impl CumulativePropagationHandler { /// Propagates the upper-bound of the `propagating_task` to not conflict with `profile` anymore. pub(crate) fn propagate_upper_bound_with_explanations( &mut self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, profile: &ResourceProfile, propagating_task: &Rc>, ) -> Result<(), EmptyDomainConflict> @@ -289,7 +289,7 @@ impl CumulativePropagationHandler { let upper_bound_predicate_propagating_task = create_predicate_propagating_task_upper_bound_propagation( self.explanation_type, - context.as_readonly(), + context.domains(), propagating_task, profile, None, @@ -301,7 +301,7 @@ impl CumulativePropagationHandler { pumpkin_assert_extreme!(check_explanation( predicate, &explanation, - context.as_readonly() + context.domains() )); let mut reason = (*explanation).clone(); @@ -323,7 +323,7 @@ impl CumulativePropagationHandler { /// bounds of `propagating_task`. pub(crate) fn propagate_holes_in_domain( &mut self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, profile: &ResourceProfile, propagating_task: &Rc>, ) -> Result<(), EmptyDomainConflict> @@ -370,7 +370,7 @@ impl CumulativePropagationHandler { pumpkin_assert_extreme!(check_explanation( predicate, &explanation, - context.as_readonly() + context.domains() )); context.post(predicate, (*explanation).clone(), self.inference_code)?; } @@ -403,7 +403,7 @@ impl CumulativePropagationHandler { pumpkin_assert_extreme!(check_explanation( predicate, &explanation, - context.as_readonly() + context.domains() )); context.post(predicate, explanation, self.inference_code)?; } @@ -422,7 +422,7 @@ impl CumulativePropagationHandler { /// Either we get the stored stored profile explanation or we initialize it. fn get_stored_profile_explanation_or_init( &mut self, - context: &mut PropagationContextMut, + context: &mut PropagationContext, profile: &ResourceProfile, ) -> Rc where @@ -432,7 +432,7 @@ impl CumulativePropagationHandler { Rc::new( match self.explanation_type { CumulativeExplanationType::Naive => { - create_naive_propagation_explanation(profile, context.as_readonly()) + create_naive_propagation_explanation(profile, context.domains()) }, CumulativeExplanationType::BigStep => { create_big_step_propagation_explanation(profile) @@ -448,7 +448,7 @@ impl CumulativePropagationHandler { /// Creates an explanation of the conflict caused by `conflict_profile` based on the provided /// `explanation_type`. -pub(crate) fn create_conflict_explanation( +pub(crate) fn create_conflict_explanation( context: Context, inference_code: InferenceCode, conflict_profile: &ResourceProfile, @@ -486,17 +486,17 @@ pub(crate) mod test_propagation_handler { use crate::engine::Assignments; use crate::engine::TrailedValues; use crate::engine::notifications::NotificationEngine; - use crate::engine::propagation::ExplanationContext; - use crate::engine::propagation::LocalId; - use crate::engine::propagation::PropagationContext; - use crate::engine::propagation::PropagationContextMut; - use crate::engine::propagation::PropagatorId; - use crate::engine::propagation::store::PropagatorStore; use crate::engine::reason::ReasonStore; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; use crate::proof::InferenceCode; + use crate::propagation::Domains; + use crate::propagation::ExplanationContext; + use crate::propagation::LocalId; + use crate::propagation::PropagationContext; + use crate::propagation::PropagatorId; + use crate::propagation::store::PropagatorStore; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::variables::DomainId; @@ -548,7 +548,7 @@ pub(crate) mod test_propagation_handler { }; let reason = create_conflict_explanation( - PropagationContext::new(&self.assignments), + Domains::new(&self.assignments, &mut self.trailed_values), self.propagation_handler.inference_code, &profile, self.propagation_handler.explanation_type, @@ -589,7 +589,7 @@ pub(crate) mod test_propagation_handler { let result = self .propagation_handler .propagate_lower_bound_with_explanations( - &mut PropagationContextMut::new( + &mut PropagationContext::new( &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, @@ -653,7 +653,7 @@ pub(crate) mod test_propagation_handler { let result = self .propagation_handler .propagate_chain_of_lower_bounds_with_explanations( - &mut PropagationContextMut::new( + &mut PropagationContext::new( &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, @@ -703,7 +703,7 @@ pub(crate) mod test_propagation_handler { let result = self .propagation_handler .propagate_upper_bound_with_explanations( - &mut PropagationContextMut::new( + &mut PropagationContext::new( &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, @@ -767,7 +767,7 @@ pub(crate) mod test_propagation_handler { let result = self .propagation_handler .propagate_chain_of_upper_bounds_with_explanations( - &mut PropagationContextMut::new( + &mut PropagationContext::new( &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs index 7be88a250..3e25450f0 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -8,18 +8,19 @@ use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::propagators::ArgTask; use crate::propagators::CumulativeParameters; use crate::propagators::CumulativePropagatorOptions; @@ -107,7 +108,7 @@ impl PropagatorConstructor fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { self.updatable_structures - .initialise_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); register_tasks(&self.parameters.tasks, context.reborrow(), false); self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); @@ -117,7 +118,7 @@ impl PropagatorConstructor } impl Propagator for TimeTableOverIntervalPropagator { - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { if self.parameters.is_infeasible { return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), @@ -126,7 +127,7 @@ impl Propagator for TimeTableOverIntervalPropaga } let time_table = create_time_table_over_interval_from_scratch( - context.as_readonly(), + context.domains(), &self.parameters, self.inference_code.unwrap(), )?; @@ -142,14 +143,14 @@ impl Propagator for TimeTableOverIntervalPropaga ) } - fn synchronise(&mut self, context: PropagationContext) { + fn synchronise(&mut self, context: Domains) { self.updatable_structures .reset_all_bounds_and_remove_fixed(context, &self.parameters); } fn notify( &mut self, - context: PropagationContextWithTrailedValues, + mut context: NotificationContext, local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { @@ -163,12 +164,12 @@ impl Propagator for TimeTableOverIntervalPropaga &self.parameters, &self.updatable_structures, &updated_task, - context.as_readonly(), + context.domains(), self.is_time_table_empty, ); update_bounds_task( - context.as_readonly(), + context.domains(), self.updatable_structures.get_stored_bounds_mut(), &updated_task, ); @@ -183,19 +184,16 @@ impl Propagator for TimeTableOverIntervalPropaga result.decision } - fn priority(&self) -> u32 { - 3 + fn priority(&self) -> Priority { + Priority::VeryLow } fn name(&self) -> &str { "CumulativeTimeTableOverInterval" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { - debug_propagate_from_scratch_time_table_interval( + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { + propagate_from_scratch_time_table_interval( &mut context, &self.parameters, &self.updatable_structures, @@ -214,16 +212,13 @@ impl Propagator for TimeTableOverIntervalPropaga /// The result of this method is either the time-table of type /// [`OverIntervalTimeTableType`] or the tasks responsible for the /// conflict in the form of an [`PropagatorConflict`]. -pub(crate) fn create_time_table_over_interval_from_scratch< - Var: IntegerVariable + 'static, - Context: ReadDomains + Copy, ->( - context: Context, +pub(crate) fn create_time_table_over_interval_from_scratch( + mut context: Domains, parameters: &CumulativeParameters, inference_code: InferenceCode, ) -> Result, PropagatorConflict> { // First we create a list of all the events (i.e. start and ends of mandatory parts) - let events = create_events(context, parameters); + let events = create_events(context.reborrow(), parameters); // Then we create a time-table using these events create_time_table_from_events(events, context, inference_code, parameters) @@ -236,7 +231,7 @@ pub(crate) fn create_time_table_over_interval_from_scratch< /// is resolved by placing the events which signify the ends of mandatory parts first (if the /// tie is between events of the same type then the tie-breaking is done on the id in /// non-decreasing order). -fn create_events( +fn create_events( context: Context, parameters: &CumulativeParameters, ) -> Vec> { @@ -296,7 +291,7 @@ fn create_events( /// Creates a time-table based on the provided `events` (which are assumed to be sorted /// chronologically, with tie-breaking performed in such a way that the ends of mandatory parts /// are before the starts of mandatory parts). -fn create_time_table_from_events( +fn create_time_table_from_events( events: Vec>, context: Context, inference_code: InferenceCode, @@ -449,8 +444,8 @@ fn check_starting_new_profile_invariants( && current_profile_tasks.is_empty() } -pub(crate) fn debug_propagate_from_scratch_time_table_interval( - context: &mut PropagationContextMut, +pub(crate) fn propagate_from_scratch_time_table_interval( + context: &mut PropagationContext, parameters: &CumulativeParameters, updatable_structures: &UpdatableStructures, inference_code: InferenceCode, @@ -458,17 +453,19 @@ pub(crate) fn debug_propagate_from_scratch_time_table_interval PropagatorConstructor for TimeTablePerPoint fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { self.updatable_structures - .initialise_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); register_tasks(&self.parameters.tasks, context.reborrow(), false); self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); @@ -108,7 +109,7 @@ impl PropagatorConstructor for TimeTablePerPoint } impl Propagator for TimeTablePerPointPropagator { - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { if self.parameters.is_infeasible { return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), @@ -117,7 +118,7 @@ impl Propagator for TimeTablePerPointPropagator< } let time_table = create_time_table_per_point_from_scratch( - context.as_readonly(), + context.domains(), self.inference_code.unwrap(), &self.parameters, )?; @@ -133,14 +134,14 @@ impl Propagator for TimeTablePerPointPropagator< ) } - fn synchronise(&mut self, context: PropagationContext) { + fn synchronise(&mut self, context: Domains) { self.updatable_structures .reset_all_bounds_and_remove_fixed(context, &self.parameters) } fn notify( &mut self, - context: PropagationContextWithTrailedValues, + mut context: NotificationContext, local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { @@ -154,14 +155,14 @@ impl Propagator for TimeTablePerPointPropagator< &self.parameters, &self.updatable_structures, &updated_task, - context.as_readonly(), + context.domains(), self.is_time_table_empty, ); // Note that the non-incremental proapgator does not make use of `result.updated` since it // propagates from scratch anyways update_bounds_task( - context.as_readonly(), + context.domains(), self.updatable_structures.get_stored_bounds_mut(), &updated_task, ); @@ -176,19 +177,16 @@ impl Propagator for TimeTablePerPointPropagator< result.decision } - fn priority(&self) -> u32 { - 3 + fn priority(&self) -> Priority { + Priority::VeryLow } fn name(&self) -> &str { "CumulativeTimeTablePerPoint" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { - debug_propagate_from_scratch_time_table_point( + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { + propagate_from_scratch_time_table_point( &mut context, self.inference_code.unwrap(), &self.parameters, @@ -207,7 +205,7 @@ impl Propagator for TimeTablePerPointPropagator< /// conflict in the form of an [`PropagatorConflict`]. pub(crate) fn create_time_table_per_point_from_scratch< Var: IntegerVariable + 'static, - Context: ReadDomains + Copy, + Context: ReadDomains, >( context: Context, inference_code: InferenceCode, @@ -253,26 +251,25 @@ pub(crate) fn create_time_table_per_point_from_scratch< Ok(time_table) } -pub(crate) fn debug_propagate_from_scratch_time_table_point( - context: &mut PropagationContextMut, +pub(crate) fn propagate_from_scratch_time_table_point( + context: &mut PropagationContext, inference_code: InferenceCode, parameters: &CumulativeParameters, updatable_structures: &UpdatableStructures, ) -> PropagationStatusCP { // We first create a time-table per point and return an error if there was // an overflow of the resource capacity while building the time-table - let time_table = create_time_table_per_point_from_scratch( - context.as_readonly(), - inference_code, - parameters, - )?; + let time_table = + create_time_table_per_point_from_scratch(context.domains(), inference_code, parameters)?; // Then we check whether propagation can take place + let mut updatable_structures_clone = + updatable_structures.recreate_from_context(context.domains(), parameters); propagate_based_on_timetable( context, inference_code, time_table.values(), parameters, - &mut updatable_structures.recreate_from_context(context.as_readonly(), parameters), + &mut updatable_structures_clone, ) } @@ -280,9 +277,9 @@ pub(crate) fn debug_propagate_from_scratch_time_table_point( parameters: &CumulativeParameters, updatable_structures: &UpdatableStructures, updated_task: &Rc>, - context: PropagationContext, + mut context: Domains, empty_time_table: bool, ) -> ShouldEnqueueResult { pumpkin_assert_extreme!( @@ -70,7 +70,7 @@ pub(crate) fn should_enqueue( } // We check whether a mandatory part was extended/introduced - if has_mandatory_part(context, updated_task) { + if has_mandatory_part(context.reborrow(), updated_task) { result.update = Some(UpdatedTaskInfo { task: Rc::clone(updated_task), old_lower_bound, @@ -106,7 +106,7 @@ pub(crate) fn should_enqueue( } pub(crate) fn has_mandatory_part( - context: PropagationContext, + context: Domains, task: &Rc>, ) -> bool { context.upper_bound(&task.start_variable) @@ -116,7 +116,7 @@ pub(crate) fn has_mandatory_part( /// Checks whether a specific task (indicated by id) has a mandatory part which overlaps with the /// interval [start, end] pub(crate) fn has_mandatory_part_in_interval( - context: PropagationContext, + context: Domains, task: &Rc>, start: i32, end: i32, @@ -133,7 +133,7 @@ pub(crate) fn has_mandatory_part_in_interval( /// Checks whether the lower and upper bound of a task overlap with the provided interval pub(crate) fn task_has_overlap_with_interval( - context: PropagationContext, + context: Domains, task: &Rc>, start: i32, end: i32, @@ -200,7 +200,7 @@ fn debug_check_whether_profiles_are_maximal_and_sorted<'a, Var: IntegerVariable /// [`ResourceProfile`] is maximal (i.e. the [`ResourceProfile::start`] and [`ResourceProfile::end`] /// cannot be increased or decreased, respectively). pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( - context: &mut PropagationContextMut, + context: &mut PropagationContext, inference_code: InferenceCode, time_table: impl Iterator> + Clone, parameters: &CumulativeParameters, @@ -255,7 +255,7 @@ pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( /// This type of propagation is likely to be less beneficial for the explanation /// [`CumulativeExplanationType::Pointwise`]. fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( - context: &mut PropagationContextMut, + context: &mut PropagationContext, inference_code: InferenceCode, time_table: impl Iterator> + Clone, updatable_structures: &mut UpdatableStructures, @@ -307,7 +307,7 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( // We get the updates which are possible (i.e. a lower-bound update, an upper-bound // update or a hole in the domain) if lower_bound_can_be_propagated_by_profile( - context.as_readonly(), + context.domains(), &task, profile, parameters.capacity, @@ -320,7 +320,7 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( } } if upper_bound_can_be_propagated_by_profile( - context.as_readonly(), + context.domains(), &task, profile, parameters.capacity, @@ -333,12 +333,7 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( } } if parameters.options.allow_holes_in_domain - && can_be_updated_by_profile( - context.as_readonly(), - &task, - profile, - parameters.capacity, - ) + && can_be_updated_by_profile(context.domains(), &task, profile, parameters.capacity) { let result = propagation_handler.propagate_holes_in_domain(context, profile, &task); @@ -363,7 +358,7 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( /// Especially in the case of [`CumulativeExplanationType::Pointwise`] this is likely to be /// beneficial. fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( - context: &mut PropagationContextMut, + context: &mut PropagationContext, inference_code: InferenceCode, time_table: impl Iterator> + Clone, updatable_structures: &mut UpdatableStructures, @@ -424,12 +419,8 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( }); for profile in &time_table[lower_bound_index..upper_bound_index] { // Check whether this profile can cause an update - if can_be_updated_by_profile( - context.as_readonly(), - task, - profile, - parameters.capacity, - ) { + if can_be_updated_by_profile(context.domains(), task, profile, parameters.capacity) + { // If we allow the propagation of holes in the domain then we simply let the // propagation handler handle it propagation_handler.propagate_holes_in_domain(context, profile, task)?; @@ -446,7 +437,7 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( fn sweep_forward<'a, Var: IntegerVariable + 'static>( task: &Rc>, propagation_handler: &mut CumulativePropagationHandler, - context: &mut PropagationContextMut, + context: &mut PropagationContext, time_table: &[&'a ResourceProfile], parameters: &CumulativeParameters, profile_buffer: &mut Vec<&'a ResourceProfile>, @@ -471,7 +462,7 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( // We check whether a lower-bound propagation can be performed using this profile if lower_bound_can_be_propagated_by_profile( - context.as_readonly(), + context.domains(), task, profile, parameters.capacity, @@ -481,7 +472,7 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( find_profiles_which_propagate_lower_bound( profile_index, time_table, - context.as_readonly(), + context.domains(), task, parameters.capacity, profile_buffer, @@ -510,7 +501,7 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( fn sweep_backward<'a, Var: IntegerVariable + 'static>( task: &Rc>, propagation_handler: &mut CumulativePropagationHandler, - context: &mut PropagationContextMut, + context: &mut PropagationContext, time_table: &[&'a ResourceProfile], parameters: &CumulativeParameters, profile_buffer: &mut Vec<&'a ResourceProfile>, @@ -539,7 +530,7 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( // We check whether an upper-bound propagation can be performed using this profile if upper_bound_can_be_propagated_by_profile( - context.as_readonly(), + context.domains(), task, profile, parameters.capacity, @@ -549,7 +540,7 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( find_profiles_which_propagate_upper_bound( profile_index, time_table, - context.as_readonly(), + context.domains(), task, parameters.capacity, profile_buffer, @@ -585,7 +576,7 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( fn find_profiles_which_propagate_lower_bound<'a, Var: IntegerVariable + 'static>( profile_index: usize, time_table: &[&'a ResourceProfile], - context: PropagationContext, + mut context: Domains, task: &Rc>, capacity: i32, profile_buffer: &mut Vec<&'a ResourceProfile>, @@ -603,7 +594,12 @@ fn find_profiles_which_propagate_lower_bound<'a, Var: IntegerVariable + 'static> break; } - if overflows_capacity_and_is_not_part_of_profile(context, task, next_profile, capacity) { + if overflows_capacity_and_is_not_part_of_profile( + context.reborrow(), + task, + next_profile, + capacity, + ) { last_propagating_index = current_index; profile_buffer.push(time_table[current_index]) } @@ -618,7 +614,7 @@ fn find_profiles_which_propagate_lower_bound<'a, Var: IntegerVariable + 'static> fn find_profiles_which_propagate_upper_bound<'a, Var: IntegerVariable + 'static>( profile_index: usize, time_table: &[&'a ResourceProfile], - context: PropagationContext, + mut context: Domains, task: &Rc>, capacity: i32, profile_buffer: &mut Vec<&'a ResourceProfile>, @@ -638,8 +634,12 @@ fn find_profiles_which_propagate_upper_bound<'a, Var: IntegerVariable + 'static> break; } - if overflows_capacity_and_is_not_part_of_profile(context, task, previous_profile, capacity) - { + if overflows_capacity_and_is_not_part_of_profile( + context.reborrow(), + task, + previous_profile, + capacity, + ) { last_propagating = current_index; profile_buffer.push(time_table[current_index]); } @@ -663,12 +663,12 @@ fn find_profiles_which_propagate_upper_bound<'a, Var: IntegerVariable + 'static> /// Note: It is assumed that task.resource_usage + height > capacity (i.e. the task has the /// potential to overflow the capacity in combination with the profile) fn lower_bound_can_be_propagated_by_profile( - context: PropagationContext, + mut context: Domains, task: &Rc>, profile: &ResourceProfile, capacity: i32, ) -> bool { - can_be_updated_by_profile(context, task, profile, capacity) + can_be_updated_by_profile(context.reborrow(), task, profile, capacity) && (context.lower_bound(&task.start_variable) + task.processing_time) > profile.start && context.lower_bound(&task.start_variable) <= profile.end } @@ -680,12 +680,12 @@ fn lower_bound_can_be_propagated_by_profile( /// * ub(s) <= end, i.e. the latest start time is before the end of the [`ResourceProfile`] /// Note: It is assumed that the task is known to overflow the [`ResourceProfile`] fn upper_bound_can_be_propagated_by_profile( - context: PropagationContext, + mut context: Domains, task: &Rc>, profile: &ResourceProfile, capacity: i32, ) -> bool { - can_be_updated_by_profile(context, task, profile, capacity) + can_be_updated_by_profile(context.reborrow(), task, profile, capacity) && (context.upper_bound(&task.start_variable) + task.processing_time) > profile.start && context.upper_bound(&task.start_variable) <= profile.end } @@ -698,13 +698,13 @@ fn upper_bound_can_be_propagated_by_profile( /// If the first condition is true, the second false and the third true then this method returns /// true (otherwise it returns false) fn can_be_updated_by_profile( - context: PropagationContext, + mut context: Domains, task: &Rc>, profile: &ResourceProfile, capacity: i32, ) -> bool { - overflows_capacity_and_is_not_part_of_profile(context, task, profile, capacity) - && task_has_overlap_with_interval(context, task, profile.start, profile.end) + overflows_capacity_and_is_not_part_of_profile(context.reborrow(), task, profile, capacity) + && task_has_overlap_with_interval(context.reborrow(), task, profile.start, profile.end) } /// Returns whether the provided `task` passes the following checks: @@ -714,7 +714,7 @@ fn can_be_updated_by_profile( /// If the first condition is true, and the second false then this method returns /// true (otherwise it returns false) fn overflows_capacity_and_is_not_part_of_profile( - context: PropagationContext, + context: Domains, task: &Rc>, profile: &ResourceProfile, capacity: i32, @@ -735,7 +735,7 @@ pub(crate) fn insert_update( } pub(crate) fn backtrack_update( - context: PropagationContext, + context: Domains, updatable_structures: &mut UpdatableStructures, updated_task: &Rc>, ) { @@ -782,8 +782,9 @@ mod tests { use super::find_profiles_which_propagate_lower_bound; use crate::engine::Assignments; - use crate::engine::propagation::LocalId; - use crate::engine::propagation::PropagationContext; + use crate::engine::TrailedValues; + use crate::propagation::Domains; + use crate::propagation::LocalId; use crate::propagators::ResourceProfile; use crate::propagators::Task; use crate::propagators::cumulative::time_table::time_table_util::find_profiles_which_propagate_upper_bound; @@ -791,6 +792,7 @@ mod tests { #[test] fn test_finding_last_index_lower_bound() { let mut assignments = Assignments::default(); + let mut trailed_values = TrailedValues::default(); let x = assignments.grow(0, 10); let y = assignments.grow(5, 5); @@ -825,7 +827,7 @@ mod tests { find_profiles_which_propagate_lower_bound( 0, &time_table, - PropagationContext::new(&assignments), + Domains::new(&assignments, &mut trailed_values), &Rc::new(Task { start_variable: x, processing_time: 6, @@ -841,6 +843,7 @@ mod tests { #[test] fn test_finding_last_index_upper_bound() { let mut assignments = Assignments::default(); + let mut trailed_values = TrailedValues::default(); let x = assignments.grow(7, 7); let y = assignments.grow(5, 5); @@ -875,7 +878,7 @@ mod tests { find_profiles_which_propagate_upper_bound( 1, &time_table, - PropagationContext::new(&assignments), + Domains::new(&assignments, &mut trailed_values), &Rc::new(Task { start_variable: x, processing_time: 6, diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs index dff382659..ba87ef1d8 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs @@ -2,7 +2,7 @@ use std::fmt::Debug; use std::hash::Hash; use std::rc::Rc; -use crate::engine::propagation::LocalId; +use crate::propagation::LocalId; use crate::variables::IntegerVariable; /// Structure which stores the variables related to a task; for now, only the start times are diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs index 948cb9c93..404501128 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs @@ -4,8 +4,8 @@ use super::CumulativeParameters; use super::Task; use super::UpdatedTaskInfo; use crate::containers::SparseSet; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::ReadDomains; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_moderate; use crate::variables::IntegerVariable; @@ -107,7 +107,7 @@ impl UpdatableStructures { /// Removes the fixed tasks from the internal structure(s). pub(crate) fn remove_fixed( &mut self, - context: PropagationContext, + context: Domains, parameters: &CumulativeParameters, ) { for task in parameters.tasks.iter() { @@ -124,7 +124,7 @@ impl UpdatableStructures { /// tasks from the internal structure(s). pub(crate) fn reset_all_bounds_and_remove_fixed( &mut self, - context: PropagationContext, + context: Domains, parameters: &CumulativeParameters, ) { for task in parameters.tasks.iter() { @@ -174,7 +174,7 @@ impl UpdatableStructures { // Initialises all stored bounds to their current values and removes any tasks which are fixed pub(crate) fn initialise_bounds_and_remove_fixed( &mut self, - context: PropagationContext, + context: Domains, parameters: &CumulativeParameters, ) { for task in parameters.tasks.iter() { @@ -244,7 +244,7 @@ impl UpdatableStructures { /// Used for creating the dynamic structures from the provided context pub(crate) fn recreate_from_context( &self, - context: PropagationContext, + context: Domains, parameters: &CumulativeParameters, ) -> Self { let mut other = self.clone(); diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs index 98ee1bcee..b02e200c1 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs @@ -5,13 +5,13 @@ use std::rc::Rc; use enumset::enum_set; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; use crate::engine::notifications::DomainEvent; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::local_id::LocalId; use crate::engine::variables::IntegerVariable; +use crate::propagation::DomainEvents; +use crate::propagation::Domains; +use crate::propagation::LocalId; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::propagators::ArgTask; use crate::propagators::Task; @@ -56,15 +56,15 @@ pub(crate) fn register_tasks( tasks.iter().for_each(|task| { context.register( task.start_variable.clone(), - DomainEvents::create_with_int_events(enum_set!( + DomainEvents::new(enum_set!( DomainEvent::LowerBound | DomainEvent::UpperBound | DomainEvent::Assign )), task.id, ); if register_backtrack { - context.register_for_backtrack_events( + context.register_backtrack( task.start_variable.clone(), - DomainEvents::create_with_int_events(enum_set!( + DomainEvents::new(enum_set!( DomainEvent::LowerBound | DomainEvent::UpperBound | DomainEvent::Assign )), task.id, @@ -76,7 +76,7 @@ pub(crate) fn register_tasks( /// Updates the bounds of the provided [`Task`] to those stored in /// `context`. pub(crate) fn update_bounds_task( - context: PropagationContext, + context: Domains, bounds: &mut [(i32, i32)], task: &Rc>, ) { @@ -88,7 +88,7 @@ pub(crate) fn update_bounds_task( /// Determines whether the stored bounds are equal when propagation occurs pub(crate) fn check_bounds_equal_at_propagation( - context: PropagationContext, + context: Domains, tasks: &[Rc>], bounds: &[(i32, i32)], ) -> bool { diff --git a/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs index 3f535962b..567a9d9aa 100644 --- a/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs @@ -7,17 +7,17 @@ use super::theta_lambda_tree::ThetaLambdaTree; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::containers::StorageKey; -use crate::engine::DomainEvents; -use crate::engine::cp::propagation::ReadDomains; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::LocalId; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::propagators::disjunctive::DisjunctiveEdgeFinding; use crate::pumpkin_assert_simple; use crate::state::Conflict; @@ -111,7 +111,7 @@ impl Propagator for DisjunctivePropagator { "DisjunctiveStrict" } - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { edge_finding( &mut self.theta_lambda_tree, &mut context, @@ -121,10 +121,7 @@ impl Propagator for DisjunctivePropagator { ) } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { let mut sorted_tasks = self.sorted_tasks.clone(); let mut theta_lambda_tree = self.theta_lambda_tree.clone(); edge_finding( @@ -141,16 +138,16 @@ impl Propagator for DisjunctivePropagator { /// this implementation is based). fn edge_finding( theta_lambda_tree: &mut ThetaLambdaTree, - context: &mut PropagationContextMut, + context: &mut PropagationContext, tasks: &[DisjunctiveTask], sorted_tasks: &mut [DisjunctiveTask], inference_code: InferenceCode, ) -> PropagationStatusCP { // First we create our Theta-Lambda tree and add all of the tasks to Theta (Lambda is empty at // this point) - theta_lambda_tree.update(context.as_readonly()); + theta_lambda_tree.update(context.domains()); for task in tasks.iter() { - theta_lambda_tree.add_to_theta(task, context.as_readonly()); + theta_lambda_tree.add_to_theta(task, context.domains()); } // Then sort in non-increasing order of latest completion time (LCT) @@ -181,7 +178,7 @@ fn edge_finding( theta_lambda_tree.remove_from_theta(j); // And then add it to Lambda (i.e. we are checking whether we can find a task i in Lambda // such that the element in Theta would cause an overflow) - theta_lambda_tree.add_to_lambda(j, context.as_readonly()); + theta_lambda_tree.add_to_lambda(j, context.domains()); // Then we go to the next task which represents the latest completion time of the set Theta index += 1; @@ -242,7 +239,7 @@ fn edge_finding( /// Edge-Finding Propagator’. fn create_conflict_explanation( theta_lambda_tree: &mut ThetaLambdaTree, - context: &PropagationContextMut, + context: &PropagationContext, lct: i32, ) -> PropositionalConjunction { // We get the set of tasks currently in theta @@ -307,7 +304,7 @@ fn create_propagation_explanation<'a, Var: IntegerVariable>( original_tasks: &'a [DisjunctiveTask], propagated_task_id: LocalId, theta_lambda_tree: &mut ThetaLambdaTree, - context: &'a PropagationContextMut, + context: &'a PropagationContext, new_bound: i32, lct_j: i32, ) -> PropositionalConjunction { diff --git a/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_task.rs b/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_task.rs index 898b769c1..658d70c4e 100644 --- a/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_task.rs +++ b/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_task.rs @@ -1,7 +1,12 @@ use std::fmt::Debug; -use crate::engine::propagation::LocalId; +#[cfg(doc)] +use crate::constraints; +use crate::propagation::LocalId; +/// Defines the input of the [`constraints::disjunctive_strict`] constraint. +/// +/// Each task has a variable starting time and a constant processing time. #[derive(Debug, Clone)] pub struct ArgDisjunctiveTask { pub start_time: Var, diff --git a/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs b/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs index 7e9fd87fa..45e8631b6 100644 --- a/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs +++ b/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs @@ -3,9 +3,9 @@ use std::cmp::max; use super::disjunctive_task::DisjunctiveTask; use crate::containers::KeyedVec; use crate::containers::StorageKey; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::ReadDomains; +use crate::propagation::Domains; +use crate::propagation::LocalId; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; use crate::variables::IntegerVariable; @@ -112,7 +112,7 @@ impl ThetaLambdaTree { /// Update the theta-lambda tree based on the provided `context`. /// /// It resets theta and lambda to be the empty set. - pub(super) fn update(&mut self, context: PropagationContext) { + pub(super) fn update(&mut self, context: Domains) { // First we sort the tasks by lower-bound/earliest start time. self.sorted_tasks .sort_by_key(|task| context.lower_bound(&task.start_time)); @@ -228,7 +228,7 @@ impl ThetaLambdaTree { pub(super) fn add_to_lambda( &mut self, task: &DisjunctiveTask, - context: PropagationContext, + context: Domains, ) { // We need to find the leaf node index; note that there are |nodes| / 2 leaves let position = self.nodes.len() / 2 + self.mapping[task.id]; @@ -249,11 +249,7 @@ impl ThetaLambdaTree { } /// Add the provided task to Theta - pub(super) fn add_to_theta( - &mut self, - task: &DisjunctiveTask, - context: PropagationContext, - ) { + pub(super) fn add_to_theta(&mut self, task: &DisjunctiveTask, context: Domains) { // We need to find the leaf node index; note that there are |nodes| / 2 leaves let position = self.nodes.len() / 2 + self.mapping[task.id]; let ect = context.lower_bound(&task.start_time) + task.processing_time; @@ -379,9 +375,9 @@ impl ThetaLambdaTree { #[cfg(test)] mod tests { - use crate::engine::propagation::LocalId; - use crate::engine::propagation::PropagationContext; use crate::engine::test_solver::TestSolver; + use crate::propagation::Domains; + use crate::propagation::LocalId; use crate::propagators::disjunctive::theta_lambda_tree::Node; use crate::propagators::disjunctive::theta_lambda_tree::ThetaLambdaTree; use crate::propagators::disjunctive_task::DisjunctiveTask; @@ -418,16 +414,20 @@ mod tests { let mut tree = ThetaLambdaTree::new(&tasks); - tree.update(PropagationContext { - assignments: &solver.state.assignments, - }); + tree.update(Domains::new( + &solver.state.assignments, + &mut solver.state.trailed_values, + )); for task in tasks.iter() { - tree.add_to_theta(task, PropagationContext::new(&solver.state.assignments)); + tree.add_to_theta( + task, + Domains::new(&solver.state.assignments, &mut solver.state.trailed_values), + ); } tree.remove_from_theta(&tasks[2]); tree.add_to_lambda( &tasks[2], - PropagationContext::new(&solver.state.assignments), + Domains::new(&solver.state.assignments, &mut solver.state.trailed_values), ); assert_eq!( diff --git a/pumpkin-crates/core/src/propagators/disjunctive/theta_tree.rs b/pumpkin-crates/core/src/propagators/disjunctive/theta_tree.rs index 6fc0da72d..77c895117 100644 --- a/pumpkin-crates/core/src/propagators/disjunctive/theta_tree.rs +++ b/pumpkin-crates/core/src/propagators/disjunctive/theta_tree.rs @@ -3,9 +3,9 @@ use std::cmp::max; use super::disjunctive_task::DisjunctiveTask; use crate::containers::KeyedVec; use crate::containers::StorageKey; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::ReadDomains; +use crate::propagation::Domains; +use crate::propagation::LocalId; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; use crate::variables::IntegerVariable; @@ -57,7 +57,7 @@ pub(super) struct ThetaTree { impl ThetaTree { pub(super) fn new( tasks: &[DisjunctiveTask], - context: PropagationContext, + context: Domains, ) -> Self { // First we sort the tasks by lower-bound let mut sorted_tasks = tasks.to_vec(); @@ -97,7 +97,7 @@ impl ThetaTree { pub(super) fn add( &mut self, task: &DisjunctiveTask, - context: PropagationContext, + context: Domains, ) { // We need to find the leaf node index; note that there are |nodes| / 2 leaves let position = self.nodes.len() / 2 + self.mapping[task.id]; diff --git a/pumpkin-crates/core/src/propagators/element.rs b/pumpkin-crates/core/src/propagators/element.rs index f2c02c8fe..351a423ea 100644 --- a/pumpkin-crates/core/src/propagators/element.rs +++ b/pumpkin-crates/core/src/propagators/element.rs @@ -5,20 +5,21 @@ use bitfield_struct::bitfield; use crate::basic_types::PropagationStatusCP; use crate::conjunction; use crate::declare_inference_label; -use crate::engine::DomainEvents; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::reason::Reason; use crate::engine::variables::IntegerVariable; use crate::predicate; use crate::predicates::Predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::DomainEvents; +use crate::propagation::ExplanationContext; +use crate::propagation::LocalId; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; #[derive(Clone, Debug)] pub(crate) struct ElementArgs { @@ -95,18 +96,15 @@ where VI: IntegerVariable + 'static, VE: IntegerVariable + 'static, { - fn priority(&self) -> u32 { - 2 + fn priority(&self) -> Priority { + Priority::Low } fn name(&self) -> &str { "Element" } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { self.propagate_index_bounds_within_array(&mut context)?; self.propagate_rhs_bounds_based_on_array(&mut context)?; @@ -154,7 +152,7 @@ where /// Propagate the bounds of `self.index` to be in the range `[0, self.array.len())`. fn propagate_index_bounds_within_array( &self, - context: &mut PropagationContextMut<'_>, + context: &mut PropagationContext<'_>, ) -> PropagationStatusCP { context.post( predicate![self.index >= 0], @@ -173,7 +171,7 @@ where /// bound (res. maximum upper bound) of the elements. fn propagate_rhs_bounds_based_on_array( &self, - context: &mut PropagationContextMut<'_>, + context: &mut PropagationContext<'_>, ) -> PropagationStatusCP { let (rhs_lb, rhs_ub) = self .array @@ -215,7 +213,7 @@ where /// right-hand side, remove it from index. fn propagate_index_based_on_domain_intersection_with_rhs( &self, - context: &mut PropagationContextMut<'_>, + context: &mut PropagationContext<'_>, ) -> PropagationStatusCP { let rhs_lb = context.lower_bound(&self.rhs); let rhs_ub = context.upper_bound(&self.rhs); @@ -248,7 +246,7 @@ where /// tightened to the bounds of lhs, through a previous propagation rule. fn propagate_equality( &self, - context: &mut PropagationContextMut<'_>, + context: &mut PropagationContext<'_>, index: i32, ) -> PropagationStatusCP { let rhs_lb = context.lower_bound(&self.rhs); diff --git a/pumpkin-crates/core/src/propagators/mod.rs b/pumpkin-crates/core/src/propagators/mod.rs index 7c8c73093..c87277c4d 100644 --- a/pumpkin-crates/core/src/propagators/mod.rs +++ b/pumpkin-crates/core/src/propagators/mod.rs @@ -1,6 +1,8 @@ //! Contains propagator implementations that are used in Pumpkin. //! -//! See the [`crate::engine::cp::propagation`] for info on propagators. +//! See the [`propagation`] for info on propagators. +#[cfg(doc)] +use crate::propagation; pub(crate) mod arithmetic; mod cumulative; diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 47f79a310..7cfe1cfbb 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -18,19 +18,20 @@ use crate::engine::Lbd; use crate::engine::SolverStatistics; use crate::engine::notifications::NotificationEngine; use crate::engine::predicates::predicate::Predicate; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::HasAssignments; use crate::engine::reason::Reason; use crate::engine::reason::ReasonStore; use crate::predicate; use crate::proof::InferenceCode; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::ExplanationContext; +use crate::propagation::HasAssignments; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::propagators::nogoods::arena_allocator::ArenaAllocator; use crate::propagators::nogoods::arena_allocator::NogoodIndex; use crate::pumpkin_assert_advanced; @@ -199,8 +200,8 @@ impl Propagator for NogoodPropagator { "NogoodPropagator" } - fn priority(&self) -> u32 { - 0 + fn priority(&self) -> Priority { + Priority::High } fn notify_predicate_id_satisfied(&mut self, predicate_id: PredicateId) -> EnqueueDecision { @@ -208,7 +209,7 @@ impl Propagator for NogoodPropagator { EnqueueDecision::Enqueue } - fn propagate(&mut self, mut context: PropagationContextMut) -> Result<(), Conflict> { + fn propagate(&mut self, mut context: PropagationContext) -> Result<(), Conflict> { pumpkin_assert_advanced!(self.debug_is_properly_watched()); // First we perform nogood management to ensure that the database does not grow excessively @@ -229,7 +230,7 @@ impl Propagator for NogoodPropagator { pumpkin_assert_moderate!( { let predicate = context.get_predicate(predicate_id); - context.is_predicate_satisfied(predicate) + context.evaluate_predicate(predicate) == Some(true) }, "The predicate {} with id {predicate_id:?} should be satisfied but was not", context.get_predicate(predicate_id), @@ -301,7 +302,7 @@ impl Propagator for NogoodPropagator { // At this point, nonwatched predicates and nogood[1] are falsified. pumpkin_assert_advanced!(nogood_predicates.iter().skip(1).all(|p| { let predicate = context.get_predicate(*p); - context.is_predicate_satisfied(predicate) + context.evaluate_predicate(predicate) == Some(true) })); // There are two scenarios: @@ -329,14 +330,11 @@ impl Propagator for NogoodPropagator { Ok(()) } - fn synchronise(&mut self, _context: PropagationContext) { + fn synchronise(&mut self, _context: Domains) { self.updated_predicate_ids.clear() } - fn debug_propagate_from_scratch( - &self, - mut context: PropagationContextMut, - ) -> Result<(), Conflict> { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> Result<(), Conflict> { // Very inefficient version! // The algorithm goes through every nogood explicitly @@ -428,7 +426,7 @@ impl NogoodPropagator { &mut self, nogood: Vec, inference_code: InferenceCode, - context: &mut PropagationContextMut, + context: &mut PropagationContext, statistics: &mut SolverStatistics, ) { // We treat unit nogoods in a special way by adding it as a permanent nogood at the @@ -516,7 +514,7 @@ impl NogoodPropagator { &mut self, nogood: Vec, inference_code: InferenceCode, - context: &mut PropagationContextMut, + context: &mut PropagationContext, ) -> PropagationStatusCP { self.add_permanent_nogood(nogood, inference_code, context) } @@ -526,7 +524,7 @@ impl NogoodPropagator { &mut self, mut nogood: Vec, inference_code: InferenceCode, - context: &mut PropagationContextMut, + context: &mut PropagationContext, ) -> PropagationStatusCP { pumpkin_assert_simple!( context.get_checkpoint() == 0, @@ -664,7 +662,7 @@ impl NogoodPropagator { impl NogoodPropagator { /// Adds a watcher to the predicate. fn add_watcher( - context: &mut PropagationContextMut, + context: &mut PropagationContext, predicate: PredicateId, watcher: Watcher, watch_lists: &mut KeyedVec>, @@ -1110,7 +1108,7 @@ impl NogoodPropagator { /// 3. Detecting predicates falsified at the root. In that case, the nogood is preprocessed /// to the empty nogood. /// 4. Conflicting predicates? - fn preprocess_nogood(nogood: &mut Vec, context: &mut PropagationContextMut) { + fn preprocess_nogood(nogood: &mut Vec, context: &mut PropagationContext) { pumpkin_assert_simple!(context.get_checkpoint() == 0); // The code below is broken down into several parts @@ -1122,13 +1120,17 @@ impl NogoodPropagator { // We assume that duplicate predicates have been removed // Check if the nogood cannot be violated, i.e., it has a falsified predicate. - if nogood.is_empty() || nogood.iter().any(|p| context.is_predicate_falsified(*p)) { + if nogood.is_empty() + || nogood + .iter() + .any(|p| context.evaluate_predicate(*p) == Some(false)) + { *nogood = vec![Predicate::trivially_false()]; return; } // Remove predicates that are satisfied at the root level. - nogood.retain(|p| !context.is_predicate_satisfied(*p)); + nogood.retain(|p| context.evaluate_predicate(*p) != Some(true)); // If the nogood is violating at the root, the previous retain would leave an empty nogood. // Return a violating nogood. @@ -1145,7 +1147,7 @@ impl NogoodPropagator { fn debug_propagate_nogood_from_scratch( &self, nogood_id: NogoodId, - context: &mut PropagationContextMut, + context: &mut PropagationContext, ) -> Result<(), Conflict> { // This is an inefficient implementation for testing purposes let nogood = &self.nogood_predicates[nogood_id]; @@ -1162,7 +1164,7 @@ impl NogoodPropagator { // First we get the number of falsified predicates let has_falsified_predicate = nogood.iter().any(|predicate| { let predicate = context.get_predicate(*predicate); - context.is_predicate_falsified(predicate) + context.evaluate_predicate(predicate) == Some(false) }); // If at least one predicate is false, then the nogood can be skipped @@ -1174,7 +1176,7 @@ impl NogoodPropagator { .iter() .filter(|predicate| { let predicate = context.get_predicate(**predicate); - context.is_predicate_satisfied(predicate) + context.evaluate_predicate(predicate) == Some(true) }) .count(); diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index 4bb1684c2..e4387f3ae 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -1,17 +1,18 @@ use crate::basic_types::PropagationStatusCP; -use crate::engine::DomainEvents; use crate::engine::notifications::OpaqueDomainEvent; -use crate::engine::propagation::EnqueueDecision; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::LocalId; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::ReadDomains; -use crate::engine::propagation::constructor::PropagatorConstructor; -use crate::engine::propagation::constructor::PropagatorConstructorContext; -use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::predicates::Predicate; +use crate::propagation::DomainEvents; +use crate::propagation::Domains; +use crate::propagation::EnqueueDecision; +use crate::propagation::ExplanationContext; +use crate::propagation::LocalId; +use crate::propagation::NotificationContext; +use crate::propagation::Priority; +use crate::propagation::PropagationContext; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; use crate::state::Conflict; use crate::variables::Literal; @@ -81,13 +82,13 @@ pub(crate) struct ReifiedPropagator { impl Propagator for ReifiedPropagator { fn notify( &mut self, - context: PropagationContextWithTrailedValues, + context: NotificationContext, local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { if local_id < self.reification_literal_id { let decision = self.propagator.notify( - PropagationContextWithTrailedValues::new( + NotificationContext::new( context.trailed_values, context.assignments, context.predicate_id_assignments, @@ -102,12 +103,7 @@ impl Propagator for ReifiedPropagator Propagator for ReifiedPropagator u32 { + fn priority(&self) -> Priority { self.propagator.priority() } - fn synchronise(&mut self, context: PropagationContext) { + fn synchronise(&mut self, context: Domains) { self.propagator.synchronise(context); } - fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP { self.propagate_reification(&mut context)?; - if context.is_literal_true(&self.reification_literal) { + if context.evaluate_literal(self.reification_literal) == Some(true) { context.with_reification(self.reification_literal); let result = self.propagator.propagate(context); @@ -141,16 +137,13 @@ impl Propagator for ReifiedPropagator PropagationStatusCP { + fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { self.propagate_reification(&mut context)?; - if context.is_literal_true(&self.reification_literal) { + if context.evaluate_literal(self.reification_literal) == Some(true) { context.with_reification(self.reification_literal); - let result = self.propagator.debug_propagate_from_scratch(context); + let result = self.propagator.propagate_from_scratch(context); self.map_propagation_status(result)?; } @@ -178,18 +171,15 @@ impl ReifiedPropagator { status } - fn propagate_reification(&self, context: &mut PropagationContextMut<'_>) -> PropagationStatusCP + fn propagate_reification(&self, context: &mut PropagationContext<'_>) -> PropagationStatusCP where Prop: Propagator, { - if context.is_literal_fixed(&self.reification_literal) { + if context.evaluate_literal(self.reification_literal) == Some(true) { return Ok(()); } - if let Some(conflict) = self - .propagator - .detect_inconsistency(context.as_trailed_readonly()) - { + if let Some(conflict) = self.propagator.detect_inconsistency(context.domains()) { context.post( self.reification_literal.get_false_predicate(), conflict.conjunction, @@ -202,7 +192,7 @@ impl ReifiedPropagator { fn filter_enqueue_decision( &mut self, - context: PropagationContextWithTrailedValues<'_>, + mut context: NotificationContext<'_>, decision: EnqueueDecision, ) -> EnqueueDecision { if decision == EnqueueDecision::Skip { @@ -210,14 +200,17 @@ impl ReifiedPropagator { return EnqueueDecision::Skip; } - if context.is_literal_true(&self.reification_literal) { + if context.evaluate_literal(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.is_literal_false(&self.reification_literal) - && self.propagator.detect_inconsistency(context).is_some() + if context.evaluate_literal(self.reification_literal) != Some(false) + && self + .propagator + .detect_inconsistency(context.domains()) + .is_some() { // Or the literal is not false already and there the propagator has found an // inconsistency (i.e. we should and can propagate the reification variable) @@ -257,14 +250,14 @@ mod tests { let _ = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( - move |_: PropagationContextMut| { + move |_: PropagationContext| { Err(PropagatorConflict { conjunction: t1.clone(), inference_code, } .into()) }, - move |_: PropagationContextWithTrailedValues| { + move |_: Domains| { Some(PropagatorConflict { conjunction: t2.clone(), inference_code, @@ -291,7 +284,7 @@ mod tests { let propagator = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( - move |mut ctx: PropagationContextMut| { + move |mut ctx: PropagationContext| { ctx.post( predicate![var >= 3], conjunction!(), @@ -299,7 +292,7 @@ mod tests { )?; Ok(()) }, - |_: PropagationContextWithTrailedValues| None, + |_: Domains| None, ), reification_literal, }) @@ -331,14 +324,14 @@ mod tests { let inconsistency = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( - move |_: PropagationContextMut| { + move |_: PropagationContext| { Err(PropagatorConflict { conjunction: conjunction!([var >= 1]), inference_code, } .into()) }, - |_: PropagationContextWithTrailedValues| None, + |_: Domains| None, ), reification_literal, }) @@ -371,8 +364,8 @@ mod tests { let propagator = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( - |_: PropagationContextMut| Ok(()), - move |context: PropagationContextWithTrailedValues| { + |_: PropagationContext| Ok(()), + move |context: Domains| { if context.is_fixed(&var) { Some(PropagatorConflict { conjunction: conjunction!([var == 5]), @@ -402,9 +395,8 @@ mod tests { impl PropagatorConstructor for GenericPropagator where - Propagation: Fn(PropagationContextMut) -> PropagationStatusCP + 'static + Clone, - ConsistencyCheck: - Fn(PropagationContextWithTrailedValues) -> Option + 'static + Clone, + Propagation: Fn(PropagationContext) -> PropagationStatusCP + 'static + Clone, + ConsistencyCheck: Fn(Domains) -> Option + 'static + Clone, { type PropagatorImpl = Self; @@ -423,33 +415,26 @@ mod tests { impl Propagator for GenericPropagator where - Propagation: Fn(PropagationContextMut) -> PropagationStatusCP + 'static + Clone, - ConsistencyCheck: - Fn(PropagationContextWithTrailedValues) -> Option + 'static + Clone, + Propagation: Fn(PropagationContext) -> PropagationStatusCP + 'static + Clone, + ConsistencyCheck: Fn(Domains) -> Option + 'static + Clone, { fn name(&self) -> &str { "Generic Propagator" } - fn debug_propagate_from_scratch( - &self, - context: PropagationContextMut, - ) -> PropagationStatusCP { + fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP { (self.propagation)(context) } - fn detect_inconsistency( - &self, - context: PropagationContextWithTrailedValues, - ) -> Option { - (self.consistency_check)(context) + fn detect_inconsistency(&self, domains: Domains) -> Option { + (self.consistency_check)(domains) } } impl GenericPropagator where - Propagation: Fn(PropagationContextMut) -> PropagationStatusCP, - ConsistencyCheck: Fn(PropagationContextWithTrailedValues) -> Option, + Propagation: Fn(PropagationContext) -> PropagationStatusCP, + ConsistencyCheck: Fn(Domains) -> Option, { pub(crate) fn new(propagation: Propagation, consistency_check: ConsistencyCheck) -> Self { GenericPropagator { diff --git a/pumpkin-crates/core/src/statistics/statistic_logger.rs b/pumpkin-crates/core/src/statistics/statistic_logger.rs index c651dd4b2..26907ff3b 100644 --- a/pumpkin-crates/core/src/statistics/statistic_logger.rs +++ b/pumpkin-crates/core/src/statistics/statistic_logger.rs @@ -4,7 +4,7 @@ use itertools::Itertools; use super::statistic_logging::log_statistic; #[cfg(doc)] -use crate::engine::propagation::Propagator; +use crate::propagation::Propagator; /// Responsible for logging the statistics with the provided prefix; currently used when logging /// the statistics of propagators.