diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2011-04-08 13:22:18 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2011-04-08 13:22:18 +0000 |
commit | 16161eb039274162e1e464522e73a17f755a4e28 (patch) | |
tree | 1e63e54a0f9154fbd123569776bed38e30c6616c | |
parent | f2696072837541f16932b1fd5f5740d45b4341b9 (diff) |
Added util class
-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 | ||||
-rw-r--r-- | test/unit/util/trans_closure_black.h | 65 |
4 files changed, 241 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 */ diff --git a/test/unit/util/trans_closure_black.h b/test/unit/util/trans_closure_black.h new file mode 100644 index 000000000..99542223c --- /dev/null +++ b/test/unit/util/trans_closure_black.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file trans_closure_black.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 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 Black box testing of CVC4::TransitiveClosure. + ** + ** Black box testing of CVC4::TransitiveClosure. + **/ + + +#include "util/trans_closure.h" + + +using namespace CVC4; +using namespace CVC4::context; +using namespace std; + + +class TransitiveClosureBlack : public CxxTest::TestSuite { + Context* d_context; + TransitiveClosure* d_tc; + +public: + + void setUp() { + d_context = new Context; + d_tc = new TransitiveClosure(d_context); + } + + void tearDown() { + try { + delete d_tc; + delete d_context; + } catch(Exception& e) { + Warning() << std::endl << e << std::endl; + throw; + } + } + + 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); + } + + +};/* class TransitiveClosureBlack */ |