fix: detection of underflows and overflows for linear inequalities

pumpkin-solver/src/propagators/arithmetic/linear_less_or_equal.rs

@@ -56,6 +56,13 @@ where
                 *bound = context.lower_bound(&self.x[index]);
             });
     }
+
+    fn create_conflict_reason(&self, context: PropagationContext) -> PropositionalConjunction {
+        self.x
+            .iter()
+            .map(|var| predicate![var >= context.lower_bound(var)])
+            .collect()
+    }
 }
 
 impl<Var: 'static> Propagator for LinearLessOrEqualPropagator<Var>
@@ -88,12 +95,7 @@ where
         context: PropagationContext,
     ) -> Option<PropositionalConjunction> {
         if (self.c as i64) < self.lower_bound_left_hand_side {
-            let reason: PropositionalConjunction = self
-                .x
-                .iter()
-                .map(|var| predicate![var >= context.lower_bound(var)])
-                .collect();
-            Some(reason)
+            Some(self.create_conflict_reason(context))
         } else {
             None
         }
@@ -140,10 +142,28 @@ where
         }
 
         for (i, x_i) in self.x.iter().enumerate() {
-            let bound = (self.c as i64
-                - (self.lower_bound_left_hand_side - context.lower_bound(x_i) as i64))
-                .try_into()
-                .expect("Could not fit the lower-bound of lhs in an i32");
+            let bound = match TryInto::<i32>::try_into(self.lower_bound_left_hand_side) {
+                Ok(lower_bound_left_hand_side) => {
+                    self.c - (lower_bound_left_hand_side - context.lower_bound(x_i))
+                }
+                Err(_) if self.lower_bound_left_hand_side.is_positive() => {
+                    // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
+                    // overflow (hence the check that the lower-bound on the left-hand side is
+                    // positive)
+                    //
+                    // This means that the lower-bounds of the current variables will always be
+                    // higher than the right-hand side (with a maximum value of i32). We thus
+                    // return a conflict
+                    return Err(self.create_conflict_reason(context.as_readonly()).into());
+                }
+                Err(_) => {
+                    // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
+                    // underflow
+                    //
+                    // This means that the constraint is always satisfied
+                    return Ok(());
+                }
+            };
 
             if context.upper_bound(x_i) > bound {
                 let reason: PropositionalConjunction = self
@@ -177,10 +197,28 @@ where
             .sum::<i64>();
 
         for (i, x_i) in self.x.iter().enumerate() {
-            let bound = (self.c as i64
-                - (lower_bound_left_hand_side - context.lower_bound(x_i) as i64))
-                .try_into()
-                .expect("Could not fit the lower-bound of lhs in an i32");
+            let bound = match TryInto::<i32>::try_into(lower_bound_left_hand_side) {
+                Ok(lower_bound_left_hand_side) => {
+                    self.c - (lower_bound_left_hand_side - context.lower_bound(x_i))
+                }
+                Err(_) if lower_bound_left_hand_side.is_positive() => {
+                    // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
+                    // overflow (hence the check that the lower-bound on the left-hand side is
+                    // positive)
+                    //
+                    // This means that the lower-bounds of the current variables will always be
+                    // higher than the right-hand side (with a maximum value of i32). We thus
+                    // return a conflict
+                    return Err(self.create_conflict_reason(context.as_readonly()).into());
+                }
+                Err(_) => {
+                    // We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
+                    // underflow
+                    //
+                    // This means that the constraint is always satisfied
+                    return Ok(());
+                }
+            };
 
             if context.upper_bound(x_i) > bound {
                 let reason: PropositionalConjunction = self
@@ -242,4 +280,28 @@ mod tests {
 
         assert_eq!(conjunction!([x >= 1]), reason);
     }
+
+    #[test]
+    fn overflow_leads_to_conflict() {
+        let mut solver = TestSolver::default();
+
+        let x = solver.new_variable(i32::MAX, i32::MAX);
+        let y = solver.new_variable(1, 1);
+
+        let _ = solver
+            .new_propagator(LinearLessOrEqualPropagator::new([x, y].into(), i32::MAX))
+            .expect_err("Expected overflow to be detected");
+    }
+
+    #[test]
+    fn underflow_leads_to_no_propagation() {
+        let mut solver = TestSolver::default();
+
+        let x = solver.new_variable(i32::MIN, i32::MIN);
+        let y = solver.new_variable(-1, -1);
+
+        let _ = solver
+            .new_propagator(LinearLessOrEqualPropagator::new([x, y].into(), i32::MIN))
+            .expect("Expected no error to be detected");
+    }
 }