diff options
Diffstat (limited to 'src/theory/uf/tim/ecdata.h')
| -rw-r--r-- | src/theory/uf/tim/ecdata.h | 261 |
1 files changed, 0 insertions, 261 deletions
diff --git a/src/theory/uf/tim/ecdata.h b/src/theory/uf/tim/ecdata.h deleted file mode 100644 index 5e72f0042..000000000 --- a/src/theory/uf/tim/ecdata.h +++ /dev/null @@ -1,261 +0,0 @@ -/********************* */ -/*! \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 */ |