From 74084011310e0af055c0055378620a5d19de1e52 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 22 Mar 2011 02:11:09 +0000 Subject: [PATCH] updating debug output usage to eliviate impact of bug 252 --- src/theory/bv/cd_set_collection.h | 9 ++-- src/theory/bv/equality_engine.h | 48 ++++++++--------- src/theory/bv/slice_manager.h | 54 ++++++++++---------- src/theory/bv/theory_bv.cpp | 24 ++++----- src/theory/bv/theory_bv_rewrite_rules.h | 5 +- src/theory/bv/theory_bv_rewrite_rules_core.h | 24 ++++----- src/theory/bv/theory_bv_rewriter.cpp | 4 +- src/theory/bv/theory_bv_utils.h | 6 +++ 8 files changed, 91 insertions(+), 83 deletions(-) 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 #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 size_t EqualityEngine::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::get template bool EqualityEngine::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::addEquality( // Depending on the merge preference (such as size), merge them std::vector 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::addEquality( template TNode EqualityEngine::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::getRepresen const_cast(this)->backtrack(); size_t representativeId = const_cast(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 bool EqualityEngine::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::areEqual(TNo size_t rep1 = const_cast(this)->getEqualityNode(t1).getFind(); size_t rep2 = const_cast(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::areEqual(TNo template void EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vector& 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::merge(Equali template void EqualityEngine::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(class2); @@ -616,7 +616,7 @@ void EqualityEngine::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::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::backtrack() template void EqualityEngine::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 ::getExplanation(TNode t1, TNode t2, std::vector& 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::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::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::getExplanati template size_t EqualityEngine::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::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::normalize(TN template Node EqualityEngine::normalizeWithCache(TNode node, std::set& 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::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::solveEquality(TNode lhs, TNode rhs) { template bool SliceManager::solveEquality(TNode lhs, TNode rhs, const std::set& 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::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 bool SliceManager::sliceAndSolve(std::vector& lhs, std::vector& rhs, const std::set& 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::sliceAndSolve(std::vector& 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 concatTerms; @@ -322,7 +322,7 @@ bool SliceManager::sliceAndSolve(std::vector& 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::sliceAndSolve(std::vector& 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::sliceAndSolve(std::vector& 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::sliceAndSolve(std::vector& 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::sliceAndSolve(std::vector& lhs, std::v template bool SliceManager::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::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 bool SliceManager::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::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::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::addSlice(Node node, unsigned slicePoint) { template inline bool SliceManager::slice(TNode node, std::vector& 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::slice(TNode node, std::vector& 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 slicePoints; if (low + 1 < high) { d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints); @@ -601,9 +601,9 @@ inline bool SliceManager::slice(TNode node, std::vector& // 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::slice(TNode node, std::vector& } // 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 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 namespace CVC4 { @@ -118,11 +119,11 @@ public: template 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::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; NodeBuilder<> result(kind::BITVECTOR_CONCAT); std::vector processing_stack; processing_stack.push_back(node); @@ -59,7 +59,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; std::vector mergedExtracts; @@ -120,7 +120,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; std::vector mergedConstants; for (unsigned i = 0, end = node.getNumChildren(); i < end;) { @@ -149,7 +149,7 @@ Node RewriteRule::apply(Node node) { } } - Debug("bv-rewrite") << "RewriteRule(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl; return utils::mkConcat(mergedConstants); } @@ -167,7 +167,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return node[0]; } @@ -180,7 +180,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; Node child = node[0]; BitVector childValue = child.getConst(); return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node))); @@ -188,7 +188,7 @@ Node RewriteRule::apply(Node node) { template<> bool RewriteRule::applies(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << 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::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; int extract_high = utils::getExtractHigh(node); int extract_low = utils::getExtractLow(node); @@ -229,7 +229,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; // x[i:j][k:l] ~> x[k+j:l+j] Node child = node[0]; @@ -243,7 +243,7 @@ Node RewriteRule::apply(Node node) { template<> bool RewriteRule::applies(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << 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::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return utils::mkTrue(); } @@ -274,7 +274,7 @@ bool RewriteRule::applies(Node node) { template<> Node RewriteRule::apply(Node node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule(" << 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 #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 { -- 2.30.2