Improved speed of no redundant lemma assertion by using hash set

2 files changed, 3 insertions, 6 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 97e8a0faa..801893107 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1296,11 +1296,8 @@ void TheoryArrays::checkModel(Effort e)
     Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl;
     d_out->lemma(d_lemmas.back());
 #ifdef CVC4_ASSERTIONS
-    context::CDList<Node>::const_iterator it = d_lemmasSaved.begin(), it_end = d_lemmasSaved.end();
-    for (; it != it_end; ++it) {
-      Assert((*it) != d_lemmas.back());
-    }
-    d_lemmasSaved.push_back(d_lemmas.back());
+    Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end());
+    d_lemmasSaved.insert(d_lemmas.back());
 #endif
     d_lemmas.pop_back();
   }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 2a0083823..e0191ccc9 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -358,7 +358,7 @@ class TheoryArrays : public Theory {
   // List of nodes that need permanent references in this context
   context::CDList<Node> d_permRef;
   context::CDList<Node> d_modelConstraints;
-  context::CDList<Node> d_lemmasSaved;
+  context::CDHashSet<Node, NodeHashFunction > d_lemmasSaved;
   std::vector<Node> d_lemmas;
 
   Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true);