From a8ff3563d965e1220d6603becab09f446cc00d35 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 11 Apr 2011 17:33:07 +0000 Subject: [PATCH] Transitive closure module is working --- src/util/trans_closure.cpp | 52 ++++++++++++--- src/util/trans_closure.h | 3 +- test/unit/Makefile.am | 1 + test/unit/util/trans_closure_black.h | 94 +++++++++++++++++++++++++++- 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 */ -- 2.30.2