From 55ab7778f4b8e7653a0e9bb8d159962b70e9997a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Nov 2022 03:46:17 -0800 Subject: [PATCH] fix perf bug in new solve_eqs. --- src/ast/simplifiers/solve_context_eqs.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index 1ccab0f6c1f..dab09a7a95a 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -150,13 +150,32 @@ namespace euf { for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i) 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) { 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; expr* last_var = nullptr; bool was_unsafe = false; for (auto const& eq : eqs) { + if (refcount.get(eq.var->get_id(), 0) > 1) + continue; + SASSERT(!m.is_bool(eq.var));