diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2011-04-11 17:33:07 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2011-04-11 17:33:07 +0000 |
commit | a8ff3563d965e1220d6603becab09f446cc00d35 (patch) | |
tree | 75d8ebc97625e5e7932cfda7793893913d788f5b /src | |
parent | a2602bd3e3ee90d50cb433e01b029d1176b4cc18 (diff) |
Transitive closure module is working
Diffstat (limited to 'src')
-rw-r--r-- | src/util/trans_closure.cpp | 52 | ||||
-rw-r--r-- | src/util/trans_closure.h | 3 |
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 */ |