smt expr: dont use a timeout with simplify when none is needed
you need latest Z3 to realize the full speedup from this patch
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -37,9 +37,15 @@ void context::init() {
Z3_global_param_set("rewriter.hi_fp_unspecified", "true");
ctx = Z3_mk_context_rc(nullptr);
Z3_set_error_handler(ctx, z3_error_handler);
+
+ no_timeout_param = Z3_mk_params(ctx);
+ Z3_params_inc_ref(ctx, no_timeout_param);
+ Z3_params_set_uint(ctx, no_timeout_param,
+ Z3_mk_string_symbol(ctx, "timeout"), 0);
}
void context::destroy() {
+ Z3_params_dec_ref(ctx, no_timeout_param);
Z3_close_log();
Z3_del_context(ctx);
}

MODIFY
smt/ctx.h
smt/ctx.h
// Distributed under the MIT license that can be found in the LICENSE file.
typedef struct _Z3_context *Z3_context;
+typedef struct _Z3_params* Z3_params;
namespace smt {
class context {
Z3_context ctx;
+ Z3_params no_timeout_param;
public:
Z3_context operator()() const { return ctx; }
+ Z3_params getNoTimeoutParam() const { return no_timeout_param; }
void init();
void destroy();

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1667,6 +1667,11 @@ expr expr::simplify() const {
return e ? e : *this;
}
+expr expr::simplifyNoTimeout() const {
+ C();
+ return Z3_simplify_ex(ctx(), ast(), ctx.getNoTimeoutParam());
+}
+
expr expr::subst(const vector<pair<expr, expr>> &repls) const {
C();
if (repls.empty())

MODIFY
smt/expr.h
smt/expr.h
@@ -55,7 +55,7 @@ class expr {
return simplify_const(std::move(e), inputs...);
return std::move(e);
}
- static expr simplify_const(expr &&e) { return e.simplify(); }
+ static expr simplify_const(expr &&e) { return e.simplifyNoTimeout(); }
bool alwaysFalse() const { return false; }
@@ -310,6 +310,7 @@ public:
static expr mkLambda(const expr &var, const expr &val);
expr simplify() const;
+ expr simplifyNoTimeout() const;
// replace v1 -> v2
expr subst(const std::vector<std::pair<expr, expr>> &repls) const;

smt expr: dont use a timeout with simplify when none is needed
you need latest Z3 to realize the full speedup from this patch