refactor(pumpkin-solver): Force checkers to be registered in propagator constructor

pumpkin-crates/checking/src/inference_checker.rs

@@ -30,8 +30,8 @@ impl<Atomic: AtomicConstraint> Clone for BoxedChecker<Atomic> {
     }
 }
 
-impl<Atomic: AtomicConstraint> From<Box<dyn InferenceChecker<Atomic>>> for BoxedChecker<Atomic> {
-    fn from(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
+impl<Atomic: AtomicConstraint> BoxedChecker<Atomic> {
+    pub fn new(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
         BoxedChecker(value)
     }
 }

pumpkin-crates/core/src/checkers/mod.rs

@@ -0,0 +1,3 @@
+mod store;
+
+pub use store::*;

pumpkin-crates/core/src/checkers/store.rs

@@ -0,0 +1,48 @@
+//! 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.
+///
+/// The runtime checkers consist of:
+/// - inference checkers, which verify that propagations are sound.
+#[derive(Clone, Debug, Default)]
+pub struct CheckerStore {
+    /// For each inference code we associate possibly many inference checkers.
+    inference_checkers: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
+}
+
+impl CheckerStore {
+    /// Get the [`InferenceChecker`]s for the given inference code.
+    pub fn for_inference_code(
+        &self,
+        inference_code: &InferenceCode,
+    ) -> impl ExactSizeIterator<Item = &BoxedChecker<Predicate>> {
+        self.inference_checkers
+            .get(inference_code)
+            .map(|checkers| itertools::Either::Left(checkers.iter()))
+            .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,
+        checker: BoxedChecker<Predicate>,
+    ) {
+        self.inference_checkers
+            .entry(inference_code.clone())
+            .or_default()
+            .push(checker);
+    }
+}

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);

pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs

@@ -918,16 +918,17 @@ impl ConstraintSatisfactionSolver {
     fn add_nogood(
         &mut self,
         nogood: Vec<Predicate>,
-        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

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 {

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,17 +25,17 @@ use crate::predicates::PredicateType;
 use crate::predicates::PropositionalConjunction;
 use crate::proof::ConstraintTag;
 use crate::proof::InferenceCode;
+use crate::proof::InferenceLabel;
 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;
 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;
@@ -81,8 +81,8 @@ pub struct State {
 
     statistics: StateStatistics,
 
-    /// Inference checkers to run in the propagation loop.
-    checkers: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
+    /// 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<Constructor::PropagatorImpl> =
             self.propagators.new_propagator().key();
 
         let constructor_context =
             PropagatorConstructorContext::new(original_handle.propagator_id(), self);
-        let (registration, propagator) = constructor.create(constructor_context);
+
+        let PropagatorSpec {
+            registration,
+            checkers,
+            propagator,
+        } = constructor.create(constructor_context);
 
         for (domain_id, events, local_id) in registration.iter() {
             let propagator_var = PropagatorVarId {
@@ -354,6 +356,15 @@ impl State {
                 .register(domain_id, events, propagator_var);
         }
 
+        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!(
             propagator.priority() as u8 <= 3,
             "The propagator priority exceeds 3.
@@ -381,11 +392,14 @@ impl State {
     /// any checker accepts the inference, the inference is accepted.
     pub fn add_inference_checker(
         &mut self,
-        inference_code: InferenceCode,
-        checker: Box<dyn InferenceChecker<Predicate>>,
-    ) {
-        let checkers = self.checkers.entry(inference_code).or_default();
-        checkers.push(BoxedChecker::from(checker));
+        constraint_tag: ConstraintTag,
+        inference_label: impl InferenceLabel,
+        checker: impl InferenceChecker<Predicate> + '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 +795,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,

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;

pumpkin-crates/core/src/proof/inference_code.rs

@@ -140,4 +140,10 @@ pub trait InferenceLabel {
     fn to_str(&self) -> Arc<str>;
 }
 
+impl InferenceLabel for Arc<str> {
+    fn to_str(&self) -> Arc<str> {
+        Arc::clone(self)
+    }
+}
+
 declare_inference_label!(pub Unknown);