Skip to content

Commit 909dba9

Browse files
fix: detection of underflows and overflows for linear inequalities
1 parent c2f7b19 commit 909dba9

File tree

1 file changed

+29
-27
lines changed

1 file changed

+29
-27
lines changed

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

Lines changed: 29 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -141,11 +141,9 @@ where
141141
return Err(conjunction.into());
142142
}
143143

144-
for (i, x_i) in self.x.iter().enumerate() {
145-
let bound = match TryInto::<i32>::try_into(self.lower_bound_left_hand_side) {
146-
Ok(lower_bound_left_hand_side) => {
147-
self.c - (lower_bound_left_hand_side - context.lower_bound(x_i))
148-
}
144+
let lower_bound_left_hand_side =
145+
match TryInto::<i32>::try_into(self.lower_bound_left_hand_side) {
146+
Ok(bound) => bound,
149147
Err(_) if self.lower_bound_left_hand_side.is_positive() => {
150148
// We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
151149
// overflow (hence the check that the lower-bound on the left-hand side is
@@ -165,6 +163,9 @@ where
165163
}
166164
};
167165

166+
for (i, x_i) in self.x.iter().enumerate() {
167+
let bound = self.c - (lower_bound_left_hand_side - context.lower_bound(x_i));
168+
168169
if context.upper_bound(x_i) > bound {
169170
let reason: PropositionalConjunction = self
170171
.x
@@ -196,29 +197,30 @@ where
196197
.map(|var| context.lower_bound(var) as i64)
197198
.sum::<i64>();
198199

200+
let lower_bound_left_hand_side = match TryInto::<i32>::try_into(lower_bound_left_hand_side)
201+
{
202+
Ok(bound) => bound,
203+
Err(_) if self.lower_bound_left_hand_side.is_positive() => {
204+
// We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
205+
// overflow (hence the check that the lower-bound on the left-hand side is
206+
// positive)
207+
//
208+
// This means that the lower-bounds of the current variables will always be
209+
// higher than the right-hand side (with a maximum value of i32). We thus
210+
// return a conflict
211+
return Err(self.create_conflict_reason(context.as_readonly()).into());
212+
}
213+
Err(_) => {
214+
// We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
215+
// underflow
216+
//
217+
// This means that the constraint is always satisfied
218+
return Ok(());
219+
}
220+
};
221+
199222
for (i, x_i) in self.x.iter().enumerate() {
200-
let bound = match TryInto::<i32>::try_into(lower_bound_left_hand_side) {
201-
Ok(lower_bound_left_hand_side) => {
202-
self.c - (lower_bound_left_hand_side - context.lower_bound(x_i))
203-
}
204-
Err(_) if lower_bound_left_hand_side.is_positive() => {
205-
// We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
206-
// overflow (hence the check that the lower-bound on the left-hand side is
207-
// positive)
208-
//
209-
// This means that the lower-bounds of the current variables will always be
210-
// higher than the right-hand side (with a maximum value of i32). We thus
211-
// return a conflict
212-
return Err(self.create_conflict_reason(context.as_readonly()).into());
213-
}
214-
Err(_) => {
215-
// We cannot fit the `lower_bound_left_hand_side` into an i32 due to an
216-
// underflow
217-
//
218-
// This means that the constraint is always satisfied
219-
return Ok(());
220-
}
221-
};
223+
let bound = self.c - (lower_bound_left_hand_side - context.lower_bound(x_i));
222224

223225
if context.upper_bound(x_i) > bound {
224226
let reason: PropositionalConjunction = self

0 commit comments

Comments
 (0)