diff options
Diffstat (limited to 'src/theory/example/ecdata.h')
-rw-r--r-- | src/theory/example/ecdata.h | 261 |
1 files changed, 261 insertions, 0 deletions
diff --git a/src/theory/example/ecdata.h b/src/theory/example/ecdata.h new file mode 100644 index 000000000..5e72f0042 --- /dev/null +++ b/src/theory/example/ecdata.h @@ -0,0 +1,261 @@ +/********************* */ +/*! \file ecdata.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** 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 Context dependent equivalence class datastructure for nodes. + ** + ** Context dependent equivalence class datastructure for nodes. + ** Currently keeps a context dependent watch list. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H +#define __CVC4__THEORY__UF__TIM__ECDATA_H + +#include "expr/node.h" +#include "context/context.h" +#include "context/cdo.h" +#include "context/context_mm.h" + +namespace CVC4 { +namespace theory { +namespace uf { +namespace tim { + +/** + * Link is a context dependent linked list of nodes. + * Link is intended to be allocated in a Context's memory manager. + * The next pointer of the list is context dependent, but the node being + * pointed to is fixed for the life of the Link. + * + * Clients of Link are intended not to modify the node that is being pointed + * to in good faith. This may change in the future. + */ +struct Link { + /** + * Pointer to the next element in linked list. + * This is context dependent. + */ + context::CDO<Link*> d_next; + + /** + * Link is supposed to be allocated in a region of a + * ContextMemoryManager. In order to avoid having to decrement the + * ref count at deletion time, it is preferrable for the user of + * Link to maintain the invariant that data will survival for the + * entire scope of the TNode. + */ + TNode d_data; + + /** + * Creates a new Link w.r.t. a context for the node n. + * An optional parameter is to specify the next element in the link. + */ + Link(context::Context* context, TNode n, Link* l = NULL) : + d_next(true, context, l), + d_data(n) { + Debug("context") << "Link: " << this + << " so cdo is " << &d_next << std::endl; + } + + /** + * Allocates a new Link in the region for the provided ContextMemoryManager. + * This allows for cheap cleanup on pop. + */ + static void* operator new(size_t size, context::ContextMemoryManager* pCMM) { + return pCMM->newData(size); + } + +private: + + /** + * The destructor isn't actually defined. This declaration keeps + * the compiler from creating (wastefully) a default definition, and + * ensures that we get a link error if someone uses Link in a way + * that requires destruction. Objects of class Link should always + * be allocated in a ContextMemoryManager, which doesn't call + * destructors. + */ + ~Link() throw(); + + /** + * Just like the destructor, this is not defined. This ensures no + * one tries to create a Link on the heap. + */ + static void* operator new(size_t size); + +};/* struct Link */ + + +/** + * ECData is a equivalence class object that is context dependent. + * It is developed in order to support the congruence closure algorithm + * in TheoryUF, and is not intended to be used outside of that package. + * + * ECData maintains: + * - find pointer for the equivalence class (disjoint set forest) + * - the node that represents the equivalence class. + * - maintains a predecessorlist/watchlist + * + * ECData does not have support for the canonical find and union operators + * for disjoint set forests. Instead it only provides access to the find + * pointer. The implementation of find is ccFind in TheoryUF. + * union is broken into 2 phases: + * 1) setting the find point with setFind + * 2) taking over the watch list of the other node. + * This is a technical requirement for the implementation of TheoryUF. + * (See ccUnion in TheoryUF for more information.) + * + * The intended paradigm for iterating over the watch list of ec is: + * for(Link* i = ec->getFirst(); i != NULL; i = i->next ); + * + * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses + * ECData lives. + */ +class ECData : public context::ContextObj { +private: + /** + * This is the standard disjoint set forest find pointer. + * + * Why an ECData pointer instead of a node? + * This was chosen to be a ECData pointer in order to shortcut at least one + * table every time the find pointer is examined. + */ + ECData* d_find; + + /** + * This is pointer back to the node that represents this equivalence class. + * + * The following invariant should be maintained: + * (n.getAttribute(ECAttr()))->rep == n + * i.e. rep is equal to the node that maps to the ECData using ECAttr. + * + * Tricky part: This needs to be a TNode, not a Node. + * Suppose that rep were a hard link. + * When a node n maps to an ECData via the ECAttr() there will be a hard + * link back to n in the ECData. The attribute does not do garbage collection + * until the node gets garbage collected, which does not happen until its + * ref count drops to 0. So because of this cycle neither the node and + * the ECData will never get garbage collected. + * So this needs to be a soft link. + */ + TNode d_rep; + + // Watch list data structures follow + + /** + * Maintains watch list size for more efficient merging. + */ + unsigned d_watchListSize; + + /** + * Pointer to the beginning of the watchlist. + * This value is NULL iff the watch list is empty. + */ + Link* d_first; + + /** + * Pointer to the end of the watch-list. + * This is maintained in order to constant time list merging. + * (This does not give any asymptotic improve as this is currently always + * preceeded by an O(|watchlist|) operation.) + * This value is NULL iff the watch list is empty. + */ + Link* d_last; + + /** Context-dependent operation: save this ECData */ + context::ContextObj* save(context::ContextMemoryManager* pCMM); + + /** Context-dependent operation: restore this ECData */ + void restore(context::ContextObj* pContextObj); + +public: + /** + * Returns true if this ECData object is the current representative of + * the equivalence class. + */ + bool isClassRep(); + + /** + * Adds a node to the watch list of the equivalence class. Does + * context-dependent memory allocation in the Context with which + * this ECData was created. + * + * @param n the node to be added. + * @pre isClassRep() == true + */ + void addPredecessor(TNode n); + + /** + * Creates a EQ with the representative n + * @param context the context to associate with this ecdata. + * This is required as ECData is context dependent + * @param n the node that corresponds to this ECData + */ + ECData(context::Context* context, TNode n); + + /** Destructor for ECDatas */ + ~ECData() { + Debug("ufgc") << "Calling ECData destructor" << std::endl; + destroy(); + } + + /** + * An ECData takes over the watch list of another ECData. + * This is the second step in the union operator for ECData. + * This should be called after nslave->setFind(nmaster); + * After this is done nslave's watch list should never be accessed by + * getLast() or getFirst() + */ + static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster); + + /** + * Returns the representative of this ECData. + */ + Node getRep(); + + /** + * Returns the size of the equivalence class. + */ + unsigned getWatchListSize(); + + /** + * Returns a pointer the first member of the watch list. + */ + Link* getFirst(); + + + /** + * Returns the find pointer of the ECData. + * If isClassRep(), then getFind() == this + */ + ECData* getFind(); + + /** + * Sets the find pointer of the equivalence class to be another ECData object. + * + * @pre isClassRep() == true + * @pre ec->isClassRep() == true + * @post isClassRep() == false + * @post ec->isClassRep() == true + */ + void setFind(ECData * ec); + +};/* class ECData */ + +}/* CVC4::theory::uf::tim namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ |