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

.github/workflows/ci.yml

@@ -26,7 +26,7 @@ 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
+    - run: cargo test --release --no-fail-fast --features pumpkin-solver/all-propagator-checks
 
   wasm-test:
     name: Test Suite for pumpkin-core in WebAssembly

Cargo.toml

@@ -9,6 +9,7 @@ members = [
 
     "./pumpkin-crates/*", # Core libraries of the solver
     "./pumpkin-solver", # The solver binary
+    "./pumpkin-proof-processor", # The proof processor
     "./pumpkin-checker", # The uncertified proof checker
     "./pumpkin-solver-py", # The python interface
     "./pumpkin-macros", # Proc-macros used by the pumpkin source (unpublished)

clippy.toml

@@ -1,4 +1,6 @@
 allowed-duplicate-crates = [
     "hashbrown", 
     "windows-sys",
+    "regex-syntax",
+    "regex-automata",
 ]

minizinc/lib/fzn_circuit.mzn

@@ -0,0 +1,5 @@
+predicate pumpkin_circuit(array[int] of var int: next);
+
+predicate fzn_circuit(array[int] of var int: next) =
+    pumpkin_circuit(next);
+

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-checker/src/inferences/mod.rs

@@ -46,7 +46,7 @@ pub enum InvalidInference {
     UndefinedConstraint,
 
     /// The inference does not state which constraint generated it.
-    #[error("missing constraint hint")]
+    #[error("the constraint hint points to an unknown constraint ID")]
     MissingConstraint,
 
     /// The premises of the inference are inconsistent.

pumpkin-crates/checking/src/atomic_constraint.rs

@@ -87,3 +87,30 @@ impl AtomicConstraint for TestAtomic {
         }
     }
 }
+
+#[macro_export]
+macro_rules! test_atom {
+    [@to_comparison ==] => {
+        $crate::Comparison::Equal
+    };
+
+    [@to_comparison !=] => {
+        $crate::Comparison::NotEqual
+    };
+
+    [@to_comparison >=] => {
+        $crate::Comparison::GreaterEqual
+    };
+
+    [@to_comparison <=] => {
+        $crate::Comparison::LessEqual
+    };
+
+    [$name:ident $token:tt $bound:expr] => {
+        $crate::TestAtomic {
+            name: stringify!($name),
+            comparison: test_atom!(@to_comparison $token),
+            value: $bound,
+        }
+    };
+}

pumpkin-crates/core/Cargo.toml

@@ -22,7 +22,7 @@ once_cell = "1.19.0"
 downcast-rs = "1.2.1"
 drcp-format = { version = "0.3.1", path = "../../drcp-format" }
 convert_case = "0.8.0"
-itertools = "0.13.0"
+itertools = "0.14.0"
 bitfield-struct = "0.9.2"
 num = "0.4.3"
 enum-map = "2.7.3"
@@ -40,5 +40,8 @@ wasm-bindgen-test = "0.3"
 
 [features]
 check-propagations = []
+check-consistency = []
+all-propagator-checks = ["check-propagations", "check-consistency"]
+
 debug-checks = []
 clap = ["dep:clap"]

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

@@ -120,6 +120,7 @@ pub mod state {
     //! See [`State`] for more information.
     pub use crate::api::solver::PropagatorHandle;
     pub use crate::basic_types::PropagatorConflict;
+    pub use crate::engine::CheckersToRun;
     pub use crate::engine::Conflict;
     pub use crate::engine::EmptyDomain;
     pub use crate::engine::EmptyDomainConflict;

pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs

@@ -32,7 +32,6 @@ use crate::propagation::HasAssignments;
 use crate::propagators::nogoods::NogoodChecker;
 use crate::propagators::nogoods::NogoodPropagator;
 use crate::pumpkin_assert_eq_simple;
-use crate::state::EmptyDomain;
 use crate::state::PropagatorHandle;
 
 /// Used during conflict analysis to provide the necessary information.
@@ -70,8 +69,9 @@ impl ConflictAnalysisContext<'_> {
     /// Returns `true` if a change to a domain occured, and `false` if the given [`Predicate`] was
     /// already true.
     ///
-    /// If a domain becomes empty due to this operation, an [`EmptyDomain`] error is returned.
-    pub fn post(&mut self, predicate: Predicate) -> Result<bool, EmptyDomain> {
+    /// If a domain becomes empty due to this operation, an [`EmptyDomainConflict`] error is
+    /// returned.
+    pub fn post(&mut self, predicate: Predicate) -> Result<bool, EmptyDomainConflict> {
         self.state.post(predicate)
     }
 
@@ -272,13 +272,16 @@ impl ConflictAnalysisContext<'_> {
         reason_buffer: &mut (impl Extend<Predicate> + AsRef<[Predicate]>),
         state: &mut State,
     ) {
-        let trail_index = state.get_propagation_reason(predicate, reason_buffer, current_nogood);
+        let inference_code = state.get_propagation_reason(predicate, reason_buffer, current_nogood);
 
-        if let Some(trail_index) = trail_index {
+        if inference_code.is_some() {
+            let trail_index = state.trail_position(predicate).expect(
+                "an inference code is only present if the propagated predicate is on the trail",
+            );
             let trail_entry = state.assignments.get_trail_entry(trail_index);
-            let (reason_ref, inference_code) = trail_entry
-                .reason
-                .expect("Cannot be a null reason for propagation.");
+            let Some((reason_ref, inference_code)) = trail_entry.reason else {
+                return;
+            };
 
             let propagator_id = state.reason_store.get_propagator(reason_ref);
 
@@ -338,7 +341,7 @@ impl ConflictAnalysisContext<'_> {
         // The reason for changing the bound cannot be a decision, so we can safely unwrap.
         let mut empty_domain_reason: Vec<Predicate> = vec![];
         let _ = self.state.reason_store.get_or_compute(
-            conflict.trigger_reason,
+            conflict.trigger_reason.expect("in conflict analysis the empty domain conflict is always triggered by a propagation"),
             ExplanationContext::without_working_nogood(
                 &self.state.assignments,
                 self.state.assignments.num_trail_entries(), // Note that we do not do a
@@ -353,7 +356,7 @@ impl ConflictAnalysisContext<'_> {
         // We also need to log this last propagation to the proof log as an inference.
         let _ = self.proof_log.log_inference(
             &mut self.state.constraint_tags,
-            conflict.trigger_inference_code,
+            conflict.trigger_inference_code.expect("in conflict analysis the empty domain conflict is always triggered by a propagation"),
             empty_domain_reason.iter().copied(),
             Some(conflict.trigger_predicate),
             &self.state.variable_names,

pumpkin-crates/core/src/containers/keyed_vec.rs

@@ -46,6 +46,17 @@ impl<Key: StorageKey, Value> KeyedVec<Key, Value> {
         self.elements.get(key.index())
     }
 
+    pub fn get_mut(&mut self, key: Key) -> Option<&mut Value> {
+        self.elements.get_mut(key.index())
+    }
+
+    pub fn pop(&mut self) -> Option<(Key, Value)> {
+        self.elements.pop().map(|value| {
+            let key = Key::create_from_index(self.elements.len());
+            (key, value)
+        })
+    }
+
     pub fn len(&self) -> usize {
         self.elements.len()
     }