From e8ae6eb3a7b3a665d34e7c131606e1af432904fb Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 22 Jul 2026 12:03:37 +0100 Subject: [PATCH 1/6] Implement runtime checkers --- .../checking/src/inference_checker.rs | 4 +- pumpkin-crates/core/src/checkers/mod.rs | 3 + pumpkin-crates/core/src/checkers/store.rs | 40 ++++++++ .../conflict_analysis_context.rs | 10 +- .../engine/constraint_satisfaction_solver.rs | 16 ++-- .../core/src/engine/cp/test_solver.rs | 9 +- pumpkin-crates/core/src/engine/state.rs | 81 ++++++++-------- pumpkin-crates/core/src/lib.rs | 1 + .../core/src/proof/inference_code.rs | 6 ++ .../core/src/propagation/constructor.rs | 76 +++------------ .../contexts/propagation_context.rs | 4 +- pumpkin-crates/core/src/propagation/mod.rs | 2 + .../core/src/propagation/runtime_checkers.rs | 95 +++++++++++++++++++ .../hypercube_linear/propagator.rs | 35 ++++--- .../propagators/nogoods/nogood_propagator.rs | 10 +- .../src/propagators/reified_propagator.rs | 60 ++++++++---- .../propagators/arithmetic/absolute_value.rs | 34 ++++--- .../arithmetic/binary/binary_equals.rs | 36 ++++--- .../arithmetic/binary/binary_not_equals.rs | 36 ++++--- .../arithmetic/integer_division.rs | 33 ++++--- .../arithmetic/integer_multiplication.rs | 38 +++++--- .../arithmetic/linear_less_or_equal.rs | 30 +++--- .../arithmetic/linear_not_equal.rs | 33 ++++--- .../src/propagators/arithmetic/maximum.rs | 34 ++++--- .../time_table_over_interval_incremental.rs | 52 +++++----- .../time_table_per_point_incremental.rs | 52 +++++----- .../time_table/time_table_over_interval.rs | 52 +++++----- .../time_table/time_table_per_point.rs | 52 +++++----- .../disjunctive/disjunctive_propagator.rs | 47 +++++---- .../propagators/src/propagators/element.rs | 32 ++++--- .../src/deduction_propagator.rs | 10 +- 31 files changed, 616 insertions(+), 407 deletions(-) create mode 100644 pumpkin-crates/core/src/checkers/mod.rs create mode 100644 pumpkin-crates/core/src/checkers/store.rs create mode 100644 pumpkin-crates/core/src/propagation/runtime_checkers.rs diff --git a/pumpkin-crates/checking/src/inference_checker.rs b/pumpkin-crates/checking/src/inference_checker.rs index badb75d8e..dc6b61fda 100644 --- a/pumpkin-crates/checking/src/inference_checker.rs +++ b/pumpkin-crates/checking/src/inference_checker.rs @@ -30,8 +30,8 @@ impl Clone for BoxedChecker { } } -impl From>> for BoxedChecker { - fn from(value: Box>) -> Self { +impl BoxedChecker { + pub fn new(value: Box>) -> Self { BoxedChecker(value) } } diff --git a/pumpkin-crates/core/src/checkers/mod.rs b/pumpkin-crates/core/src/checkers/mod.rs new file mode 100644 index 000000000..fca730d27 --- /dev/null +++ b/pumpkin-crates/core/src/checkers/mod.rs @@ -0,0 +1,3 @@ +mod store; + +pub use store::*; diff --git a/pumpkin-crates/core/src/checkers/store.rs b/pumpkin-crates/core/src/checkers/store.rs new file mode 100644 index 000000000..f90c4911e --- /dev/null +++ b/pumpkin-crates/core/src/checkers/store.rs @@ -0,0 +1,40 @@ +//! This module facilitates runtime verification in Pumpkin. It defines common types as well as the +//! [`CheckerStore`] that owns the checkers that are active in the solver. + +use pumpkin_checking::BoxedChecker; +#[cfg(doc)] +use pumpkin_checking::InferenceChecker; + +use crate::containers::HashMap; +use crate::predicates::Predicate; +use crate::proof::InferenceCode; + +/// Owns the runtime checkers present in the solver. +#[derive(Clone, Debug, Default)] +pub struct CheckerStore { + inference_codes: HashMap>>, +} + +impl CheckerStore { + /// Get the [`InferenceChecker`]s for the given inference code. + pub fn for_inference_code( + &self, + inference_code: &InferenceCode, + ) -> impl ExactSizeIterator> { + self.inference_codes + .get(inference_code) + .map(|checkers| itertools::Either::Left(checkers.iter())) + .unwrap_or(itertools::Either::Right(std::iter::empty())) + } + + pub fn add_inference_checker( + &mut self, + inference_code: InferenceCode, + checker: BoxedChecker, + ) { + self.inference_codes + .entry(inference_code.clone()) + .or_default() + .push(checker); + } +} diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index ffebd61e5..f17177a7c 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -281,13 +281,13 @@ impl ConflictAnalysisContext<'_> { LearnedNogood::create_from_vec(learned_nogood_predicates, self, uses_cpip); let constraint_tag = self.log_deduction(learned_nogood.predicates.iter().copied()); - let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); - self.state.add_inference_checker( - inference_code.clone(), - Box::new(NogoodChecker { + let inference_code = self.state.add_inference_checker( + constraint_tag, + NogoodLabel, + NogoodChecker { nogood: learned_nogood.predicates.clone().into(), - }), + }, ); self.restore_to(learned_nogood.backtrack_level); diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index eabeed1ff..0d8dde371 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -918,16 +918,17 @@ impl ConstraintSatisfactionSolver { fn add_nogood( &mut self, nogood: Vec, - inference_code: InferenceCode, + constraint_tag: ConstraintTag, ) -> Result<(), ConstraintOperationError> { pumpkin_assert_eq_simple!(self.get_checkpoint(), 0); let num_trail_entries = self.state.trail_len(); - self.state.add_inference_checker( - inference_code.clone(), - Box::new(NogoodChecker { + let inference_code = self.state.add_inference_checker( + constraint_tag, + NogoodLabel, + NogoodChecker { nogood: nogood.clone().into(), - }), + }, ); let (nogood_propagator, mut context) = self @@ -1010,7 +1011,6 @@ impl ConstraintSatisfactionSolver { return Err(ConstraintOperationError::InfeasibleClause); } - let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); if are_all_falsified_at_root { // Since the propagation is not actually performed, we log the inference // explicitly here for the proof. @@ -1019,7 +1019,7 @@ impl ConstraintSatisfactionSolver { .proof_log .log_inference( &mut self.state.constraint_tags, - inference_code, + InferenceCode::new(constraint_tag, NogoodLabel), predicates.iter().copied(), None, &self.state.variable_names, @@ -1040,7 +1040,7 @@ impl ConstraintSatisfactionSolver { return Err(ConstraintOperationError::InfeasibleClause); } - if let Err(constraint_operation_error) = self.add_nogood(predicates, inference_code) { + if let Err(constraint_operation_error) = self.add_nogood(predicates, constraint_tag) { let _ = self.conclude_proof_unsat(); self.solver_state diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 7a9ecc7cb..71ed429cb 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -17,6 +17,7 @@ use crate::predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::proof::InferenceLabel; use crate::propagation::EnqueueDecision; use crate::propagation::ExplanationContext; use crate::propagation::NotificationContext; @@ -60,7 +61,11 @@ impl Default for TestSolver { #[deprecated = "Will be replaced by the state API"] impl TestSolver { - pub fn accept_inferences_by(&mut self, inference_code: InferenceCode) { + pub fn accept_inferences_by( + &mut self, + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + ) -> InferenceCode { #[derive(Debug, Clone, Copy)] struct Checker; @@ -76,7 +81,7 @@ impl TestSolver { } self.state - .add_inference_checker(inference_code, Box::new(Checker)); + .add_inference_checker(constraint_tag, inference_label, Checker) } pub fn new_variable(&mut self, lb: i32, ub: i32) -> DomainId { diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 177897111..731312f56 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -5,7 +5,7 @@ use pumpkin_checking::InferenceChecker; #[cfg(feature = "check-propagations")] use pumpkin_checking::VariableState; -use crate::containers::HashMap; +use crate::checkers::CheckerStore; use crate::containers::KeyGenerator; use crate::create_statistics_struct; use crate::engine::Assignments; @@ -25,11 +25,11 @@ use crate::predicates::PredicateType; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::proof::InferenceLabel; +use crate::propagation::ConstructedPropagator; use crate::propagation::CurrentNogood; use crate::propagation::Domains; use crate::propagation::ExplanationContext; -#[cfg(feature = "check-propagations")] -use crate::propagation::InferenceCheckers; use crate::propagation::NotificationContext; use crate::propagation::PropagationContext; use crate::propagation::Propagator; @@ -81,8 +81,8 @@ pub struct State { statistics: StateStatistics, - /// Inference checkers to run in the propagation loop. - checkers: HashMap>>, + /// Runtime checkers to run in the propagation loop. + checkers: CheckerStore, } create_statistics_struct!(StateStatistics { @@ -112,7 +112,7 @@ impl Default for State { notification_engine: NotificationEngine::default(), statistics: StateStatistics::default(), constraint_tags: KeyGenerator::default(), - checkers: HashMap::default(), + checkers: CheckerStore::default(), }; // As a convention, the assignments contain a dummy domain_id=0, which represents a 0-1 // variable that is assigned to one. We use it to represent predicates that are @@ -334,15 +334,17 @@ impl State { Constructor: PropagatorConstructor, Constructor::PropagatorImpl: 'static, { - #[cfg(feature = "check-propagations")] - constructor.add_inference_checkers(InferenceCheckers::new(self)); - let original_handle: PropagatorHandle = self.propagators.new_propagator().key(); let constructor_context = PropagatorConstructorContext::new(original_handle.propagator_id(), self); - let (registration, propagator) = constructor.create(constructor_context); + + let ConstructedPropagator { + registration, + checkers, + propagator, + } = constructor.create(constructor_context); for (domain_id, events, local_id) in registration.iter() { let propagator_var = PropagatorVarId { @@ -354,6 +356,10 @@ impl State { .register(domain_id, events, propagator_var); } + for (inference_code, checker) in checkers.into_iter() { + self.checkers.add_inference_checker(inference_code, checker); + } + pumpkin_assert_simple!( propagator.priority() as u8 <= 3, "The propagator priority exceeds 3. @@ -381,11 +387,14 @@ impl State { /// any checker accepts the inference, the inference is accepted. pub fn add_inference_checker( &mut self, - inference_code: InferenceCode, - checker: Box>, - ) { - let checkers = self.checkers.entry(inference_code).or_default(); - checkers.push(BoxedChecker::from(checker)); + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + checker: impl InferenceChecker + 'static, + ) -> InferenceCode { + let inference_code = InferenceCode::new(constraint_tag, inference_label); + self.checkers + .add_inference_checker(inference_code.clone(), BoxedChecker::new(Box::new(checker))); + inference_code } } @@ -781,31 +790,23 @@ impl State { ) { let premises: Vec<_> = premises.into_iter().collect(); - let checkers = self - .checkers - .get(inference_code) - .map(|vec| vec.as_slice()) - .unwrap_or(&[]); - - assert!( - !checkers.is_empty(), - "missing checker for inference code {inference_code:?}" - ); - - let any_checker_accepts_inference = checkers.iter().any(|checker| { - // Construct the variable state for the conflict check. - let variable_state = VariableState::prepare_for_conflict_check( - premises.clone(), - consequent, - ) - .unwrap_or_else(|domain| { - panic!( - "inconsistent atomics over domain {domain:?} in inference by {inference_code:?}" - ) - }); - - checker.check(variable_state, &premises, consequent.as_ref()) - }); + let any_checker_accepts_inference = + self.checkers + .for_inference_code(inference_code) + .any(|checker| { + // Construct the variable state for the conflict check. + let variable_state = VariableState::prepare_for_conflict_check( + premises.clone(), + consequent, + ) + .unwrap_or_else(|domain| { + panic!( + "inconsistent atomics over domain {domain:?} in inference by {inference_code:?}" + ) + }); + + checker.check(variable_state, &premises, consequent.as_ref()) + }); assert!( any_checker_accepts_inference, diff --git a/pumpkin-crates/core/src/lib.rs b/pumpkin-crates/core/src/lib.rs index 2a8680544..19d6fcefb 100644 --- a/pumpkin-crates/core/src/lib.rs +++ b/pumpkin-crates/core/src/lib.rs @@ -12,6 +12,7 @@ use crate::branching::Brancher; use crate::termination::TerminationCondition; pub mod branching; +pub mod checkers; pub mod conflict_resolving; pub mod constraints; pub mod optimisation; diff --git a/pumpkin-crates/core/src/proof/inference_code.rs b/pumpkin-crates/core/src/proof/inference_code.rs index afc4a4ece..78ca55a88 100644 --- a/pumpkin-crates/core/src/proof/inference_code.rs +++ b/pumpkin-crates/core/src/proof/inference_code.rs @@ -140,4 +140,10 @@ pub trait InferenceLabel { fn to_str(&self) -> Arc; } +impl InferenceLabel for Arc { + fn to_str(&self) -> Arc { + Arc::clone(self) + } +} + declare_inference_label!(pub Unknown); diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index 6aa22776b..bc9b34ec7 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -1,5 +1,3 @@ -use pumpkin_checking::InferenceChecker; - use super::Domains; use super::LocalId; use super::Propagator; @@ -17,14 +15,12 @@ use crate::engine::variables::AffineView; #[cfg(doc)] use crate::engine::variables::DomainId; use crate::predicates::Predicate; -use crate::proof::InferenceCode; #[cfg(doc)] use crate::propagation::DomainEvent; use crate::propagation::DomainEvents; use crate::propagation::EventsToRegister; -use crate::propagators::reified_propagator::ReifiedChecker; +use crate::propagation::RuntimeCheckers; use crate::variables::IntegerVariable; -use crate::variables::Literal; /// A propagator constructor creates a fully initialized instance of a [`Propagator`]. /// @@ -36,14 +32,6 @@ pub trait PropagatorConstructor { /// The propagator that is produced by this constructor. type PropagatorImpl: Propagator + Clone; - /// Add inference checkers to the solver if applicable. - /// - /// If the `check-propagations` feature is turned on, then the inference checker will be used - /// to verify the propagations done by this propagator are correct. - /// - /// See [`InferenceChecker`] for more information. - fn add_inference_checkers(&self, _checkers: InferenceCheckers<'_>) {} - /// Create the propagator instance from `Self`. /// /// Alongside the propagator instance, this returns the events for which the propagator should @@ -51,48 +39,18 @@ pub trait PropagatorConstructor { fn create( self, context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl); -} - -/// Interface used to add [`InferenceChecker`]s to the [`State`]. -#[derive(Debug)] -pub struct InferenceCheckers<'state> { - state: &'state mut State, - reification_literal: Option, + ) -> ConstructedPropagator; } -impl<'state> InferenceCheckers<'state> { - #[cfg(feature = "check-propagations")] - pub(crate) fn new(state: &'state mut State) -> Self { - InferenceCheckers { - state, - reification_literal: None, - } - } -} - -impl InferenceCheckers<'_> { - /// Forwards to [`State::add_inference_checker`]. - pub fn add_inference_checker( - &mut self, - inference_code: InferenceCode, - checker: Box>, - ) { - if let Some(reification_literal) = self.reification_literal { - let reification_checker = ReifiedChecker { - inner: checker.into(), - reification_literal, - }; - self.state - .add_inference_checker(inference_code, Box::new(reification_checker)); - } else { - self.state.add_inference_checker(inference_code, checker); - } - } - - pub fn with_reification_literal(&mut self, literal: Literal) { - self.reification_literal = Some(literal) - } +/// The result of [`PropagatorConstructor::create`]. +#[derive(Clone, Debug)] +pub struct ConstructedPropagator

{ + /// The domain events the propagator needs to be be registered for. + pub registration: EventsToRegister, + /// Any runtime checkers that verify the propagator's implementation. + pub checkers: RuntimeCheckers, + /// The propagator + pub propagator: P, } /// [`PropagatorConstructorContext`] is used when [`Propagator`]s are initialised after creation. @@ -169,18 +127,6 @@ impl PropagatorConstructorContext<'_> { state: self.state, } } - - /// Add an inference checker for inferences produced by the propagator. - /// - /// If the `check-propagations` feature is not enabled, adding an [`InferenceChecker`] will not - /// do anything. - pub fn add_inference_checker( - &mut self, - inference_code: InferenceCode, - checker: Box>, - ) { - self.state.add_inference_checker(inference_code, checker); - } } mod private { diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs index 57187434c..f39d337b0 100644 --- a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -300,7 +300,9 @@ pub(crate) fn build_reason( } } -/// A wrapper around the notification engine that implements [`EventDispatcher`]. +/// Wrapper around the [`NotificationEngine`] that is tied to a specific propagator. +/// +/// Implements [`EventDispatcher`] to handle registration of domain events. struct NotificationEngineWatchers<'a> { propagator_id: PropagatorId, notificaton_engine: &'a mut NotificationEngine, diff --git a/pumpkin-crates/core/src/propagation/mod.rs b/pumpkin-crates/core/src/propagation/mod.rs index 1646dda63..2e00f75c2 100644 --- a/pumpkin-crates/core/src/propagation/mod.rs +++ b/pumpkin-crates/core/src/propagation/mod.rs @@ -72,12 +72,14 @@ mod domains; mod event_registration; mod local_id; mod propagator; +mod runtime_checkers; pub(crate) mod propagator_id; pub(crate) mod propagator_var_id; pub(crate) mod store; pub use event_registration::*; +pub use runtime_checkers::*; mod reexports { // Re-exports of types not in this module according to the file tree. diff --git a/pumpkin-crates/core/src/propagation/runtime_checkers.rs b/pumpkin-crates/core/src/propagation/runtime_checkers.rs new file mode 100644 index 000000000..0a8b0a08f --- /dev/null +++ b/pumpkin-crates/core/src/propagation/runtime_checkers.rs @@ -0,0 +1,95 @@ +use pumpkin_checking::BoxedChecker; +use pumpkin_checking::InferenceChecker; + +use crate::predicates::Predicate; +use crate::proof::ConstraintTag; +use crate::proof::InferenceCode; +use crate::proof::InferenceLabel; + +/// Holds the runtime checkers that are added by a propagator. +#[derive(Clone, Debug)] +pub struct RuntimeCheckers { + inference_checkers: Vec<(InferenceCode, BoxedChecker)>, +} + +impl RuntimeCheckers { + /// Create a [`RuntimeCheckers`] value which we accept may be empty. + /// + /// This is often not what you want. If it is expected that some checkers should be added, + /// use [`RuntimeCheckers::builder`] instead to communicate that intention. + pub fn empty() -> RuntimeCheckers { + RuntimeCheckers { + inference_checkers: vec![], + } + } + + /// Create a [`RuntimeCheckersBuilder`] to add runtime checkers. + /// + /// The [`RuntimeCheckersBuilder::build`] will panic if no checkers are added. + pub fn builder() -> RuntimeCheckersBuilder { + RuntimeCheckersBuilder { + checkers: RuntimeCheckers { + inference_checkers: vec![], + }, + } + } + + /// Add an [`InferenceChecker`] to verify the soundness of propagations. + pub fn add_inference_checker( + &mut self, + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + checker: impl InferenceChecker + 'static, + ) -> InferenceCode { + let inference_code = InferenceCode::new(constraint_tag, inference_label); + + self.inference_checkers + .push((inference_code.clone(), BoxedChecker::new(Box::new(checker)))); + + inference_code + } +} + +impl IntoIterator for RuntimeCheckers { + type Item = (InferenceCode, BoxedChecker); + + type IntoIter = std::vec::IntoIter; + + fn into_iter(self) -> Self::IntoIter { + self.inference_checkers.into_iter() + } +} + +/// A builder for the [`RuntimeCheckers`] that ensures at least one checker is added. +#[derive(Clone, Debug)] +pub struct RuntimeCheckersBuilder { + checkers: RuntimeCheckers, +} + +impl RuntimeCheckersBuilder { + /// Add an [`InferenceChecker`] to verify the soundness of propagations. + pub fn add_inference_checker( + &mut self, + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + checker: impl InferenceChecker + 'static, + ) -> InferenceCode { + self.checkers + .add_inference_checker(constraint_tag, inference_label, checker) + } + + /// Finish adding runtime checkers. + /// + /// Panics if runtime verification is enabled and no checkers are added. If it is expected + /// behavior that no checkers are added, use [`RuntimeCheckers::empty`]. + pub fn build(self) -> RuntimeCheckers { + if cfg!(feature = "check-propagations") { + assert!( + !self.checkers.inference_checkers.is_empty(), + "did not register any inference checkers" + ); + } + + self.checkers + } +} diff --git a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs index 11b6fb604..1e4d31cd8 100644 --- a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs +++ b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs @@ -6,15 +6,16 @@ use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; +use crate::propagation::ConstructedPropagator; use crate::propagation::DomainEvents; use crate::propagation::EventsToRegister; -use crate::propagation::InferenceCheckers; 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::propagation::RuntimeCheckers; use crate::propagators::hypercube_linear::Hypercube; use crate::propagators::hypercube_linear::HypercubeLinearChecker; use crate::propagators::hypercube_linear::LinearInequality; @@ -34,21 +35,10 @@ pub struct HypercubeLinearConstructor { impl PropagatorConstructor for HypercubeLinearConstructor { type PropagatorImpl = HypercubeLinearPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, HypercubeLinear), - Box::new(HypercubeLinearChecker { - hypercube: self.hypercube.iter_predicates().collect(), - terms: self.linear.terms().collect(), - bound: self.linear.bound(), - }), - ); - } - fn create( self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let HypercubeLinearConstructor { hypercube, linear, @@ -69,18 +59,33 @@ impl PropagatorConstructor for HypercubeLinearConstructor { ] }; + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + HypercubeLinear, + HypercubeLinearChecker { + hypercube: hypercube.iter_predicates().collect(), + terms: linear.terms().collect(), + bound: linear.bound(), + }, + ); + let propagator = HypercubeLinearPropagator { linear, hypercube_predicates, watched_predicates, - inference_code: InferenceCode::new(constraint_tag, HypercubeLinear), + inference_code, }; // TODO: This will be expanded with registration of predicates. let registration = EventsToRegister::empty(); - (registration, propagator) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 82936e569..53bc754d1 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -24,6 +24,7 @@ use crate::engine::reason::ReasonStore; use crate::predicate; use crate::predicates::PredicateType; use crate::proof::InferenceCode; +use crate::propagation::ConstructedPropagator; use crate::propagation::EnqueueDecision; use crate::propagation::EventsToRegister; use crate::propagation::ExplanationContext; @@ -36,6 +37,7 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::ReadDomains; +use crate::propagation::RuntimeCheckers; use crate::propagators::nogoods::PropagationMode; use crate::propagators::nogoods::WatcherProcessingStatus; use crate::propagators::nogoods::arena_allocator::ArenaAllocator; @@ -173,7 +175,7 @@ impl PropagatorConstructor for NogoodPropagatorConstructor { fn create( self, context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let propagator = NogoodPropagator { statistics: NogoodPropagatorStatistics::default(), handle: PropagatorHandle::new(context.propagator_id), @@ -193,7 +195,11 @@ impl PropagatorConstructor for NogoodPropagatorConstructor { priority: self.priority, }; - (EventsToRegister::empty(), propagator) + ConstructedPropagator { + registration: EventsToRegister::empty(), + checkers: RuntimeCheckers::empty(), + propagator, + } } } diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index d49059289..001e4e138 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -6,12 +6,11 @@ use pumpkin_checking::InferenceChecker; use crate::engine::PropagationStatusCP; use crate::engine::notifications::OpaqueDomainEvent; use crate::predicates::Predicate; +use crate::propagation::ConstructedPropagator; use crate::propagation::DomainEvents; use crate::propagation::Domains; use crate::propagation::EnqueueDecision; -use crate::propagation::EventsToRegister; use crate::propagation::ExplanationContext; -use crate::propagation::InferenceCheckers; use crate::propagation::LazyExplanation; use crate::propagation::LocalId; use crate::propagation::NotificationContext; @@ -21,6 +20,7 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::ReadDomains; +use crate::propagation::RuntimeCheckers; use crate::pumpkin_assert_simple; use crate::state::Conflict; use crate::variables::Literal; @@ -42,14 +42,20 @@ where fn create( self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let ReifiedPropagatorArgs { propagator, reification_literal, } = self; - let (mut registration, propagator) = propagator.create(context.reborrow()); + let ConstructedPropagator { + mut registration, + propagator, + checkers, + } = propagator.create(context.reborrow()); + // The local ID for the reification literal will be one larger than the largest ID + // registered by the wrapped propagator. let reification_literal_id = registration .iter() .map(|(_, _, lid)| lid) @@ -63,6 +69,18 @@ where reification_literal_id, ); + let mut wrapped_checkers = RuntimeCheckers::empty(); + for (inference_code, checker) in checkers.into_iter() { + let _ = wrapped_checkers.add_inference_checker( + inference_code.tag(), + inference_code.label(), + ReifiedChecker { + inner: checker, + reification_literal, + }, + ); + } + let name = format!("Reified({})", propagator.name()); let propagator = ReifiedPropagator { @@ -73,13 +91,11 @@ where reason_buffer: vec![], }; - (registration, propagator) - } - - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.with_reification_literal(self.reification_literal); - - self.propagator.add_inference_checkers(checkers); + ConstructedPropagator { + registration, + checkers: wrapped_checkers, + propagator, + } } } @@ -286,6 +302,8 @@ mod tests { use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; + use crate::proof::Unknown; + use crate::propagation::EventsToRegister; use crate::variables::DomainId; #[test] @@ -300,8 +318,8 @@ mod tests { let t1 = triggered_conflict.clone(); let t2 = triggered_conflict.clone(); - let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); - solver.accept_inferences_by(inference_code.clone()); + let inference_code = + solver.accept_inferences_by(ConstraintTag::create_from_index(0), Unknown); let i1 = inference_code.clone(); let i2 = inference_code.clone(); @@ -381,8 +399,8 @@ mod tests { let _ = solver.set_literal(reification_literal, true); let var = solver.new_variable(1, 1); - let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); - solver.accept_inferences_by(inference_code.clone()); + let inference_code = + solver.accept_inferences_by(ConstraintTag::create_from_index(0), Unknown); let inconsistency = solver .new_propagator(ReifiedPropagatorArgs { @@ -423,8 +441,8 @@ mod tests { let reification_literal = solver.new_literal(); let var = solver.new_variable(1, 5); - let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); - solver.accept_inferences_by(inference_code.clone()); + let inference_code = + solver.accept_inferences_by(ConstraintTag::create_from_index(0), Unknown); let propagator = solver .new_propagator(ReifiedPropagatorArgs { @@ -469,14 +487,18 @@ mod tests { fn create( self, _: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let mut registration = EventsToRegister::empty(); for (index, variable) in self.variables_to_register.iter().enumerate() { registration.add(variable, DomainEvents::ANY_INT, LocalId::from(index as u32)); } - (registration, self) + ConstructedPropagator { + registration, + checkers: RuntimeCheckers::empty(), + propagator: self, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index 9934e6821..face0b7c9 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -7,9 +7,9 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; @@ -17,6 +17,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -36,17 +37,10 @@ where { type PropagatorImpl = AbsoluteValuePropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, AbsoluteValue), - Box::new(AbsoluteValueChecker { - signed: self.signed.clone(), - absolute: self.absolute.clone(), - }), - ); - } - - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let AbsoluteValueArgs { signed, absolute, @@ -58,7 +52,15 @@ where .add(&absolute, DomainEvents::BOUNDS, LocalId::from(1)) .build(); - let inference_code = InferenceCode::new(constraint_tag, AbsoluteValue); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + AbsoluteValue, + AbsoluteValueChecker { + signed: signed.clone(), + absolute: absolute.clone(), + }, + ); let propagator = AbsoluteValuePropagator { signed, @@ -66,7 +68,11 @@ where inference_code, }; - (registration, propagator) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs index b43ccb585..2c080940f 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs @@ -16,13 +16,13 @@ use pumpkin_core::predicates::PredicateConstructor; use pumpkin_core::predicates::PredicateType; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LazyExplanation; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -33,6 +33,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::EmptyDomainConflict; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; @@ -55,17 +56,10 @@ where { type PropagatorImpl = BinaryEqualsPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, BinaryEquals), - Box::new(BinaryEqualsChecker { - lhs: self.a.clone(), - rhs: self.b.clone(), - }), - ); - } - - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let BinaryEqualsPropagatorArgs { a, b, @@ -77,6 +71,16 @@ where .add(&b, DomainEvents::ANY_INT, LocalId::from(1)) .build(); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + BinaryEquals, + BinaryEqualsChecker { + lhs: a.clone(), + rhs: b.clone(), + }, + ); + let propagator = BinaryEqualsPropagator { a, b, @@ -84,14 +88,18 @@ where a_removed_values: HashSet::default(), b_removed_values: HashSet::default(), - inference_code: InferenceCode::new(constraint_tag, BinaryEquals), + inference_code, has_backtracked: false, first_propagation_loop: true, reason: Predicate::trivially_false(), }; - (registration, propagator) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs index 4ca2c4032..ce7f8864d 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -6,10 +6,10 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; @@ -17,6 +17,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -38,17 +39,10 @@ where { type PropagatorImpl = BinaryNotEqualsPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, BinaryNotEquals), - Box::new(BinaryNotEqualsChecker { - lhs: self.a.clone(), - rhs: self.b.clone(), - }), - ); - } - - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let BinaryNotEqualsPropagatorArgs { a, b, @@ -61,14 +55,28 @@ where .add(&b, DomainEvents::ASSIGN, LocalId::from(1)) .build(); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + BinaryNotEquals, + BinaryNotEqualsChecker { + lhs: a.clone(), + rhs: b.clone(), + }, + ); + let propagator = BinaryNotEqualsPropagator { a, b, - inference_code: InferenceCode::new(constraint_tag, BinaryNotEquals), + inference_code, }; - (registration, propagator) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs index 300b26e96..10aba7a22 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs @@ -8,9 +8,9 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; @@ -18,6 +18,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -47,7 +48,7 @@ where fn create( self, context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let DivisionArgs { numerator, denominator, @@ -66,7 +67,16 @@ where .add(&rhs, DomainEvents::BOUNDS, ID_RHS) .build(); - let inference_code = InferenceCode::new(constraint_tag, Division); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + Division, + IntegerDivisionChecker { + numerator: numerator.clone(), + denominator: denominator.clone(), + rhs: rhs.clone(), + }, + ); let propagator = DivisionPropagator { numerator, @@ -75,18 +85,11 @@ where inference_code, }; - (registration, propagator) - } - - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, Division), - Box::new(IntegerDivisionChecker { - numerator: self.numerator.clone(), - denominator: self.denominator.clone(), - rhs: self.rhs.clone(), - }), - ); + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs index 6811e17bc..dbfa263de 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs @@ -7,9 +7,9 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; @@ -17,6 +17,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::propagator_conflict; use pumpkin_core::variables::IntegerVariable; @@ -40,18 +41,10 @@ where { type PropagatorImpl = IntegerMultiplicationPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, IntegerMultiplication), - Box::new(IntegerMultiplicationChecker { - a: self.a.clone(), - b: self.b.clone(), - c: self.c.clone(), - }), - ); - } - - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let IntegerMultiplicationArgs { a, b, @@ -65,14 +58,29 @@ where .add(&c, DomainEvents::ANY_INT, ID_C) .build(); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + IntegerMultiplication, + IntegerMultiplicationChecker { + a: a.clone(), + b: b.clone(), + c: c.clone(), + }, + ); + let propagator = IntegerMultiplicationPropagator { a, b, c, - inference_code: InferenceCode::new(constraint_tag, IntegerMultiplication), + inference_code, }; - (registration, propagator) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index a3a03be1c..806848492 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -10,12 +10,12 @@ use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LazyExplanation; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -26,6 +26,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::propagation::TrailedInteger; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; @@ -47,20 +48,10 @@ where { type PropagatorImpl = LinearLessOrEqualPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, LinearBounds), - Box::new(LinearLessOrEqualInferenceChecker::new( - self.x.clone(), - self.c, - )), - ); - } - fn create( self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let LinearLessOrEqualPropagatorArgs { x, c, @@ -80,16 +71,27 @@ where let lower_bound_left_hand_side = context.new_trailed_integer(lower_bound_left_hand_side); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + LinearBounds, + LinearLessOrEqualInferenceChecker::new(x.clone(), c), + ); + let propagator = LinearLessOrEqualPropagator { x, c, lower_bound_left_hand_side, current_bounds: current_bounds.into(), - inference_code: InferenceCode::new(constraint_tag, LinearBounds), + inference_code, reason_buffer: Vec::default(), }; - (registration.build(), propagator) + ConstructedPropagator { + registration: registration.build(), + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs index d92290960..bf78d8700 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -14,12 +14,12 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; use pumpkin_core::propagation::OpaqueDomainEvent; @@ -29,6 +29,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -51,20 +52,10 @@ where { type PropagatorImpl = LinearNotEqualPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, LinearNotEquals), - Box::new(LinearNotEqualChecker { - terms: self.terms.as_ref().into(), - bound: self.rhs, - }), - ); - } - fn create( self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let LinearNotEqualPropagatorArgs { terms, rhs, @@ -81,6 +72,16 @@ where ); } + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + LinearNotEquals, + LinearNotEqualChecker { + terms: terms.as_ref().into(), + bound: rhs, + }, + ); + let mut propagator = LinearNotEqualPropagator { terms, rhs, @@ -88,12 +89,16 @@ where fixed_lhs: 0, unfixed_variable_has_been_updated: false, should_recalculate_lhs: false, - inference_code: InferenceCode::new(constraint_tag, LinearNotEquals), + inference_code, }; propagator.recalculate_fixed_variables(context.domains()); - (registration.build(), propagator) + ConstructedPropagator { + registration: registration.build(), + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs index 6f658ace3..80e094a63 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs @@ -8,9 +8,9 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; @@ -18,6 +18,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -37,17 +38,10 @@ where { type PropagatorImpl = MaximumPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, Maximum), - Box::new(MaximumChecker { - array: self.array.clone(), - rhs: self.rhs.clone(), - }), - ); - } - - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let MaximumArgs { array, rhs, @@ -65,7 +59,15 @@ where LocalId::from(array.len() as u32), ); - let inference_code = InferenceCode::new(constraint_tag, Maximum); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + Maximum, + MaximumChecker { + array: array.clone(), + rhs: rhs.clone(), + }, + ); let propagator = MaximumPropagator { array, @@ -73,7 +75,11 @@ where inference_code, }; - (registration.build(), propagator) + ConstructedPropagator { + registration: registration.build(), + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index ea2af2fda..bb0df4aac 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -8,11 +8,10 @@ use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; -use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; use pumpkin_core::propagation::OpaqueDomainEvent; @@ -21,6 +20,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::propagator_conflict; use pumpkin_core::variables::IntegerVariable; @@ -111,29 +111,10 @@ impl PropagatorConstruc { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, TimeTable), - Box::new(TimeTableChecker { - tasks: self - .parameters - .tasks - .iter() - .map(|task| CheckerTask { - start_time: task.start_variable.clone(), - processing_time: task.processing_time, - resource_usage: task.resource_usage, - }) - .collect(), - capacity: self.parameters.capacity, - }), - ); - } - fn create( mut self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { // We only register for notifications of backtrack events if incremental backtracking is // enabled let registration = register_tasks( @@ -148,9 +129,32 @@ impl PropagatorConstruc self.is_time_table_outdated = true; - self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); + let mut checkers = RuntimeCheckers::builder(); + self.inference_code = Some( + checkers.add_inference_checker( + self.constraint_tag, + TimeTable, + TimeTableChecker { + tasks: self + .parameters + .tasks + .iter() + .map(|task| CheckerTask { + start_time: task.start_variable.clone(), + processing_time: task.processing_time, + resource_usage: task.resource_usage, + }) + .collect(), + capacity: self.parameters.capacity, + }, + ), + ); - (registration, self) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator: self, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index 661df8e50..b3a09fb3c 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -8,11 +8,10 @@ use pumpkin_core::asserts::pumpkin_assert_extreme; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; -use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; use pumpkin_core::propagation::OpaqueDomainEvent; @@ -21,6 +20,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::propagator_conflict; use pumpkin_core::variables::IntegerVariable; @@ -108,29 +108,10 @@ impl Propagator { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, TimeTable), - Box::new(TimeTableChecker { - tasks: self - .parameters - .tasks - .iter() - .map(|task| CheckerTask { - start_time: task.start_variable.clone(), - processing_time: task.processing_time, - resource_usage: task.resource_usage, - }) - .collect(), - capacity: self.parameters.capacity, - }), - ); - } - fn create( mut self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { let registration = register_tasks(&self.parameters.tasks, context.reborrow(), true); self.updatable_structures .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); @@ -138,9 +119,32 @@ impl Propagator // Then we do normal propagation self.is_time_table_outdated = true; - self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); + let mut checkers = RuntimeCheckers::builder(); + self.inference_code = Some( + checkers.add_inference_checker( + self.constraint_tag, + TimeTable, + TimeTableChecker { + tasks: self + .parameters + .tasks + .iter() + .map(|task| CheckerTask { + start_time: task.start_variable.clone(), + processing_time: task.processing_time, + resource_usage: task.resource_usage, + }) + .collect(), + capacity: self.parameters.capacity, + }, + ), + ); - (registration, self) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator: self, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs index 86b6adfef..602c6b03c 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -6,11 +6,10 @@ use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; -use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; use pumpkin_core::propagation::OpaqueDomainEvent; @@ -20,6 +19,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::state::propagator_conflict; @@ -111,36 +111,40 @@ impl PropagatorConstructor { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, TimeTable), - Box::new(TimeTableChecker { - tasks: self - .parameters - .tasks - .iter() - .map(|task| CheckerTask { - start_time: task.start_variable.clone(), - processing_time: task.processing_time, - resource_usage: task.resource_usage, - }) - .collect(), - capacity: self.parameters.capacity, - }), - ); - } - fn create( mut self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { self.updatable_structures .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); let registration = register_tasks(&self.parameters.tasks, context.reborrow(), false); - self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); + let mut checkers = RuntimeCheckers::builder(); + self.inference_code = Some( + checkers.add_inference_checker( + self.constraint_tag, + TimeTable, + TimeTableChecker { + tasks: self + .parameters + .tasks + .iter() + .map(|task| CheckerTask { + start_time: task.start_variable.clone(), + processing_time: task.processing_time, + resource_usage: task.resource_usage, + }) + .collect(), + capacity: self.parameters.capacity, + }, + ), + ); - (registration, self) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator: self, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs index a8d11a955..16723f457 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -9,10 +9,9 @@ use pumpkin_core::asserts::pumpkin_assert_extreme; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::EnqueueDecision; -use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; use pumpkin_core::propagation::OpaqueDomainEvent; @@ -22,6 +21,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::state::propagator_conflict; @@ -101,36 +101,40 @@ impl TimeTablePerPointPropagator { impl PropagatorConstructor for TimeTablePerPointPropagator { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, TimeTable), - Box::new(TimeTableChecker { - tasks: self - .parameters - .tasks - .iter() - .map(|task| CheckerTask { - start_time: task.start_variable.clone(), - processing_time: task.processing_time, - resource_usage: task.resource_usage, - }) - .collect(), - capacity: self.parameters.capacity, - }), - ); - } - fn create( mut self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { self.updatable_structures .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); let registration = register_tasks(&self.parameters.tasks, context.reborrow(), false); - self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); + let mut checkers = RuntimeCheckers::builder(); + self.inference_code = Some( + checkers.add_inference_checker( + self.constraint_tag, + TimeTable, + TimeTableChecker { + tasks: self + .parameters + .tasks + .iter() + .map(|task| CheckerTask { + start_time: task.start_variable.clone(), + processing_time: task.processing_time, + resource_usage: task.resource_usage, + }) + .collect(), + capacity: self.parameters.capacity, + }, + ), + ); - (registration, self) + ConstructedPropagator { + registration, + checkers: checkers.build(), + propagator: self, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs index 753f71494..0b7c39e2d 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs @@ -7,15 +7,16 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::propagator_conflict; use pumpkin_core::variables::IntegerVariable; @@ -80,7 +81,10 @@ impl DisjunctiveConstructor { impl PropagatorConstructor for DisjunctiveConstructor { type PropagatorImpl = DisjunctivePropagator; - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let tasks = self .tasks .into_iter() @@ -93,13 +97,26 @@ impl PropagatorConstructor for DisjunctiveConstr .collect::>(); let theta_lambda_tree = ThetaLambdaTree::new(&tasks); - let inference_code = InferenceCode::new(self.constraint_tag, DisjunctiveEdgeFinding); - let mut registration = EventsToRegister::builder(); for task in tasks.iter() { registration = registration.add(&task.start_time, DomainEvents::BOUNDS, task.id); } + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + self.constraint_tag, + DisjunctiveEdgeFinding, + DisjunctiveEdgeFindingChecker { + tasks: tasks + .iter() + .map(|task| ArgDisjunctiveTask { + start_time: task.start_time.clone(), + processing_time: task.processing_time, + }) + .collect(), + }, + ); + let propagator = DisjunctivePropagator { tasks: tasks.clone().into_boxed_slice(), sorted_tasks: tasks, @@ -108,23 +125,11 @@ impl PropagatorConstructor for DisjunctiveConstr inference_code, }; - (registration.build(), propagator) - } - - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, DisjunctiveEdgeFinding), - Box::new(DisjunctiveEdgeFindingChecker { - tasks: self - .tasks - .iter() - .map(|task| ArgDisjunctiveTask { - start_time: task.start_time.clone(), - processing_time: task.processing_time, - }) - .collect(), - }), - ); + ConstructedPropagator { + registration: registration.build(), + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-crates/propagators/src/propagators/element.rs b/pumpkin-crates/propagators/src/propagators/element.rs index 3ce5516e1..684a079dc 100644 --- a/pumpkin-crates/propagators/src/propagators/element.rs +++ b/pumpkin-crates/propagators/src/propagators/element.rs @@ -16,10 +16,10 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; -use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LazyExplanation; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -28,6 +28,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; use pumpkin_core::variables::Reason; @@ -50,18 +51,10 @@ where { type PropagatorImpl = ElementPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { - checkers.add_inference_checker( - InferenceCode::new(self.constraint_tag, Element), - Box::new(ElementChecker::new( - self.array.clone(), - self.index.clone(), - self.rhs.clone(), - )), - ); - } - - fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { + fn create( + self, + _: PropagatorConstructorContext, + ) -> ConstructedPropagator { let ElementArgs { array, index, @@ -81,7 +74,12 @@ where registration = registration.add(&index, DomainEvents::ANY_INT, ID_INDEX); registration = registration.add(&rhs, DomainEvents::ANY_INT, ID_RHS); - let inference_code = InferenceCode::new(constraint_tag, Element); + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_inference_checker( + constraint_tag, + Element, + ElementChecker::new(array.clone(), index.clone(), rhs.clone()), + ); let propagator = ElementPropagator { array, @@ -91,7 +89,11 @@ where rhs_reason_buffer: vec![], }; - (registration.build(), propagator) + ConstructedPropagator { + registration: registration.build(), + checkers: checkers.build(), + propagator, + } } } diff --git a/pumpkin-proof-processor/src/deduction_propagator.rs b/pumpkin-proof-processor/src/deduction_propagator.rs index 26d6b86f3..46767d886 100644 --- a/pumpkin-proof-processor/src/deduction_propagator.rs +++ b/pumpkin-proof-processor/src/deduction_propagator.rs @@ -2,6 +2,7 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::PredicateId; use pumpkin_core::propagation::PropagationContext; @@ -9,6 +10,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::Conflict; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; @@ -28,7 +30,7 @@ impl PropagatorConstructor for DeductionPropagatorConstructor { fn create( self, mut context: PropagatorConstructorContext, - ) -> (EventsToRegister, Self::PropagatorImpl) { + ) -> ConstructedPropagator { declare_inference_label!(Nogood); let DeductionPropagatorConstructor { @@ -48,7 +50,11 @@ impl PropagatorConstructor for DeductionPropagatorConstructor { active: true, }; - (EventsToRegister::empty(), propagator) + ConstructedPropagator { + registration: EventsToRegister::empty(), + checkers: RuntimeCheckers::empty(), + propagator, + } } } From 0ac658d3bb445946af1f952e6617ad585e1f6398 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 22 Jul 2026 12:10:23 +0100 Subject: [PATCH 2/6] Rename ConstructedPropagator to PropagatorSpec --- pumpkin-crates/core/src/engine/state.rs | 4 ++-- .../core/src/propagation/constructor.rs | 10 +++++----- .../propagators/hypercube_linear/propagator.rs | 6 +++--- .../src/propagators/nogoods/nogood_propagator.rs | 9 +++------ .../core/src/propagators/reified_propagator.rs | 15 ++++++--------- .../src/propagators/arithmetic/absolute_value.rs | 9 +++------ .../arithmetic/binary/binary_equals.rs | 9 +++------ .../arithmetic/binary/binary_not_equals.rs | 9 +++------ .../propagators/arithmetic/integer_division.rs | 9 +++------ .../arithmetic/integer_multiplication.rs | 9 +++------ .../arithmetic/linear_less_or_equal.rs | 6 +++--- .../propagators/arithmetic/linear_not_equal.rs | 6 +++--- .../src/propagators/arithmetic/maximum.rs | 9 +++------ .../time_table_over_interval_incremental.rs | 6 +++--- .../time_table_per_point_incremental.rs | 6 +++--- .../time_table/time_table_over_interval.rs | 6 +++--- .../cumulative/time_table/time_table_per_point.rs | 6 +++--- .../disjunctive/disjunctive_propagator.rs | 9 +++------ .../propagators/src/propagators/element.rs | 9 +++------ .../src/deduction_propagator.rs | 6 +++--- 20 files changed, 64 insertions(+), 94 deletions(-) diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 731312f56..7bea3c893 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -26,7 +26,6 @@ use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::proof::InferenceLabel; -use crate::propagation::ConstructedPropagator; use crate::propagation::CurrentNogood; use crate::propagation::Domains; use crate::propagation::ExplanationContext; @@ -36,6 +35,7 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::PropagatorId; +use crate::propagation::PropagatorSpec; use crate::propagation::PropagatorVarId; use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_advanced; @@ -340,7 +340,7 @@ impl State { let constructor_context = PropagatorConstructorContext::new(original_handle.propagator_id(), self); - let ConstructedPropagator { + let PropagatorSpec { registration, checkers, propagator, diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index bc9b34ec7..a7cfedad8 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -36,15 +36,15 @@ pub trait PropagatorConstructor { /// /// Alongside the propagator instance, this returns the events for which the propagator should /// be enqueued. - fn create( - self, - context: PropagatorConstructorContext, - ) -> ConstructedPropagator; + fn create(self, context: PropagatorConstructorContext) -> PropagatorSpec; } /// The result of [`PropagatorConstructor::create`]. +/// +/// Contains an initialized [`Propagator`], alongside runtime checkers and the events that should +/// cause the propagator to be enqueued #[derive(Clone, Debug)] -pub struct ConstructedPropagator

{ +pub struct PropagatorSpec

{ /// The domain events the propagator needs to be be registered for. pub registration: EventsToRegister, /// Any runtime checkers that verify the propagator's implementation. diff --git a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs index 1e4d31cd8..337a3e548 100644 --- a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs +++ b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs @@ -6,7 +6,6 @@ use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; -use crate::propagation::ConstructedPropagator; use crate::propagation::DomainEvents; use crate::propagation::EventsToRegister; use crate::propagation::LocalId; @@ -14,6 +13,7 @@ use crate::propagation::PropagationContext; use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; +use crate::propagation::PropagatorSpec; use crate::propagation::ReadDomains; use crate::propagation::RuntimeCheckers; use crate::propagators::hypercube_linear::Hypercube; @@ -38,7 +38,7 @@ impl PropagatorConstructor for HypercubeLinearConstructor { fn create( self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { let HypercubeLinearConstructor { hypercube, linear, @@ -81,7 +81,7 @@ impl PropagatorConstructor for HypercubeLinearConstructor { // TODO: This will be expanded with registration of predicates. let registration = EventsToRegister::empty(); - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 53bc754d1..a09d7684d 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -24,7 +24,6 @@ use crate::engine::reason::ReasonStore; use crate::predicate; use crate::predicates::PredicateType; use crate::proof::InferenceCode; -use crate::propagation::ConstructedPropagator; use crate::propagation::EnqueueDecision; use crate::propagation::EventsToRegister; use crate::propagation::ExplanationContext; @@ -36,6 +35,7 @@ use crate::propagation::PropagationContext; use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; +use crate::propagation::PropagatorSpec; use crate::propagation::ReadDomains; use crate::propagation::RuntimeCheckers; use crate::propagators::nogoods::PropagationMode; @@ -172,10 +172,7 @@ impl NogoodPropagatorConstructor { impl PropagatorConstructor for NogoodPropagatorConstructor { type PropagatorImpl = NogoodPropagator; - fn create( - self, - context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, context: PropagatorConstructorContext) -> PropagatorSpec { let propagator = NogoodPropagator { statistics: NogoodPropagatorStatistics::default(), handle: PropagatorHandle::new(context.propagator_id), @@ -195,7 +192,7 @@ impl PropagatorConstructor for NogoodPropagatorConstructor { priority: self.priority, }; - ConstructedPropagator { + PropagatorSpec { registration: EventsToRegister::empty(), checkers: RuntimeCheckers::empty(), propagator, diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index 001e4e138..a6ccede2e 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -6,7 +6,6 @@ use pumpkin_checking::InferenceChecker; use crate::engine::PropagationStatusCP; use crate::engine::notifications::OpaqueDomainEvent; use crate::predicates::Predicate; -use crate::propagation::ConstructedPropagator; use crate::propagation::DomainEvents; use crate::propagation::Domains; use crate::propagation::EnqueueDecision; @@ -19,6 +18,7 @@ use crate::propagation::PropagationContext; use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; +use crate::propagation::PropagatorSpec; use crate::propagation::ReadDomains; use crate::propagation::RuntimeCheckers; use crate::pumpkin_assert_simple; @@ -42,13 +42,13 @@ where fn create( self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { let ReifiedPropagatorArgs { propagator, reification_literal, } = self; - let ConstructedPropagator { + let PropagatorSpec { mut registration, propagator, checkers, @@ -91,7 +91,7 @@ where reason_buffer: vec![], }; - ConstructedPropagator { + PropagatorSpec { registration, checkers: wrapped_checkers, propagator, @@ -484,17 +484,14 @@ mod tests { { type PropagatorImpl = Self; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let mut registration = EventsToRegister::empty(); for (index, variable) in self.variables_to_register.iter().enumerate() { registration.add(variable, DomainEvents::ANY_INT, LocalId::from(index as u32)); } - ConstructedPropagator { + PropagatorSpec { registration, checkers: RuntimeCheckers::empty(), propagator: self, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index face0b7c9..ef27dfe70 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -7,7 +7,6 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::LocalId; @@ -16,6 +15,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -37,10 +37,7 @@ where { type PropagatorImpl = AbsoluteValuePropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let AbsoluteValueArgs { signed, absolute, @@ -68,7 +65,7 @@ where inference_code, }; - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs index 2c080940f..565ce762c 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs @@ -16,7 +16,6 @@ use pumpkin_core::predicates::PredicateConstructor; use pumpkin_core::predicates::PredicateType; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; @@ -32,6 +31,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::EmptyDomainConflict; @@ -56,10 +56,7 @@ where { type PropagatorImpl = BinaryEqualsPropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let BinaryEqualsPropagatorArgs { a, b, @@ -95,7 +92,7 @@ where reason: Predicate::trivially_false(), }; - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs index ce7f8864d..c9bde00eb 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -6,7 +6,6 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EventsToRegister; @@ -16,6 +15,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -39,10 +39,7 @@ where { type PropagatorImpl = BinaryNotEqualsPropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let BinaryNotEqualsPropagatorArgs { a, b, @@ -72,7 +69,7 @@ where inference_code, }; - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs index 10aba7a22..7cc40188e 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs @@ -8,7 +8,6 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::LocalId; @@ -17,6 +16,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -45,10 +45,7 @@ where { type PropagatorImpl = DivisionPropagator; - fn create( - self, - context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, context: PropagatorConstructorContext) -> PropagatorSpec { let DivisionArgs { numerator, denominator, @@ -85,7 +82,7 @@ where inference_code, }; - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs index dbfa263de..8358e4355 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs @@ -7,7 +7,6 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::LocalId; @@ -16,6 +15,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -41,10 +41,7 @@ where { type PropagatorImpl = IntegerMultiplicationPropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let IntegerMultiplicationArgs { a, b, @@ -76,7 +73,7 @@ where inference_code, }; - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index 806848492..4611cb1c0 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -10,7 +10,6 @@ use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; @@ -25,6 +24,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::propagation::TrailedInteger; @@ -51,7 +51,7 @@ where fn create( self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { let LinearLessOrEqualPropagatorArgs { x, c, @@ -87,7 +87,7 @@ where reason_buffer: Vec::default(), }; - ConstructedPropagator { + PropagatorSpec { registration: registration.build(), checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs index bf78d8700..e5a7cbe7a 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -14,7 +14,6 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; @@ -28,6 +27,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -55,7 +55,7 @@ where fn create( self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { let LinearNotEqualPropagatorArgs { terms, rhs, @@ -94,7 +94,7 @@ where propagator.recalculate_fixed_variables(context.domains()); - ConstructedPropagator { + PropagatorSpec { registration: registration.build(), checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs index 80e094a63..316cfca8a 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs @@ -8,7 +8,6 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::LocalId; @@ -17,6 +16,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -38,10 +38,7 @@ where { type PropagatorImpl = MaximumPropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let MaximumArgs { array, rhs, @@ -75,7 +72,7 @@ where inference_code, }; - ConstructedPropagator { + PropagatorSpec { registration: registration.build(), checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index bb0df4aac..be07bbb5d 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -8,7 +8,6 @@ use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; @@ -20,6 +19,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::propagator_conflict; @@ -114,7 +114,7 @@ impl PropagatorConstruc fn create( mut self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { // We only register for notifications of backtrack events if incremental backtracking is // enabled let registration = register_tasks( @@ -150,7 +150,7 @@ impl PropagatorConstruc ), ); - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator: self, diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index b3a09fb3c..34d9e8e3b 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -8,7 +8,6 @@ use pumpkin_core::asserts::pumpkin_assert_extreme; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; @@ -20,6 +19,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::propagator_conflict; @@ -111,7 +111,7 @@ impl Propagator fn create( mut self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { let registration = register_tasks(&self.parameters.tasks, context.reborrow(), true); self.updatable_structures .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); @@ -140,7 +140,7 @@ impl Propagator ), ); - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator: self, diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs index 602c6b03c..00b841972 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -6,7 +6,6 @@ use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; @@ -18,6 +17,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -114,7 +114,7 @@ impl PropagatorConstructor fn create( mut self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { self.updatable_structures .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); let registration = register_tasks(&self.parameters.tasks, context.reborrow(), false); @@ -140,7 +140,7 @@ impl PropagatorConstructor ), ); - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator: self, diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs index 16723f457..cabed34c0 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -9,7 +9,6 @@ use pumpkin_core::asserts::pumpkin_assert_extreme; use pumpkin_core::conjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::EnqueueDecision; use pumpkin_core::propagation::LocalId; @@ -20,6 +19,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -104,7 +104,7 @@ impl PropagatorConstructor for TimeTablePerPoint fn create( mut self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { self.updatable_structures .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); let registration = register_tasks(&self.parameters.tasks, context.reborrow(), false); @@ -130,7 +130,7 @@ impl PropagatorConstructor for TimeTablePerPoint ), ); - ConstructedPropagator { + PropagatorSpec { registration, checkers: checkers.build(), propagator: self, diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs index 0b7c39e2d..ee3beaf45 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs @@ -7,7 +7,6 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::LocalId; @@ -15,6 +14,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -81,10 +81,7 @@ impl DisjunctiveConstructor { impl PropagatorConstructor for DisjunctiveConstructor { type PropagatorImpl = DisjunctivePropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let tasks = self .tasks .into_iter() @@ -125,7 +122,7 @@ impl PropagatorConstructor for DisjunctiveConstr inference_code, }; - ConstructedPropagator { + PropagatorSpec { registration: registration.build(), checkers: checkers.build(), propagator, diff --git a/pumpkin-crates/propagators/src/propagators/element.rs b/pumpkin-crates/propagators/src/propagators/element.rs index 684a079dc..56d2bd9eb 100644 --- a/pumpkin-crates/propagators/src/propagators/element.rs +++ b/pumpkin-crates/propagators/src/propagators/element.rs @@ -16,7 +16,6 @@ use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; @@ -27,6 +26,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; @@ -51,10 +51,7 @@ where { type PropagatorImpl = ElementPropagator; - fn create( - self, - _: PropagatorConstructorContext, - ) -> ConstructedPropagator { + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { let ElementArgs { array, index, @@ -89,7 +86,7 @@ where rhs_reason_buffer: vec![], }; - ConstructedPropagator { + PropagatorSpec { registration: registration.build(), checkers: checkers.build(), propagator, diff --git a/pumpkin-proof-processor/src/deduction_propagator.rs b/pumpkin-proof-processor/src/deduction_propagator.rs index 46767d886..25e17619d 100644 --- a/pumpkin-proof-processor/src/deduction_propagator.rs +++ b/pumpkin-proof-processor/src/deduction_propagator.rs @@ -2,13 +2,13 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::ConstructedPropagator; use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::PredicateId; use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::Conflict; @@ -30,7 +30,7 @@ impl PropagatorConstructor for DeductionPropagatorConstructor { fn create( self, mut context: PropagatorConstructorContext, - ) -> ConstructedPropagator { + ) -> PropagatorSpec { declare_inference_label!(Nogood); let DeductionPropagatorConstructor { @@ -50,7 +50,7 @@ impl PropagatorConstructor for DeductionPropagatorConstructor { active: true, }; - ConstructedPropagator { + PropagatorSpec { registration: EventsToRegister::empty(), checkers: RuntimeCheckers::empty(), propagator, From 61b1d6d574930a03b29f659efa45fb0fb97e0ba4 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 22 Jul 2026 12:21:57 +0100 Subject: [PATCH 3/6] Document CheckerStore::add_inference_checker --- pumpkin-crates/core/src/checkers/store.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pumpkin-crates/core/src/checkers/store.rs b/pumpkin-crates/core/src/checkers/store.rs index f90c4911e..740345e78 100644 --- a/pumpkin-crates/core/src/checkers/store.rs +++ b/pumpkin-crates/core/src/checkers/store.rs @@ -27,6 +27,10 @@ impl CheckerStore { .unwrap_or(itertools::Either::Right(std::iter::empty())) } + /// Add a new inference checker for the inference code. + /// + /// An inference code can have multiple checkers, so if an inference checker was already + /// registered for the given code, this new checker is simply added to the collection. pub fn add_inference_checker( &mut self, inference_code: InferenceCode, From c0a5dfd23c63c6cdfaba5c0cf211f94350f41862 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 22 Jul 2026 12:23:40 +0100 Subject: [PATCH 4/6] Update docs of PropagatorConstructor::create --- pumpkin-crates/core/src/propagation/constructor.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index a7cfedad8..eeb74e714 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -34,8 +34,10 @@ pub trait PropagatorConstructor { /// Create the propagator instance from `Self`. /// - /// Alongside the propagator instance, this returns the events for which the propagator should - /// be enqueued. + /// Returns a [`PropagatorSpec`] that contains: + /// - the propagator instance, + /// - the events for which the propagator should be enqueued, + /// - and the runtime checkers that verify the propagator's behavior. fn create(self, context: PropagatorConstructorContext) -> PropagatorSpec; } From c73fbdd0cb5d029244561f50b6b66064ea964766 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Tue, 28 Jul 2026 10:13:59 +0100 Subject: [PATCH 5/6] Apply suggestions --- pumpkin-crates/core/src/checkers/store.rs | 3 +++ pumpkin-crates/core/src/propagation/constructor.rs | 2 +- pumpkin-crates/core/src/propagation/runtime_checkers.rs | 4 ++++ 3 files changed, 8 insertions(+), 1 deletion(-) diff --git a/pumpkin-crates/core/src/checkers/store.rs b/pumpkin-crates/core/src/checkers/store.rs index 740345e78..abe4290e6 100644 --- a/pumpkin-crates/core/src/checkers/store.rs +++ b/pumpkin-crates/core/src/checkers/store.rs @@ -10,6 +10,9 @@ use crate::predicates::Predicate; use crate::proof::InferenceCode; /// Owns the runtime checkers present in the solver. +/// +/// The runtime checkers consist of: +/// - inference checkers, which verify that propagations are sound. #[derive(Clone, Debug, Default)] pub struct CheckerStore { inference_codes: HashMap>>, diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index eeb74e714..6950f14cc 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -44,7 +44,7 @@ pub trait PropagatorConstructor { /// The result of [`PropagatorConstructor::create`]. /// /// Contains an initialized [`Propagator`], alongside runtime checkers and the events that should -/// cause the propagator to be enqueued +/// cause the propagator to be enqueued. #[derive(Clone, Debug)] pub struct PropagatorSpec

{ /// The domain events the propagator needs to be be registered for. diff --git a/pumpkin-crates/core/src/propagation/runtime_checkers.rs b/pumpkin-crates/core/src/propagation/runtime_checkers.rs index 0a8b0a08f..aa2917247 100644 --- a/pumpkin-crates/core/src/propagation/runtime_checkers.rs +++ b/pumpkin-crates/core/src/propagation/runtime_checkers.rs @@ -5,8 +5,12 @@ use crate::predicates::Predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::proof::InferenceLabel; +#[cfg(doc)] +use crate::propagation::PropagatorConstructor; /// Holds the runtime checkers that are added by a propagator. +/// +/// Used when creating a new propagator in [`PropagatorConstructor::create`]. #[derive(Clone, Debug)] pub struct RuntimeCheckers { inference_checkers: Vec<(InferenceCode, BoxedChecker)>, From b45cfe4024b4ec5ce3c872ea004dafa1b11c74dd Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Tue, 28 Jul 2026 20:05:06 +0200 Subject: [PATCH 6/6] Final PR suggestions --- pumpkin-crates/core/src/checkers/store.rs | 7 ++++--- pumpkin-crates/core/src/engine/state.rs | 9 +++++++-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/pumpkin-crates/core/src/checkers/store.rs b/pumpkin-crates/core/src/checkers/store.rs index abe4290e6..5806afb38 100644 --- a/pumpkin-crates/core/src/checkers/store.rs +++ b/pumpkin-crates/core/src/checkers/store.rs @@ -15,7 +15,8 @@ use crate::proof::InferenceCode; /// - inference checkers, which verify that propagations are sound. #[derive(Clone, Debug, Default)] pub struct CheckerStore { - inference_codes: HashMap>>, + /// For each inference code we associate possibly many inference checkers. + inference_checkers: HashMap>>, } impl CheckerStore { @@ -24,7 +25,7 @@ impl CheckerStore { &self, inference_code: &InferenceCode, ) -> impl ExactSizeIterator> { - self.inference_codes + self.inference_checkers .get(inference_code) .map(|checkers| itertools::Either::Left(checkers.iter())) .unwrap_or(itertools::Either::Right(std::iter::empty())) @@ -39,7 +40,7 @@ impl CheckerStore { inference_code: InferenceCode, checker: BoxedChecker, ) { - self.inference_codes + self.inference_checkers .entry(inference_code.clone()) .or_default() .push(checker); diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 7bea3c893..2e71cefd4 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -356,8 +356,13 @@ impl State { .register(domain_id, events, propagator_var); } - for (inference_code, checker) in checkers.into_iter() { - self.checkers.add_inference_checker(inference_code, checker); + if cfg!(feature = "check-propagations") { + // Only register the checkers when this feature is enabled. This is an if statement + // instead of a #[cfg(...)] to avoid the 'unused variable' warning that we would + // otherwise get on `self.checkers`. + for (inference_code, checker) in checkers.into_iter() { + self.checkers.add_inference_checker(inference_code, checker); + } } pumpkin_assert_simple!(