smt expr: constant fold top-level loads of lambdas
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1898,7 +1898,7 @@ expr expr::load(const expr &idx) const {
Z3_is_lambda(ctx(), ast())) {
assert(Z3_get_quantifier_num_bound(ctx(), ast()) == 1);
expr body = Z3_get_quantifier_body(ctx(), ast());
- return body.subst({ idx });
+ return body.subst({ idx }).foldTopLevel();
}
return Z3_mk_select(ctx(), ast(), idx());
@@ -1976,6 +1976,28 @@ expr expr::simplifyNoTimeout() const {
return Z3_simplify_ex(ctx(), ast(), ctx.getNoTimeoutParam());
}
+expr expr::foldTopLevel() const {
+ expr cond, then, els;
+ if (isIf(cond, then, els))
+ return
+ expr::mkIf(cond.foldTopLevel(), then.foldTopLevel(), els.foldTopLevel());
+
+ expr array, idx;
+ if (isLoad(array, idx) && idx.isConst())
+ return array.load(idx);
+
+ if (isApp()) {
+ bool is_const = true;
+ for (unsigned i = 0, e = getFnNumArgs(); i < e; ++i) {
+ if (!(is_const &= getFnArg(i).isConst()))
+ break;
+ }
+ if (is_const)
+ return simplifyNoTimeout();
+ }
+ return *this;
+}
+
expr expr::subst(const vector<pair<expr, expr>> &repls) const {
C();
if (repls.empty())
@@ -2132,6 +2154,12 @@ string expr::fn_name() const {
return "";
}
+unsigned expr::getFnNumArgs() const {
+ auto app = isApp();
+ assert(app);
+ return Z3_get_app_num_args(ctx(), app);
+}
+
expr expr::getFnArg(unsigned i) const {
auto app = isApp();
assert(app && i < Z3_get_app_num_args(ctx(), app));

MODIFY
smt/expr.h
smt/expr.h
@@ -339,6 +339,8 @@ public:
expr simplify() const;
expr simplifyNoTimeout() const;
+ expr foldTopLevel() const;
+
// replace v1 -> v2
expr subst(const std::vector<std::pair<expr, expr>> &repls) const;
expr subst(const expr &from, const expr &to) const;
@@ -356,6 +358,7 @@ public:
void printHexadecimal(std::ostream &os) const;
std::string numeral_string() const;
std::string fn_name() const; // empty if not a function
+ unsigned getFnNumArgs() const;
expr getFnArg(unsigned i) const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);

smt expr: constant fold top-level loads of lambdas