From a8ff3563d965e1220d6603becab09f446cc00d35 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 11 Apr 2011 17:33:07 +0000
Subject: Transitive closure module is working

---
 test/unit/Makefile.am                |  1 +
 test/unit/util/trans_closure_black.h | 94 +++++++++++++++++++++++++++++++++++-
 2 files changed, 93 insertions(+), 2 deletions(-)

(limited to 'test')

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 */
-- 
cgit v1.2.3