Fix Engine: Add method to assign linear variables and update references to value retrieval

Author: riccardodebenedictis

src/lib.rs

@@ -59,13 +59,20 @@ impl Engine {
         index
     }
 
+    pub fn add_lin_var(&mut self, lin: Lin) -> usize {
+        let index = self.add_var();
+        self.assignments[index] = self.lin_val(&lin);
+        self.new_row(index, lin);
+        index
+    }
+
     pub fn add_constraint(&mut self) -> usize {
         let index = self.constraints.len();
         self.constraints.push(Constraint { lbs: HashMap::new(), ubs: HashMap::new() });
         index
     }
 
-    pub fn value(&self, var: usize) -> &InfRational {
+    pub fn val(&self, var: usize) -> &InfRational {
         &self.assignments[var]
     }
 
@@ -80,7 +87,7 @@ impl Engine {
     pub fn lin_val(&self, lin: &Lin) -> InfRational {
         let mut result = i_rat(lin.known_term);
         for (&var, &coeff) in &lin.vars {
-            result += coeff * self.value(var);
+            result += coeff * self.val(var);
         }
         result
     }
@@ -141,7 +148,7 @@ impl Engine {
         if let Some(reason) = reason {
             entry.insert(reason);
         }
-        if self.value(var) < &lb && !self.is_basic(var) {
+        if self.val(var) < &lb && !self.is_basic(var) {
             self.update(var, lb);
         }
 
@@ -176,7 +183,7 @@ impl Engine {
         if let Some(reason) = reason {
             entry.insert(reason);
         }
-        if self.value(var) > &ub && !self.is_basic(var) {
+        if self.val(var) > &ub && !self.is_basic(var) {
             self.update(var, ub);
         }
 
@@ -206,9 +213,7 @@ impl Engine {
             _ => {
                 // More than one variable, need to add a new tableau row
                 let val = inf(-std::mem::take(&mut expr.known_term), if strict { r(-1) } else { Rational::ZERO });
-                let slack = self.add_var();
-                self.assignments[slack] = self.lin_val(&expr);
-                self.new_row(slack, expr);
+                let slack = self.add_lin_var(expr);
                 self.set_ub(slack, val, reason)
             }
         }
@@ -241,9 +246,7 @@ impl Engine {
             _ => {
                 // More than one variable, need to add a new tableau row
                 let val = i_rat(-std::mem::take(&mut expr.known_term));
-                let slack = self.add_var();
-                self.assignments[slack] = self.lin_val(&expr);
-                self.new_row(slack, expr);
+                let slack = self.add_lin_var(expr);
                 self.set_lb(slack, val, reason) && self.set_ub(slack, val, reason)
             }
         }
@@ -266,7 +269,7 @@ impl Engine {
         assert!(&new_value >= self.lb(var) && &new_value <= self.ub(var), "New value must be within bounds");
 
         for &watch in &self.t_watches[var] {
-            let delta = self.tableau[&watch].vars[&var] * (new_value - self.value(var));
+            let delta = self.tableau[&watch].vars[&var] * (new_value - self.val(var));
             self.assignments[watch] += delta;
             self.notify(watch);
         }
@@ -279,18 +282,18 @@ impl Engine {
         loop {
             // we search for a basic variable whose value is not within its bounds..
             let var = self.tableau.iter().find_map(|(&var, _)| {
-                if self.value(var) < self.lb(var) {
+                if self.val(var) < self.lb(var) {
                     Some((var, *self.lb(var)))
-                } else if self.value(var) > self.ub(var) {
+                } else if self.val(var) > self.ub(var) {
                     Some((var, *self.ub(var)))
                 } else {
                     None
                 }
             });
             if let Some((leaving, val)) = var {
                 // .. if we find one, we try to pivot it with a non-basic variable that can take it back within bounds
-                if self.value(leaving) < &val {
-                    let entering = self.tableau[&leaving].vars.iter().find_map(|(&v, &coeff)| if coeff.is_positive() && self.value(v) < self.ub(v) || coeff.is_negative() && self.value(v) > self.lb(v) { Some(v) } else { None });
+                if self.val(leaving) < &val {
+                    let entering = self.tableau[&leaving].vars.iter().find_map(|(&v, &coeff)| if coeff.is_positive() && self.val(v) < self.ub(v) || coeff.is_negative() && self.val(v) > self.lb(v) { Some(v) } else { None });
                     if let Some(entering) = entering {
                         self.pivot_and_update(entering, leaving, val);
                     } else {
@@ -311,8 +314,8 @@ impl Engine {
                         return false;
                     }
                 }
-                if self.value(leaving) > &val {
-                    let entering = self.tableau[&leaving].vars.iter().find_map(|(&v, &coeff)| if coeff.is_positive() && self.value(v) > self.lb(v) || coeff.is_negative() && self.value(v) < self.ub(v) { Some(v) } else { None });
+                if self.val(leaving) > &val {
+                    let entering = self.tableau[&leaving].vars.iter().find_map(|(&v, &coeff)| if coeff.is_positive() && self.val(v) > self.lb(v) || coeff.is_negative() && self.val(v) < self.ub(v) { Some(v) } else { None });
                     if let Some(entering) = entering {
                         self.pivot_and_update(entering, leaving, val);
                     } else {
@@ -343,7 +346,7 @@ impl Engine {
         assert!(self.is_basic(leaving), "Leaving variable must be basic");
         assert!(!self.is_basic(entering), "Entering variable must be non-basic");
 
-        let theta = (new_value - self.value(leaving)) / &self.tableau[&leaving].vars[&entering];
+        let theta = (new_value - self.val(leaving)) / &self.tableau[&leaving].vars[&entering];
         self.assignments[leaving] = new_value;
         self.notify(leaving);
         self.assignments[entering] += theta;
@@ -454,7 +457,7 @@ impl Engine {
 impl Display for Engine {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         for i in 0..self.assignments.len() {
-            writeln!(f, "x{} = {}, [{}, {}]", i, self.value(i), self.lb(i), self.ub(i))?;
+            writeln!(f, "x{} = {}, [{}, {}]", i, self.val(i), self.lb(i), self.ub(i))?;
         }
         for (var, lin) in &self.tableau {
             writeln!(f, "x{} = {}", var, lin)?;
@@ -476,7 +479,7 @@ mod tests {
         let y = e.add_var();
         assert_eq!(x, 0);
         assert_eq!(y, 1);
-        assert_eq!(e.value(x), &InfRational::ZERO);
+        assert_eq!(e.val(x), &InfRational::ZERO);
         assert_eq!(e.lb(x), &InfRational::NEGATIVE_INFINITY);
         assert_eq!(e.ub(x), &InfRational::POSITIVE_INFINITY);
     }
@@ -542,7 +545,7 @@ mod tests {
         let x = e.add_var();
         assert!(e.new_eq(&v(x), &c(42), None));
         assert_eq!(e.lb(x), e.ub(x));
-        assert_eq!(e.value(x), &i_rat(r(42)));
+        assert_eq!(e.val(x), &i_rat(r(42)));
     }
 
     #[test]
@@ -623,7 +626,7 @@ mod tests {
 
         engine.set_listener(a, move |e, var| {
             assert_eq!(var, a);
-            assert_eq!(e.value(var), &i_rat(r(5)));
+            assert_eq!(e.val(var), &i_rat(r(5)));
             *called_clone.lock().unwrap() = true;
         });
 
@@ -725,6 +728,32 @@ mod tests {
         assert!(conflict.contains(&c2));
     }
 
+    #[test]
+    fn complex_conflict_explanation_generation() {
+        let mut e = Engine::new();
+        let x = e.add_var();
+        let y = e.add_var();
+        let s1 = e.add_lin_var(vc(x, -1) + vc(y, 1)); // s1 = y - x
+        let s2 = e.add_lin_var(vc(x, 1) + vc(y, 1)); // s2 = x + y
+
+        let c0 = e.add_constraint();
+        assert!(e.new_le(&v(x), &c(-4), Some(c0))); // x <= -4
+        assert!(e.check());
+        let c1 = e.add_constraint();
+        assert!(e.new_ge(&v(x), &c(-8), Some(c1))); // x >= -8
+        assert!(e.check());
+        let c2 = e.add_constraint();
+        assert!(e.new_le(&v(s1), &c(1), Some(c2))); // s1 <= 1
+        assert!(e.check());
+        let c3 = e.add_constraint();
+        assert!(e.new_ge(&v(s2), &c(-3), Some(c3))); // s2 >= -3
+        assert!(!e.check());
+        let conflict = e.get_conflict_explanation().unwrap();
+        assert!(conflict.contains(&c0));
+        assert!(conflict.contains(&c2));
+        assert!(conflict.contains(&c3));
+    }
+
     #[test]
     fn add_retract_readd() {
         let mut e = Engine::new();
@@ -735,7 +764,7 @@ mod tests {
         assert!(e.check());
         assert!(e.lb(x) == &i_rat(r(5)));
         assert!(e.ub(x) == &InfRational::POSITIVE_INFINITY);
-        assert!(e.value(x) >= &i_rat(r(5)));
+        assert!(e.val(x) >= &i_rat(r(5)));
 
         // Retract constraint
         e.retract(c0);
@@ -748,7 +777,7 @@ mod tests {
         assert!(e.check());
         assert!(e.lb(x) == &i_rat(r(5)));
         assert!(e.ub(x) == &InfRational::POSITIVE_INFINITY);
-        assert!(e.value(x) >= &i_rat(r(5)));
+        assert!(e.val(x) >= &i_rat(r(5)));
     }
 
     #[test]