Transitive closure module is working

2 files changed, 46 insertions, 9 deletions

diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index fd90cd6a2..092dfb358 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -18,6 +18,7 @@
 
 
 #include "util/trans_closure.h"
+#include "util/Assert.h"
 
 
 using namespace std;
@@ -29,28 +30,63 @@ namespace CVC4 {
 TransitiveClosure::~TransitiveClosure() {
   unsigned i;
   for (i = 0; i < adjMatrix.size(); ++i) {
-    adjMatrix[i]->deleteSelf();
+    if (adjMatrix[i]) {
+      adjMatrix[i]->deleteSelf();
+    }
   }
 }
 
 
 bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 {
-  if (adjMatrix.size() > j && adjMatrix[j]->read(i)) {
-    return false;
+  // Check for loops
+  Assert(i != j, "Cannot add self-loop");
+  if (adjMatrix.size() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
+    return true;
+  }
+
+  // Grow matrix if necessary
+  unsigned maxSize = ((i > j) ? i : j) + 1;
+  while (maxSize > adjMatrix.size()) {
+    adjMatrix.push_back(NULL);
   }
-  while (i >= adjMatrix.size()) {
-    adjMatrix.push_back(new (true) CDBV(d_context));
+
+  // Add edge from i to j and everything j can reach
+  if (adjMatrix[i] == NULL) {
+    adjMatrix[i] = new (true) CDBV(d_context);
   }
   adjMatrix[i]->write(j);
+  if (adjMatrix[j] != NULL) {
+    adjMatrix[i]->merge(adjMatrix[j]);
+  }
+
+  // Add edges from everything that can reach i to j and everything that j can reach
   unsigned k;
   for (k = 0; k < adjMatrix.size(); ++k) {
-    if (adjMatrix[k]->read(i)) {
+    if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) {
       adjMatrix[k]->write(j);
-      adjMatrix[k]->merge(adjMatrix[j]);
+      if (adjMatrix[j] != NULL) {
+        adjMatrix[k]->merge(adjMatrix[j]);
+      }
     }
   }
-  return true;
+
+  return false;
+}
+
+
+void TransitiveClosure::debugPrintMatrix()
+{
+  unsigned i,j;
+  for (i = 0; i < adjMatrix.size(); ++i) {
+    for (j = 0; j < adjMatrix.size(); ++j) {
+      if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) {
+        cout << "1 ";
+      }
+      else cout << "0 ";
+    }
+    cout << endl;
+  }      
 }
 
 
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index 922e29afc..56951d531 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -107,8 +107,9 @@ public:
   TransitiveClosure(context::Context* context) : d_context(context) {}
   ~TransitiveClosure();
 
-  /* Add an edge from node i to node j.  Return true if successful, false if this edge would create a cycle */
+  /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
   bool addEdge(unsigned i, unsigned j);
+  void debugPrintMatrix();
 };
 
 }/* CVC4 namespace */