diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-11 12:47:47 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-11 12:47:47 -0400 |
commit | 5074826887fc34423a9179eec85813a245709f11 (patch) | |
tree | 7a3df37180650ac1f3e63813d841aaf8ce6d1e5f | |
parent | f9ab7f28104831a05f485c346bf8c997d88975dd (diff) |
Improved speed of no redundant lemma assertion by using hash set
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 7 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 |
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); |