smt: special case substitution of quantified vars
Z3 is faster when replacing quant vars than regular vars
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -215,10 +215,6 @@ expr expr::mkConst(Z3_func_decl decl) {
return Z3_mk_app(ctx(), decl, 0, {});
}
-expr expr::mkQuantVar(unsigned i, Z3_sort sort) {
- return Z3_mk_bound(ctx(), i, sort);
-}
-
bool expr::isBinOp(expr &a, expr &b, int z3op) const {
if (auto app = isAppOf(z3op)) {
if (Z3_get_app_num_args(ctx(), app) != 2)
@@ -1586,21 +1582,17 @@ expr expr::load(const expr &idx) const {
if (body.isConst())
return body;
- auto subst = [&](const expr &e, const expr &var) {
+ auto subst = [&](const expr &e) {
if (e.isLoad(array, str_idx)) {
- expr new_idx = str_idx.subst(var, idx).simplify();
- assert(!idx.isValid() || !str_idx.eq(new_idx));
- return array.load(new_idx);
+ return array.load(str_idx.subst({ idx }));
}
- return e.subst(var, idx);
+ return e.subst({ idx });
};
expr cond, then, els;
if (body.isIf(cond, then, els)) {
- auto sort = Z3_get_quantifier_bound_sort(ctx(), ast(), 0);
- expr var = expr::mkQuantVar(0, sort);
- cond = cond.subst(var, idx).simplify();
- return mkIf_fold(cond, subst(then, var), subst(els, var));
+ cond = cond.subst({ idx }).simplify();
+ return mkIf_fold(cond, subst(then), subst(els));
}
}
@@ -1699,6 +1691,20 @@ expr expr::subst(const expr &from, const expr &to) const {
return Z3_substitute(ctx(), ast(), 1, &f, &t);
}
+expr expr::subst(const vector<expr> &repls) const {
+ C();
+ if (repls.empty())
+ return *this;
+
+ unique_ptr<Z3_ast[]> vars(new Z3_ast[repls.size()]);
+ unsigned i = 0;
+ for (auto &v : repls) {
+ C2(v);
+ vars[i++] = v();
+ }
+ return Z3_substitute_vars(ctx(), ast(), repls.size(), vars.get());
+}
+
set<expr> expr::vars() const {
return vars({ this });
}

MODIFY
smt/expr.h
smt/expr.h
@@ -64,7 +64,6 @@ class expr {
static expr mkUInt(uint64_t n, Z3_sort sort);
static expr mkInt(int64_t n, Z3_sort sort);
static expr mkConst(Z3_func_decl decl);
- static expr mkQuantVar(unsigned i, Z3_sort sort);
bool isBinOp(expr &a, expr &b, int z3op) const;
@@ -316,6 +315,9 @@ public:
expr subst(const std::vector<std::pair<expr, expr>> &repls) const;
expr subst(const expr &from, const expr &to) const;
+ // replace quantified variables in increasing index order
+ expr subst(const std::vector<expr> &repls) const;
+
std::set<expr> vars() const;
static std::set<expr> vars(const std::vector<const expr*> &exprs);

smt: special case substitution of quantified vars
Z3 is faster when replacing quant vars than regular vars