From 4c71e9479d00048a9a6f8666499d7e1f4b616c73 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 30 Sep 2014 11:21:34 -0700
Subject: [PATCH] optimizing array final check

---
 src/smt/theory_array_base.cpp | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 3f96a1d62..6325a2a99 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -376,8 +376,10 @@ namespace smt {
         enode_vector::const_iterator end = r->end_parents();
         for (; it != end; ++it) {
             enode * parent       = *it;
+#if 0
             if (!ctx.is_relevant(parent))
                 continue;
+#endif
             unsigned    num_args = parent->get_num_args();
             if (is_store(parent)) {
                 SET_ARRAY(parent->get_arg(0));
@@ -399,6 +401,7 @@ namespace smt {
         return false;
     }
 
+#if 0
     void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
         TRACE("array_shared", tout << "collecting shared vars...\n";);
         context & ctx = get_context();
@@ -420,6 +423,29 @@ namespace smt {
         }
         unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
     }
+#else
+    void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
+        TRACE("array_shared", tout << "collecting shared vars...\n";);
+        context & ctx = get_context();
+        ptr_buffer<enode> to_unmark;
+        unsigned num_vars = get_num_vars();
+        for (unsigned i = 0; i < num_vars; i++) {
+	    enode * n = get_enode(i);
+            if (ctx.is_relevant(n)) {
+	        enode * r = n->get_root();
+		if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) {
+		  TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+		  theory_var r_th_var = r->get_th_var(get_id());
+		  SASSERT(r_th_var != null_theory_var);
+		  result.push_back(r_th_var);
+		}
+		r->set_mark();
+		to_unmark.push_back(r);
+            }
+        }
+        unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
+    }
+#endif
 
     /**
        \brief Create interface variables for shared array variables.