| 1461 | } |
| 1462 | |
| 1463 | expr expr::operator^(const expr &rhs) const { |
| 1464 | if (eq(rhs)) |
| 1465 | return mkUInt(0, sort()); |
| 1466 | if (isAllOnes()) |
| 1467 | return bits() == 1 ? (rhs == 0).toBVBool() : ~rhs; |
| 1468 | if (rhs.isAllOnes()) |
| 1469 | return bits() == 1 ? (*this == 0).toBVBool() : ~*this; |
| 1470 | return binopc(Z3_mk_bvxor, operator^, Z3_OP_BXOR, isZero, alwaysFalse); |
| 1471 | } |
| 1472 | |
| 1473 | expr expr::operator!() const { |
| 1474 | C(); |