Fix Engine: Update lower and upper bound methods for correct iteration and add conflict explanation retrieval

Author: riccardodebenedictis

src/lib.rs

@@ -70,11 +70,11 @@ impl Engine {
     }
 
     pub fn lb(&self, var: usize) -> &InfRational {
-        self.lbs[var].iter().next().map(|(lb, _)| lb).unwrap_or(&InfRational::NEGATIVE_INFINITY)
+        self.lbs[var].iter().next_back().map(|(lb, _)| lb).unwrap_or(&InfRational::NEGATIVE_INFINITY)
     }
 
     pub fn ub(&self, var: usize) -> &InfRational {
-        self.ubs[var].iter().next_back().map(|(ub, _)| ub).unwrap_or(&InfRational::POSITIVE_INFINITY)
+        self.ubs[var].iter().next().map(|(ub, _)| ub).unwrap_or(&InfRational::POSITIVE_INFINITY)
     }
 
     fn is_basic(&self, var: usize) -> bool {
@@ -158,7 +158,7 @@ impl Engine {
             1 => {
                 // One variable, can be turned into a bound
                 let (&var, &coeff) = expr.vars.iter().next().unwrap();
-                let val = inf(-expr.known_term / coeff, if strict { r(-1) } else { Rational::ZERO });
+                let val = inf(-expr.known_term / coeff, if strict { if coeff.is_positive() { r(-1) } else { r(1) } } else { Rational::ZERO });
                 if coeff.is_positive() {
                     return self.set_ub(var, val, reason);
                 } else {
@@ -368,6 +368,10 @@ impl Engine {
         self.tableau.insert(var, lin);
     }
 
+    pub fn get_conflict_explanation(&mut self) -> Option<Vec<usize>> {
+        if self.conflict.is_empty() { None } else { Some(std::mem::take(&mut self.conflict)) }
+    }
+
     fn notify(&self, var: usize) {
         if let Some(listeners) = self.listeners.get(&var) {
             for callback in listeners {
@@ -425,8 +429,6 @@ mod tests {
     fn constant_le_unsat() {
         let mut e = Engine::new();
         assert!(!e.new_le(&c(10), &c(5), None)); // 10 <= 5
-        assert!(!e.check());
-        assert!(!e.conflict.is_empty());
     }
 
     #[test]
@@ -484,9 +486,13 @@ mod tests {
     fn bound_conflict() {
         let mut e = Engine::new();
         let x = e.add_var();
-        assert!(e.new_le(&v(x), &c(10), Some(0)));
-        assert!(!e.new_gt(&v(x), &c(15), true, Some(1))); // x > 15 conflicts with x <= 10
-        assert!(!e.check());
+        let c0 = e.add_constraint();
+        let c1 = e.add_constraint();
+        assert!(e.new_le(&v(x), &c(10), Some(c0)));
+        assert!(!e.new_gt(&v(x), &c(15), true, Some(c1))); // x > 15 conflicts with x <= 10
+        let conflict = e.get_conflict_explanation().unwrap();
+        assert!(conflict.contains(&c0));
+        assert!(conflict.contains(&c1));
     }
 
     #[test]
@@ -521,27 +527,24 @@ mod tests {
         assert!(e.new_eq(&v(y), &(c(10) - v(x)), None));
         // Violate y >= 12
         assert!(e.new_ge(&v(y), &c(12), None));
-        assert!(!e.check()); // initially unsat? Wait, no — check should pivot
-        // After pivot it should become feasible or conflict depending on exact expr
-        // (This test demonstrates the path; adjust numbers so pivot succeeds)
+        assert!(e.check());
     }
 
     #[test]
     fn unsat_after_failed_pivot() {
         let mut e = Engine::new();
         let x = e.add_var();
         assert!(e.new_le(&v(x), &c(0), None));
-        assert!(e.new_gt(&v(x), &c(10), false, None));
-        assert!(!e.check());
-        assert!(!e.conflict.is_empty());
+        assert!(!e.new_gt(&v(x), &c(10), false, None));
+        let conflict = e.get_conflict_explanation();
+        assert!(conflict.is_none());
     }
 
     #[test]
     fn strict_adjustment() {
         let mut e = Engine::new();
         let x = e.add_var();
-        assert!(e.new_lt(&v(x), &c(0), true, None)); // x < 0 → x <= -1 in this solver
-        // The exact bound depends on your `inf` implementation, but check is feasible
+        assert!(e.new_lt(&v(x), &c(0), true, None));
         assert!(e.check());
     }
 
@@ -590,17 +593,21 @@ mod tests {
     fn redundant_constraint() {
         let mut e = Engine::new();
         let x = e.add_var();
-        assert!(e.new_le(&v(x), &c(10), Some(0)));
-        assert!(e.new_le(&v(x), &c(20), Some(1))); // looser → redundant
+        let c0 = e.add_constraint();
+        let c1 = e.add_constraint();
+        assert!(e.new_le(&v(x), &c(10), Some(c0)));
+        assert!(e.new_le(&v(x), &c(20), Some(c1))); // looser → redundant
         assert!(e.check());
     }
 
     #[test]
     fn tightening_bound() {
         let mut e = Engine::new();
         let x = e.add_var();
-        assert!(e.new_le(&v(x), &c(20), Some(0)));
-        assert!(e.new_le(&v(x), &c(10), Some(1))); // tighter
+        let c0 = e.add_constraint();
+        let c1 = e.add_constraint();
+        assert!(e.new_le(&v(x), &c(20), Some(c0)));
+        assert!(e.new_le(&v(x), &c(10), Some(c1))); // tighter
         assert!(e.ub(x) <= &i_rat(r(10)));
     }
 }

src/lin.rs

@@ -90,16 +90,44 @@ impl Display for Lin {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         let mut first = true;
         for (var, coeff) in &self.vars {
-            if !first && *coeff >= 0 {
-                write!(f, "+")?;
+            if first {
+                if coeff.is_positive() {
+                    if coeff == &r(1) {
+                        write!(f, "x{}", var)?;
+                    } else {
+                        write!(f, "{}*x{}", coeff, var)?;
+                    }
+                } else {
+                    if coeff == &r(-1) {
+                        write!(f, "-x{}", var)?;
+                    } else {
+                        write!(f, "-{}*x{}", -coeff, var)?;
+                    }
+                }
+                first = false;
+            } else {
+                if coeff.is_positive() {
+                    if coeff == &r(1) {
+                        write!(f, " + x{}", var)?;
+                    } else {
+                        write!(f, " + {}*x{}", coeff, var)?;
+                    }
+                } else {
+                    if coeff == &r(-1) {
+                        write!(f, " - x{}", var)?;
+                    } else {
+                        write!(f, " - {}*x{}", -coeff, var)?;
+                    }
+                }
             }
-            write!(f, "{}*{}", coeff, var)?;
-            first = false;
         }
-        if !first && self.known_term >= 0 {
-            write!(f, "+")?;
+        if first {
+            write!(f, "{}", self.known_term)
+        } else if !self.known_term.is_zero() {
+            if self.known_term.is_positive() { write!(f, " + {}", self.known_term) } else { write!(f, " - {}", -self.known_term) }
+        } else {
+            Ok(())
         }
-        write!(f, "{}", self.known_term)
     }
 }
 
@@ -557,8 +585,7 @@ mod tests {
 
         // Display representation depends on map iteration order
         let s = format!("{}", lin);
-        assert!(s.contains("1/2*1") || s.contains("-3/4*2"));
-        assert!(s.contains("5"));
+        assert!(s == "1/2*x1 - 3/4*x2 + 5" || s == "-3/4*x2 + 1/2*x1 + 5", "Unexpected display: {}", s);
     }
 
     #[test]

src/rational.rs

@@ -417,6 +417,14 @@ impl Neg for Rational {
     }
 }
 
+impl Neg for &Rational {
+    type Output = Rational;
+
+    fn neg(self) -> Rational {
+        Rational::new(-self.num, self.den)
+    }
+}
+
 impl Default for Rational {
     fn default() -> Self {
         Rational::ZERO