| 1444 | } |
| 1445 | |
| 1446 | expr expr::operator|(const expr &rhs) const { |
| 1447 | if (eq(rhs) || isAllOnes() || rhs.isZero()) |
| 1448 | return *this; |
| 1449 | if (isZero() || rhs.isAllOnes()) |
| 1450 | return rhs; |
| 1451 | |
| 1452 | if (bits() == 1) { |
| 1453 | if (auto a = get_bool(*this); |
| 1454 | a.isValid()) |
| 1455 | if (auto b = get_bool(rhs); |
| 1456 | b.isValid()) |
| 1457 | return (a || b).toBVBool(); |
| 1458 | } |
| 1459 | |
| 1460 | return binopc(Z3_mk_bvor, operator|, Z3_OP_BOR, isZero, isAllOnes); |
| 1461 | } |
| 1462 | |
| 1463 | expr expr::operator^(const expr &rhs) const { |
| 1464 | if (eq(rhs)) |