do simple rewrites that cover the common cases
| 98 | |
| 99 | // do simple rewrites that cover the common cases |
| 100 | static expr simplify(const expr &e, const expr &cond, bool negate) { |
| 101 | // (bvadd ((_ extract ..) (ite cond X Y)) Z) |
| 102 | // -> (bvadd ((_ extract ..) X) Z) or (bvadd ((_ extract ..) Y) Z) |
| 103 | // NB: although this potentially increases the circuit size, it allows further |
| 104 | // simplifications down the road, and has been shown to be beneficial to perf |
| 105 | expr a, b; |
| 106 | if (e.isAdd(a, b)) { |
| 107 | auto test = [&](const expr &a, const expr &b) -> expr { |
| 108 | expr extract, ifcond, t, e; |
| 109 | unsigned high, low; |
| 110 | if (b.isExtract(extract, high, low) && |
| 111 | extract.isIf(ifcond, t, e) && |
| 112 | ifcond.eq(cond)) { |
| 113 | return a + (negate ? e : t).extract(high, low); |
| 114 | } |
| 115 | return {}; |
| 116 | }; |
| 117 | if (auto r = test(a, b); r.isValid()) return r; |
| 118 | if (auto r = test(b, a); r.isValid()) return r; |
| 119 | } |
| 120 | return e; |
| 121 | } |
| 122 | |
| 123 | template<> |
| 124 | DisjointExpr<expr>::DisjointExpr(const expr &e, unsigned depth_limit) { |