diff options
Diffstat (limited to 'src/theory/bv/equality_engine.h')
| -rw-r--r-- | src/theory/bv/equality_engine.h | 48 |
1 files changed, 24 insertions, 24 deletions
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; |