mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

touch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-01 14:13:05 -08:00
parent faf14012ba
commit a15a7cee7b
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -137,6 +137,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
m_subst.insert(p, m.mk_true()); m_subst.insert(p, m.mk_true());
fmls.push_back(p); fmls.push_back(p);
} }
bool new_eq = false;
for (auto& [a, b] : m_eqs) { for (auto& [a, b] : m_eqs) {
if (m.is_value(a)) if (m.is_value(a))
std::swap(a, b); std::swap(a, b);
@ -146,6 +147,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
result = m.mk_false(); result = m.mk_false();
return BR_DONE; return BR_DONE;
} }
new_eq = true;
m_subst.insert(a, b); m_subst.insert(a, b);
fmls.push_back(m.mk_eq(a, b)); fmls.push_back(m.mk_eq(a, b));
} }
@ -154,7 +156,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
fmls.push_back(ors); fmls.push_back(ors);
result = mk_and(fmls); result = mk_and(fmls);
TRACE("hoist", tout << ors << " => " << result << "\n";); TRACE("hoist", tout << ors << " => " << result << "\n";);
return BR_DONE; return new_eq ? BR_REWRITE3 : BR_DONE;
} }
unsigned hoist_rewriter::mk_var(expr* e) { unsigned hoist_rewriter::mk_var(expr* e) {