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 /src/util/trans_closure.h | |
parent | f2696072837541f16932b1fd5f5740d45b4341b9 (diff) |
Added util class
Diffstat (limited to 'src/util/trans_closure.h')
-rw-r--r-- | src/util/trans_closure.h | 116 |
1 files changed, 116 insertions, 0 deletions
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 */ |