mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5259 again

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-10 11:15:19 -07:00
parent 987099c765
commit e2a52ed6ee
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -52,9 +52,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
arith_util m_a_util; arith_util m_a_util;
bv_util m_bv_util; bv_util m_bv_util;
expr_safe_replace m_rep; expr_safe_replace m_rep;
bool m_new_subst { false };
expr_ref_vector m_pinned; expr_ref_vector m_pinned;
unsigned long long m_max_memory; // in bytes unsigned long long m_max_memory; // in bytes
unsigned m_max_steps; unsigned m_max_steps;
bool m_pull_cheap_ite; bool m_pull_cheap_ite;
bool m_flat; bool m_flat;
bool m_cache_all; bool m_cache_all;
@ -688,6 +689,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return; return;
if (patterns.empty()) if (patterns.empty())
return; return;
if (m_new_subst) {
m_rep.reset();
for (auto kv : m_subst->sub())
m_rep.insert(kv.m_key, kv.m_value);
m_new_subst = false;
}
expr_ref tmp(m()); expr_ref tmp(m());
for (unsigned i = 0; i < patterns.size(); ++i) { for (unsigned i = 0; i < patterns.size(); ++i) {
m_rep(patterns[i], tmp); m_rep(patterns[i], tmp);
@ -806,9 +813,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
void set_substitution(expr_substitution * s) { void set_substitution(expr_substitution * s) {
reset(); reset();
m_subst = s; m_subst = s;
m_rep.reset(); m_new_subst = true;
for (auto kv : m_subst->sub())
m_rep.insert(kv.m_key, kv.m_value);
} }
void reset() { void reset() {