refactor(pumpkin-solver): Bulk create propagators before root propagation in FlatZinc reader

pumpkin-crates/constraints/src/constraints/all_different.rs

@@ -3,6 +3,7 @@ use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
 
 use super::binary_not_equals;
+use crate::EqualityConsistency;
 
 /// Creates the [`Constraint`] that enforces that all the given `variables` are distinct.
 pub fn all_different<Var: IntegerVariable + 'static>(
@@ -18,6 +19,7 @@ pub fn all_different<Var: IntegerVariable + 'static>(
                 variables[i].clone(),
                 variables[j].clone(),
                 constraint_tag,
+                EqualityConsistency::Bound,
             ));
         }
     }

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

@@ -1,9 +1,8 @@
-use pumpkin_core::ConstraintOperationError;
-use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::constraints::NegatableConstraint;
 use pumpkin_core::options::ReifiedPropagatorArgs;
 use pumpkin_core::proof::ConstraintTag;
+use pumpkin_core::state::State;
 use pumpkin_core::variables::IntegerVariable;
 use pumpkin_core::variables::Literal;
 use pumpkin_core::variables::TransformableVariable;
@@ -13,10 +12,23 @@ use pumpkin_propagators::arithmetic::LinearNotEqualPropagatorArgs;
 
 use super::less_than_or_equals;
 
+/// The requested consistency level.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum EqualityConsistency {
+    /// Use bound consistent propagation.
+    Bound,
+    /// If the constraint is over two variables, use domain consistent propagation.
+    ///
+    /// This is only useful when variables are actually equal. In the future this will likely
+    /// become a preprocessing step to unify the variables.
+    Domain,
+}
+
 struct EqualConstraint<Var> {
     terms: Box<[Var]>,
     rhs: i32,
     constraint_tag: ConstraintTag,
+    consistency: EqualityConsistency,
 }
 
 /// Creates the [`NegatableConstraint`] `∑ terms_i = rhs`.
@@ -26,11 +38,13 @@ pub fn equals<Var: IntegerVariable + Clone + 'static>(
     terms: impl Into<Box<[Var]>>,
     rhs: i32,
     constraint_tag: ConstraintTag,
+    consistency: EqualityConsistency,
 ) -> impl NegatableConstraint {
     EqualConstraint {
         terms: terms.into(),
         rhs,
         constraint_tag,
+        consistency,
     }
 }
 
@@ -41,18 +55,21 @@ pub fn binary_equals<Var: IntegerVariable + 'static>(
     lhs: Var,
     rhs: Var,
     constraint_tag: ConstraintTag,
+    consistency: EqualityConsistency,
 ) -> impl NegatableConstraint {
     EqualConstraint {
         terms: [lhs.scaled(1), rhs.scaled(-1)].into(),
         rhs: 0,
         constraint_tag,
+        consistency,
     }
 }
 
 struct NotEqualConstraint<Var> {
     terms: Box<[Var]>,
     rhs: i32,
     constraint_tag: ConstraintTag,
+    consistency: EqualityConsistency,
 }
 
 /// Create the [`NegatableConstraint`] `∑ terms_i != rhs`.
@@ -62,8 +79,9 @@ pub fn not_equals<Var: IntegerVariable + Clone + 'static>(
     terms: impl Into<Box<[Var]>>,
     rhs: i32,
     constraint_tag: ConstraintTag,
+    consistency: EqualityConsistency,
 ) -> impl NegatableConstraint {
-    equals(terms, rhs, constraint_tag).negation()
+    equals(terms, rhs, constraint_tag, consistency).negation()
 }
 
 /// Creates the [`NegatableConstraint`] `lhs != rhs`.
@@ -73,67 +91,61 @@ pub fn binary_not_equals<Var: IntegerVariable + 'static>(
     lhs: Var,
     rhs: Var,
     constraint_tag: ConstraintTag,
+    consistency: EqualityConsistency,
 ) -> impl NegatableConstraint {
     NotEqualConstraint {
         terms: [lhs.scaled(1), rhs.scaled(-1)].into(),
         rhs: 0,
         constraint_tag,
+        consistency,
     }
 }
 
 impl<Var> Constraint for EqualConstraint<Var>
 where
     Var: IntegerVariable + Clone + 'static,
 {
-    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
-        if self.terms.len() == 2 && !solver.is_logging_proof() {
-            let _ = solver.add_propagator(BinaryEqualsPropagatorArgs {
+    fn post(self, state: &mut State) {
+        if self.terms.len() == 2 && self.consistency == EqualityConsistency::Domain {
+            let _ = state.add_propagator(BinaryEqualsPropagatorArgs {
                 a: self.terms[0].clone(),
                 b: self.terms[1].scaled(-1).offset(self.rhs),
                 constraint_tag: self.constraint_tag,
-            })?;
+            });
         } else {
-            less_than_or_equals(self.terms.clone(), self.rhs, self.constraint_tag).post(solver)?;
+            less_than_or_equals(self.terms.clone(), self.rhs, self.constraint_tag).post(state);
 
             let negated = self
                 .terms
                 .iter()
                 .map(|var| var.scaled(-1))
                 .collect::<Box<[_]>>();
-            less_than_or_equals(negated, -self.rhs, self.constraint_tag).post(solver)?;
+            less_than_or_equals(negated, -self.rhs, self.constraint_tag).post(state);
         }
-
-        Ok(())
     }
 
-    fn implied_by(
-        self,
-        solver: &mut Solver,
-        reification_literal: Literal,
-    ) -> Result<(), ConstraintOperationError> {
-        if self.terms.len() == 2 && !solver.is_logging_proof() {
-            let _ = solver.add_propagator(ReifiedPropagatorArgs {
+    fn implied_by(self, state: &mut State, reification_literal: Literal) {
+        if self.terms.len() == 2 && self.consistency == EqualityConsistency::Domain {
+            let _ = state.add_propagator(ReifiedPropagatorArgs {
                 propagator: BinaryEqualsPropagatorArgs {
                     a: self.terms[0].clone(),
                     b: self.terms[1].scaled(-1).offset(self.rhs),
                     constraint_tag: self.constraint_tag,
                 },
                 reification_literal,
-            })?;
+            });
         } else {
             less_than_or_equals(self.terms.clone(), self.rhs, self.constraint_tag)
-                .implied_by(solver, reification_literal)?;
+                .implied_by(state, reification_literal);
 
             let negated = self
                 .terms
                 .iter()
                 .map(|var| var.scaled(-1))
                 .collect::<Box<[_]>>();
             less_than_or_equals(negated, -self.rhs, self.constraint_tag)
-                .implied_by(solver, reification_literal)?;
+                .implied_by(state, reification_literal);
         }
-
-        Ok(())
     }
 }
 
@@ -148,6 +160,7 @@ where
             terms: self.terms.clone(),
             rhs: self.rhs,
             constraint_tag: self.constraint_tag,
+            consistency: self.consistency,
         }
     }
 }
@@ -156,59 +169,54 @@ impl<Var> Constraint for NotEqualConstraint<Var>
 where
     Var: IntegerVariable + Clone + 'static,
 {
-    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
+    fn post(self, state: &mut State) {
         let NotEqualConstraint {
             terms,
             rhs,
             constraint_tag,
+            consistency: _,
         } = self;
 
         if terms.len() == 2 {
-            let _ = solver.add_propagator(BinaryNotEqualsPropagatorArgs {
+            let _ = state.add_propagator(BinaryNotEqualsPropagatorArgs {
                 a: terms[0].clone(),
                 b: terms[1].scaled(-1).offset(self.rhs),
                 constraint_tag: self.constraint_tag,
-            })?;
-
-            Ok(())
+            });
         } else {
             LinearNotEqualPropagatorArgs {
                 terms: terms.into(),
                 rhs,
                 constraint_tag,
             }
-            .post(solver)
+            .post(state)
         }
     }
 
-    fn implied_by(
-        self,
-        solver: &mut Solver,
-        reification_literal: Literal,
-    ) -> Result<(), ConstraintOperationError> {
+    fn implied_by(self, state: &mut State, reification_literal: Literal) {
         let NotEqualConstraint {
             terms,
             rhs,
             constraint_tag,
+            consistency: _,
         } = self;
 
         if terms.len() == 2 {
-            let _ = solver.add_propagator(ReifiedPropagatorArgs {
+            let _ = state.add_propagator(ReifiedPropagatorArgs {
                 propagator: BinaryNotEqualsPropagatorArgs {
                     a: terms[0].clone(),
                     b: terms[1].scaled(-1).offset(self.rhs),
                     constraint_tag: self.constraint_tag,
                 },
                 reification_literal,
-            })?;
-            Ok(())
+            });
         } else {
             LinearNotEqualPropagatorArgs {
                 terms: terms.into(),
                 rhs,
                 constraint_tag,
             }
-            .implied_by(solver, reification_literal)
+            .implied_by(state, reification_literal)
         }
     }
 }
@@ -224,6 +232,7 @@ where
             terms: self.terms.clone(),
             rhs: self.rhs,
             constraint_tag: self.constraint_tag,
+            consistency: self.consistency,
         }
     }
 }

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

@@ -1,8 +1,7 @@
-use pumpkin_core::ConstraintOperationError;
-use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::constraints::NegatableConstraint;
 use pumpkin_core::proof::ConstraintTag;
+use pumpkin_core::state::State;
 use pumpkin_core::variables::IntegerVariable;
 use pumpkin_core::variables::Literal;
 use pumpkin_propagators::arithmetic::LinearLessOrEqualPropagatorArgs;
@@ -107,26 +106,22 @@ struct Inequality<Var> {
 }
 
 impl<Var: IntegerVariable + 'static> Constraint for Inequality<Var> {
-    fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
+    fn post(self, state: &mut State) {
         LinearLessOrEqualPropagatorArgs {
             x: self.terms,
             c: self.rhs,
             constraint_tag: self.constraint_tag,
         }
-        .post(solver)
+        .post(state)
     }
 
-    fn implied_by(
-        self,
-        solver: &mut Solver,
-        reification_literal: Literal,
-    ) -> Result<(), ConstraintOperationError> {
+    fn implied_by(self, state: &mut State, reification_literal: Literal) {
         LinearLessOrEqualPropagatorArgs {
             x: self.terms,
             c: self.rhs,
             constraint_tag: self.constraint_tag,
         }
-        .implied_by(solver, reification_literal)
+        .implied_by(state, reification_literal)
     }
 }
 
@@ -141,38 +136,3 @@ impl<Var: IntegerVariable + 'static> NegatableConstraint for Inequality<Var> {
         }
     }
 }
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    #[test]
-    fn less_than_conflict() {
-        let mut solver = Solver::default();
-
-        let constraint_tag = solver.new_constraint_tag();
-        let x = solver.new_named_bounded_integer(0, 0, "x");
-
-        let result = less_than([x], 0, constraint_tag).post(&mut solver);
-        assert_eq!(
-            result,
-            Err(ConstraintOperationError::InfeasiblePropagator),
-            "Expected {result:?} to be an `InfeasiblePropagator` error"
-        );
-    }
-
-    #[test]
-    fn greater_than_conflict() {
-        let mut solver = Solver::default();
-
-        let constraint_tag = solver.new_constraint_tag();
-        let x = solver.new_named_bounded_integer(0, 0, "x");
-
-        let result = greater_than([x], 0, constraint_tag).post(&mut solver);
-        assert_eq!(
-            result,
-            Err(ConstraintOperationError::InfeasiblePropagator),
-            "Expected {result:?} to be an `InfeasiblePropagator` error"
-        );
-    }
-}

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

@@ -18,7 +18,12 @@ pub fn plus<Var: IntegerVariable + 'static>(
     c: Var,
     constraint_tag: ConstraintTag,
 ) -> impl Constraint {
-    equals([a.scaled(1), b.scaled(1), c.scaled(-1)], 0, constraint_tag)
+    equals(
+        [a.scaled(1), b.scaled(1), c.scaled(-1)],
+        0,
+        constraint_tag,
+        EqualityConsistency::Bound,
+    )
 }
 
 /// Creates the [`Constraint`] `a * b = c`.