mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Hoist creation of m_rep for #5259

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-10 10:54:21 -07:00
parent a61e9d6b49
commit 987099c765
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/th_rewriter.cpp
View file

@ -51,6 +51,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
recfun_rewriter m_rec_rw;
arith_util m_a_util;
bv_util m_bv_util;
expr_safe_replace m_rep;
expr_ref_vector m_pinned;
unsigned long long m_max_memory; // in bytes
unsigned m_max_steps;
@ -685,12 +686,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
void apply_subst(ptr_buffer<expr>& patterns) {
if (!m_subst)
return;
if (patterns.empty())
return;
expr_ref tmp(m());
expr_safe_replace rep(m());
for (auto kv : m_subst->sub())
rep.insert(kv.m_key, kv.m_value);
for (unsigned i = 0; i < patterns.size(); ++i) {
rep(patterns[i], tmp);
m_rep(patterns[i], tmp);
m_pinned.push_back(tmp);
patterns[i] = tmp;
}
@ -796,6 +796,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_rec_rw(m),
m_a_util(m),
m_bv_util(m),
m_rep(m),
m_pinned(m),
m_used_dependencies(m),
m_subst(nullptr) {
@ -805,6 +806,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
void set_substitution(expr_substitution * s) {
reset();
m_subst = s;
m_rep.reset();
for (auto kv : m_subst->sub())
m_rep.insert(kv.m_key, kv.m_value);
}
void reset() {