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 d005e9473462cbec31fbd1a8e34f5379fe49dc50..445b2d2426de54845a752ddd95fb58822b5c8122 100644 (file)
--- 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 6ef9d18dd8076a726306c653b26f772f0d2e42dc..9ab5f8e1c9918aa1c0f6e051e99c94ab286c9c8b 100644 (file)
--- 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;