feat(pumpkin-core): If the check-propagations flag is enabled, the state will run inference checkers on all propagations immediately

.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
+    - run: cargo test --release --no-fail-fast --features pumpkin-core/check-propagations
 
   wasm-test:
     name: Test Suite for pumpkin-core in WebAssembly

Cargo.toml

@@ -1,6 +1,18 @@
 [workspace]
-members = ["./pumpkin-solver", "./pumpkin-checker", "./drcp-format", "./pumpkin-solver-py", "./pumpkin-macros", "./drcp-debugger", "./pumpkin-crates/*", "./fzn-rs", "./fzn-rs-derive"]
 resolver = "2"
+members = [
+    # Libraries used by Pumpkin but in principle are independent
+    "./drcp-format", 
+    "./drcp-debugger", 
+    "./fzn-rs", 
+    "./fzn-rs-derive",
+
+    "./pumpkin-crates/*", # Core libraries of the solver
+    "./pumpkin-solver", # The solver binary
+    "./pumpkin-checker", # The uncertified proof checker
+    "./pumpkin-solver-py", # The python interface
+    "./pumpkin-macros", # Proc-macros used by the pumpkin source (unpublished)
+]
 
 [workspace.package]
 repository = "https://github.com/consol-lab/pumpkin"

clippy.toml

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

pumpkin-checker/Cargo.toml

@@ -7,6 +7,9 @@ license.workspace = true
 authors.workspace = true
 
 [dependencies]
+pumpkin-core = { version = "0.2.2", path = "../pumpkin-crates/core/" }
+pumpkin-checking = { version = "0.2.2", path = "../pumpkin-crates/checking/" }
+pumpkin-propagators = { version = "0.2.2", path = "../pumpkin-crates/propagators/" }
 anyhow = "1.0.99"
 clap = { version = "4.5.47", features = ["derive"] }
 drcp-format = { version = "0.3.0", path = "../drcp-format" }

pumpkin-checker/src/deductions.rs

@@ -3,10 +3,11 @@ use std::rc::Rc;
 
 use drcp_format::ConstraintId;
 use drcp_format::IntAtomic;
+use pumpkin_checking::AtomicConstraint;
+use pumpkin_checking::VariableState;
 
 use crate::inferences::Fact;
 use crate::model::Nogood;
-use crate::state::VariableState;
 
 /// An inference that was ignored when checking a deduction.
 #[derive(Clone, Debug)]
@@ -50,9 +51,11 @@ pub fn verify_deduction(
     // At some point, this should either reach a fact without a consequent or derive an
     // inconsistent domain.
 
-    let mut variable_state =
-        VariableState::prepare_for_conflict_check(&Fact::nogood(deduction.premises.clone()))
-            .ok_or(InvalidDeduction::InconsistentPremises)?;
+    let mut variable_state = VariableState::prepare_for_conflict_check(
+        deduction.premises.iter().cloned().map(Into::into),
+        None,
+    )
+    .ok_or(InvalidDeduction::InconsistentPremises)?;
 
     let mut unused_inferences = Vec::new();
 
@@ -75,9 +78,22 @@ pub fn verify_deduction(
                     // `String`. The former does not implement `Send`, but that is
                     // required for our error type to be used with anyhow.
                     Some(IntAtomic {
-                        name: String::from(premise.name.as_ref()),
-                        comparison: premise.comparison,
-                        value: premise.value,
+                        name: String::from(premise.identifier().as_ref()),
+                        comparison: match premise.comparison() {
+                            pumpkin_checking::Comparison::GreaterEqual => {
+                                drcp_format::IntComparison::GreaterEqual
+                            }
+                            pumpkin_checking::Comparison::LessEqual => {
+                                drcp_format::IntComparison::LessEqual
+                            }
+                            pumpkin_checking::Comparison::Equal => {
+                                drcp_format::IntComparison::Equal
+                            }
+                            pumpkin_checking::Comparison::NotEqual => {
+                                drcp_format::IntComparison::NotEqual
+                            }
+                        },
+                        value: premise.value(),
                     })
                 }
             })

pumpkin-checker/src/inferences/all_different.rs

@@ -1,9 +1,12 @@
 use std::collections::HashSet;
 
+use pumpkin_checking::CheckerVariable;
+use pumpkin_checking::VariableState;
+
 use super::Fact;
 use crate::inferences::InvalidInference;
+use crate::model::Atomic;
 use crate::model::Constraint;
-use crate::state::VariableState;
 
 /// Verify an `all_different` inference.
 ///
@@ -12,8 +15,9 @@ use crate::state::VariableState;
 ///
 /// The checker will reject inferences with redundant atomic constraints.
 pub(crate) fn verify_all_different(
-    fact: &Fact,
+    _: &Fact,
     constraint: &Constraint,
+    state: VariableState<Atomic>,
 ) -> Result<(), InvalidInference> {
     // This checker takes the union of the domains of the variables in the constraint. If there
     // are fewer values in the union of the domain than there are variables, then there is a
@@ -23,14 +27,11 @@ pub(crate) fn verify_all_different(
         return Err(InvalidInference::ConstraintLabelMismatch);
     };
 
-    let variable_state = VariableState::prepare_for_conflict_check(fact)
-        .ok_or(InvalidInference::InconsistentPremises)?;
-
     // Collect all values present in at least one of the domains.
     let union_of_domains = all_different
         .variables
         .iter()
-        .filter_map(|variable| variable_state.iter_domain(variable))
+        .filter_map(|variable| variable.iter_induced_domain(&state))
         .flatten()
         .collect::<HashSet<_>>();
 
@@ -40,7 +41,7 @@ pub(crate) fn verify_all_different(
     let num_variables = all_different
         .variables
         .iter()
-        .filter(|variable| variable_state.iter_domain(variable).is_some())
+        .filter(|variable| variable.iter_induced_domain(&state).is_some())
         .count();
 
     if union_of_domains.len() < num_variables {

pumpkin-checker/src/inferences/arithmetic.rs

@@ -1,16 +1,15 @@
 use std::collections::BTreeSet;
-use std::rc::Rc;
 
-use drcp_format::IntComparison;
-use fzn_rs::VariableExpr;
+use pumpkin_checking::CheckerVariable;
+use pumpkin_checking::InferenceChecker;
+use pumpkin_checking::VariableState;
+use pumpkin_propagators::arithmetic::BinaryEqualsChecker;
 
 use super::Fact;
 use crate::inferences::InvalidInference;
 use crate::model::AllDifferent;
 use crate::model::Atomic;
 use crate::model::Constraint;
-use crate::state::I32Ext;
-use crate::state::VariableState;
 
 /// Verify a `binary_equals` inference.
 ///
@@ -20,6 +19,7 @@ use crate::state::VariableState;
 pub(crate) fn verify_binary_equals(
     fact: &Fact,
     constraint: &Constraint,
+    state: VariableState<Atomic>,
 ) -> Result<(), InvalidInference> {
     // To check this inference we expect the intersection of both domains to be empty.
 
@@ -32,89 +32,34 @@ pub(crate) fn verify_binary_equals(
         return Err(InvalidInference::Unsound);
     }
 
-    let (weight_a, variable_a) = &linear.terms[0];
-    let (weight_b, variable_b) = &linear.terms[1];
+    let lhs = linear.terms[0].clone();
+    let rhs = linear.terms[1].clone();
 
-    // TODO: Generalize this rule to work with non-unit weights.
-    // At the moment we expect one term to have weight `-1` and the other term to have weight
-    // `1`.
-    if weight_a + weight_b != 0 || weight_a.abs() != 1 || weight_b.abs() != 1 {
-        return Err(InvalidInference::Unsound);
-    }
-
-    let mut variable_state = VariableState::prepare_for_conflict_check(fact)
-        .ok_or(InvalidInference::InconsistentPremises)?;
-
-    // We apply the domain of variable 2 to variable 1. If the state remains consistent, then
-    // the step is unsound!
-    let state_is_consistent = match variable_a {
-        VariableExpr::Identifier(var1) => {
-            let mut consistent = true;
+    let checker = BinaryEqualsChecker { lhs, rhs };
 
-            if let I32Ext::I32(value) = variable_state.upper_bound(variable_b) {
-                consistent &= variable_state.apply(&Atomic {
-                    name: Rc::clone(var1),
-                    comparison: IntComparison::LessEqual,
-                    value: linear.bound + value,
-                });
-            }
-
-            if let I32Ext::I32(value) = variable_state.lower_bound(variable_b) {
-                consistent &= variable_state.apply(&Atomic {
-                    name: Rc::clone(var1),
-                    comparison: IntComparison::GreaterEqual,
-                    value: linear.bound + value,
-                });
-            }
-
-            for value in variable_state.holes(variable_b).collect::<Vec<_>>() {
-                consistent &= variable_state.apply(&Atomic {
-                    name: Rc::clone(var1),
-                    comparison: IntComparison::NotEqual,
-                    value: linear.bound + value,
-                });
-            }
-
-            consistent
-        }
-
-        VariableExpr::Constant(value) => match variable_b {
-            VariableExpr::Identifier(var2) => variable_state.apply(&Atomic {
-                name: Rc::clone(var2),
-                comparison: IntComparison::NotEqual,
-                value: linear.bound + *value,
-            }),
-            VariableExpr::Constant(_) => panic!("Binary equals over two constants is unexpected."),
-        },
-    };
-
-    if state_is_consistent {
-        // The intersection of the domains should yield an inconsistent state for the
-        // inference to be sound.
-        return Err(InvalidInference::Unsound);
+    if checker.check(state, &fact.premises, fact.consequent.as_ref()) {
+        Ok(())
+    } else {
+        Err(InvalidInference::Unsound)
     }
-
-    Ok(())
 }
 
 /// Verify a `binary_not_equals` inference.
 ///
 /// Tests that the premise of the inference and the negation of the consequent force the linear sum
 /// to equal the right-hand side of the not equals constraint.
 pub(crate) fn verify_binary_not_equals(
-    fact: &Fact,
+    _: &Fact,
     constraint: &Constraint,
+    state: VariableState<Atomic>,
 ) -> Result<(), InvalidInference> {
     let Constraint::AllDifferent(AllDifferent { variables }) = constraint else {
         return Err(InvalidInference::ConstraintLabelMismatch);
     };
 
-    let variable_state = VariableState::prepare_for_conflict_check(fact)
-        .ok_or(InvalidInference::InconsistentPremises)?;
-
     let mut values = BTreeSet::new();
     for variable in variables {
-        let Some(value) = variable_state.fixed_value(variable) else {
+        let Some(value) = variable.induced_fixed_value(&state) else {
             continue;
         };