From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 22 Mar 2011 02:11:09 +0000 (+0000)
Subject: updating debug output usage to eliviate impact of bug 252
X-Git-Tag: cvc5-1.0.0~8637
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=74084011310e0af055c0055378620a5d19de1e52;p=cvc5.git

updating debug output usage to eliviate impact of bug 252
---

diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index d020ef362..217ebadcd 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -9,6 +9,7 @@
 
 #include <iostream>
 #include "context/cdo.h"
+#include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
 namespace context {
@@ -50,7 +51,7 @@ class BacktrackableSetCollection {
     while (d_nodesInserted < d_memory.size()) {
       const tree_entry_type& node = d_memory.back();
 
-      Debug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
+      BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
                                  << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
 
       if (node.hasParent()) {
@@ -256,7 +257,7 @@ public:
 
     // Find the biggest node smaleer than value (it must exist)
     while (set != null) {
-      Debug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+      BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() >= value) {
         // If the node is bigger than the value, we need a smaller one
@@ -283,7 +284,7 @@ public:
 
     // Find the smallest node bigger than value (it must exist)
     while (set != null) {
-      Debug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+      BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() <= value) {
         // If the node is smaller than the value, we need a bigger one
@@ -350,7 +351,7 @@ public:
     backtrack();
     Assert(isValid(set));
 
-    Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+    BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
 
     // Empty set no elements
     if (set == null) {
diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 5d4212849..0450c4535 100644
--- a/src/theory/bv/equality_engine.h
+++ b/src/theory/bv/equality_engine.h
@@ -313,7 +313,7 @@ public:
    */
   EqualityEngine(OwnerClass& owner, context::Context* context, std::string name)
   : d_notify(owner), d_assertedEqualitiesCount(context, 0), d_stats(name) {
-    Debug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null <<
+    BVDebug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null <<
         ", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl;
   }
 
@@ -379,7 +379,7 @@ private:
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 size_t EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addTerm(TNode t) {
 
-  Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl;
 
   // If term already added, retrurn it's id
   if (hasTerm(t)) return getNodeId(t);
@@ -429,7 +429,7 @@ EqualityNode& EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::get
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality(TNode t1, TNode t2, Node reason) {
 
-  Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
 
   // Backtrack if necessary
   backtrack();
@@ -466,11 +466,11 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality(
   // Depending on the merge preference (such as size), merge them
   std::vector<size_t> triggers;
   if (UnionFindPreferences::mergePreference(d_nodes[t2classId], node2.getSize(), d_nodes[t1classId], node1.getSize())) {
-    Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t1 << " into " << t2 << std::endl;
+    BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t1 << " into " << t2 << std::endl;
     merge(node2, node1, triggers);
     d_assertedEqualities.push_back(Equality(t2classId, t1classId));
   } else {
-    Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t2 << " into " << t1 << std::endl;
+    BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t2 << " into " << t1 << std::endl;
     merge(node1, node2, triggers);
     d_assertedEqualities.push_back(Equality(t1classId, t2classId));
   }
@@ -496,7 +496,7 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality(
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 TNode EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getRepresentative(TNode t) const {
 
-  Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
 
   Assert(hasTerm(t));
 
@@ -504,14 +504,14 @@ TNode EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getRepresen
   const_cast<EqualityEngine*>(this)->backtrack();
   size_t representativeId = const_cast<EqualityEngine*>(this)->getEqualityNode(t).getFind();
 
-  Debug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
+  BVDebug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
 
   return d_nodes[representativeId];
 }
 
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::areEqual(TNode t1, TNode t2) const {
-  Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl;
 
   Assert(hasTerm(t1));
   Assert(hasTerm(t2));
@@ -521,7 +521,7 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::areEqual(TNo
   size_t rep1 = const_cast<EqualityEngine*>(this)->getEqualityNode(t1).getFind();
   size_t rep2 = const_cast<EqualityEngine*>(this)->getEqualityNode(t2).getFind();
 
-  Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
+  BVDebug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
 
   return rep1 == rep2;
 }
@@ -529,7 +529,7 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::areEqual(TNo
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::merge(EqualityNode& class1, EqualityNode& class2, std::vector<size_t>& triggers) {
 
-  Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
 
   Assert(triggers.empty());
 
@@ -579,7 +579,7 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::merge(Equali
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id) {
 
-  Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
 
   // Now unmerge the lists (same as merge)
   class1.merge<false>(class2);
@@ -616,7 +616,7 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::backtrack()
 
     ++ d_stats.backtracksCount;
 
-    Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl;
+    BVDebug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl;
 
     for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) {
       // Get the ids of the merged classes
@@ -627,7 +627,7 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::backtrack()
 
     d_assertedEqualities.resize(d_assertedEqualitiesCount);
 
-    Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl;
+    BVDebug("equality") << "EqualityEngine::backtrack(): edges" << std::endl;
 
     for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) {
       EqualityEdge& edge1 = d_equalityEdges[i];
@@ -644,7 +644,7 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::backtrack()
 
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addGraphEdge(size_t t1, size_t t2, Node reason) {
-  Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << ")" << std::endl;
   size_t edge = d_equalityEdges.size();
   d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1]));
   d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2]));
@@ -672,7 +672,7 @@ template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferenc
 void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
   Assert(getRepresentative(t1) == getRepresentative(t2));
 
-  Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
 
   // If the nodes are the same, we're done
   if (t1 == t2) return;
@@ -697,12 +697,12 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanati
     BfsData current = bfsQueue[currentIndex];
     size_t currentNode = current.nodeId;
 
-    Debug("equality") << "EqualityEngine::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
+    BVDebug("equality") << "EqualityEngine::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
 
     // Go through the equality edges of this node
     size_t currentEdge = d_equalityGraph[currentNode];
 
-    Debug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
+    BVDebug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
 
     while (currentEdge != BitSizeTraits::id_null) {
       // Get the edge
@@ -711,18 +711,18 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanati
       // If not just the backwards edge
       if ((currentEdge | 1u) != (current.edgeId | 1u)) {
 
-        Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+        BVDebug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
 
         // Did we find the path
         if (edge.getNodeId() == t2Id) {
 
-          Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl;
+          BVDebug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl;
 
           // Reconstruct the path
           do {
             // Add the actual equality to the vector
             equalities.push_back(d_equalityReasons[currentEdge >> 1]);
-            Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityReasons[currentEdge >> 1] << std::endl;
+            BVDebug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityReasons[currentEdge >> 1] << std::endl;
 
             // Go to the previous
             currentEdge = bfsQueue[currentIndex].edgeId;
@@ -749,7 +749,7 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanati
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 size_t EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addTrigger(TNode t1, TNode t2) {
 
-  Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ")" << std::endl;
+  BVDebug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ")" << std::endl;
 
   Assert(hasTerm(t1));
   Assert(hasTerm(t2));
@@ -774,7 +774,7 @@ size_t EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addTrigger
   d_nodeTriggers[t1Id] = t1NewTriggerId;
   d_nodeTriggers[t2Id] = t2NewTriggerId;
 
-  Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => " << t1NewTriggerId / 2 << std::endl;
+  BVDebug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => " << t1NewTriggerId / 2 << std::endl;
 
   // Return the global id of the trigger
   return t1NewTriggerId / 2;
@@ -792,7 +792,7 @@ Node EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::normalize(TN
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 Node EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::normalizeWithCache(TNode node, std::set<TNode>& assumptions) {
 
-  Debug("equality") << "EqualityEngine::normalize(" << node << ")" << push << std::endl;
+  BVDebug("equality") << "EqualityEngine::normalize(" << node << ")" << push << std::endl;
 
   normalization_cache::iterator find = d_normalizationCache.find(node);
   if (find != d_normalizationCache.end()) {
@@ -830,7 +830,7 @@ Node EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::normalizeWit
     result = builder;
   }
 
-  Debug("equality") << "EqualityEngine::normalize(" << node << ") => " << result << pop << std::endl;
+  BVDebug("equality") << "EqualityEngine::normalize(" << node << ") => " << result << pop << std::endl;
 
   // Cache the result for real now
   d_normalizationCache[node] = result;
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
index ed516fa31..78ed4f265 100644
--- a/src/theory/bv/slice_manager.h
+++ b/src/theory/bv/slice_manager.h
@@ -222,7 +222,7 @@ bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs) {
 template <class TheoryBitvector>
 bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs, const std::set<TNode>& assumptions) {
 
-  Debug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << push << std::endl;
+  BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << push << std::endl;
 
   bool ok;
 
@@ -249,7 +249,7 @@ bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs, const st
   // Slice the individual terms to align them
   ok = sliceAndSolve(lhsTerms, rhsTerms, assumptions);
 
-  Debug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << pop << std::endl;
+  BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << pop << std::endl;
 
   return ok;
 }
@@ -259,27 +259,27 @@ template <class TheoryBitvector>
 bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::vector<Node>& rhs, const std::set<TNode>& assumptions)
 {
 
-  Debug("slicing") << "SliceManager::sliceAndSolve()" << std::endl;
+  BVDebug("slicing") << "SliceManager::sliceAndSolve()" << std::endl;
 
   // Go through the work-list, solve and align
   while (!lhs.empty()) {
 
     Assert(!rhs.empty());
 
-    Debug("slicing") << "SliceManager::sliceAndSolve(): lhs " << utils::vectorToString(lhs) << std::endl;
-    Debug("slicing") << "SliceManager::sliceAndSolve(): rhs " << utils::vectorToString(rhs) << std::endl;
+    BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs " << utils::vectorToString(lhs) << std::endl;
+    BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs " << utils::vectorToString(rhs) << std::endl;
 
     // The terms that we need to slice
     Node lhsTerm = lhs.back();
     Node rhsTerm = rhs.back();
 
-    Debug("slicing") << "SliceManager::sliceAndSolve(): " << lhsTerm << " : " << rhsTerm << std::endl;
+    BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << lhsTerm << " : " << rhsTerm << std::endl;
 
     // If the terms are not sliced wrt the current slicing, we have them sliced
     lhs.pop_back();
     if (!isSliced(lhsTerm)) {
       if (!slice(lhsTerm, lhs)) return false;
-      Debug("slicing") << "SliceManager::sliceAndSolve(): lhs sliced" << std::endl;
+      BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs sliced" << std::endl;
       continue;
     }
     rhs.pop_back();
@@ -287,11 +287,11 @@ bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::v
       if (!slice(rhsTerm, rhs)) return false;
       // We also need to put lhs back
       lhs.push_back(lhsTerm);
-      Debug("slicing") << "SliceManager::sliceAndSolve(): rhs sliced" << std::endl;
+      BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs sliced" << std::endl;
       continue;
     }
 
-    Debug("slicing") << "SliceManager::sliceAndSolve(): both lhs and rhs sliced already" << std::endl;
+    BVDebug("slicing") << "SliceManager::sliceAndSolve(): both lhs and rhs sliced already" << std::endl;
 
     // The solving concatenation
     std::vector<Node> concatTerms;
@@ -322,7 +322,7 @@ bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::v
       SOLVING_FOR_RHS
     } solvingFor = sizeDifference < 0 || lhsTerm.getKind() == kind::CONST_BITVECTOR ? SOLVING_FOR_RHS : SOLVING_FOR_LHS;
 
-    Debug("slicing") << "SliceManager::sliceAndSolve(): " << (solvingFor == SOLVING_FOR_LHS ? "solving for LHS" : "solving for RHS") << std::endl;
+    BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << (solvingFor == SOLVING_FOR_LHS ? "solving for LHS" : "solving for RHS") << std::endl;
 
     // When we slice in order to align, we might have to reslice the one we are solving for
     bool reslice = false;
@@ -404,7 +404,7 @@ bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::v
     Assert(sizeDifference == 0);
 
     Node concat = utils::mkConcat(concatTerms);
-    Debug("slicing") << "SliceManager::sliceAndSolve(): concatenation " << concat << std::endl;
+    BVDebug("slicing") << "SliceManager::sliceAndSolve(): concatenation " << concat << std::endl;
 
     // We have them equal size now. If the base term of the one we are solving is solved into a
     // non-trivial concatenation already, we have to normalize. A concatenation is non-trivial if
@@ -423,7 +423,7 @@ bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::v
         if (!ok) return false;
       } else {
         // We're fine, just add the equality
-        Debug("slicing") << "SliceManager::sliceAndSolve(): adding " << lhsTerm << " = " << concat << " " << utils::setToString(assumptions) << std::endl;
+        BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << lhsTerm << " = " << concat << " " << utils::setToString(assumptions) << std::endl;
         d_equalityEngine.addTerm(concat);
         bool ok = d_equalityEngine.addEquality(lhsTerm, concat, utils::mkConjunction(assumptions));
         if (!ok) return false;
@@ -443,7 +443,7 @@ bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::v
         if (!ok) return false;
       } else {
         // We're fine, just add the equality
-        Debug("slicing") << "SliceManager::sliceAndSolve(): adding " << rhsTerm << " = " << concat << utils::setToString(assumptions) << std::endl;
+        BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << rhsTerm << " = " << concat << utils::setToString(assumptions) << std::endl;
         d_equalityEngine.addTerm(concat);
         bool ok = d_equalityEngine.addEquality(rhsTerm, concat, utils::mkConjunction(assumptions));
         if (!ok) return false;
@@ -459,7 +459,7 @@ bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::v
 template <class TheoryBitvector>
 bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
 
-  Debug("slicing") << "SliceManager::isSliced(" << node << ")" << std::endl;
+  BVDebug("slicing") << "SliceManager::isSliced(" << node << ")" << std::endl;
 
   bool result = false;
 
@@ -493,13 +493,13 @@ bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
     }
   }
 
-  Debug("slicing") << "SliceManager::isSliced(" << node << ") => " << (result ? "true" : "false") << std::endl;
+  BVDebug("slicing") << "SliceManager::isSliced(" << node << ") => " << (result ? "true" : "false") << std::endl;
   return result;
 }
 
 template <class TheoryBitvector>
 bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
-  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl;
+  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl;
 
   bool ok = true;
 
@@ -526,7 +526,7 @@ bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
 
   // Add the slice to the set
   d_setCollection.insert(sliceSet, slicePoint);
-  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl;
+  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl;
 
   // Add the terms and the equality to the equality engine
   Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint);
@@ -554,7 +554,7 @@ bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
     ok = solveEquality(nodeSliceRepresentative, concat, assumptions);
   }
 
-  Debug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl;
+  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl;
 
   return ok;
 }
@@ -562,15 +562,15 @@ bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
 template <class TheoryBitvector>
 inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) {
 
-  Debug("slicing") << "SliceManager::slice(" << node << ")" << std::endl;
+  BVDebug("slicing") << "SliceManager::slice(" << node << ")" << std::endl;
 
   Assert(!isSliced(node));
 
   // The indices of the beginning and (one past) end
   unsigned high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1 : utils::getSize(node);
   unsigned low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-  Debug("slicing") << "SliceManager::slice(" << node << "): low: " << low << std::endl;
-  Debug("slicing") << "SliceManager::slice(" << node << "): high: " << high << std::endl;
+  BVDebug("slicing") << "SliceManager::slice(" << node << "): low: " << low << std::endl;
+  BVDebug("slicing") << "SliceManager::slice(" << node << "): high: " << high << std::endl;
 
   // Get the base term
   TNode nodeBase = baseTerm(node);
@@ -591,7 +591,7 @@ inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>&
 
   Assert(d_setCollection.size(nodeSliceSet) >= 2);
 
-  Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl;
+  BVDebug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl;
   std::vector<size_t> slicePoints;
   if (low + 1 < high) {
     d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints);
@@ -601,9 +601,9 @@ inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>&
   // and generate the slices [i_0:low-1][low:i_1-1] [i_1:i2] ... [i_{n-1}:high-1][high:i_n-1]. They are in reverse order,
   // as they should be
   size_t i_0 = low == 0 ? 0 : d_setCollection.prev(nodeSliceSet, low + 1);
-  Debug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl;
+  BVDebug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl;
   size_t i_n = high == utils::getSize(nodeBase) ? high: d_setCollection.next(nodeSliceSet, high - 1);
-  Debug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl;
+  BVDebug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl;
 
   // Add the new points to the slice set (they might be there already)
   if (high < i_n) {
@@ -611,13 +611,13 @@ inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>&
   }
   // Construct the actuall slicing
   if (slicePoints.size() > 0) {
-    Debug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[0] - 1, low) << std::endl;
+    BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[0] - 1, low) << std::endl;
     sliced.push_back(utils::mkExtract(nodeBase, slicePoints[0] - 1, low));
     for (unsigned i = 1; i < slicePoints.size(); ++ i) {
-      Debug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1])<< std::endl;
+      BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1])<< std::endl;
       sliced.push_back(utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1]));
     }
-    Debug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, high-1, slicePoints.back()) << std::endl;
+    BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, high-1, slicePoints.back()) << std::endl;
     sliced.push_back(utils::mkExtract(nodeBase, high-1, slicePoints.back()));
   } else {
     sliced.push_back(utils::mkExtract(nodeBase, high - 1, low));
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 51de8df28..258345ad8 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -31,7 +31,7 @@ using namespace std;
 
 void TheoryBV::preRegisterTerm(TNode node) {
 
-  Debug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+  BVDebug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
   if (node.getKind() == kind::EQUAL) {
     d_eqEngine.addTerm(node[0]);
@@ -54,7 +54,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
 
 void TheoryBV::check(Effort e) {
 
-  Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+  BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
   while(!done()) {
 
@@ -62,7 +62,7 @@ void TheoryBV::check(Effort e) {
     TNode assertion = get();
     d_assertions.insert(assertion);
 
-    Debug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl;
+    BVDebug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl;
 
     // Do the right stuff
     switch (assertion.getKind()) {
@@ -81,11 +81,11 @@ void TheoryBV::check(Effort e) {
       Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions);
       Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions);
 
-      Debug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
+      BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
       
       // No need to slice the equality, the whole thing *should* be deduced
       if (lhsNormalized == rhsNormalized) {
-        Debug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
+        BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
         assumptions.insert(assertion);
         d_out->conflict(mkConjunction(assumptions));
         return;
@@ -101,11 +101,11 @@ void TheoryBV::check(Effort e) {
 
   if (fullEffort(e)) {
 
-    Debug("bitvector") << "TheoryBV::check(" << e << "): checking dis-equalities" << std::endl;
+    BVDebug("bitvector") << "TheoryBV::check(" << e << "): checking dis-equalities" << std::endl;
 
     for (unsigned i = 0, i_end = d_disequalities.size(); i < i_end; ++ i) {
 
-      Debug("bitvector") << "TheoryBV::check(" << e << "): checking " << d_disequalities[i] << std::endl;
+      BVDebug("bitvector") << "TheoryBV::check(" << e << "): checking " << d_disequalities[i] << std::endl;
 
       TNode equality = d_disequalities[i][0];
       // Assumptions
@@ -113,11 +113,11 @@ void TheoryBV::check(Effort e) {
       Node lhsNormalized = d_eqEngine.normalize(equality[0], assumptions);
       Node rhsNormalized = d_eqEngine.normalize(equality[1], assumptions);
 
-      Debug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
+      BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
 
       // No need to slice the equality, the whole thing *should* be deduced
       if (lhsNormalized == rhsNormalized) {
-        Debug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
+        BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl;
         assumptions.insert(d_disequalities[i]);
         d_out->conflict(mkConjunction(assumptions));
         return;
@@ -127,9 +127,9 @@ void TheoryBV::check(Effort e) {
 }
 
 bool TheoryBV::triggerEquality(size_t triggerId) {
-  Debug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl;
+  BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl;
   Assert(triggerId < d_triggers.size());
-  Debug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl;
+  BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl;
 
   TNode equality = d_triggers[triggerId];
 
@@ -173,7 +173,7 @@ Node TheoryBV::getValue(TNode n, Valuation* valuation) {
 }
 
 void TheoryBV::explain(TNode node) {
-  Debug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+  BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
   if(node.getKind() == kind::EQUAL) {
     std::vector<TNode> reasons;
     d_eqEngine.getExplanation(node[0], node[1], reasons);
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 5815f2c7f..b66fef0a9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -23,6 +23,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "util/stats.h"
+#include "theory/bv/theory_bv_utils.h"
 #include <sstream>
 
 namespace CVC4 {
@@ -118,11 +119,11 @@ public:
   template<bool checkApplies>
   static inline Node run(Node node) {
     if (!checkApplies || applies(node)) {
-      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
+      BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
       Assert(checkApplies || applies(node));
       ++ s_statictics->d_ruleApplications;
       Node result = apply(node);
-      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
+      BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
       return result;
     } else {
       return node;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index dfc401616..e94388754 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -33,7 +33,7 @@ bool RewriteRule<ConcatFlatten>::applies(Node node) {
 
 template<>
 Node RewriteRule<ConcatFlatten>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
   std::vector<Node> processing_stack;
   processing_stack.push_back(node);
@@ -59,7 +59,7 @@ bool RewriteRule<ConcatExtractMerge>::applies(Node node) {
 template<>
 Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
 
-  Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
 
   std::vector<Node> mergedExtracts;
 
@@ -120,7 +120,7 @@ bool RewriteRule<ConcatConstantMerge>::applies(Node node) {
 template<>
 Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
 
-  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
 
   std::vector<Node> mergedConstants;
   for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
@@ -149,7 +149,7 @@ Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
     }
   }
 
-  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
 
   return utils::mkConcat(mergedConstants);
 }
@@ -167,7 +167,7 @@ bool RewriteRule<ExtractWhole>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractWhole>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
   return node[0];
 }
 
@@ -180,7 +180,7 @@ bool RewriteRule<ExtractConstant>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractConstant>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
   Node child = node[0];
   BitVector childValue = child.getConst<BitVector>();
   return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
@@ -188,7 +188,7 @@ Node RewriteRule<ExtractConstant>::apply(Node node) {
 
 template<>
 bool RewriteRule<ExtractConcat>::applies(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
   return true;
@@ -196,7 +196,7 @@ bool RewriteRule<ExtractConcat>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractConcat>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   int extract_high = utils::getExtractHigh(node);
   int extract_low = utils::getExtractLow(node);
 
@@ -229,7 +229,7 @@ bool RewriteRule<ExtractExtract>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractExtract>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
 
   // x[i:j][k:l] ~>  x[k+j:l+j]
   Node child = node[0];
@@ -243,7 +243,7 @@ Node RewriteRule<ExtractExtract>::apply(Node node) {
 
 template<>
 bool RewriteRule<FailEq>::applies(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
   if (node.getKind() != kind::EQUAL) return false;
   if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
   if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
@@ -263,7 +263,7 @@ bool RewriteRule<SimplifyEq>::applies(Node node) {
 
 template<>
 Node RewriteRule<SimplifyEq>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
   return utils::mkTrue();
 }
 
@@ -274,7 +274,7 @@ bool RewriteRule<ReflexivityEq>::applies(Node node) {
 
 template<>
 Node RewriteRule<ReflexivityEq>::apply(Node node) {
-  Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
   return node[1].eqNode(node[0]);;
 }
 
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 9b5c8b0f9..5bcbdf746 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::theory::bv;
 
 RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
 
-  Debug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
+  BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
 
   Node result;
 
@@ -79,7 +79,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
     }
   }
 
-  Debug("bitvector") << "TheoryBV::postRewrite(" << node << ") => " << result << std::endl;
+  BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ") => " << result << std::endl;
 
   return RewriteResponse(REWRITE_DONE, result);
 }
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 781b5cddb..80751fe4c 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -24,6 +24,12 @@
 #include <sstream>
 #include "expr/node_manager.h"
 
+#ifdef CVC4_DEBUG
+#define BVDebug(x) Debug(x)
+#else
+#define BVDebug(x) if (false) Debug(x)
+#endif
+
 namespace CVC4 {
 namespace theory {
 namespace bv {