| 62 | } |
| 63 | |
| 64 | static bool is_power2(const expr &e, unsigned &log) { |
| 65 | if (!e.isConst()) |
| 66 | return false; |
| 67 | |
| 68 | if (e.isZero() || !(e & (e - expr::mkUInt(1, e))).isZero()) |
| 69 | return false; |
| 70 | |
| 71 | for (unsigned i = 0, bits = e.bits(); i < bits; ++i) { |
| 72 | if (e.extract(i, i).isAllOnes()) { |
| 73 | log = i; |
| 74 | return true; |
| 75 | } |
| 76 | } |
| 77 | UNREACHABLE(); |
| 78 | } |
| 79 | |
| 80 | |
| 81 | namespace smt { |