TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again

3 files changed, 19 insertions, 22 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index e079d67bd..f5b1e9b44 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -22,7 +22,7 @@
 #include "context/context.h"
 
 #include <queue>
-#include <vector>
+#include <list>
 
 #include <typeinfo>
 
@@ -293,13 +293,13 @@ Node TheoryImpl<T>::get() {
   d_facts.pop();
 
   if(! fact.getAttribute(RegisteredAttr())) {
-    std::vector<TNode> toReg;
+    std::list<TNode> toReg;
     toReg.push_back(fact);
 
     /* Essentially this is doing a breadth-first numbering of
      * non-registered subterms with children.  Any non-registered
      * leaves are immediately registered. */
-    for(std::vector<TNode>::iterator workp = toReg.begin();
+    for(std::list<TNode>::iterator workp = toReg.begin();
         workp != toReg.end();
         ++workp) {
 
@@ -323,7 +323,7 @@ Node TheoryImpl<T>::get() {
      * and the above registration of leaves, this should ensure that
      * all subterms in the entire tree were registered in
      * reverse-topological order. */
-    for(std::vector<TNode>::reverse_iterator i = toReg.rend();
+    for(std::list<TNode>::reverse_iterator i = toReg.rend();
         i != toReg.rbegin();
         ++i) {
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2a5eb682e..0c58d45e4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -26,13 +26,9 @@ using namespace CVC4::theory::uf;
 
 
 
-//TODO remove
-Node getOperator(Node x) { return Node::null(); }
-
-
-
 TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
   TheoryImpl<TheoryUF>(c, out),
+  d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
   d_disequality(c),
@@ -47,6 +43,7 @@ void TheoryUF::preRegisterTerm(TNode n){
 void TheoryUF::registerTerm(TNode n){
 
   d_registered.push_back(n);
+  n.printAst(Warning());
 
   ECData* ecN;
 
@@ -148,7 +145,7 @@ bool TheoryUF::equiv(TNode x, TNode y){
   if(x.getNumChildren() != y.getNumChildren())
     return false;
 
-  if(getOperator(x) != getOperator(y))
+  if(x.getOperator() != y.getOperator())
     return false;
 
   TNode::iterator xIter = x.begin();
@@ -213,7 +210,8 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
   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)){
-        d_pending.push_back((Px->data).eqNode(Py->data));
+        Node pendingEq = (Px->data).eqNode(Py->data);
+        d_pending.push_back(pendingEq);
       }
     }
   }
@@ -229,8 +227,11 @@ void TheoryUF::merge(){
     TNode x = assertion[0];
     TNode y = assertion[1];
 
-    ECData* ecX = ccFind(x.getAttribute(ECAttr()));
-    ECData* ecY = ccFind(y.getAttribute(ECAttr()));
+    ECData* tmpX = x.getAttribute(ECAttr());
+    ECData* tmpY = y.getAttribute(ECAttr());
+
+    ECData* ecX = ccFind(tmpX);
+    ECData* ecY = ccFind(tmpY);
     if(ecX == ecY)
       continue;
 
@@ -241,8 +242,8 @@ void TheoryUF::merge(){
 Node TheoryUF::constructConflict(TNode diseq){
   NodeBuilder<> nb(kind::AND);
   nb << diseq;
-  for(unsigned i=0; i<d_pending.size(); ++i)
-    nb << d_pending[i];
+  for(unsigned i=0; i<d_assertions.size(); ++i)
+    nb << d_assertions[i];
 
   return nb;
 }
@@ -253,6 +254,7 @@ void TheoryUF::check(Effort level){
 
     switch(assertion.getKind()){
     case EQUAL:
+      d_assertions.push_back(assertion);
       d_pending.push_back(assertion);
       merge();
       break;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 4fc835223..34b6719d7 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -33,15 +33,10 @@ class TheoryUF : public TheoryImpl<TheoryUF> {
 
 private:
 
-
+  //TODO document
+  context::CDList<Node> d_assertions;
 
   /**
-   * 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. 
    *
    * Tricky part: