** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ **
**/
#include "theory/uf/ecdata.h"
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)
{}
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;
}
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();
}
-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 );
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);
}
};
-
+/**
+ * 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);
/**
* 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);
+
/**
* 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);
/**
/**
+ * 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 */
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ **
**/
#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)){
* 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:
"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));
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()){
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){
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;
continue;
ccUnion(ecX, ecY);
- }while( d_currentPendingIdx < d_pending.size() );
+ }
}
void TheoryUF::check(OutputChannel& out, Effort level){
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ **
**/
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<Node> d_pending;
/** Index of the next pending equality to merge. */
/** List of all disequalities this theory has seen. */
context::CDList<Node> 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<Node> 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){}
* 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
*/
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<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
+} /* CVC4::theory::uf namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
projects / cvc5.git / commitdiff