From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 15 May 2012 22:02:47 +0000 (+0000)
Subject: fixed QF_BV performance problem due to using CDList instead of CDQueue
X-Git-Tag: cvc5-1.0.0~8168
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03930f2a6fdfb85ecc81594ec65f41d7c1284577;p=cvc5.git

fixed QF_BV performance problem due to using CDList instead of CDQueue
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d005e9473..445b2d242 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -205,9 +205,10 @@ void TheoryBV::check(Effort e)
 
   // bit-blasting atoms on queue
 
-  for (unsigned i = 0; i < d_bitblastQueue.size(); ++i) {
-    d_bitblaster->bbAtom(d_bitblastQueue[i]);
-    // would be nice to clear the bitblastQueue?
+  while (!d_bitblastQueue.empty()) {
+    TNode node = d_bitblastQueue.front();
+    d_bitblaster->bbAtom(node);
+    d_bitblastQueue.pop(); 
   }
   
   // bit-blaster propagation 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 6ef9d18dd..9ab5f8e1c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -56,7 +56,7 @@ private:
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
 
-  context::CDList<TNode> d_bitblastQueue; 
+  context::CDQueue<TNode> d_bitblastQueue; 
   
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;