From b5d531f079d6b678dc8accf6fd165185361c18d6 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 2 Apr 2018 13:37:12 -0500
Subject: [PATCH] perf(datatype): improve caching in occurs_check

---
 src/smt/theory_datatype.cpp | 10 +++++++---
 src/smt/theory_datatype.h   | 16 ++++++++++++++++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 3d3d56055..a3c0ecc96 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -389,12 +389,14 @@ namespace smt {
     final_check_status theory_datatype::final_check_eh() {
         int num_vars = get_num_vars();
         final_check_status r = FC_DONE;
+        init_final_check();
         for (int v = 0; v < num_vars; v++) {
             if (v == static_cast<int>(m_find.find(v))) {
                 enode * node = get_enode(v);
                 if (occurs_check(node)) {
                     // conflict was detected... 
                     // return...
+                    cleanup_final_check();
                     return FC_CONTINUE;
                 }
                 if (m_params.m_dt_lazy_splits > 0) {
@@ -407,6 +409,7 @@ namespace smt {
                 }
             }
         }
+        cleanup_final_check();
         return r;
     }
 
@@ -434,6 +437,8 @@ namespace smt {
                       tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
                       tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n";
                   });
+        } else {
+            oc_mark_cycle_free(n);
         }
         return res;
     }
@@ -443,12 +448,11 @@ namespace smt {
        TODO: improve performance.
     */
     bool theory_datatype::occurs_check_core(enode * app) {
-        if (app->is_marked())
+        if (oc_cycle_free(app) || oc_explored(app))
             return false;
         
         m_stats.m_occurs_check++;
-        app->set_mark();
-        m_to_unmark.push_back(app);
+        oc_mark_explore(app);
         
         TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";);
 
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 2337fd0ea..1ccc15314 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -74,8 +74,24 @@ namespace smt {
         void sign_recognizer_conflict(enode * c, enode * r);
 
         ptr_vector<enode>    m_to_unmark;
+        ptr_vector<enode>    m_to_unmark2;
         enode_pair_vector    m_used_eqs;
         enode *              m_main;
+
+        void oc_mark_explore(enode * n) { n->set_mark(); m_to_unmark.push_back(n); }
+        bool oc_explored(enode * n) const { n->is_marked(); }
+
+        void oc_mark_cycle_free(enode * n) { n->set_mark2(); m_to_unmark2.push_back(n); }
+        bool oc_cycle_free(enode * n) const { n->is_marked2(); }
+
+        void init_final_check() {
+          m_to_unmark2.reset();
+        }
+        void cleanup_final_check() {
+          unmark_enodes2(m_to_unmark2.size(), m_to_unmark2.c_ptr());
+          m_to_unmark2.reset();
+        }
+
         bool occurs_check(enode * n);
         bool occurs_check_core(enode * n);