From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sun, 20 Mar 2011 16:31:19 +0000 (+0000)
Subject: fixing the failure from last nigth, due to using a reference to an element in a growi... 
X-Git-Tag: cvc5-1.0.0~8642
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8dd7462696b1d354f2dbdf840e9f50226f4c489a;p=cvc5.git

fixing the failure from last nigth, due to using a reference to an element in a growing vector
---

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"
@@ -216,6 +217,11 @@ private:
    */
   std::vector<EqualityEdge> d_equalityEdges;
 
+  /**
+   * Returns the string representation of the edges.
+   */
+  std::string edgesToString(size_t edgeId) const;
+
   /**
    * Reasons for equalities.
    */
@@ -642,6 +648,21 @@ void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addGraphEdge
   d_equalityReasons.push_back(reason);
 }
 
+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());
@@ -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));
       }