Returns an element that is "self && other".
(&self, other: Rc<SymbolicValue>)
| 542 | |
| 543 | /// Returns an element that is "self && other". |
| 544 | fn and(&self, other: Rc<SymbolicValue>) -> Rc<SymbolicValue> { |
| 545 | let self_bool = self.as_bool_if_known(); |
| 546 | if let Some(false) = self_bool { |
| 547 | // [false && other] -> false |
| 548 | return Rc::new(SymbolicValue::new_false()); |
| 549 | }; |
| 550 | let other_bool = other.as_bool_if_known(); |
| 551 | if let Some(false) = other_bool { |
| 552 | // [self && false] -> false |
| 553 | return Rc::new(SymbolicValue::new_false()); |
| 554 | }; |
| 555 | if self_bool.unwrap_or(false) { |
| 556 | if other_bool.unwrap_or(false) { |
| 557 | // [true && true] -> true |
| 558 | Rc::new(SymbolicValue::new_true()) |
| 559 | } else { |
| 560 | // [true && other] -> other |
| 561 | other |
| 562 | } |
| 563 | } else if other_bool.unwrap_or(false) || self.is_bottom() { |
| 564 | // [self && true] -> self |
| 565 | // [BOTTOM && other] -> BOTTOM |
| 566 | self.clone() |
| 567 | } else if other.is_bottom() { |
| 568 | // [self && BOTTOM] -> BOTTOM |
| 569 | other |
| 570 | } else { |
| 571 | match &self.expression { |
| 572 | Expression::And { left: x, right: y } => { |
| 573 | // [(x && y) && x] -> x && y |
| 574 | // [(x && y) && y] -> x && y |
| 575 | if *x == other || *y == other { |
| 576 | return self.clone(); |
| 577 | } |
| 578 | } |
| 579 | Expression::LogicalNot { operand } if *operand == other => { |
| 580 | // [!x && x] -> false |
| 581 | return Rc::new(SymbolicValue::new_false()); |
| 582 | } |
| 583 | Expression::Or { left: x, right: y } => { |
| 584 | // [(x || y) && x] -> x |
| 585 | // [(x || y) && y] -> y |
| 586 | if *x == other || *y == other { |
| 587 | return other; |
| 588 | } |
| 589 | if let Expression::LogicalNot { operand } = &other.expression { |
| 590 | // [(x || y) && (!x)] -> y |
| 591 | if *x == *operand { |
| 592 | return y.clone(); |
| 593 | } |
| 594 | // [(x || y) && (!y)] -> x |
| 595 | if *y == *operand { |
| 596 | return x.clone(); |
| 597 | } |
| 598 | } |
| 599 | } |
| 600 | _ => (), |
| 601 | } |
no test coverage detected