feat(pumpkin-core): Introduce runtime consistency verification of propagators

pumpkin-checker/src/inferences/linear.rs

@@ -1,6 +1,6 @@
 use pumpkin_checking::InferenceChecker;
 use pumpkin_checking::VariableState;
-use pumpkin_propagators::arithmetic::LinearLessOrEqualInferenceChecker;
+use pumpkin_propagators::arithmetic::LinearLessOrEqualChecker;
 
 use crate::inferences::Fact;
 use crate::inferences::InvalidInference;
@@ -52,7 +52,7 @@ fn verify_linear_inference(
     fact: &Fact,
     state: VariableState<Atomic>,
 ) -> Result<(), InvalidInference> {
-    let checker = LinearLessOrEqualInferenceChecker::new(linear.terms.clone().into(), linear.bound);
+    let checker = LinearLessOrEqualChecker::new(linear.terms.clone().into(), linear.bound);
 
     if checker.check(state, &fact.premises, fact.consequent.as_ref()) {
         Ok(())

pumpkin-crates/core/src/engine/notifications/mod.rs

@@ -11,6 +11,8 @@ use enumset::EnumSet;
 pub(crate) use predicate_notification::PredicateNotifier;
 
 use crate::basic_types::PredicateId;
+#[cfg(feature = "check-propagations")]
+use crate::containers::HashSet;
 use crate::containers::KeyedVec;
 use crate::engine::Assignments;
 use crate::engine::PropagatorQueue;
@@ -43,6 +45,10 @@ pub(crate) struct NotificationEngine {
     /// Backtrack events which have occurred since the last of backtrack notifications have taken
     /// place
     backtrack_events: EventSink,
+    /// All the propagators that have been notified since the last call to
+    /// [`Self::drain_notified_propagators`].
+    #[cfg(feature = "check-propagations")]
+    notified_propagators: HashSet<PropagatorId>,
 }
 
 impl Default for NotificationEngine {
@@ -54,6 +60,8 @@ impl Default for NotificationEngine {
             last_notified_trail_index: 0,
             events: Default::default(),
             backtrack_events: Default::default(),
+            #[cfg(feature = "check-propagations")]
+            notified_propagators: Default::default(),
         };
         // Grow for the dummy predicate
         result.grow();
@@ -77,6 +85,8 @@ impl NotificationEngine {
             last_notified_trail_index: usize::MAX,
             events: Default::default(),
             backtrack_events: Default::default(),
+            #[cfg(feature = "check-propagations")]
+            notified_propagators: Default::default(),
         };
         // Grow for the dummy predicate
         result.grow();
@@ -333,6 +343,9 @@ impl NotificationEngine {
                     assignments,
                     trailed_values,
                 );
+
+                #[cfg(feature = "check-propagations")]
+                let _ = self.notified_propagators.insert(propagator_id);
             }
         }
 
@@ -579,4 +592,10 @@ impl NotificationEngine {
             .predicate_id_assignments
             .synchronise(backtrack_level)
     }
+
+    /// Get all propagagators that have been notified since the previous call to this function.
+    #[cfg(feature = "check-propagations")]
+    pub(crate) fn drain_notified_propagators(&mut self) -> impl Iterator<Item = PropagatorId> {
+        self.notified_propagators.drain()
+    }
 }

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

@@ -39,6 +39,10 @@ use crate::propagation::Propagator;
 use crate::propagation::PropagatorConstructor;
 use crate::propagation::PropagatorConstructorContext;
 use crate::propagation::PropagatorId;
+#[cfg(feature = "check-propagations")]
+use crate::propagation::checkers::BoxedConsistencyChecker;
+#[cfg(feature = "check-propagations")]
+use crate::propagation::checkers::Scope;
 use crate::propagation::store::PropagatorStore;
 use crate::pumpkin_assert_advanced;
 use crate::pumpkin_assert_eq_simple;
@@ -83,6 +87,11 @@ pub struct State {
 
     /// Inference checkers to run in the propagation loop.
     checkers: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
+    /// For every propagator identify what variables are associated with it.
+    #[cfg(feature = "check-propagations")]
+    pub(crate) scopes: HashMap<PropagatorId, Scope>,
+    #[cfg(feature = "check-propagations")]
+    consistency_checkers: HashMap<PropagatorId, BoxedConsistencyChecker>,
 }
 
 create_statistics_struct!(StateStatistics {
@@ -177,6 +186,10 @@ impl Default for State {
             statistics: StateStatistics::default(),
             constraint_tags: KeyGenerator::default(),
             checkers: HashMap::default(),
+            #[cfg(feature = "check-propagations")]
+            scopes: HashMap::default(),
+            #[cfg(feature = "check-propagations")]
+            consistency_checkers: HashMap::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
@@ -389,7 +402,7 @@ impl State {
         Constructor::PropagatorImpl: 'static,
     {
         #[cfg(feature = "check-propagations")]
-        constructor.add_inference_checkers(InferenceCheckers::new(self));
+        let consistency_checker = constructor.add_inference_checkers(InferenceCheckers::new(self));
 
         let original_handle: PropagatorHandle<Constructor::PropagatorImpl> =
             self.propagators.new_propagator().key();
@@ -408,6 +421,23 @@ impl State {
         let slot = self.propagators.new_propagator();
         let handle = slot.populate(propagator);
 
+        #[cfg(feature = "check-propagations")]
+        {
+            use crate::propagation::checkers::ConsistencyChecker;
+
+            #[allow(trivial_casts, reason = "removing it causes a compiler error")]
+            let previous_checker = self.consistency_checkers.insert(
+                handle.propagator_id(),
+                BoxedConsistencyChecker::from(
+                    Box::new(consistency_checker) as Box<dyn ConsistencyChecker>
+                ),
+            );
+            assert!(
+                previous_checker.is_none(),
+                "somehow adding multiple consistency checkers to the same propagator"
+            );
+        }
+
         pumpkin_assert_eq_simple!(handle.propagator_id(), original_handle.propagator_id());
 
         #[allow(deprecated, reason = "Will be refactored")]
@@ -790,6 +820,22 @@ impl State {
             self.propagate(propagator_id)?;
         }
 
+        #[cfg(feature = "check-propagations")]
+        for propagator in self.notification_engine.drain_notified_propagators() {
+            let checker = &self.consistency_checkers[&propagator];
+            let scope = &self.scopes[&propagator];
+
+            let propagator_name = self.propagators[propagator].name();
+
+            assert!(
+                checker.check_consistency(
+                    Domains::new(&self.assignments, &mut self.trailed_values),
+                    scope,
+                ),
+                "propagator {propagator_name} is not at its reported consistency"
+            );
+        }
+
         // Only check fixed point propagation if there was no reported conflict,
         // since otherwise the state may be inconsistent.
         pumpkin_assert_extreme!(DebugHelper::debug_fixed_point_propagation(

pumpkin-crates/core/src/engine/variables/affine_view.rs

@@ -14,6 +14,11 @@ use crate::engine::predicates::predicate_constructor::PredicateConstructor;
 use crate::engine::variables::DomainId;
 use crate::engine::variables::IntegerVariable;
 use crate::math::num_ext::NumExt;
+use crate::propagation::LocalId;
+use crate::propagation::checkers::ScopeBuilder;
+use crate::propagation::checkers::SingleVariableAssignment;
+use crate::propagation::checkers::ValueToWitness;
+use crate::propagation::checkers::WitnessedVariable;
 
 /// Models the constraint `y = ax + b`, by expressing the domain of `y` as a transformation of the
 /// domain of `x`.
@@ -406,6 +411,24 @@ enum Rounding {
     Down,
 }
 
+impl<Inner: WitnessedVariable> WitnessedVariable for AffineView<Inner> {
+    fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId) {
+        self.inner.add_to_scope(scope, local_id);
+    }
+
+    fn unpack_value(&self, value: ValueToWitness) -> i32 {
+        let inner_value = self.inner.unpack_value(value);
+
+        self.map(inner_value)
+    }
+
+    fn assign(&self, value: i32) -> SingleVariableAssignment {
+        assert_eq!((value - self.offset) % self.scale, 0);
+        let inner_assignment = (value - self.offset) / self.scale;
+        self.inner.assign(inner_assignment)
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

pumpkin-crates/core/src/engine/variables/domain_id.rs

@@ -10,6 +10,11 @@ use crate::engine::notifications::Watchers;
 use crate::engine::variables::AffineView;
 use crate::engine::variables::IntegerVariable;
 use crate::predicates::Predicate;
+use crate::propagation::LocalId;
+use crate::propagation::checkers::ScopeBuilder;
+use crate::propagation::checkers::SingleVariableAssignment;
+use crate::propagation::checkers::ValueToWitness;
+use crate::propagation::checkers::WitnessedVariable;
 use crate::pumpkin_assert_simple;
 
 /// A structure which represents the most basic [`IntegerVariable`]; it is simply the id which links
@@ -191,6 +196,20 @@ impl TransformableVariable<AffineView<DomainId>> for DomainId {
     }
 }
 
+impl WitnessedVariable for DomainId {
+    fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId) {
+        scope.add(local_id, *self);
+    }
+
+    fn unpack_value(&self, value: ValueToWitness) -> i32 {
+        value.unpack()
+    }
+
+    fn assign(&self, value: i32) -> SingleVariableAssignment {
+        SingleVariableAssignment::new(*self, value)
+    }
+}
+
 impl StorageKey for DomainId {
     fn index(&self) -> usize {
         self.id as usize

pumpkin-crates/core/src/engine/variables/integer_variable.rs

@@ -10,6 +10,7 @@ use crate::engine::notifications::OpaqueDomainEvent;
 use crate::engine::notifications::Watchers;
 use crate::engine::predicates::predicate_constructor::PredicateConstructor;
 use crate::predicates::Predicate;
+use crate::propagation::checkers::WitnessedVariable;
 
 /// A trait specifying the required behaviour of an integer variable such as retrieving a
 /// lower-bound ([`IntegerVariable::lower_bound`]).
@@ -19,6 +20,7 @@ pub trait IntegerVariable:
     + TransformableVariable<Self::AffineView>
     + Debug
     + CheckerVariable<Predicate>
+    + WitnessedVariable
 {
     type AffineView: IntegerVariable;
 

pumpkin-crates/core/src/engine/variables/literal.rs

@@ -15,6 +15,10 @@ use crate::engine::notifications::Watchers;
 use crate::engine::predicates::predicate::Predicate;
 use crate::engine::predicates::predicate_constructor::PredicateConstructor;
 use crate::engine::variables::AffineView;
+use crate::propagation::LocalId;
+use crate::propagation::checkers::ScopeBuilder;
+use crate::propagation::checkers::ValueToWitness;
+use crate::propagation::checkers::WitnessedVariable;
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub struct Literal {
@@ -222,3 +226,17 @@ impl TransformableVariable<AffineView<Literal>> for Literal {
         AffineView::new(*self, 1, offset)
     }
 }
+
+impl WitnessedVariable for Literal {
+    fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId) {
+        self.integer_variable.add_to_scope(scope, local_id);
+    }
+
+    fn unpack_value(&self, value: ValueToWitness) -> i32 {
+        self.integer_variable.unpack_value(value)
+    }
+
+    fn assign(&self, value: i32) -> crate::propagation::checkers::SingleVariableAssignment {
+        self.integer_variable.assign(value)
+    }
+}

pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs

@@ -0,0 +1,34 @@
+use pumpkin_checking::InferenceChecker;
+
+use crate::predicates::Predicate;
+use crate::propagation::Domains;
+use crate::propagation::checkers::ConsistencyChecker;
+use crate::propagation::checkers::Scope;
+use crate::propagation::checkers::WitnessGenerator;
+
+#[derive(Clone, Debug)]
+pub struct BoundConsistencyChecker<C> {
+    witness_generator: C,
+}
+
+impl<C> BoundConsistencyChecker<C> {
+    pub fn new(witness_generator: C) -> Self {
+        BoundConsistencyChecker { witness_generator }
+    }
+}
+
+impl<C> ConsistencyChecker for BoundConsistencyChecker<C>
+where
+    C: WitnessGenerator + InferenceChecker<Predicate> + Clone,
+{
+    fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool {
+        super::assert_consistency(
+            domains,
+            scope,
+            &self.witness_generator,
+            super::Consistency::Bounds,
+        );
+
+        true
+    }
+}

pumpkin-crates/core/src/propagation/checkers/consistency_checker.rs

@@ -0,0 +1,39 @@
+use std::fmt::Debug;
+
+use dyn_clone::DynClone;
+
+use crate::propagation::Domains;
+use crate::propagation::checkers::Scope;
+
+/// A consistency checker ensures that a propagator is at a certain level of consistency.
+///
+/// Given a current set of domains and a scope, the checker identifies whether the desired
+/// consistency level is reached.
+pub trait ConsistencyChecker: Debug + DynClone {
+    /// Returns `true` if the variables in `scope` are at the required consistency in
+    /// `domains`.
+    fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool;
+}
+
+/// Wrapper around `Box<dyn ConsistencyChecker>` that implements [`Clone`].
+#[derive(Debug)]
+pub struct BoxedConsistencyChecker(Box<dyn ConsistencyChecker>);
+
+impl Clone for BoxedConsistencyChecker {
+    fn clone(&self) -> Self {
+        BoxedConsistencyChecker(dyn_clone::clone_box(&*self.0))
+    }
+}
+
+impl From<Box<dyn ConsistencyChecker>> for BoxedConsistencyChecker {
+    fn from(value: Box<dyn ConsistencyChecker>) -> Self {
+        BoxedConsistencyChecker(value)
+    }
+}
+
+impl BoxedConsistencyChecker {
+    /// See [`ConsistencyChecker::check_consistency`].
+    pub fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool {
+        self.0.check_consistency(domains, scope)
+    }
+}

pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs

@@ -0,0 +1,34 @@
+use pumpkin_checking::InferenceChecker;
+
+use crate::predicates::Predicate;
+use crate::propagation::Domains;
+use crate::propagation::checkers::ConsistencyChecker;
+use crate::propagation::checkers::Scope;
+use crate::propagation::checkers::WitnessGenerator;
+
+#[derive(Clone, Debug)]
+pub struct DomainConsistencyChecker<C> {
+    witness_generator: C,
+}
+
+impl<C> DomainConsistencyChecker<C> {
+    pub fn new(witness_generator: C) -> Self {
+        DomainConsistencyChecker { witness_generator }
+    }
+}
+
+impl<C> ConsistencyChecker for DomainConsistencyChecker<C>
+where
+    C: WitnessGenerator + InferenceChecker<Predicate> + Clone,
+{
+    fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool {
+        super::assert_consistency(
+            domains,
+            scope,
+            &self.witness_generator,
+            super::Consistency::Domain,
+        );
+
+        true
+    }
+}