diff options
-rw-r--r-- | src/theory/bv/equality_engine.h | 33 |
1 files changed, 28 insertions, 5 deletions
diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 954253269..6b9551950 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -23,6 +23,7 @@ #include <vector> #include <ext/hash_map> +#include <sstream> #include "expr/node.h" #include "context/cdo.h" @@ -217,6 +218,11 @@ private: std::vector<EqualityEdge> d_equalityEdges; /** + * Returns the string representation of the edges. + */ + std::string edgesToString(size_t edgeId) const; + + /** * Reasons for equalities. */ std::vector<Node> d_equalityReasons; @@ -643,6 +649,21 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addGraphEdge } template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences> +std::string EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::edgesToString(size_t edgeId) const { + std::stringstream out; + bool first = true; + while (edgeId != BitSizeTraits::id_null) { + const EqualityEdge& edge = d_equalityEdges[edgeId]; + if (!first) out << ","; + out << d_nodes[edge.getNodeId()]; + edgeId = edge.getNext(); + first = false; + } + return out.str(); +} + + +template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences> void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const { Assert(equalities.empty()); Assert(t1 != t2); @@ -675,6 +696,8 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanati // Go through the equality edges of this node size_t currentEdge = d_equalityGraph[currentNode]; + Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + while (currentEdge != BitSizeTraits::id_null) { // Get the edge const EqualityEdge& edge = d_equalityEdges[currentEdge]; @@ -698,13 +721,13 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanati // Go to the previous currentEdge = bfsQueue[currentIndex].edgeId; currentIndex = bfsQueue[currentIndex].previousIndex; - } while (currentEdge != BitSizeTraits::id_null); + } while (currentEdge != BitSizeTraits::id_null); - // Done - return; - } + // Done + return; + } - // Push to the visitation queue if it's not the backward edge + // Push to the visitation queue if it's not the backward edge bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex)); } |