From 18fe28c0f0db547e52f96d7d7a2755a8becbaf7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Sep 2019 20:01:06 -0700 Subject: [PATCH] fix perf bug exposed by Shelly Grossman Signed-off-by: Nikolaj Bjorner --- src/ast/expr_substitution.h | 2 ++ src/tactic/core/solve_eqs_tactic.cpp | 37 ++++++++++++++++++---------- 2 files changed, 26 insertions(+), 13 deletions(-) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index cbe00433c..93658f413 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -43,6 +43,7 @@ public: bool unsat_core_enabled() const { return m_cores_enabled; } bool empty() const { return m_subst.empty(); } + unsigned size() const { return m_subst.size(); } void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr); void erase(expr * s); bool find(expr * s, expr * & def, proof * & def_pr); @@ -82,6 +83,7 @@ public: } unsigned scope_level() const { return m_trail_lim.size(); } bool empty() const { return m_subst.empty(); } + unsigned size() const { return m_subst.size(); } expr* find(expr * e) { proof* pr; expr* d = nullptr; if (find(e, d, pr)) return d; else return e; } bool find(expr * s, expr * & def, proof * & def_pr) { return m_subst.find(s, def, def_pr); } bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 1eef58ce5..52d43f109 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -452,6 +452,7 @@ class solve_eqs_tactic : public tactic { {} }; + ptr_vector m_todo; void mark_occurs(expr_mark& occ, goal const& g, expr* v) { expr_fast_mark2 visited; occ.mark(v, true); @@ -500,14 +501,15 @@ class solve_eqs_tactic : public tactic { bool is_compatible(goal const& g, unsigned idx, vector const & path, expr* v, expr* eq) { expr_mark occ; + svector cache; mark_occurs(occ, g, v); - return is_goal_compatible(g, occ, idx, v, eq) && is_path_compatible(occ, path, v, eq); + return is_goal_compatible(g, occ, cache, idx, v, eq) && is_path_compatible(occ, cache, path, v, eq); } - bool is_goal_compatible(goal const& g, expr_mark& occ, unsigned idx, expr* v, expr* eq) { + bool is_goal_compatible(goal const& g, expr_mark& occ, svector& cache, unsigned idx, expr* v, expr* eq) { bool all_e = false; for (unsigned j = 0; j < g.size(); ++j) { - if (j != idx && !check_eq_compat_rec(occ, g.form(j), v, eq, all_e)) { + if (j != idx && !check_eq_compat_rec(occ, cache, g.form(j), v, eq, all_e)) { TRACE("solve_eqs", tout << "occurs goal " << mk_pp(eq, m()) << "\n";); return false; } @@ -524,7 +526,7 @@ class solve_eqs_tactic : public tactic { // and, all_e -> all_e // - bool is_path_compatible(expr_mark& occ, vector const & path, expr* v, expr* eq) { + bool is_path_compatible(expr_mark& occ, svector& cache, vector const & path, expr* v, expr* eq) { bool all_e = true; for (unsigned i = path.size(); i-- > 0; ) { auto const& p = path[i]; @@ -541,7 +543,7 @@ class solve_eqs_tactic : public tactic { for (unsigned j = 0; j < args.size(); ++j) { if (j != p.m_index) { if (occurs(v, args[j])) { - if (!check_eq_compat_rec(occ, args[j], v, eq, all_e)) { + if (!check_eq_compat_rec(occ, cache, args[j], v, eq, all_e)) { TRACE("solve_eqs", tout << "occurs or " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";); return false; } @@ -556,18 +558,23 @@ class solve_eqs_tactic : public tactic { return true; } - ptr_vector m_todo; - bool check_eq_compat_rec(expr_mark& occ, expr* f, expr* v, expr* eq, bool& all) { + bool check_eq_compat_rec(expr_mark& occ, svector& cache, expr* f, expr* v, expr* eq, bool& all) { expr_ref_vector args(m()); expr* f1 = nullptr; if (!occ.is_marked(f)) { all = false; return true; } + unsigned idx = f->get_id(); + if (cache.size() > idx && cache[idx] != l_undef) { + return cache[idx] == l_true; + } if (m().is_not(f, f1) && m().is_or(f1)) { flatten_and(f, args); for (expr* arg : args) { if (arg == eq) { + cache.reserve(idx+1, l_undef); + cache[idx] = l_true; return true; } } @@ -580,10 +587,14 @@ class solve_eqs_tactic : public tactic { } for (expr* arg : args) { - if (!check_eq_compat_rec(occ, arg, v, eq, all)) { + if (!check_eq_compat_rec(occ, cache, arg, v, eq, all)) { + cache.reserve(idx+1, l_undef); + cache[idx] = l_false; return false; } } + cache.reserve(idx+1, l_undef); + cache[idx] = l_true; return true; } @@ -889,9 +900,7 @@ class solve_eqs_tactic : public tactic { return; } g.elim_true(); - TRACE("solve_eqs", - tout << "after applying substitution\n"; - g.display(tout);); + TRACE("solve_eqs", g.display(tout << "after applying substitution\n");); #if 0 DEBUG_CODE({ for (expr* v : m_ordered_vars) { @@ -987,11 +996,13 @@ class solve_eqs_tactic : public tactic { if (m_context_solve) { collect_hoist(*g); } - if (m_subst->empty()) + if (m_subst->empty()) { break; + } sort_vars(); - if (m_ordered_vars.empty()) + if (m_ordered_vars.empty()) { break; + } normalize(); substitute(*(g.get())); if (g->inconsistent()) {