Cleaned up and documented ecdata and theory_uf.

4 files changed, 211 insertions, 85 deletions

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<Node> 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<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){}
@@ -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<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
 
+} /* CVC4::theory::uf namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */