chore(eq): Update usage of equality theory for splitted version.

plaans · Mar 5, 2024 · fe2f4c6 · fe2f4c6
1 parent c2aaf73
commit fe2f4c6
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs
@@ -169,7 +169,7 @@ impl<Lbl: Label> Solver<Lbl> {
             ReifExpr::EqVal(a, b) => {
                 let (lb, ub) = self.model.state.bounds(*a);
                 let lit = if (lb..=ub).contains(b) {
-                    self.reasoners.eq.add_edge(*a, *b, &mut self.model)
+                    self.reasoners.eq.add_val_edge(*a, *b, &mut self.model)
                 } else {
                     Lit::FALSE
                 };
@@ -180,7 +180,7 @@ impl<Lbl: Label> Solver<Lbl> {
                 Ok(())
             }
             ReifExpr::NeqVal(a, b) => {
-                let lit = !self.reasoners.eq.add_edge(*a, *b, &mut self.model);
+                let lit = !self.reasoners.eq.add_val_edge(*a, *b, &mut self.model);
                 if lit != value {
                     self.add_clause([!value, lit], scope)?; // value => lit
                     self.add_clause([!lit, value], scope)?; // lit => value