DisjointExpr: add unpack_concat flag to work harder bringing ITEs to top-level for pointers
makes some sqlite3 test cases go from 18 mins to 2 secs due to less undef rewriting
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -528,7 +528,7 @@ void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
expr bytes = bytes0.zextOrTrunc(bits_size_t);
DisjointExpr<expr> UB(expr(false)), is_aligned(expr(false)), all_ptrs;
- for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, true)) {
+ for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, true, true)) {
Pointer ptr(m, ptr_expr);
auto [ub, aligned] = ::is_dereferenceable(ptr, bytes_off, bytes, align,
iswrite);

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1260,8 +1260,13 @@ expr expr::extract(unsigned high, unsigned low) const {
}
{
expr cond, then, els;
- if (isIf(cond, then, els) && then.isConst() && els.isConst()) {
- return mkIf(cond, then.extract(high, low), els.extract(high, low));
+ if (isIf(cond, then, els)) {
+ then = then.extract(high, low);
+ els = els.extract(high, low);
+ if (then.eq(els))
+ return then;
+ if (then.isConst() && els.isConst())
+ return mkIf(cond, then, els);
}
}
return simplify_const(Z3_mk_extract(ctx(), high, low, ast()), *this);

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -50,18 +50,52 @@ ostream &operator<<(ostream &os, const OrExpr &e) {
}
-template<> DisjointExpr<expr>::DisjointExpr(const expr &e, bool unpack_ite) {
+template<> DisjointExpr<expr>::DisjointExpr(const expr &e, bool unpack_ite,
+ bool unpack_concat) {
assert(unpack_ite);
vector<pair<expr, expr>> worklist = { {e, true} };
- expr cond, then, els;
+ expr cond, then, els, a, b;
+ unsigned high, low;
do {
auto [v, c] = worklist.back();
worklist.pop_back();
+
if (v.isIf(cond, then, els)) {
worklist.emplace_back(move(then), c && cond);
worklist.emplace_back(move(els), c && !cond);
+ }
+ else if (unpack_concat && v.isConcat(a, b)) {
+ DisjointExpr<expr> lhs(a, unpack_ite, unpack_concat);
+ DisjointExpr<expr> rhs(b, unpack_ite, unpack_concat);
+ if (lhs.size() == 1 && rhs.size() == 1) {
+ add(move(v), move(c));
+ continue;
+ }
+
+ for (auto &[lhs_v, lhs_domain] : lhs) {
+ if (auto rhs_val = rhs.lookup(lhs_domain)) {
+ add(lhs_v.concat(*rhs_val), lhs_domain);
} else {
+ for (auto &[rhs_v, rhs_domain] : rhs) {
+ add(lhs_v.concat(rhs_v.subst(lhs_domain, true).simplify()),
+ lhs_domain && rhs_domain);
+ }
+ }
+ }
+ }
+ else if (unpack_concat && v.isExtract(a, high, low)) {
+ DisjointExpr<expr> vals(a, unpack_ite, true);
+ if (vals.size() == 1) {
+ add(move(v), move(c));
+ continue;
+ }
+
+ for (auto &[v, domain] : vals) {
+ add(v.extract(high, low), domain);
+ }
+ }
+ else {
add(move(v), move(c));
}
} while (!worklist.empty());

MODIFY
smt/exprs.h
smt/exprs.h
@@ -44,7 +44,7 @@ public:
DisjointExpr(const T &default_val) : default_val(default_val) {}
DisjointExpr(const std::optional<T> &default_val) : default_val(default_val){}
DisjointExpr(T &&default_val) : default_val(std::move(default_val)) {}
- DisjointExpr(const expr &e, bool unpack_ite);
+ DisjointExpr(const expr &e, bool unpack_ite, bool unpack_concat = false);
template <typename V, typename D>
void add(V &&val, D &&domain) {
@@ -74,8 +74,17 @@ public:
return {};
}
+ std::optional<T> lookup(const expr &domain) const {
+ for (auto &[v, d] : vals) {
+ if (d.eq(domain))
+ return v;
+ }
+ return {};
+ }
+
auto begin() const { return vals.begin(); }
auto end() const { return vals.end(); }
+ auto size() const { return vals.size(); }
};

DisjointExpr: add unpack_concat flag to work harder bringing ITEs to top-level for pointers
makes some sqlite3 test cases go from 18 mins to 2 secs due to less undef rewriting