Transitive closure module is working

4 files changed, 139 insertions, 11 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 */
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 7089951ad..bc49a7fac 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -42,6 +42,7 @@ UNIT_TESTS = \
 	util/rational_black \
 	util/rational_white \
 	util/stats_black \
+	util/trans_closure_black \
 	main/interactive_shell_black
 
 export VERBOSE = 1
diff --git a/test/unit/util/trans_closure_black.h b/test/unit/util/trans_closure_black.h
index 99542223c..dfa066194 100644
--- a/test/unit/util/trans_closure_black.h
+++ b/test/unit/util/trans_closure_black.h
@@ -47,19 +47,109 @@ public:
   }
 
   void testSimple() {
-    //Debug.on("cc");
-    // add terms, then add equalities
+    bool b;
+    b = d_tc->addEdge(1,2);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(2,3);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(3,1);
+    TS_ASSERT(b);
+
+    b = d_tc->addEdge(2,4);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(2,5);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(4,6);
+    TS_ASSERT(!b);
 
+    b = d_tc->addEdge(6,2);
+    TS_ASSERT(b);
+  }
+
+
+  void test1() {
     bool b;
     b = d_tc->addEdge(1,2);
     TS_ASSERT(!b);
 
+    d_context->push();
+
     b = d_tc->addEdge(2,3);
     TS_ASSERT(!b);
 
     b = d_tc->addEdge(3,1);
     TS_ASSERT(b);
+
+    d_context->pop();
+
+    b = d_tc->addEdge(3,1);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(2,3);
+    TS_ASSERT(b);
+
+    d_context->push();
+
+    b = d_tc->addEdge(6,4);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(2,6);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(4,1);
+    TS_ASSERT(b);
+
+    d_context->pop();
+
+    b = d_tc->addEdge(4,1);
+
+    TS_ASSERT(!b);
   }
 
+  void test2() {
+    bool b;
+    b = d_tc->addEdge(1,2);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,3);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,4);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,5);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,6);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,7);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,8);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(1,9);
+    TS_ASSERT(!b);
+
+    b = d_tc->addEdge(3,2);
+    TS_ASSERT(!b);
+    b = d_tc->addEdge(4,7);
+    TS_ASSERT(!b);
+    
+    b = d_tc->addEdge(2,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(3,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(4,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(5,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(6,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(7,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(8,1);
+    TS_ASSERT(b);
+    b = d_tc->addEdge(9,1);
+    TS_ASSERT(b);
+  }
 
 };/* class TransitiveClosureBlack */