| 1488 | } |
| 1489 | |
| 1490 | expr expr::cmp_eq(const expr &rhs, bool simplify) const { |
| 1491 | if (!simplify) |
| 1492 | goto end; |
| 1493 | |
| 1494 | if (eq(rhs)) |
| 1495 | return true; |
| 1496 | if (isConst()) { |
| 1497 | if (rhs.isConst()) |
| 1498 | return false; |
| 1499 | return rhs == *this; |
| 1500 | } |
| 1501 | // constants on rhs from now on. |
| 1502 | |
| 1503 | if (rhs.isTrue()) |
| 1504 | return *this; |
| 1505 | if (rhs.isFalse()) |
| 1506 | return !*this; |
| 1507 | |
| 1508 | // (= (= a bit) (= b bit)) -> (= a b) |
| 1509 | { |
| 1510 | expr lhs_a, lhs_b, rhs_a, rhs_b; |
| 1511 | if (isEq(lhs_a, lhs_b) && lhs_a.isBV() && lhs_a.bits() == 1 && |
| 1512 | rhs.isEq(rhs_a, rhs_b) && lhs_a.eq(rhs_a)) |
| 1513 | return lhs_b == rhs_b; |
| 1514 | } |
| 1515 | |
| 1516 | // (= (+ a c1) (+ a c2)) -> false |
| 1517 | { |
| 1518 | expr lhs_base, rhs_base; |
| 1519 | uint64_t lhs_offset, rhs_offset; |
| 1520 | if (isBasePlusOffset(lhs_base, lhs_offset) && |
| 1521 | rhs.isBasePlusOffset(rhs_base, rhs_offset) && |
| 1522 | lhs_base.eq(rhs_base) && |
| 1523 | lhs_offset != rhs_offset) |
| 1524 | return false; |
| 1525 | } |
| 1526 | |
| 1527 | if (auto app = isAppOf(Z3_OP_CONCAT)) { |
| 1528 | unsigned num_args = Z3_get_app_num_args(ctx(), app); |
| 1529 | // (concat x y) == const -> x == const[..] /\ y == const[..] |
| 1530 | if (rhs.isConst()) { |
| 1531 | AndExpr eqs; |
| 1532 | unsigned high = bits(); |
| 1533 | for (unsigned i = 0; i < num_args; ++i) { |
| 1534 | expr arg = Z3_get_app_arg(ctx(), app, i); |
| 1535 | unsigned low = high - arg.bits(); |
| 1536 | eqs.add(arg == rhs.extract(high - 1, low)); |
| 1537 | high = low; |
| 1538 | } |
| 1539 | return eqs(); |
| 1540 | } |
| 1541 | |
| 1542 | // (concat ..) == (concat ..) |
| 1543 | if (auto app_rhs = rhs.isAppOf(Z3_OP_CONCAT); |
| 1544 | app_rhs != nullptr && |
| 1545 | num_args == Z3_get_app_num_args(ctx(), app_rhs)) { |
| 1546 | AndExpr eqs; |
| 1547 | bool all_aligned = true; |
no test coverage detected