From: Tim King Date: Wed, 24 Feb 2010 23:52:38 +0000 (+0000) Subject: Cleaned up and documented ecdata and theory_uf. X-Git-Tag: cvc5-1.0.0~9225 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff9bda51dfb047af2005f464847edd61314bb50c;p=cvc5.git Cleaned up and documented ecdata and theory_uf. --- diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp index cb7add487..5a89a4939 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/ecdata.cpp @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** **/ #include "theory/uf/ecdata.h" @@ -18,14 +18,15 @@ using namespace CVC4; using namespace context; using namespace theory; +using namespace uf; -ECData::ECData(Context * context, const Node & n) : +ECData::ECData(Context * context, TNode n) : ContextObj(context), - find(this), - rep(n), - watchListSize(0), - first(NULL), + find(this), + rep(n), + watchListSize(0), + first(NULL), last(NULL) {} @@ -34,13 +35,13 @@ bool ECData::isClassRep(){ return this == this->find; } -void ECData::addPredecessor(Node n, Context* context){ +void ECData::addPredecessor(TNode n, Context* context){ Assert(isClassRep()); makeCurrent(); Link * newPred = new (context->getCMM()) Link(context, n, first); - first = newPred; + first = newPred; if(last == NULL){ last = newPred; } @@ -59,17 +60,11 @@ void ECData::restore(ContextObj* pContextObj) { Node ECData::getRep(){ return rep; } - + unsigned ECData::getWatchListSize(){ return watchListSize; } -void ECData::setWatchListSize(unsigned newSize){ - Assert(isClassRep()); - - makeCurrent(); - watchListSize = newSize; -} void ECData::setFind(ECData * ec){ makeCurrent(); @@ -86,21 +81,6 @@ Link* ECData::getFirst(){ } -Link* ECData::getLast(){ - return last; -} - -void ECData::setFirst(Link * nfirst){ - makeCurrent(); - first = nfirst; -} - -void ECData::setLast(Link * nlast){ - makeCurrent(); - last = nlast; -} - - void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){ Assert(nslave != nmaster); Assert(nslave->getFind() == nmaster ); 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 */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 652eb4a55..1efe13b9b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** **/ @@ -19,22 +19,31 @@ #include "expr/kind.h" using namespace CVC4; -using namespace theory; using namespace context; +using namespace theory; +using namespace uf; + +//TODO remove Node getOperator(Node x) { return Node::null(); } TheoryUF::TheoryUF(Context* c) : - Theory(c), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c) + Theory(c), + d_pending(c), + d_currentPendingIdx(c,0), + d_disequality(c), + d_registered(c) {} TheoryUF::~TheoryUF(){} void TheoryUF::registerTerm(TNode n){ + d_registered.push_back(n); + ECData* ecN; if(n.hasAttribute(ECAttr(),&ecN)){ @@ -46,7 +55,8 @@ void TheoryUF::registerTerm(TNode n){ * predecessors lists. * Also we do not have to worry about duplicates because all of the Link* * setup before are removed when the context n was setup in was popped out - * of. All we are going to do here are sanity checks.*/ + * of. All we are going to do here are sanity checks. + */ /* * Consider the following chain of events: @@ -84,17 +94,26 @@ void TheoryUF::registerTerm(TNode n){ "This data is either already in use or was not properly maintained " "during backtracking"); }else{ + //The attribute does not exist, so it is created and set ecN = new (true) ECData(d_context, n); n.setAttribute(ECAttr(), ecN); } + /* If the node is an APPLY, we need to add it to the predecessor list + * of its children. + */ if(n.getKind() == APPLY){ for(TNode::iterator cIter = n.begin(); cIter != n.end(); ++cIter){ TNode child = *cIter; - ECData* ecChild = child.getAttribute(ECAttr()); - ecChild = ccFind(ecChild); + /* Because this can be called after nodes have been merged, we need + * to lookup the representative in the UnionFind datastructure. + */ + ECData* ecChild = ccFind(child.getAttribute(ECAttr())); + /* Because this can be called after nodes have been merged we may need + * to be merged with other predecessors of the equivalence class. + */ for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->next ){ if(equiv(n, Px->data)){ d_pending.push_back(n.eqNode(Px->data)); @@ -113,15 +132,15 @@ bool TheoryUF::sameCongruenceClass(TNode x, TNode y){ ccFind(y.getAttribute(ECAttr())); } -bool TheoryUF::equiv(Node x, Node y){ +bool TheoryUF::equiv(TNode x, TNode y){ if(x.getNumChildren() != y.getNumChildren()) return false; if(getOperator(x) != getOperator(y)) return false; - Node::iterator xIter = x.begin(); - Node::iterator yIter = y.begin(); + TNode::iterator xIter = x.begin(); + TNode::iterator yIter = y.begin(); while(xIter != x.end()){ @@ -135,12 +154,30 @@ bool TheoryUF::equiv(Node x, Node y){ return true; } +/* This is a very basic, but *obviously correct* find implementation + * of the classic find algorithm. + * TODO after we have done some more testing: + * 1) Add path compression. This is dependent on changes to ccUnion as + * many better algorithms use eager path compression. + * 2) Elminate recursion. + */ ECData* TheoryUF::ccFind(ECData * x){ if( x->getFind() == x) return x; else{ return ccFind(x->getFind()); } + /* Slightly better Find w/ path compression and no recursion*/ + /* + ECData* start; + ECData* next = x; + while(x != x->getFind()) x=x->getRep(); + while( (start = next) != x){ + next = start->getFind(); + start->setFind(x); + } + return x; + */ } void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ @@ -168,9 +205,8 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ ECData::takeOverDescendantWatchList(nslave, nmaster); } -//TODO make parameters soft references void TheoryUF::merge(){ - do{ + while(d_currentPendingIdx < d_pending.size() ) { TNode assertion = d_pending[d_currentPendingIdx]; d_currentPendingIdx = d_currentPendingIdx + 1; @@ -183,7 +219,7 @@ void TheoryUF::merge(){ continue; ccUnion(ecX, ecY); - }while( d_currentPendingIdx < d_pending.size() ); + } } void TheoryUF::check(OutputChannel& out, Effort level){ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 6a1dfb886..b68a96e65 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** **/ @@ -28,18 +28,28 @@ namespace CVC4 { namespace theory { +namespace uf { + class TheoryUF : public Theory { private: + + /** * The associated context. Needed for allocating context dependent objects * and objects in context dependent memory. */ context::Context* d_context; - - /** List of pending equivalence class merges. */ + + /** + * List of pending equivalence class merges. + * + * Tricky part: + * Must keep a hard link because new equality terms are created and appended + * to this list. + */ context::CDList d_pending; /** Index of the next pending equality to merge. */ @@ -48,15 +58,31 @@ private: /** List of all disequalities this theory has seen. */ context::CDList d_disequality; + /** + * List of all of the terms that are registered in the current context. + * When registerTerm is called on a term we want to guarentee that there + * is a hard link to the term for the duration of the context in which + * register term is called. + * This invariant is enough for us to use soft links where we want is the + * current implementation as well as making ECAttr() not context dependent. + * Soft links used both in ECData, and Link. + */ + context::CDList d_registered; public: + /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF(context::Context* c); + + /** Destructor for the TheoryUF object. */ ~TheoryUF(); + + //TODO Tim: I am going to delay documenting these functions while Morgan + //has pending changes to the contracts + void registerTerm(TNode n); - - + void check(OutputChannel& out, Effort level= FULL_EFFORT); void propagate(OutputChannel& out, Effort level= FULL_EFFORT){} @@ -83,7 +109,7 @@ private: * x.getOperator() == y.getOperator() and * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i]) */ - bool equiv(Node x, Node y); + bool equiv(TNode x, TNode y); /** * Merges 2 equivalence classes, checks wether any predecessors need to @@ -100,22 +126,31 @@ private: */ ECData* ccFind(ECData* x); - /* Performs Congruence Closure to reflect the new additions to d_pending. */ + /** Performs Congruence Closure to reflect the new additions to d_pending. */ void merge(); }; - +/** + * Cleanup function for ECData. This will be used for called whenever + * a ECAttr is being destructed. + */ struct ECCleanupFcn{ static void cleanup(ECData* & ec){ ec->deleteSelf(); } }; +/** Unique name to use for constructing ECAttr. */ struct EquivClass; + +/** + * ECAttr is the attribute that maps a node to an equivalence class. + */ typedef expr::Attribute ECAttr; +} /* CVC4::theory::uf namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */