Committing a bug fix from Dejan. This resolves an issue with restoring ECData.

5 files changed, 50 insertions, 47 deletions

diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 67fa0664a..f5edc5464 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -24,8 +24,8 @@ namespace CVC4 {
 
 class Expr;
 class Type;
-class BooleanType; 
-class FunctionType; 
+class BooleanType;
+class FunctionType;
 class KindType;
 class SmtEngine;
 class NodeManager;
@@ -91,12 +91,12 @@ public:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /** Make a function type from domain to range. */
-  const FunctionType* 
-    mkFunctionType(const Type* domain, 
+  const FunctionType*
+    mkFunctionType(const Type* domain,
                    const Type* range);
 
   /** Make a function type with input types from argTypes. */
-  const FunctionType* 
+  const FunctionType*
     mkFunctionType(const std::vector<const Type*>& argTypes, 
                    const Type* range);
 
diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp
index 5a89a4939..22db1e6d0 100644
--- a/src/theory/uf/ecdata.cpp
+++ b/src/theory/uf/ecdata.cpp
@@ -23,16 +23,16 @@ using namespace uf;
 
 ECData::ECData(Context * context, TNode n) :
   ContextObj(context),
-  find(this),
-  rep(n),
-  watchListSize(0),
-  first(NULL),
-  last(NULL)
+  d_find(this),
+  d_rep(n),
+  d_watchListSize(0),
+  d_first(NULL),
+  d_last(NULL)
 {}
 
 
 bool ECData::isClassRep(){
-  return this == this->find;
+  return this == this->d_find;
 }
 
 void ECData::addPredecessor(TNode n, Context* context){
@@ -40,13 +40,13 @@ void ECData::addPredecessor(TNode n, Context* context){
 
   makeCurrent();
 
-  Link * newPred = new (context->getCMM())  Link(context, n, first);
-  first = newPred;
-  if(last == NULL){
-    last = newPred;
+  Link * newPred = new (context->getCMM())  Link(context, n, d_first);
+  d_first = newPred;
+  if(d_last == NULL){
+    d_last = newPred;
   }
 
-  ++watchListSize;
+  ++d_watchListSize;
 }
 
 ContextObj* ECData::save(ContextMemoryManager* pCMM) {
@@ -54,30 +54,35 @@ ContextObj* ECData::save(ContextMemoryManager* pCMM) {
 }
 
 void ECData::restore(ContextObj* pContextObj) {
-  *this = *((ECData*)pContextObj);
+  ECData* data = (ECData*)pContextObj;
+  d_find = data->d_find;
+  d_first = data->d_first;
+  d_last = data->d_last;
+  d_rep = data->d_rep;
+  d_watchListSize = data->d_watchListSize;
 }
 
 Node ECData::getRep(){
-  return rep;
+  return d_rep;
 }
 
 unsigned ECData::getWatchListSize(){
-  return watchListSize;
+  return d_watchListSize;
 }
 
 
 void ECData::setFind(ECData * ec){
   makeCurrent();
-  find = ec;
+  d_find = ec;
 }
 
 ECData * ECData::getFind(){
-  return find;
+  return d_find;
 }
 
 
 Link* ECData::getFirst(){
-  return first;
+  return d_first;
 }
 
 
@@ -87,14 +92,14 @@ void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){
 
   nmaster->makeCurrent();
 
-  nmaster->watchListSize +=  nslave->watchListSize;
+  nmaster->d_watchListSize +=  nslave->d_watchListSize;
 
-  if(nmaster->first == NULL){
-    nmaster->first = nslave->first;
-    nmaster->last = nslave->last;
-  }else if(nslave->first != NULL){
-    Link * currLast = nmaster->last;
-    currLast->next = nslave->first;
-    nmaster->last = nslave->last;
+  if(nmaster->d_first == NULL){
+    nmaster->d_first = nslave->d_first;
+    nmaster->d_last = nslave->d_last;
+  }else if(nslave->d_first != NULL){
+    Link * currLast = nmaster->d_last;
+    currLast->d_next = nslave->d_first;
+    nmaster->d_last = nslave->d_last;
   }
 }
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index 5bb3a57bd..735712cdc 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -41,21 +41,21 @@ struct Link {
    * Pointer to the next element in linked list.
    * This is context dependent. 
    */
-  context::CDO< Link* > next;
+  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 data;
+  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):
-    next(context, l), data(n)
+    d_next(context, l), d_data(n)
   {}
 
   /**
@@ -103,7 +103,7 @@ private:
    * 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;
+  ECData* d_find;
 
 
   /**
@@ -122,17 +122,17 @@ private:
    * the ECData will never get garbage collected.
    * So this needs to be a soft link.
    */
-  TNode rep;
+  TNode d_rep;
 
   /* Watch list datastructures. */
   /** Maintains watch list size for more efficient merging */
-  unsigned watchListSize;
+  unsigned d_watchListSize;
 
   /**
    *Pointer to the beginning of the watchlist.
    *This value is NULL iff the watch list is empty.
    */
-  Link* first;
+  Link* d_first;
 
   /**
    * Pointer to the end of the watch-list.
@@ -141,7 +141,7 @@ private:
    * preceeded by an O(|watchlist|) operation.)
    * This value is NULL iff the watch list is empty.
    */
-  Link* last;
+  Link* d_last;
 
 
   /** Context dependent operations */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 485f5f6d3..b4597c7c7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -122,9 +122,9 @@ void TheoryUF::registerTerm(TNode n){
       /* 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)){
-          Node pend = n.eqNode(Px->data);
+      for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ){
+        if(equiv(n, Px->d_data)){
+          Node pend = n.eqNode(Px->d_data);
           d_pending.push_back(pend);
         }
       }
@@ -210,10 +210,10 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
 
   nslave->setFind(nmaster);
 
-  for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->next ){
-    for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->next ){
-      if(equiv(Px->data,Py->data)){
-        Node pendingEq = (Px->data).eqNode(Py->data);
+  for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ){
+    for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ){
+      if(equiv(Px->d_data,Py->d_data)){
+        Node pendingEq = (Px->d_data).eqNode(Py->d_data);
         d_pending.push_back(pendingEq);
       }
     }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 5ac5e3001..d432d733f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -84,8 +84,6 @@ public:
   ~TheoryUF();
 
 
-  //TODO Tim: I am going to delay documenting these functions while Morgan
-  //has pending changes to the contracts
 
   /**
    * Registers a previously unseen [in this context] node n.