Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup.

7 files changed, 461 insertions, 1 deletions

diff --git a/src/context/context.h b/src/context/context.h
index ff40542d1..1af4480f9 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -102,6 +102,11 @@ public:
   int getLevel() const { return ((int)d_scopeList.size()) - 1; }
 
   /**
+   * Return the ContextMemoryManager associated with the context.
+   */
+  ContextMemoryManager* getCMM(){ return d_pCMM; }
+
+  /**
    * Save the current state, create a new Scope
    */
   void push();
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 8aa76ea81..8b83f71cf 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "theory/output_channel.h"
+#include "context/context.h"
 
 namespace CVC4 {
 namespace theory {
@@ -101,6 +102,19 @@ public:
                        const Node& n,
                        Effort level = FULL_EFFORT) = 0;
 
+protected:
+  /**
+   * Returns the next atom in the assertFact() queue.
+   * Guarentees that registerTerm is called on the theory specific subterms.
+   * @return the next atom in the assertFact() queue.
+   */
+  Node get();
+
+  /**
+   * Returns true if the assertFactQueue is empty
+   */
+  bool done() { return true; }
+
 };/* class Theory */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 7895803a6..537b8b124 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -5,6 +5,10 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LTLIBRARIES = libuf.la
 
-libuf_la_SOURCES =
+libuf_la_SOURCES = \
+	ecdata.h \
+	ecdata.cpp \
+	theory_uf.h \
+	theory_uf.cpp
 
 EXTRA_DIST = kinds
diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp
new file mode 100644
index 000000000..a22faf61e
--- /dev/null
+++ b/src/theory/uf/ecdata.cpp
@@ -0,0 +1,105 @@
+#include "theory/uf/ecdata.h"
+
+using namespace CVC4;
+using namespace context;
+using namespace theory;
+
+
+ECData::ECData(Context * context, const Node & n) :
+  ContextObj(context),
+  find(this), 
+  rep(n), 
+  watchListSize(0), 
+  first(NULL), 
+  last(NULL)
+{}
+
+
+bool ECData::isClassRep(){
+  return this == this->find;
+}
+
+void ECData::addPredecessor(Node n, Context* context){
+  Assert(isClassRep());
+
+  makeCurrent();
+
+  Link * newPred = new (context->getCMM())  Link(context, n, first);
+  first = newPred; 
+  if(last == NULL){
+    last = newPred;
+  }
+
+  ++watchListSize;
+}
+
+ContextObj* ECData::save(ContextMemoryManager* pCMM) {
+  return new(pCMM) ECData(*this);
+}
+
+void ECData::restore(ContextObj* pContextObj) {
+  *this = *((ECData*)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();
+  find = ec;
+}
+
+ECData * ECData::getFind(){
+  return find;
+}
+
+
+Link* ECData::getFirst(){
+  return first;
+}
+
+
+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 );
+
+  nmaster->makeCurrent();
+
+  nmaster->watchListSize +=  nslave->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;
+  }
+}
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
new file mode 100644
index 000000000..fd0855bee
--- /dev/null
+++ b/src/theory/uf/ecdata.h
@@ -0,0 +1,147 @@
+/*********************                                                        */
+/** ecdata.h
+ ** Original author: taking
+ ** Major contributors: barrett
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context dependent equivalence class datastructure for nodes.
+ ** Currently keeps a context dependent watch list.
+ **/
+
+#ifndef __CVC4__THEORY__UF__ECDATA_H
+#define __CVC4__THEORY__UF__ECDATA_H
+
+#include "expr/node.h"
+#include "context/context.h"
+#include "context/context_mm.h"
+
+namespace CVC4 {
+namespace theory {
+
+struct Link {
+  context::CDO< Link* > next;
+  
+  //TODO soft reference
+  Node data;
+  
+  Link(context::Context* context, Node n, Link * l = NULL):
+    next(context, l), data(n)
+  {}
+
+  static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
+    return pCMM->newData(size);
+  }
+  
+};
+
+
+
+class ECData : public context::ContextObj {
+private:
+  ECData * find;
+
+  Node rep;
+  
+  unsigned watchListSize;
+  Link * first;
+  Link * last;
+
+
+  context::ContextObj* save(context::ContextMemoryManager* pCMM);
+  void restore(context::ContextObj* pContextObj);
+
+
+public:
+  /**
+   * Returns true if this ECData object is the current representative of
+   * the equivalence class.
+   */
+  bool isClassRep();
+
+  /**
+   * Adds a node to the watch list of the equivalence class.
+   * Requires a context to do memory management.
+   * @param n the node to be added.
+   * @pre isClassRep() == true
+   */
+  void addPredecessor(Node n, context::Context* context);
+  
+
+
+  /**
+   * Creates a EQ with the representative n
+   * @param context the context to associate with this ecdata.
+   *   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);
+
+  static ECData * ccFind(ECData * fp);
+
+
+  /**
+   * Returns the representative of this ECData.
+   */
+  Node getRep();
+
+  /**
+   * Returns the size of the equivalence class.
+   */
+  unsigned getWatchListSize();
+
+  /**
+   * Returns a pointer the first member of the watch list.
+   */
+  Link* getFirst();
+
+
+  /**
+   * Returns the find pointer of the ECData.
+   * If isClassRep(), then getFind() == this
+   */
+  ECData* getFind();
+
+
+  /**
+   * @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 namespace */
+}/* CVC4 namespace */
+
+
+#endif /* __CVC4__THEORY__UF__ECDATA_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
new file mode 100644
index 000000000..840c7b51e
--- /dev/null
+++ b/src/theory/uf/theory_uf.cpp
@@ -0,0 +1,138 @@
+
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/ecdata.h"
+#include "expr/kind.h"
+
+using namespace CVC4;
+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);
+
+  if(n.getKind() == APPLY){
+    for(Node::iterator cIter = n.begin(); cIter != n.end(); ++cIter){
+      Node child = *cIter;
+      
+      ECData * ecChild = getAttribute(child, EC);
+      ecChild = ccFind(ecChild);
+
+      ecChild->addPredecessor(n, d_context);
+    }
+  }
+}
+
+bool TheoryUF::equiv(Node x, Node 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();
+
+  while(xIter != x.end()){
+    
+    if(ccFind(getAttribute(*xIter, EC)) !=
+       ccFind(getAttribute(*yIter, EC)))
+      return false;
+
+    ++xIter;
+    ++yIter;
+  }
+  return true;
+}
+
+ECData* TheoryUF::ccFind(ECData * x){
+  if( x->getFind() == x)
+    return x;
+  else{
+    return ccFind(x->getFind());
+  }
+}
+
+void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
+  ECData* nslave;
+  ECData* nmaster;
+
+  if(ecX->getWatchListSize() <= ecY->getWatchListSize()){
+    nslave = ecX;
+    nmaster = ecY;
+  }else{
+    nslave = ecY;
+    nmaster = ecX;
+  }
+
+  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)){
+        d_pending.push_back((Px->data).eqExpr(Py->data));
+      }
+    }
+  }
+
+  ECData::takeOverDescendantWatchList(nslave, nmaster);
+}
+
+//TODO make parameters soft references
+void TheoryUF::merge(){
+  do{
+    Node 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));
+    
+    if(ecX == ecY)
+      continue;
+    
+    ccUnion(ecX, ecY);
+  }while( d_currentPendingIdx < d_pending.size() );
+}
+
+void TheoryUF::check(OutputChannel& out, Effort level){
+  while(!done()){
+    Node assertion = get();
+    
+
+    switch(assertion.getKind()){
+    case EQUAL:
+      d_pending.push_back(assertion);
+      merge();
+      break;
+    case NOT:
+      d_disequality.push_back(assertion[0]);
+      break;
+    default:
+      Unreachable();
+    }
+  }
+  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))){
+        out.conflict(*diseqIter, true);
+      }
+    }
+  }
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
new file mode 100644
index 000000000..06b0ee4f8
--- /dev/null
+++ b/src/theory/uf/theory_uf.h
@@ -0,0 +1,47 @@
+
+#ifndef __CVC4__THEORY__THEORY_UF_H
+#define __CVC4__THEORY__THEORY_UF_H
+
+#include "expr/node.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:
+  context::Context* d_context;
+  context::CDList<Node> d_pending;
+  context::CDList<Node> d_disequality;
+  context::CDO<unsigned> d_currentPendingIdx;
+
+public:
+  void setup(const Node& n);
+  
+  void check(OutputChannel& out, Effort level= FULL_EFFORT);
+
+  void propagate(OutputChannel& out, Effort level= FULL_EFFORT){}
+
+  void explain(OutputChannel& out,
+               const Node& n,
+               Effort level = FULL_EFFORT){}
+
+private:
+  bool equiv(Node x, Node y);
+  void ccUnion(ECData* ecX, ECData* ecY);
+  ECData* ccFind(ECData* x);
+
+  void merge();
+  //TODO put back in theory
+
+
+};
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+
+#endif /* __CVC4__THEORY__THEORY_UF_H */