Removing BVDebug and replacing with Debug.

1 files changed, 51 insertions, 51 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c25c40c22..a952b2929 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -191,13 +191,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
 
 
 Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+  Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
 
 Node DefaultEqBB(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   
   Assert(node.getKind() == kind::EQUAL);
   Bits lhs, rhs; 
@@ -219,7 +219,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) {
 
 
 Node AdderUltBB(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -241,7 +241,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) {
 
 
 Node DefaultUltBB(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -254,7 +254,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) {
 }
 
 Node DefaultUleBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULE);
   Bits a, b;
   
@@ -267,31 +267,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultUgtBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 Node DefaultUgeBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 // Node DefaultSltBB(TNode node, Bitblaster* bb){
-//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ult
 //   Unimplemented(); 
 // }
 
 // Node DefaultSleBB(TNode node, Bitblaster* bb){
-//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ule
 //   Unimplemented(); 
 // }
 
 
 Node DefaultSltBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -303,7 +303,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultSleBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -315,13 +315,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){
 }
  
 Node DefaultSgtBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 Node DefaultSgeBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
@@ -330,7 +330,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){
 /// Term bitblasting strategies 
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+  Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
@@ -342,15 +342,15 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
 
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
-    BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
+    Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+    Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
 
    bb->storeVariable(node);
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::CONST_BITVECTOR);
   Assert(bits.size() == 0);
   
@@ -364,13 +364,13 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+    Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
   }
 }
 
 
 void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NOT);
   Assert(bits.size() == 0);
   Bits bv; 
@@ -379,7 +379,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
   Assert(bits.size() == 0);
   
   Assert (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -394,12 +394,12 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
   Assert (bits.size() == utils::getSize(node)); 
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+    Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
   }
 }
 
 void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
   
   Assert(node.getKind() == kind::BITVECTOR_AND &&
          bits.size() == 0);
@@ -417,7 +417,7 @@ void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
 
   Assert(node.getKind() == kind::BITVECTOR_OR &&
          bits.size() == 0);
@@ -435,7 +435,7 @@ void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
 
   Assert(node.getKind() == kind::BITVECTOR_XOR &&
          bits.size() == 0);
@@ -456,7 +456,7 @@ void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
 
   Assert(node.getNumChildren() == 2 &&
          node.getKind() == kind::BITVECTOR_XNOR &&
@@ -473,17 +473,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 
 void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+  Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
 
   Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
   Bits a, b;
@@ -501,7 +501,7 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+  Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
   Assert(res.size() == 0 &&
          node.getKind() == kind::BITVECTOR_MULT);
 
@@ -517,12 +517,12 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
     res = newres;
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_PLUS &&
          res.size() == 0);
 
@@ -543,7 +543,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
 
 
 void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_SUB &&
          node.getNumChildren() == 2 &&
          bits.size() == 0);
@@ -561,7 +561,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
   
   Bits a;
@@ -639,7 +639,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 }
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&  q.size() == 0);
 
   Bits a, b;
@@ -666,7 +666,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL &&  rem.size() == 0);
 
   Bits a, b;
@@ -694,23 +694,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
 
 void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 
 void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_SHL &&
           res.size() == 0);
   Bits a, b;
@@ -738,12 +738,12 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
 void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_LSHR &&
           res.size() == 0);
   Bits a, b;
@@ -771,13 +771,13 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
 void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_ASHR &&
           res.size() == 0);
   Bits a, b;
@@ -806,7 +806,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
@@ -825,14 +825,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
   Assert (bits.size() == high - low + 1);   
 
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
-    BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
+    Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+    Debug("bitvector-bb") << "                               with bits " << toString(bits); 
   }
 }
 
 
 void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   // this should be rewritten 
   Unimplemented(); 
@@ -840,7 +840,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
  
   // this should be rewritten 
   Unimplemented();
@@ -848,7 +848,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
 
   Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
           res_bits.size() == 0);
@@ -871,14 +871,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
 
   Unimplemented(); 
 }
 
 void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }