feat(pumpkin-solver): Implement consistency checker infrastructure

.github/workflows/ci.yml

@@ -26,7 +26,13 @@ jobs:
           target/
         key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
     - uses: dtolnay/rust-toolchain@stable
-    - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations --features pumpkin-core/check-deductions
+    - run: |
+        cargo test                                     \
+          --release                                    \
+          --no-fail-fast                               \
+          --features pumpkin-solver/check-propagations \
+          --features pumpkin-core/check-consistency    \
+          --features pumpkin-core/check-deductions
 
   wasm-test:
     name: Test Suite for pumpkin-core in WebAssembly

pumpkin-crates/constraints/src/constraints/arithmetic/mod.rs

@@ -3,6 +3,7 @@ mod inequality;
 
 pub use equality::*;
 pub use inequality::*;
+use pumpkin_core::checkers::support::SupportsValue;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
@@ -23,9 +24,9 @@ pub fn plus<Var: IntegerVariable + 'static>(
 
 /// Creates the [`Constraint`] `a * b = c`.
 pub fn times(
-    a: impl IntegerVariable + 'static,
-    b: impl IntegerVariable + 'static,
-    c: impl IntegerVariable + 'static,
+    a: impl IntegerVariable + SupportsValue<f32> + 'static,
+    b: impl IntegerVariable + SupportsValue<f32> + 'static,
+    c: impl IntegerVariable + SupportsValue<f32> + 'static,
     constraint_tag: ConstraintTag,
 ) -> impl Constraint {
     IntegerMultiplicationArgs {

pumpkin-crates/core/Cargo.toml

@@ -30,6 +30,8 @@ clap = { version = "4.5.40", optional = true, features=["derive"] }
 indexmap = "2.10.0"
 dyn-clone = "1.0.20"
 flate2 = { version = "1.1.2" }
+bit-set = "0.10.0"
+replace_with = "0.1.8"
 
 [target.'cfg(target_arch = "wasm32")'.dependencies]
 web-time = "1.1"
@@ -39,6 +41,7 @@ getrandom = { version = "0.4.2", features = ["wasm_js"] }
 wasm-bindgen-test = "0.3"
 
 [features]
+check-consistency = []
 check-propagations = []
 check-deductions = []
 debug-checks = []

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

@@ -69,8 +69,8 @@ pub mod options {
     pub use crate::engine::ConflictResolverType;
     pub use crate::engine::RestartOptions;
     pub use crate::engine::SatisfactionSolverOptions as SolverOptions;
+    pub use crate::propagators::ReifiedPropagatorArgs;
     pub use crate::propagators::nogoods::LearningOptions;
-    pub use crate::propagators::reified_propagator::ReifiedPropagatorArgs;
 }
 
 pub mod termination {

pumpkin-crates/core/src/basic_types/propositional_conjunction.rs

@@ -21,6 +21,12 @@ impl Deref for PropositionalConjunction {
     }
 }
 
+impl Into<Box<[Predicate]>> for PropositionalConjunction {
+    fn into(self) -> Box<[Predicate]> {
+        self.predicates_in_conjunction.into()
+    }
+}
+
 impl PropositionalConjunction {
     pub fn new(predicates_in_conjunction: Vec<Predicate>) -> Self {
         PropositionalConjunction {

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

@@ -0,0 +1,14 @@
+mod propagation_checker;
+mod retention_checker;
+mod scope;
+mod self_disabling;
+mod store;
+mod strong_retention_checker;
+pub mod support;
+
+pub use propagation_checker::*;
+pub use retention_checker::*;
+pub use scope::*;
+pub use self_disabling::*;
+pub use store::*;
+pub use strong_retention_checker::*;

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

@@ -0,0 +1,64 @@
+use pumpkin_checking::BoxedChecker;
+use pumpkin_checking::VariableState;
+
+use crate::predicates::Predicate;
+use crate::propagation::Domains;
+use crate::propagation::ReadDomains;
+use crate::variables::DomainId;
+
+/// Tests whether an inference is correct given the solver state.
+///
+/// An inference is correct when:
+/// 1. All premises are satisfied.
+/// 2. The conjunction of the premises and negation of the consequent is consistent.
+/// 3. The consequent is logically entailed given the inference code.
+#[derive(Clone, Debug)]
+pub struct PropagationChecker {
+    inference_checker: BoxedChecker<Predicate>,
+}
+
+impl PropagationChecker {
+    /// Create a new propagation checker given an inference checker and inference code.
+    pub fn new(inference_checker: BoxedChecker<Predicate>) -> PropagationChecker {
+        PropagationChecker { inference_checker }
+    }
+
+    /// Run the propagation checker for the given inference.
+    pub fn check(
+        &self,
+        premises: &[Predicate],
+        consequent: Option<Predicate>,
+        domains: Domains<'_>,
+    ) -> Result<(), InvalidInference> {
+        let premises_satisfied = premises
+            .iter()
+            .all(|&premise| domains.evaluate_predicate(premise) == Some(true));
+
+        if !premises_satisfied {
+            return Err(InvalidInference::UnsatisfiedPremises);
+        }
+
+        let variable_state =
+            VariableState::prepare_for_conflict_check(premises.iter().copied(), consequent)
+                .map_err(InvalidInference::InconsistentPredicates)?;
+
+        if self
+            .inference_checker
+            .check(variable_state, &premises, consequent.as_ref())
+        {
+            Ok(())
+        } else {
+            Err(InvalidInference::Unsound)
+        }
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum InvalidInference {
+    /// Not all premises are true given the current state.
+    UnsatisfiedPremises,
+    /// The predicates that make up the inference are trivially inconsistent.
+    InconsistentPredicates(DomainId),
+    /// Cannot establish that the inference is sound.
+    Unsound,
+}

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

@@ -0,0 +1,39 @@
+use std::fmt::Debug;
+
+use dyn_clone::DynClone;
+
+use crate::checkers::Scope;
+use crate::propagation::Domains;
+
+/// A runtime verifier that determines whether domains are sufficiently pruned.
+pub trait RetentionChecker: Debug + DynClone {
+    /// Ensure the domains do not have values that should have been removed by propagation.
+    ///
+    /// Returns `true` if the domains are sufficiently pruned, or `false` otherwise.
+    fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool;
+}
+
+/// Wrapper around `Box<dyn RetentionChecker>` that implements [`Clone`].
+#[derive(Debug)]
+pub struct BoxedRetentionChecker(Box<dyn RetentionChecker>);
+
+impl Clone for BoxedRetentionChecker {
+    fn clone(&self) -> Self {
+        BoxedRetentionChecker(dyn_clone::clone_box(&*self.0))
+    }
+}
+
+impl<T> From<T> for BoxedRetentionChecker
+where
+    T: RetentionChecker + 'static,
+{
+    fn from(value: T) -> Self {
+        BoxedRetentionChecker(Box::new(value))
+    }
+}
+
+impl BoxedRetentionChecker {
+    pub fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool {
+        self.0.check_retention(scope, domains)
+    }
+}

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

@@ -0,0 +1,71 @@
+use crate::containers::HashMap;
+use crate::propagation::LocalId;
+use crate::variables::DomainId;
+
+/// The scope of a constraint is the collection of variables involved in the relation.
+#[derive(Clone, Debug, Default)]
+pub struct Scope {
+    domains: HashMap<LocalId, DomainId>,
+}
+
+impl FromIterator<(LocalId, DomainId)> for Scope {
+    fn from_iter<T: IntoIterator<Item = (LocalId, DomainId)>>(iter: T) -> Self {
+        Scope {
+            domains: iter.into_iter().collect(),
+        }
+    }
+}
+
+impl Scope {
+    /// Add a new domain to the scope with the given local id.
+    ///
+    /// Any previous occurrance of this local id will be overridden.
+    pub fn add_domain(&mut self, local_id: LocalId, domain_id: DomainId) {
+        let _ = self.domains.insert(local_id, domain_id);
+    }
+
+    /// The integer domains in the scope with the [`LocalId`]s they are registered.
+    pub fn domains(&self) -> impl ExactSizeIterator<Item = (LocalId, DomainId)> {
+        self.domains.iter().map(|(lid, did)| (*lid, *did))
+    }
+
+    /// Returns a copy of this scope with the entry for `local_id` removed.
+    pub fn without(&self, local_id: LocalId) -> Scope {
+        let mut scope = self.clone();
+        let _ = scope.domains.remove(&local_id);
+        scope
+    }
+}
+
+macro_rules! impl_scope_from_tuple {
+    ($($lid_name:ident,$var_name:ident : $ty_name:ident),+) => {
+        impl<$($ty_name),+> From<($((LocalId, &$ty_name)),+)> for Scope
+        where
+            $($ty_name: ScopeItem),+
+        {
+            fn from(
+                ($(($lid_name, $var_name)),+): ($((LocalId, &$ty_name)),+),
+            ) -> Self {
+                let mut scope = Scope::default();
+
+                $($var_name.add_to_scope(&mut scope, $lid_name);)+
+
+                scope
+            }
+        }
+    };
+}
+
+impl_scope_from_tuple!(la,va: VA, lb,vb: VB);
+impl_scope_from_tuple!(la,va: VA, lb,vb: VB, lc,vc: VC);
+
+pub trait ScopeItem {
+    /// Adds self to the given scope with the given [`LocalId`].
+    fn add_to_scope(&self, scope: &mut Scope, local_id: LocalId);
+}
+
+impl ScopeItem for i32 {
+    fn add_to_scope(&self, _: &mut Scope, _: LocalId) {
+        // Do nothing
+    }
+}

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

@@ -0,0 +1,44 @@
+use std::sync::Arc;
+use std::sync::atomic::AtomicBool;
+use std::sync::atomic::Ordering;
+
+use super::RetentionChecker;
+use super::Scope;
+use crate::propagation::Domains;
+
+/// A [`ConsistencyChecker`] wrapper that skips the inner check when the associated constraint has
+/// been deleted.
+///
+/// The deletion flag is shared with the constraint owner (e.g. the nogood propagator). Setting the
+/// flag to `true` causes the checker to become a permanent no-op.
+#[derive(Debug, Clone)]
+pub struct SelfDisablingChecker<T> {
+    inner: T,
+    is_deleted: Arc<AtomicBool>,
+}
+
+impl<T> SelfDisablingChecker<T> {
+    /// Create a new self-disabling checker.
+    ///
+    /// The deletion flag can be obtained with [`SelfDisablingChecker::deletion_flag`].
+    pub fn new(checker: T) -> Self {
+        SelfDisablingChecker {
+            inner: checker,
+            is_deleted: Arc::new(AtomicBool::new(false)),
+        }
+    }
+
+    /// The deletion flag for this self-disabling checker.
+    pub fn deletion_flag(&self) -> Arc<AtomicBool> {
+        Arc::clone(&self.is_deleted)
+    }
+}
+
+impl<T: RetentionChecker + Clone> RetentionChecker for SelfDisablingChecker<T> {
+    fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool {
+        if self.is_deleted.load(Ordering::Relaxed) {
+            return true;
+        }
+        self.inner.check_retention(scope, domains)
+    }
+}