diff options
Diffstat (limited to 'src/theory/uf/ecdata.h')
| -rw-r--r-- | src/theory/uf/ecdata.h | 145 |
1 files changed, 110 insertions, 35 deletions
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 221512669..9b87aa6cb 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -23,20 +23,43 @@ namespace CVC4 { namespace theory { - +namespace uf { + +/** + * 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* > next; - /** - * As I have not yet succeeded in justifying to myself that soft references are safe - * I am leaving this a hard refernce for now. + /* 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. */ - Node data; + TNode data; - Link(context::Context* context, Node n, Link * l = NULL): + /** + * 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): next(context, l), data(n) {} + /** + * 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); } @@ -44,21 +67,82 @@ 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* find; + /** - * Is it safe to make this a soft link? Why or why not? + * 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. */ - Node rep; + TNode rep; + /* Watch list datastructures. */ + /** Maintains watch list size for more efficient merging */ unsigned watchListSize; + + /** + *Pointer to the beginning of the watchlist. + *This value is NULL iff the watch list is empty. + */ Link* 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* last; + /** Context dependent operations */ context::ContextObj* save(context::ContextMemoryManager* pCMM); void restore(context::ContextObj* pContextObj); @@ -72,12 +156,13 @@ public: /** * Adds a node to the watch list of the equivalence class. - * Requires a context to do memory management. + * Requires a Context in-order to do context dependent memory allocation. + * * @param n the node to be added. * @pre isClassRep() == true */ - void addPredecessor(Node n, context::Context* context); - + void addPredecessor(TNode n, context::Context* context); + /** @@ -86,11 +171,16 @@ public: * This is required as ECData is context dependent * @param n the node that corresponds to this ECData */ - ECData(context::Context* context, const Node & n); - - static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster); + ECData(context::Context* context, TNode n); - static ECData * ccFind(ECData * fp); + /** + * 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); /** @@ -117,35 +207,20 @@ public: /** + * 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); - -private: - - - /** - * @pre isClassRep() == true - */ - void setWatchListSize(unsigned newSize); - - /** - * @pre isClassRep() == true - */ - void setFirst(Link * nfirst); - Link* getLast(); - /** - * @pre isClassRep() == true - */ - void setLast(Link * nlast); - }; /* class ECData */ + +}/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |