mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix perf bug in new solve_eqs.

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-16 03:46:17 -08:00
parent d70dbdad50
commit 55ab7778f4
1 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/simplifiers/solve_context_eqs.cpp
View file

@ -150,13 +150,32 @@ namespace euf {
for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i) for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i)
collect_nested_equalities(m_fmls[i], visited, eqs); collect_nested_equalities(m_fmls[i], visited, eqs);
if (eqs.empty())
return;
std::stable_sort(eqs.begin(), eqs.end(), [&](dependent_eq const& e1, dependent_eq const& e2) { std::stable_sort(eqs.begin(), eqs.end(), [&](dependent_eq const& e1, dependent_eq const& e2) {
return e1.var->get_id() < e2.var->get_id(); }); return e1.var->get_id() < e2.var->get_id(); });
// quickly weed out variables that occur in more than two assertions.
unsigned_vector refcount;
{
expr_mark visited;
for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i) {
visited.reset();
expr* f = m_fmls[i].fml();
for (expr* t : subterms::all(expr_ref(f, m), &m_todo, &visited))
refcount.setx(t->get_id(), refcount.get(t->get_id(), 0) + 1, 0);
}
}
unsigned j = 0; unsigned j = 0;
expr* last_var = nullptr; expr* last_var = nullptr;
bool was_unsafe = false; bool was_unsafe = false;
for (auto const& eq : eqs) { for (auto const& eq : eqs) {
if (refcount.get(eq.var->get_id(), 0) > 1)
continue;
SASSERT(!m.is_bool(eq.var)); SASSERT(!m.is_bool(eq.var));