(&mut self, cst: &LinearConstraint)
| 369 | } |
| 370 | |
| 371 | fn add_constraint(&mut self, cst: &LinearConstraint) { |
| 372 | if cst.is_contradiction() { |
| 373 | self.set_to_bottom(); |
| 374 | return; |
| 375 | } |
| 376 | if cst.is_tautology() { |
| 377 | return; |
| 378 | } |
| 379 | match cst { |
| 380 | LinearConstraint::Equality(expr) => self.refine_equality(expr), |
| 381 | LinearConstraint::LessEq(expr) => self.refine_less_equal(expr), |
| 382 | LinearConstraint::LessThan(_) => { |
| 383 | let non_strict = cst.strict_to_non_strict(); |
| 384 | if let LinearConstraint::LessEq(expr) = non_strict { |
| 385 | self.refine_less_equal(&expr); |
| 386 | } |
| 387 | } |
| 388 | LinearConstraint::Inequality(_) => {} |
| 389 | } |
| 390 | } |
| 391 | |
| 392 | fn refine_equality(&mut self, expr: &LinearExpression) { |
| 393 | if let Some((path, low, high)) = interval_from_unary_expr(expr) { |
no test coverage detected