Improved speed of no redundant lemma assertion by using hash set

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 97e8a0faa8e13ea85b0e2ad51a4ffc394689fc06..8018931078d15a85f3b1484495e438148e66ebb7 100644 (file)
--- 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 2a008382302f70a178962df43d419c46ee43ae6e..e0191ccc940f7f1442f4280c914854e7bef686a5 100644 (file)
--- 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);