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-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/Cargo.toml

@@ -30,6 +30,7 @@ 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"
 
 [target.'cfg(target_arch = "wasm32")'.dependencies]
 web-time = "1.1"
@@ -39,6 +40,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

@@ -70,8 +70,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 From<PropositionalConjunction> for Box<[Predicate]> {
+    fn from(val: PropositionalConjunction) -> Self {
+        val.predicates_in_conjunction.into()
+    }
+}
+
 impl PropositionalConjunction {
     pub fn new(predicates_in_conjunction: Vec<Predicate>) -> Self {
         PropositionalConjunction {

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

@@ -1,3 +1,13 @@
+mod propagation_checker;
+mod retention_checker;
+mod retention_store;
+mod scope;
+mod self_disabling;
 mod store;
 
+pub use propagation_checker::*;
+pub use retention_checker::*;
+pub use retention_store::*;
+pub use scope::*;
+pub use self_disabling::*;
 pub use store::*;

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,43 @@
+use std::fmt::Debug;
+
+use dyn_clone::DynClone;
+
+use crate::checkers::Scope;
+use crate::propagation::Domains;
+
+/// A runtime verifier that determines whether a propagator has nothing left to propagate.
+///
+/// The contract mirrors the retention conditions of the formally verified proof checker: in the
+/// current domains no inference of the propagator's rule applies, i.e. giving any variable in
+/// the scope any value of its domain does not let the rule report a conflict. Each propagator
+/// supplies its own checker, which may exploit the structure of its rule to decide this cheaply.
+pub trait RetentionChecker: Debug + DynClone {
+    /// Returns `true` if the propagator has nothing left to propagate in `domains`, and `false`
+    /// if some inference of its rule still applies.
+    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/retention_store.rs

@@ -0,0 +1,90 @@
+use crate::checkers::BoxedRetentionChecker;
+use crate::checkers::Scope;
+use crate::containers::KeyedBitSet;
+use crate::containers::KeyedVec;
+use crate::containers::StorageKey;
+use crate::propagation::Domains;
+use crate::variables::DomainId;
+
+/// Holds the retention checkers in the solver.
+///
+/// Also responsible for enqueueing the checkers and dispatching them when instructed via
+/// [`RetentionCheckerStore::run_enqueued`].
+#[derive(Clone, Debug, Default)]
+pub struct RetentionCheckerStore {
+    /// The checkers in the store.
+    store: KeyedVec<CheckerId, (Scope, BoxedRetentionChecker)>,
+    /// Map from [`DomainId`] to the relevant checkers via their ID.
+    watch_list: KeyedVec<DomainId, Vec<CheckerId>>,
+    /// The checkers to run the next time.
+    queue: Vec<CheckerId>,
+    /// Marks which checkers are enqueued to prevent duplicate checkers in
+    /// [`RetentionCheckerStore::queue`].
+    enqueued: KeyedBitSet<CheckerId>,
+}
+
+impl RetentionCheckerStore {
+    /// Add a new `checker` to the store with the given `scope`.
+    pub fn register(&mut self, scope: Scope, checker: BoxedRetentionChecker) {
+        let checker_slot = self.store.new_slot();
+
+        for (_, domain) in scope.domains() {
+            self.watch_list.accomodate(domain, vec![]);
+            self.watch_list[domain].push(checker_slot.key());
+        }
+
+        let _ = checker_slot.populate((scope, checker));
+    }
+
+    /// Called when the domain is modified.
+    ///
+    /// Causes the checkers for this domain to be enqueued.
+    pub fn on_domain_event(&mut self, domain_id: DomainId) {
+        let Some(list) = self.watch_list.get(domain_id) else {
+            return;
+        };
+
+        for &checker_id in list {
+            if !self.enqueued.insert(checker_id) {
+                continue;
+            }
+
+            self.queue.push(checker_id);
+        }
+    }
+
+    /// Run the enqueued retention checkers.
+    pub fn run_enqueued(&mut self, mut domains: Domains<'_>) -> bool {
+        for checker_id in self.queue.drain(..) {
+            assert!(self.enqueued.remove(checker_id));
+
+            let (scope, checker) = &mut self.store[checker_id];
+
+            if !checker.check_retention(scope, domains.reborrow()) {
+                return false;
+            }
+        }
+
+        true
+    }
+
+    /// Clear the queue of retention checkers.
+    pub fn clear_queue(&mut self) {
+        self.queue.clear();
+        self.enqueued.clear();
+    }
+}
+
+/// An identifier for added checkers.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
+struct CheckerId(u32);
+
+impl StorageKey for CheckerId {
+    fn index(&self) -> usize {
+        self.0 as usize
+    }
+
+    fn create_from_index(index: usize) -> Self {
+        CheckerId(index as u32)
+    }
+}