Cleaned up and documented ecdata and theory_uf.

1 files changed, 10 insertions, 30 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 );