| 1652 | } |
| 1653 | |
| 1654 | expr expr::operator||(const expr &rhs) const { |
| 1655 | if (eq(rhs) || rhs.isFalse() || isTrue()) |
| 1656 | return *this; |
| 1657 | if (rhs.isTrue() || isFalse()) |
| 1658 | return rhs; |
| 1659 | |
| 1660 | expr n; |
| 1661 | if ((isNot(n) && n.eq(rhs)) || |
| 1662 | (rhs.isNot(n) && eq(n))) |
| 1663 | return true; |
| 1664 | |
| 1665 | // (a & b) | (!a & b) -> b |
| 1666 | expr a, b, c, d; |
| 1667 | if (isAnd(a, b) && rhs.isAnd(c, d) && b.eq(d)) { |
| 1668 | if ((a.isNot(n) && n.eq(c)) || |
| 1669 | (c.isNot(n) && n.eq(a))) |
| 1670 | return b; |
| 1671 | } |
| 1672 | |
| 1673 | C(rhs); |
| 1674 | Z3_ast args[] = { ast(), rhs() }; |
| 1675 | return Z3_mk_or(ctx(), 2, args); |
| 1676 | } |
| 1677 | |
| 1678 | void expr::operator&=(const expr &rhs) { |
| 1679 | *this = *this && rhs; |