| 1399 | } |
| 1400 | |
| 1401 | expr expr::operator&(const expr &rhs) const { |
| 1402 | if (eq(rhs) || isZero() || rhs.isAllOnes()) |
| 1403 | return *this; |
| 1404 | if (isAllOnes() || rhs.isZero()) |
| 1405 | return rhs; |
| 1406 | |
| 1407 | auto fold_extract = [](auto &a, auto &b) { |
| 1408 | uint64_t n; |
| 1409 | if (!a.isUInt(n) || n == 0 || n == numeric_limits<uint64_t>::max()) |
| 1410 | return expr(); |
| 1411 | |
| 1412 | auto lead = countl_zero(n); |
| 1413 | auto trail = countr_zero(n); |
| 1414 | |
| 1415 | if (!is_power2((n >> trail) + 1)) |
| 1416 | return expr(); |
| 1417 | |
| 1418 | auto r = b.extract(63 - lead, trail); |
| 1419 | lead -= 64 - a.bits(); |
| 1420 | if (lead > 0) |
| 1421 | r = mkUInt(0, lead).concat(r); |
| 1422 | if (trail > 0) |
| 1423 | r = r.concat(mkUInt(0, trail)); |
| 1424 | return r; |
| 1425 | }; |
| 1426 | |
| 1427 | if (bits() <= 64) { |
| 1428 | if (auto f = fold_extract(*this, rhs); |
| 1429 | f.isValid()) |
| 1430 | return f; |
| 1431 | if (auto f = fold_extract(rhs, *this); |
| 1432 | f.isValid()) |
| 1433 | return f; |
| 1434 | |
| 1435 | if (bits() == 1) { |
| 1436 | if (auto a = get_bool(*this); |
| 1437 | a.isValid()) |
| 1438 | if(auto b = get_bool(rhs); |
| 1439 | b.isValid()) |
| 1440 | return (a && b).toBVBool(); |
| 1441 | } |
| 1442 | } |
| 1443 | return binopc(Z3_mk_bvand, operator&, Z3_OP_BAND, isAllOnes, isZero); |
| 1444 | } |
| 1445 | |
| 1446 | expr expr::operator|(const expr &rhs) const { |
| 1447 | if (eq(rhs) || isAllOnes() || rhs.isZero()) |