From da805f6016a846e45c7c2c2a0560759f95fee6fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Sep 2019 18:31:52 +0200
Subject: [PATCH] address perf bottleneck exposed by #2552

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.cpp | 68 ++++++++++++++++++++++++----
 1 file changed, 59 insertions(+), 9 deletions(-)

diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index bb600cb7049..a588368b37c 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -452,14 +452,63 @@ class solve_eqs_tactic : public tactic {
             {}
         };
 
+        void mark_occurs(expr_mark& occ, goal const& g, expr* v) {
+            expr_fast_mark2 visited;
+            occ.mark(v, true);
+            visited.mark(v, true);
+            for (unsigned j = 0; j < g.size(); ++j) {              
+                m_todo.push_back(g.form(j));
+            }
+            while (!m_todo.empty()) {
+                expr* e = m_todo.back();
+                if (visited.is_marked(e)) {
+                    m_todo.pop_back();
+                    continue;
+                }
+                if (is_app(e)) {
+                    bool does_occur = false;
+                    bool all_visited = true;
+                    for (expr* arg : *to_app(e)) {
+                        if (!visited.is_marked(arg)) {
+                            m_todo.push_back(arg);
+                            all_visited = false;
+                        }
+                        else {
+                            does_occur |= occ.is_marked(arg);
+                        }
+                    }
+                    if (all_visited) {
+                        occ.mark(e, does_occur);
+                        visited.mark(e, true);
+                        m_todo.pop_back();
+                    }
+                }
+                else if (is_quantifier(e)) {
+                    expr* body = to_quantifier(e)->get_expr();
+                    if (visited.is_marked(body)) {
+                        visited.mark(e, true);
+                        occ.mark(e, occ.is_marked(body));
+                        m_todo.pop_back();
+                    }
+                }
+                else {
+                    visited.mark(e, true);
+                    m_todo.pop_back();
+                }
+            }
+        }
+
         bool is_compatible(goal const& g, unsigned idx, vector<nnf_context> const & path, expr* v, expr* eq) {
-            return is_goal_compatible(g, idx, v, eq) && is_path_compatible(path, v, eq);
+            expr_mark occ;
+            //std::cout << mk_pp(v, m()) << "\n";
+            mark_occurs(occ, g, v);
+            return is_goal_compatible(g, occ, idx, v, eq) && is_path_compatible(occ, path, v, eq);
         }
 
-        bool is_goal_compatible(goal const& g, unsigned idx, expr* v, expr* eq) {
+        bool is_goal_compatible(goal const& g, expr_mark& occ, unsigned idx, expr* v, expr* eq) {
             bool all_e = false;
             for (unsigned j = 0; j < g.size(); ++j) {              
-                if (j != idx && !check_eq_compat(g.form(j), v, eq, all_e)) {
+                if (j != idx && !check_eq_compat_rec(occ, g.form(j), v, eq, all_e)) {
                     TRACE("solve_eqs", tout << "occurs goal " << mk_pp(eq, m()) << "\n";);
                     return false;
                 }
@@ -476,14 +525,14 @@ class solve_eqs_tactic : public tactic {
         // and, all_e -> all_e
         //
 
-        bool is_path_compatible(vector<nnf_context> const & path, expr* v, expr* eq) {
+        bool is_path_compatible(expr_mark& occ, vector<nnf_context> const & path, expr* v, expr* eq) {
             bool all_e = true;
             for (unsigned i = path.size(); i-- > 0; ) {
                 auto const& p = path[i];
                 auto const& args = p.m_args;
                 if (p.m_is_and && !all_e) {
                     for (unsigned j = 0; j < args.size(); ++j) {
-                        if (j != p.m_index && occurs(v, args[j])) {
+                        if (j != p.m_index && occ.is_marked(args[j])) {
                             TRACE("solve_eqs", tout << "occurs and " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
                             return false;
                         }
@@ -493,7 +542,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(args[j], v, eq, all_e)) {
+                                if (!check_eq_compat_rec(occ, args[j], v, eq, all_e)) {
                                     TRACE("solve_eqs", tout << "occurs or " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
                                     return false;
                                 }
@@ -508,10 +557,11 @@ class solve_eqs_tactic : public tactic {
             return true;
         }
 
-        bool check_eq_compat(expr* f, expr* v, expr* eq, bool& all) {
+        ptr_vector<expr> m_todo;       
+        bool check_eq_compat_rec(expr_mark& occ, expr* f, expr* v, expr* eq, bool& all) {
             expr_ref_vector args(m());
             expr* f1 = nullptr;
-            if (!occurs(v, f)) {
+            if (!occ.is_marked(f)) {
                 all = false;
                 return true;
             }
@@ -531,7 +581,7 @@ class solve_eqs_tactic : public tactic {
             }
 
             for (expr* arg : args) {
-                if (!check_eq_compat(arg, v, eq, all)) {
+                if (!check_eq_compat_rec(occ, arg, v, eq, all)) {
                     return false;
                 }
             }