mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-02 15:40:47 -08:00
parent 585d027668
commit ba8d8f0af7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -270,7 +270,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
return BR_DONE; return BR_DONE;
} }
#if 1 #if 0
br_status st; br_status st;
expr_ref r(m()); expr_ref r(m());
st = m_hoist.mk_or(buffer.size(), buffer.data(), r); st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
@ -282,7 +282,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
get_num_internal_exprs(m_counts2, m_todo2, args[i]); get_num_internal_exprs(m_counts2, m_todo2, args[i]);
unsigned count1 = count_internal_nodes(m_counts1, m_todo1); unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
unsigned count2 = count_internal_nodes(m_counts2, m_todo2); unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
if (count1 > count2 + num_args) if (count1 > count2)
st = BR_FAILED; st = BR_FAILED;
} }
if (st != BR_FAILED) if (st != BR_FAILED)