Committing small changes to attribute, and theory to avoid future merge problems for Moragn. Also cleaned up theory uf and ecdata, and updated both to reflect attribute. Should be close now.

5 files changed, 200 insertions, 43 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 61b2fdfa3..cf52de75e 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -18,5 +18,20 @@
 namespace CVC4 {
 namespace theory {
 
+bool Theory::done() {
+  return d_nextAssertion >= d_assertions.size(); 
+}
+
+
+Node Theory::get() {
+  Node n = d_assertions[d_nextAssertion];
+  d_nextAssertion = d_nextAssertion + 1;
+  return n;
+}
+
+void Theory::assertFact(const Node& n){
+  d_assertions.push_back(n);
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 831a185f8..76b9697dc 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -60,8 +60,7 @@ public:
   /**
    * Construct a Theory.
    */
-  Theory() {
-  }
+  Theory(context::Context* c) : d_assertions(c),  d_nextAssertion(c, 0){}
 
   /**
    * Destructs a Theory.  This implementation does nothing, but we
@@ -82,7 +81,10 @@ public:
    * setup() MUST NOT MODIFY context-dependent objects that it hasn't
    * itself just created.
    */
-  virtual void setup(const Node& n) = 0;
+
+  /*virtual void setup(const Node& n) = 0;*/
+
+  virtual void registerTerm(TNode n) = 0;
 
   /**
    * Assert a fact in the current context.
@@ -109,6 +111,9 @@ public:
   virtual void explain(OutputChannel& out,
                        const Node& n,
                        Effort level = FULL_EFFORT) = 0;
+private:
+  context::CDList<Node> d_assertions;
+  context::CDO<unsigned> d_nextAssertion;
 
 protected:
   /**
@@ -121,7 +126,7 @@ protected:
   /**
    * Returns true if the assertFactQueue is empty
    */
-  bool done() { return true; }
+  bool done();
 
 };/* class Theory */
 
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index c8303a245..221512669 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -26,10 +26,13 @@ namespace theory {
 
 struct Link {
   context::CDO< Link* > next;
-  
-  //TODO soft reference
+
+  /**
+   * As I have not yet succeeded in justifying to myself that soft references are safe
+   * I am leaving this a hard refernce for now.
+   */
   Node data;
-  
+
   Link(context::Context* context, Node n, Link * l = NULL):
     next(context, l), data(n)
   {}
@@ -37,20 +40,23 @@ struct Link {
   static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
     return pCMM->newData(size);
   }
-  
+
 };
 
 
 
 class ECData : public context::ContextObj {
 private:
-  ECData * find;
+  ECData* find;
 
+  /**
+   * Is it safe to make this a soft link?  Why or why not?
+   */
   Node rep;
-  
+
   unsigned watchListSize;
-  Link * first;
-  Link * last;
+  Link* first;
+  Link* last;
 
 
   context::ContextObj* save(context::ContextMemoryManager* pCMM);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6f9171f36..652eb4a55 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -23,29 +23,94 @@ using namespace theory;
 using namespace context;
 
 
-/* Temporaries to facilitate compiling. */
-enum TmpEnum {EC};
-void setAttribute(Node n, TmpEnum te, ECData * ec){}
-ECData* getAttribute(Node n, TmpEnum te) { return NULL; }
 Node getOperator(Node x) { return Node::null(); }
 
 
-void TheoryUF::setup(const Node& n){
-  ECData * ecN = new (true) ECData(d_context, n);
 
-  //TODO Make sure attribute manager owns the pointer
-  setAttribute(n, EC, ecN);
+TheoryUF::TheoryUF(Context* c) :
+  Theory(c), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c)
+{}
+
+TheoryUF::~TheoryUF(){}
+
+void TheoryUF::registerTerm(TNode n){
+
+  ECData* ecN;
+
+  if(n.hasAttribute(ECAttr(),&ecN)){
+    /* registerTerm(n) is only called when a node has not been seen in the
+     * current context.  ECAttr() is not a context-dependent attribute.
+     * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
+     * then it must be the case that this attribute was created in a previous
+     * and no longer valid context. Because of this we have to reregister the
+     * 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.*/
+
+    /*
+     * Consider the following chain of events:
+     * 1) registerTerm(n) is called on node n where n : f(m) in context level X,
+     * 2) A new ECData is created on the heap, ecN,
+     * 3) n is added to the predessecor list of m in context level X,
+     * 4) We pop out of X,
+     * 5) n is removed from the predessecor list of m because this is context
+     *    dependent, the Link* will be destroyed and pointers to the Link
+     *    structs in the ECData objects will be updated.
+     * 6) registerTerm(n) is called on node n in context level Y,
+     * 7) If n.hasAttribute(ECAttr(), &ecN), then ecN is still around,
+     *    but the predecessor list is not
+     *
+     * The above assumes that the code is working correctly.
+     */
+    Assert(ecN->getFirst() == NULL,
+           "Equivalence class data exists for the node being registered.  "
+           "Expected getFirst() == NULL.  "
+           "This data is either already in use or was not properly maintained "
+           "during backtracking");
+    /*Assert(ecN->getLast() == NULL,
+           "Equivalence class data exists for the node being registered.  "
+           "Expected getLast() == NULL.  "
+           "This data is either already in use or was not properly maintained "
+           "during backtracking.");*/
+    Assert(ecN->isClassRep(),
+           "Equivalence class data exists for the node being registered.  "
+           "Expected isClassRep() to be true.  "
+           "This data is either already in use or was not properly maintained "
+           "during backtracking");
+    Assert(ecN->getWatchListSize() == 0,
+           "Equivalence class data exists for the node being registered.  "
+           "Expected getWatchListSize() == 0.  "
+           "This data is either already in use or was not properly maintained "
+           "during backtracking");
+  }else{
+    ecN = new (true) ECData(d_context, n);
+    n.setAttribute(ECAttr(), ecN);
+  }
 
   if(n.getKind() == APPLY){
-    for(Node::iterator cIter = n.begin(); cIter != n.end(); ++cIter){
-      Node child = *cIter;
-      
-      ECData * ecChild = getAttribute(child, EC);
+    for(TNode::iterator cIter = n.begin(); cIter != n.end(); ++cIter){
+      TNode child = *cIter;
+
+      ECData* ecChild = child.getAttribute(ECAttr());
       ecChild = ccFind(ecChild);
 
+      for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->next ){
+        if(equiv(n, Px->data)){
+          d_pending.push_back(n.eqNode(Px->data));
+        }
+      }
+
       ecChild->addPredecessor(n, d_context);
     }
   }
+
+}
+
+bool TheoryUF::sameCongruenceClass(TNode x, TNode y){
+  return
+    ccFind(x.getAttribute(ECAttr())) ==
+    ccFind(y.getAttribute(ECAttr()));
 }
 
 bool TheoryUF::equiv(Node x, Node y){
@@ -59,10 +124,10 @@ bool TheoryUF::equiv(Node x, Node y){
   Node::iterator yIter = y.begin();
 
   while(xIter != x.end()){
-    
-    if(ccFind(getAttribute(*xIter, EC)) !=
-       ccFind(getAttribute(*yIter, EC)))
+
+    if(!sameCongruenceClass(*xIter, *yIter)){
       return false;
+    }
 
     ++xIter;
     ++yIter;
@@ -106,18 +171,17 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
 //TODO make parameters soft references
 void TheoryUF::merge(){
   do{
-    Node assertion = d_pending[d_currentPendingIdx];
+    TNode assertion = d_pending[d_currentPendingIdx];
     d_currentPendingIdx = d_currentPendingIdx + 1;
-    
-    Node x = assertion[0];
-    Node y = assertion[1];
-    
-    ECData* ecX = ccFind(getAttribute(x, EC));
-    ECData* ecY = ccFind(getAttribute(y, EC));
-    
+
+    TNode x = assertion[0];
+    TNode y = assertion[1];
+
+    ECData* ecX = ccFind(x.getAttribute(ECAttr()));
+    ECData* ecY = ccFind(y.getAttribute(ECAttr()));
     if(ecX == ecY)
       continue;
-    
+
     ccUnion(ecX, ecY);
   }while( d_currentPendingIdx < d_pending.size() );
 }
@@ -125,7 +189,6 @@ void TheoryUF::merge(){
 void TheoryUF::check(OutputChannel& out, Effort level){
   while(!done()){
     Node assertion = get();
-    
 
     switch(assertion.getKind()){
     case EQUAL:
@@ -139,13 +202,20 @@ void TheoryUF::check(OutputChannel& out, Effort level){
       Unreachable();
     }
   }
+
+  //Make sure all outstanding merges are completed.
+  if(d_currentPendingIdx < d_pending.size()){
+    merge();
+  }
+
   if(fullEffort(level)){
     for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
         diseqIter != d_disequality.end();
         ++diseqIter){
-      
-      if(ccFind(getAttribute((*diseqIter)[0], EC)) ==
-         ccFind(getAttribute((*diseqIter)[1], EC))){
+
+      TNode left  = (*diseqIter)[0];
+      TNode right = (*diseqIter)[1];
+      if(sameCongruenceClass(left, right)){
         out.conflict(*diseqIter, true);
       }
     }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 0ab51ca2c..6a1dfb886 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -18,23 +18,44 @@
 #define __CVC4__THEORY__THEORY_UF_H
 
 #include "expr/node.h"
+#include "expr/attribute.h"
+
 #include "theory/theory.h"
 #include "theory/output_channel.h"
+
 #include "context/context.h"
 #include "theory/uf/ecdata.h"
 
 namespace CVC4 {
 namespace theory {
 
+
 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. */
   context::CDList<Node> d_pending;
-  context::CDList<Node> d_disequality;
+
+  /** Index of the next pending equality to merge. */
   context::CDO<unsigned> d_currentPendingIdx;
 
+  /** List of all disequalities this theory has seen. */
+  context::CDList<Node> d_disequality;
+
+
 public:
-  void setup(const Node& n);
+
+  TheoryUF(context::Context* c);
+  ~TheoryUF();
+
+  void registerTerm(TNode n);
+  
   
   void check(OutputChannel& out, Effort level= FULL_EFFORT);
 
@@ -45,16 +66,56 @@ public:
                Effort level = FULL_EFFORT){}
 
 private:
+  /**
+   * Checks whether 2 nodes are already in the same equivalence class tree.
+   * This should only be used internally, and it should only be done when
+   * the only thing done with the equivalence classes is an equality check.
+   *
+   * @returns true iff ccFind(x) == ccFind(y);
+   */
+  bool sameCongruenceClass(TNode x, TNode y);
+
+  /**
+   * Checks whether Node x and Node y are currently congruent
+   * using the equivalence class data structures.
+   * @returns true iff
+   *    |x| = n = |y| and
+   *    x.getOperator() == y.getOperator() and
+   *    forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
+   */
   bool equiv(Node x, Node y);
+
+  /**
+   * Merges 2 equivalence classes, checks wether any predecessors need to
+   * be set equal to complete congruence closure.
+   * The class with the smaller class size will be merged.
+   * @pre ecX->isClassRep()
+   * @pre ecY->isClassRep()
+   */
   void ccUnion(ECData* ecX, ECData* ecY);
+
+  /**
+   * Returns the representative of the equivalence class.
+   * May modify the find pointers associated with equivalence classes.
+   */
   ECData* ccFind(ECData* x);
 
+  /* Performs Congruence Closure to reflect the new additions to d_pending. */
   void merge();
-  //TODO put back in theory
+
+};
 
 
+
+struct ECCleanupFcn{
+  static void cleanup(ECData* & ec){
+    ec->deleteSelf();
+  }
 };
 
+struct EquivClass;
+typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
+
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */