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

perf and memory smash fixes to internal node count routine

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-12 21:01:05 -07:00
parent f0afbcbb87
commit 7cd8edce1f
4 changed files with 26 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/rewriter/bool_rewriter.cpp
View file

@ -269,19 +269,28 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
return BR_DONE;
}
#if 1
br_status st;
st = m_hoist.mk_or(buffer.size(), buffer.data(), result);
expr_ref r(m());
st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
if (st != BR_FAILED) {
unsigned count1 = get_num_internal_exprs(result);
unsigned count2 = get_num_internal_exprs(buffer.size(), buffer.data());
m_counts1.reserve(m().get_num_asts() + 1);
m_counts2.reserve(m().get_num_asts() + 1);
get_num_internal_exprs(m_counts1, m_todo1, r);
for (unsigned i = 0; i < num_args; ++i)
get_num_internal_exprs(m_counts2, m_todo2, args[i]);
unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
if (count1 > count2)
st = BR_FAILED;
}
if (st != BR_FAILED)
result = r;
if (st == BR_DONE)
return BR_REWRITE1;
if (st != BR_FAILED)
return st;
#endif
if (s) {
ast_lt lt;
std::sort(buffer.begin(), buffer.end(), lt);