From c5fb1c1223f6123d0e2ac9b762344c7b600ecd24 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 7 Jun 2018 09:45:17 -0700
Subject: [PATCH] Use vector instead of a hashtable to represent a set

---
 src/muz/spacer/spacer_proof_utils.cpp | 42 ++++++++++++++++++---------
 src/muz/spacer/spacer_proof_utils.h   |  9 +++---
 2 files changed, 33 insertions(+), 18 deletions(-)

diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp
index a8a90fa2b..4a64f3d08 100644
--- a/src/muz/spacer/spacer_proof_utils.cpp
+++ b/src/muz/spacer/spacer_proof_utils.cpp
@@ -229,29 +229,43 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
 
         m_visited.mark(p);
 
-        // create active_hyps-set and parent_hyps-set for step p
-        proof_set* active_hyps = alloc(proof_set);
-        m_pinned_active_hyps.insert(active_hyps);
-        m_active_hyps.insert(p, active_hyps);
 
+        proof_ptr_vector* active_hyps = nullptr;
         // fill both sets
         if (m.is_hypothesis(p)) {
-            active_hyps->insert(p);
+            // create active_hyps-set for step p
+            proof_ptr_vector* active_hyps = alloc(proof_ptr_vector);
+            m_pinned_active_hyps.insert(active_hyps);
+            m_active_hyps.insert(p, active_hyps);
+            active_hyps->push_back(p);
             m_open_mark.mark(p);
-
             m_hyp_mark.mark(m.get_fact(p));
+            continue;
         }
-        else {
-            for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
-                proof* parent = m.get_parent(p, i);
 
-                if (!m.is_lemma(p)) {
-                    // lemmas clear all hypotheses
-                    set_union(*active_hyps, *m_active_hyps.find(parent));
-                    m_open_mark.mark(p, !active_hyps->empty());
+        ast_fast_mark1 seen;
+
+        active_hyps = alloc(proof_ptr_vector);
+        for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
+            proof* parent = m.get_parent(p, i);
+            // lemmas clear all hypotheses above them
+            if (m.is_lemma(p)) continue;
+            for (auto *x : *m_active_hyps.find(parent)) {
+                if (!seen.is_marked(x)) {
+                    seen.mark(x);
+                    active_hyps->push_back(x);
+                    m_open_mark.mark(p);
                 }
             }
         }
+        if (active_hyps->empty()) {
+            dealloc(active_hyps);
+            m_active_hyps.insert(p, &m_empty_vector);
+        }
+        else {
+            m_pinned_active_hyps.push_back(active_hyps);
+            m_active_hyps.insert(p, active_hyps);
+        }
     }
 }
 
@@ -404,7 +418,7 @@ proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
     SASSERT(m.is_false(m.get_fact(premise)));
     SASSERT(m_active_hyps.contains(premise));
 
-    proof_set* active_hyps = m_active_hyps.find(premise);
+    proof_ptr_vector* active_hyps = m_active_hyps.find(premise);
 
     // if there is no active hypothesis return the premise
     if (!m_open_mark.is_marked(premise)) {
diff --git a/src/muz/spacer/spacer_proof_utils.h b/src/muz/spacer/spacer_proof_utils.h
index f8d8d263b..ead85f885 100644
--- a/src/muz/spacer/spacer_proof_utils.h
+++ b/src/muz/spacer/spacer_proof_utils.h
@@ -57,16 +57,17 @@ public:
     proof_ref reduce(proof* pf);
 
 private:
-    typedef obj_hashtable<expr> expr_set;
-    typedef obj_hashtable<proof> proof_set;
+    typedef ptr_vector<proof> proof_ptr_vector;
 
     ast_manager &m;
 
+    proof_ptr_vector m_empty_vector;
+
     // created expressions
     expr_ref_vector m_pinned;
 
     // created sets of active hypothesis
-    ptr_vector<proof_set> m_pinned_active_hyps;
+    ptr_vector<proof_ptr_vector> m_pinned_active_hyps;
 
     // maps a proof to the transformed proof
     obj_map<proof, proof*> m_cache;
@@ -75,7 +76,7 @@ private:
     obj_map<expr, proof*> m_units;
 
     // maps a proof node to the set of its  active (i.e., in scope) hypotheses
-    obj_map<proof, proof_set*> m_active_hyps;
+    obj_map<proof, proof_ptr_vector*> m_active_hyps;
 
     /// marks if an expression is ever used as a hypothesis in a proof
     expr_mark m_hyp_mark;