diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/trans_closure.cpp | 57 | ||||
-rw-r--r-- | src/util/trans_closure.h | 116 |
3 files changed, 176 insertions, 1 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index c94d208d2..9644aa12c 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -38,7 +38,9 @@ libutil_la_SOURCES = \ stats.cpp \ dynamic_array.h \ language.h \ - triple.h + triple.h \ + trans_closure.h \ + trans_closure.cpp libutil_la_LIBADD = \ @builddir@/libutilcudd.la libutilcudd_la_SOURCES = \ diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp new file mode 100644 index 000000000..fd90cd6a2 --- /dev/null +++ b/src/util/trans_closure.cpp @@ -0,0 +1,57 @@ +/********************* */ +/*! \file trans_closure.cpp + ** \verbatim + ** Original author: barrett + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The transitive closure module implementation + ** + ** Implementation file for TransitiveClosure class. + **/ + + +#include "util/trans_closure.h" + + +using namespace std; + + +namespace CVC4 { + + +TransitiveClosure::~TransitiveClosure() { + unsigned i; + for (i = 0; i < adjMatrix.size(); ++i) { + adjMatrix[i]->deleteSelf(); + } +} + + +bool TransitiveClosure::addEdge(unsigned i, unsigned j) +{ + if (adjMatrix.size() > j && adjMatrix[j]->read(i)) { + return false; + } + while (i >= adjMatrix.size()) { + adjMatrix.push_back(new (true) CDBV(d_context)); + } + adjMatrix[i]->write(j); + unsigned k; + for (k = 0; k < adjMatrix.size(); ++k) { + if (adjMatrix[k]->read(i)) { + adjMatrix[k]->write(j); + adjMatrix[k]->merge(adjMatrix[j]); + } + } + return true; +} + + +}/* CVC4 namespace */ diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h new file mode 100644 index 000000000..922e29afc --- /dev/null +++ b/src/util/trans_closure.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file transitive_closure.h + ** \verbatim + ** Original author: barrett + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The transitive closure module + ** + ** The transitive closure module. + **/ + +#ifndef __CVC4__UTIL__TRANSITIVE_CLOSURE_H +#define __CVC4__UTIL__TRANSITIVE_CLOSURE_H + +#include "context/context.h" + +namespace CVC4 { + +/* + * Implements context-dependent variable-sized boolean vector + */ +class CDBV :public context::ContextObj { + uint64_t d_data; + CDBV* d_next; + + CDBV(const CDBV& cdbv) : ContextObj(cdbv), d_data(cdbv.d_data), d_next(cdbv.d_next) {} + + /** + * operator= for CDBV is private to ensure CDBV object is not copied. + */ + CDBV& operator=(const CDBV& cdbv); + +protected: + context::ContextObj* save(context::ContextMemoryManager* pCMM) { + return new(pCMM) CDBV(*this); + } + + void restore(context::ContextObj* pContextObj) { + d_data = ((CDBV*) pContextObj)->d_data; + } + + uint64_t data() { return d_data; } + + CDBV* next() { return d_next; } + +public: + CDBV(context::Context* context) : + ContextObj(context), d_data(0), d_next(NULL) + {} + + ~CDBV() { + if (d_next != NULL) { + d_next->deleteSelf(); + } + destroy(); + } + + bool read(unsigned index) { + if (index < 64) return (d_data & (unsigned(1) << index)) != 0; + else if (d_next == NULL) return false; + else return d_next->read(index - 64); + } + + void write(unsigned index) { + if (index < 64) { + unsigned mask = unsigned(1) << index; + if ((d_data & mask) != 0) return; + makeCurrent(); + d_data = d_data | mask; + } + else if (d_next != NULL) { + d_next->write(index - 64); + } + else { + makeCurrent(); + d_next = new(true) CDBV(getContext()); + d_next->write(index - 64); + } + } + + void merge(CDBV* pcdbv) { + d_data = d_data | pcdbv->data(); + if (d_next != NULL && pcdbv->next() != NULL) { + d_next->merge(pcdbv->next()); + } + } + +}; + + +/** + * Transitive closure module for CVC4. + * + */ +class TransitiveClosure { + context::Context* d_context; + std::vector<CDBV* > adjMatrix; + +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 */ + bool addEdge(unsigned i, unsigned j); +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */ |