* added propagation as lemmas to TheoryBV:

   * modified BVMinisat to work incrementally
   * added more bv regressions 

1 files changed, 129 insertions, 108 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c0855122e..edaf8c154 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -106,7 +106,7 @@ void inline makeZero(Bits& bits, unsigned width) {
  * @return the carry-out
  */
 Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry) {
-  Assert(res.size() == 0 && a.size() == b.size());
+  Assert(a.size() == b.size() && res.size() == 0);
   
   for (unsigned i = 0 ; i < a.size(); ++i) {
     Node sum = mkXor(mkXor(a[i], b[i]), carry);
@@ -119,6 +119,24 @@ Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry)
   return carry;
 }
 
+inline void shiftAddMultiplier(const Bits&a, const Bits&b, Bits& res) {
+  
+  for (unsigned i = 0; i < a.size(); ++i) {
+    res.push_back(mkNode(kind::AND, b[0], a[i])); 
+  }
+  
+  for(unsigned k = 1; k < res.size(); ++k) {
+  Node carry_in = mkFalse();
+  Node carry_out;
+    for(unsigned j = 0; j < res.size() -k; ++j) {
+      Node aj = mkAnd(a[j], b[k]);
+      carry_out = mkOr(mkAnd(res[j+k], aj),
+                       mkAnd( mkXor(res[j+k], aj), carry_in));
+      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
+      carry_in = carry_out; 
+    }
+  }
+}
 
 Node inline uLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
   Assert (a.size() && b.size());
@@ -175,13 +193,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
 
 
 Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
-  Trace("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+  BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
 
 Node DefaultEqBB(TNode node, Bitblaster* bb) {
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   
   Assert(node.getKind() == kind::EQUAL);
   Bits lhs, rhs; 
@@ -203,7 +221,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) {
 
 
 Node AdderUltBB(TNode node, Bitblaster* bb) {
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -225,7 +243,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) {
 
 
 Node DefaultUltBB(TNode node, Bitblaster* bb) {
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -238,7 +256,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) {
 }
 
 Node DefaultUleBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULE);
   Bits a, b;
   
@@ -251,31 +269,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultUgtBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 Node DefaultUgeBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 // Node DefaultSltBB(TNode node, Bitblaster* bb){
-//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ult
 //   Unimplemented(); 
 // }
 
 // Node DefaultSleBB(TNode node, Bitblaster* bb){
-//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ule
 //   Unimplemented(); 
 // }
 
 
 Node DefaultSltBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -287,7 +305,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultSleBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -299,13 +317,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){
 }
  
 Node DefaultSgtBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 Node DefaultSgeBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
@@ -314,7 +332,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){
 /// Term bitblasting strategies 
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
-  Trace("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+  BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
@@ -327,12 +345,12 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     bits.push_back(utils::mkBitOf(node, i));
   }
 
-  Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
-  Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
+  BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+  BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::CONST_BITVECTOR);
   Assert(bits.size() == 0);
   
@@ -345,12 +363,12 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
       bits.push_back(utils::mkTrue()); 
     }
   }
-  Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
 }
 
 
 void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NOT);
   Assert(bits.size() == 0);
   Bits bv; 
@@ -359,7 +377,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
   Assert(bits.size() == 0);
   
   Assert (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -373,64 +391,68 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
     }
   }
   Assert (bits.size() == utils::getSize(node)); 
-  Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
 }
 
-
 void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
-
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_AND &&
+  BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+  
+  Assert(node.getKind() == kind::BITVECTOR_AND &&
          bits.size() == 0);
   
-  Bits lhs, rhs;
-  bb->bbTerm(node[0], rhs);
-  bb->bbTerm(node[1], lhs);
-
-  Assert (lhs.size() == rhs.size()); 
-  for (unsigned i = 0; i < lhs.size(); ++i) {
-    bits.push_back(utils::mkAnd(lhs[i], rhs[i])); 
+  for(unsigned j = 0; j < utils::getSize(node); ++j) {
+    NodeBuilder<> andBuilder(kind::AND);
+    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+      Bits current;
+      bb->bbTerm(node[i], current);
+      andBuilder << current[j];
+      Assert(utils::getSize(node) == current.size());
+    }
+    bits.push_back(andBuilder); 
   }
-
 }
 
 void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
 
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_OR &&
+  Assert(node.getKind() == kind::BITVECTOR_OR &&
          bits.size() == 0);
   
-  Bits lhs, rhs;
-  bb->bbTerm(node[0], lhs);
-  bb->bbTerm(node[1], rhs);
-  Assert(lhs.size() == rhs.size()); 
-  
-  for (unsigned i = 0; i < lhs.size(); ++i) {
-    bits.push_back(utils::mkOr(lhs[i], rhs[i])); 
+  for(unsigned j = 0; j < utils::getSize(node); ++j) {
+    NodeBuilder<> orBuilder(kind::OR);
+    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+      Bits current;
+      bb->bbTerm(node[i], current);
+      orBuilder << current[j];
+      Assert(utils::getSize(node) == current.size());
+    }
+    bits.push_back(orBuilder); 
   }
 }
 
 void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
 
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_XOR &&
+  Assert(node.getKind() == kind::BITVECTOR_XOR &&
          bits.size() == 0);
   
-  Bits lhs, rhs;
-  bb->bbTerm(node[0], lhs);
-  bb->bbTerm(node[1], rhs);
-  Assert(lhs.size() == rhs.size()); 
-  
-  for (unsigned i = 0; i < lhs.size(); ++i) {
-    bits.push_back(utils::mkXor(lhs[i], rhs[i])); 
+  for(unsigned j = 0; j < utils::getSize(node); ++j) {
+    Bits first;
+    bb->bbTerm(node[0], first); 
+    Node bitj = first[j];
+    
+    for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+      Bits current;
+      bb->bbTerm(node[i], current);
+      bitj = utils::mkNode(kind::XOR, bitj, current[j]);
+      Assert(utils::getSize(node) == current.size());
+    }
+    bits.push_back(bitj); 
   }
 }
 
 void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
 
   Assert(node.getNumChildren() == 2 &&
          node.getKind() == kind::BITVECTOR_XNOR &&
@@ -447,17 +469,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 
 void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+  BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
 
   Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
   Bits a, b;
@@ -475,51 +497,50 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+  BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
   Assert(res.size() == 0 &&
          node.getKind() == kind::BITVECTOR_MULT);
-  Bits a, b;
-  bb->bbTerm(node[0], a);
-  bb->bbTerm(node[1], b);
 
-  // constructs a simple shift and add multiplier building the result in
-  // in res
-  
-  for (unsigned i = 0; i < a.size(); ++i) {
-    res.push_back(mkNode(kind::AND, b[0], a[i])); 
-  }
-  
-  for(unsigned k = 1; k < res.size(); ++k) {
-  Node carry_in = mkFalse();
-  Node carry_out;
-    for(unsigned j = 0; j < res.size() -k; ++j) {
-      Node aj = mkAnd(a[j], b[k]);
-      carry_out = mkOr(mkAnd(res[j+k], aj),
-                       mkAnd( mkXor(res[j+k], aj), carry_in));
-      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
-      carry_in = carry_out; 
-    }
+  Bits newres; 
+  bb->bbTerm(node[0], res); 
+  for(unsigned i = 1; i < node.getNumChildren(); ++i) {
+    Bits current;
+    bb->bbTerm(node[i], current);
+    newres.clear(); 
+    // constructs a simple shift and add multiplier building the result
+    // in res
+    shiftAddMultiplier(res, current, newres);
+    res = newres;
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_PLUS &&
          res.size() == 0);
 
-  Bits a, b;
-  bb->bbTerm(node[0], a);
-  bb->bbTerm(node[1], b); 
+  bb->bbTerm(node[0], res);
 
-  Assert(a.size() == b.size() && utils::getSize(node) == a.size());
-  rippleCarryAdder(a, b, res, mkFalse());
+  Bits newres;
+
+  for(unsigned i = 1; i < node.getNumChildren(); ++i) {
+    Bits current;
+    bb->bbTerm(node[i], current);
+    newres.clear(); 
+    rippleCarryAdder(res, current, newres, utils::mkFalse());
+    res = newres; 
+  }
+  
+  Assert(res.size() == utils::getSize(node));
 }
 
 
 void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_SUB &&  bits.size() == 0);
+  BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_SUB &&
+         node.getNumChildren() == 2 &&
+         bits.size() == 0);
     
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -534,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
   
   Bits a;
@@ -612,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 }
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UDIV &&  q.size() == 0);
 
   Bits a, b;
@@ -628,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UREM &&  rem.size() == 0);
 
   Bits a, b;
@@ -645,23 +666,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
 
 void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 
 void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_SHL &&
           res.size() == 0);
   Bits a, b;
@@ -688,11 +709,11 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 }
 
 void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_LSHR &&
           res.size() == 0);
   Bits a, b;
@@ -719,12 +740,12 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 }
 
 void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
 
-  Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_ASHR &&
           res.size() == 0);
   Bits a, b;
@@ -752,7 +773,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 
 }
 
@@ -770,14 +791,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
   Assert (bits.size() == high - low + 1);   
 
-  Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
-  Debug("bitvector-bb") << "                               with bits " << toString(bits); 
+  BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
        
 }
 
 
 void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   // this should be rewritten 
   Unimplemented(); 
@@ -785,7 +806,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 
-  Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
  
   // this should be rewritten 
   Unimplemented();
@@ -793,7 +814,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
 
   Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
           res_bits.size() == 0);
@@ -816,14 +837,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
 
   Unimplemented(); 
 }
 
 void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }