Merge from "cc" branch:

CongruenceClosure implementation; CongruenceClosure white-box test.

New UF theory implementation based on new CC module.  This one
supports predicates.  The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").

Added type infrastructure for TUPLE.

Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).

Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)

Other minor changes.

5 files changed, 941 insertions, 0 deletions

diff --git a/src/theory/uf/tim/Makefile.am b/src/theory/uf/tim/Makefile.am
new file mode 100644
index 000000000..647783885
--- /dev/null
+++ b/src/theory/uf/tim/Makefile.am
@@ -0,0 +1,14 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libuftim.la
+
+libuftim_la_SOURCES = \
+	ecdata.h \
+	ecdata.cpp \
+	theory_uf_tim.h \
+	theory_uf_tim.cpp
+
+EXTRA_DIST =
diff --git a/src/theory/uf/tim/ecdata.cpp b/src/theory/uf/tim/ecdata.cpp
new file mode 100644
index 000000000..52a110ff2
--- /dev/null
+++ b/src/theory/uf/tim/ecdata.cpp
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file ecdata.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** 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.\endverbatim
+ **
+ ** \brief Implementation of equivalence class data for UF theory.
+ **
+ ** Implementation of equivalence class data for UF theory.  This is a
+ ** context-dependent object.
+ **/
+
+#include "theory/uf/tim/ecdata.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
+
+ECData::ECData(Context * context, TNode n) :
+  ContextObj(context),
+  d_find(this),
+  d_rep(n),
+  d_watchListSize(0),
+  d_first(NULL),
+  d_last(NULL) {
+}
+
+bool ECData::isClassRep() {
+  return this == this->d_find;
+}
+
+void ECData::addPredecessor(TNode n) {
+  Assert(isClassRep());
+
+  makeCurrent();
+
+  Link * newPred = new(getCMM()) Link(getContext(), n, d_first);
+  d_first = newPred;
+  if(d_last == NULL) {
+    d_last = newPred;
+  }
+
+  ++d_watchListSize;
+}
+
+ContextObj* ECData::save(ContextMemoryManager* pCMM) {
+  return new(pCMM) ECData(*this);
+}
+
+void ECData::restore(ContextObj* 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 d_rep;
+}
+
+unsigned ECData::getWatchListSize() {
+  return d_watchListSize;
+}
+
+void ECData::setFind(ECData * ec) {
+  makeCurrent();
+  d_find = ec;
+}
+
+ECData* ECData::getFind() {
+  return d_find;
+}
+
+Link* ECData::getFirst() {
+  return d_first;
+}
+
+void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) {
+  Assert(nslave != nmaster);
+  Assert(nslave->getFind() == nmaster);
+
+  nmaster->makeCurrent();
+
+  nmaster->d_watchListSize += nslave->d_watchListSize;
+
+  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/tim/ecdata.h b/src/theory/uf/tim/ecdata.h
new file mode 100644
index 000000000..5e72f0042
--- /dev/null
+++ b/src/theory/uf/tim/ecdata.h
@@ -0,0 +1,261 @@
+/*********************                                                        */
+/*! \file ecdata.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** 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.\endverbatim
+ **
+ ** \brief Context dependent equivalence class datastructure for nodes.
+ **
+ ** Context dependent equivalence class datastructure for nodes.
+ ** Currently keeps a context dependent watch list.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H
+#define __CVC4__THEORY__UF__TIM__ECDATA_H
+
+#include "expr/node.h"
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/context_mm.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace tim {
+
+/**
+ * Link is a context dependent linked list of nodes.
+ * Link is intended to be allocated in a Context's memory manager.
+ * The next pointer of the list is context dependent, but the node being
+ * pointed to is fixed for the life of the Link.
+ *
+ * Clients of Link are intended not to modify the node that is being pointed
+ * to in good faith.  This may change in the future.
+ */
+struct Link {
+  /**
+   * Pointer to the next element in linked list.
+   * This is context dependent. 
+   */
+  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 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) :
+    d_next(true, context, l),
+    d_data(n) {
+    Debug("context") << "Link: " << this
+                     << " so cdo is " << &d_next << std::endl;
+  }
+
+  /**
+   * Allocates a new Link in the region for the provided ContextMemoryManager.
+   * This allows for cheap cleanup on pop.
+   */
+  static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
+    return pCMM->newData(size);
+  }
+
+private:
+
+  /**
+   * The destructor isn't actually defined.  This declaration keeps
+   * the compiler from creating (wastefully) a default definition, and
+   * ensures that we get a link error if someone uses Link in a way
+   * that requires destruction.  Objects of class Link should always
+   * be allocated in a ContextMemoryManager, which doesn't call
+   * destructors.
+   */
+  ~Link() throw();
+
+  /**
+   * Just like the destructor, this is not defined.  This ensures no
+   * one tries to create a Link on the heap.
+   */
+  static void* operator new(size_t size);
+
+};/* struct Link */
+
+
+/**
+ * ECData is a equivalence class object that is context dependent.
+ * It is developed in order to support the congruence closure algorithm
+ * in TheoryUF, and is not intended to be used outside of that package.
+ *
+ * ECData maintains:
+ * - find pointer for the equivalence class (disjoint set forest)
+ * - the node that represents the equivalence class.
+ * - maintains a predecessorlist/watchlist
+ *
+ * ECData does not have support for the canonical find and union operators
+ * for disjoint set forests.  Instead it only provides access to the find
+ * pointer. The implementation of find is ccFind in TheoryUF.
+ * union is broken into 2 phases:
+ *  1) setting the find point with setFind
+ *  2) taking over the watch list of the other node.
+ * This is a technical requirement for the implementation of TheoryUF.
+ * (See ccUnion in TheoryUF for more information.)
+ *
+ * The intended paradigm for iterating over the watch list of ec is:
+ *      for(Link* i = ec->getFirst(); i != NULL; i = i->next );
+ *
+ * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses
+ * ECData lives.
+ */
+class ECData : public context::ContextObj {
+private:
+  /**
+   * This is the standard disjoint set forest find pointer.
+   *
+   * Why an ECData pointer instead of a node?
+   * This was chosen to be a ECData pointer in order to shortcut at least one
+   * table every time the find pointer is examined.
+   */
+  ECData* d_find;
+
+  /**
+   * This is pointer back to the node that represents this equivalence class.
+   *
+   * The following invariant should be maintained:
+   *  (n.getAttribute(ECAttr()))->rep == n
+   * i.e. rep is equal to the node that maps to the ECData using ECAttr.
+   *
+   * Tricky part: This needs to be a TNode, not a Node.
+   * Suppose that rep were a hard link.
+   * When a node n maps to an ECData via the ECAttr() there will be a hard
+   * link back to n in the ECData. The attribute does not do garbage collection
+   * until the node gets garbage collected, which does not happen until its
+   * ref count drops to 0. So because of this cycle neither the node and
+   * the ECData will never get garbage collected.
+   * So this needs to be a soft link.
+   */
+  TNode d_rep;
+
+  // Watch list data structures follow
+
+  /**
+   * Maintains watch list size for more efficient merging.
+   */
+  unsigned d_watchListSize;
+
+  /**
+   * Pointer to the beginning of the watchlist.
+   * This value is NULL iff the watch list is empty.
+   */
+  Link* d_first;
+
+  /**
+   * Pointer to the end of the watch-list.
+   * This is maintained in order to constant time list merging.
+   * (This does not give any asymptotic improve as this is currently always
+   * preceeded by an O(|watchlist|) operation.)
+   * This value is NULL iff the watch list is empty.
+   */
+  Link* d_last;
+
+  /** Context-dependent operation: save this ECData */
+  context::ContextObj* save(context::ContextMemoryManager* pCMM);
+
+  /** Context-dependent operation: restore this ECData */
+  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.  Does
+   * context-dependent memory allocation in the Context with which
+   * this ECData was created.
+   *
+   * @param n the node to be added.
+   * @pre isClassRep() == true
+   */
+  void addPredecessor(TNode n);
+
+  /**
+   * 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, TNode n);
+
+  /** Destructor for ECDatas */
+  ~ECData() {
+    Debug("ufgc") << "Calling ECData destructor" << std::endl;
+    destroy();
+  }
+
+  /**
+   * An ECData takes over the watch list of another ECData.
+   * This is the second step in the union operator for ECData.
+   * This should be called after nslave->setFind(nmaster);
+   * After this is done nslave's watch list should never be accessed by
+   * getLast() or getFirst()
+   */
+  static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
+
+  /**
+   * 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();
+
+  /**
+   * Sets the find pointer of the equivalence class to be another ECData object.
+   *
+   * @pre isClassRep() == true
+   * @pre ec->isClassRep() == true
+   * @post isClassRep() == false
+   * @post ec->isClassRep() == true
+   */
+  void setFind(ECData * ec);
+
+};/* class ECData */
+
+}/* CVC4::theory::uf::tim namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */
diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
new file mode 100644
index 000000000..ccc37a24b
--- /dev/null
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -0,0 +1,332 @@
+/*********************                                                        */
+/*! \file theory_uf_tim.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** 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.\endverbatim
+ **
+ ** \brief Implementation of the theory of uninterpreted functions.
+ **
+ ** Implementation of the theory of uninterpreted functions.
+ **/
+
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/uf/tim/ecdata.h"
+#include "expr/kind.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
+
+TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
+  TheoryUF(id, c, out),
+  d_assertions(c),
+  d_pending(c),
+  d_currentPendingIdx(c,0),
+  d_disequality(c),
+  d_registered(c) {
+}
+
+TheoryUFTim::~TheoryUFTim() {
+}
+
+Node TheoryUFTim::rewrite(TNode n){
+  Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+  Node ret(n);
+  if(n.getKind() == EQUAL){
+    Assert(n.getNumChildren() == 2);
+    if(n[0] == n[1]) {
+      ret = NodeManager::currentNM()->mkConst(true);
+    }
+  }
+  Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+  return ret;
+}
+void TheoryUFTim::preRegisterTerm(TNode n) {
+  Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
+  Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
+}
+
+void TheoryUFTim::registerTerm(TNode n) {
+
+  Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl;
+
+  d_registered.push_back(n);
+
+  ECData* ecN;
+
+  if(n.getAttribute(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 {
+    //The attribute does not exist, so it is created and set
+    ecN = new (true) ECData(getContext(), n);
+    n.setAttribute(ECAttr(), ecN);
+  }
+
+  /* If the node is an APPLY_UF, we need to add it to the predecessor list
+   * of its children.
+   */
+  if(n.getKind() == APPLY_UF) {
+    TNode::iterator cIter = n.begin();
+
+    for(; cIter != n.end(); ++cIter) {
+      TNode child = *cIter;
+
+      /* Because this can be called after nodes have been merged, we need
+       * to lookup the representative in the UnionFind datastructure.
+       */
+      ECData* ecChild = ccFind(child.getAttribute(ECAttr()));
+
+      /* 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->d_next ) {
+        if(equiv(n, Px->d_data)) {
+          Node pend = n.eqNode(Px->d_data);
+          d_pending.push_back(pend);
+        }
+      }
+
+      ecChild->addPredecessor(n);
+    }
+  }
+  Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
+
+}
+
+bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) {
+  return
+    ccFind(x.getAttribute(ECAttr())) ==
+    ccFind(y.getAttribute(ECAttr()));
+}
+
+bool TheoryUFTim::equiv(TNode x, TNode y) {
+  Assert(x.getKind() == kind::APPLY_UF);
+  Assert(y.getKind() == kind::APPLY_UF);
+
+  if(x.getNumChildren() != y.getNumChildren()) {
+    return false;
+  }
+
+  if(x.getOperator() != y.getOperator()) {
+    return false;
+  }
+
+  // intentionally don't look at operator
+
+  TNode::iterator xIter = x.begin();
+  TNode::iterator yIter = y.begin();
+
+  while(xIter != x.end()) {
+
+    if(!sameCongruenceClass(*xIter, *yIter)) {
+      return false;
+    }
+
+    ++xIter;
+    ++yIter;
+  }
+  return true;
+}
+
+/* This is a very basic, but *obviously correct* find implementation
+ * of the classic find algorithm.
+ * TODO after we have done some more testing:
+ * 1) Add path compression.  This is dependent on changes to ccUnion as
+ *    many better algorithms use eager path compression.
+ * 2) Elminate recursion.
+ */
+ECData* TheoryUFTim::ccFind(ECData * x) {
+  if(x->getFind() == x) {
+    return x;
+  } else {
+    return ccFind(x->getFind());
+  }
+  /* Slightly better Find w/ path compression and no recursion*/
+  /*
+    ECData* start;
+    ECData* next = x;
+    while(x != x->getFind()) x=x->getRep();
+    while( (start = next) != x) {
+      next = start->getFind();
+      start->setFind(x);
+    }
+    return x;
+  */
+}
+
+void TheoryUFTim::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->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);
+      }
+    }
+  }
+
+  ECData::takeOverDescendantWatchList(nslave, nmaster);
+}
+
+void TheoryUFTim::merge() {
+  while(d_currentPendingIdx < d_pending.size() ) {
+    Node assertion = d_pending[d_currentPendingIdx];
+    d_currentPendingIdx = d_currentPendingIdx + 1;
+
+    TNode x = assertion[0];
+    TNode y = assertion[1];
+
+    ECData* tmpX = x.getAttribute(ECAttr());
+    ECData* tmpY = y.getAttribute(ECAttr());
+
+    ECData* ecX = ccFind(tmpX);
+    ECData* ecY = ccFind(tmpY);
+    if(ecX == ecY)
+      continue;
+
+    Debug("uf") << "merging equivalence classes for " << std::endl;
+    Debug("uf") << "left equivalence class :" << (ecX->getRep()) << std::endl;
+    Debug("uf") << "right equivalence class :" << (ecY->getRep()) << std::endl;
+    Debug("uf") << std::endl;
+
+    ccUnion(ecX, ecY);
+  }
+}
+
+Node TheoryUFTim::constructConflict(TNode diseq) {
+  Debug("uf") << "uf: begin constructConflict()" << std::endl;
+
+  NodeBuilder<> nb(kind::AND);
+  nb << diseq;
+  for(unsigned i = 0; i < d_assertions.size(); ++i) {
+    nb << d_assertions[i];
+  }
+
+  Assert(nb.getNumChildren() > 0);
+  Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb;
+
+  Debug("uf") << "conflict constructed : " << conflict << std::endl;
+
+  Debug("uf") << "uf: ending constructConflict()" << std::endl;
+
+  return conflict;
+}
+
+void TheoryUFTim::check(Effort level) {
+
+  Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
+
+  while(!done()) {
+    Node assertion = get();
+    Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl;
+
+    switch(assertion.getKind()) {
+    case EQUAL:
+      d_assertions.push_back(assertion);
+      d_pending.push_back(assertion);
+      merge();
+      break;
+    case NOT:
+      Assert(assertion[0].getKind() == EQUAL,
+             "predicates not supported in this UF implementation");
+      d_disequality.push_back(assertion[0]);
+      break;
+    case APPLY_UF:
+      Unhandled("predicates not supported in this UF implementation");
+    default:
+      Unhandled(assertion.getKind());
+    }
+
+    Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl;
+  }
+
+  //Make sure all outstanding merges are completed.
+  if(d_currentPendingIdx < d_pending.size()) {
+    merge();
+  }
+
+  if(standardEffortOrMore(level)) {
+    for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
+        diseqIter != d_disequality.end();
+        ++diseqIter) {
+
+      TNode left  = (*diseqIter)[0];
+      TNode right = (*diseqIter)[1];
+      if(sameCongruenceClass(left, right)) {
+        Node remakeNeq = (*diseqIter).notNode();
+        Node conflict = constructConflict(remakeNeq);
+        d_out->conflict(conflict, false);
+        return;
+      }
+    }
+  }
+
+  Debug("uf") << "uf: end check(" << level << ")" << std::endl;
+}
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
new file mode 100644
index 000000000..1591cc05c
--- /dev/null
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -0,0 +1,229 @@
+/*********************                                                        */
+/*! \file theory_uf.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** 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.\endverbatim
+ **
+ ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.
+ **
+ ** This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.  It is based on the Nelson-Oppen algorithm given in
+ ** "Fast Decision Procedures Based on Congruence Closure"
+ **  (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
+ ** This has been extended to work in a context-dependent way.
+ ** This interacts heavily with the data-structures given in ecdata.h .
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/theory.h"
+
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/ecdata.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace tim {
+
+class TheoryUFTim : public TheoryUF {
+
+private:
+
+  /**
+   * List of all of the non-negated literals from the assertion queue.
+   * This is used only for conflict generation.
+   * This differs from pending as the program generates new equalities that
+   * are not in this list.
+   * This will probably be phased out in future version.
+   */
+  context::CDList<Node> d_assertions;
+
+  /**
+   * List of pending equivalence class merges.
+   *
+   * Tricky part:
+   * Must keep a hard link because new equality terms are created and appended
+   * to this list.
+   */
+  context::CDList<Node> d_pending;
+
+  /** 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;
+
+  /**
+   * List of all of the terms that are registered in the current context.
+   * When registerTerm is called on a term we want to guarentee that there
+   * is a hard link to the term for the duration of the context in which
+   * register term is called.
+   * This invariant is enough for us to use soft links where we want is the
+   * current implementation as well as making ECAttr() not context dependent.
+   * Soft links used both in ECData, and Link.
+   */
+  context::CDList<Node> d_registered;
+
+public:
+
+  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+  TheoryUFTim(int id, context::Context* c, OutputChannel& out);
+
+  /** Destructor for the TheoryUF object. */
+  ~TheoryUFTim();
+
+
+
+  /**
+   * Registers a previously unseen [in this context] node n.
+   * For TheoryUF, this sets up and maintains invaraints about
+   * equivalence class data-structures.
+   *
+   * Overloads a void registerTerm(TNode n); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void registerTerm(TNode n);
+
+  /**
+   * Currently this does nothing.
+   *
+   * Overloads a void preRegisterTerm(TNode n); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void preRegisterTerm(TNode n);
+
+  /**
+   * Checks whether the set of literals provided to the theory is consistent.
+   *
+   * If this is called at any effort level, it computes the congruence closure
+   * of all of the positive literals in the context.
+   *
+   * If this is called at full effort it checks if any of the negative literals
+   * are inconsistent with the congruence closure.
+   *
+   * Overloads  void check(Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void check(Effort level);
+
+
+  /**
+   * Rewrites a node in the theory of uninterpreted functions.
+   * This is fairly basic and only ensures that atoms that are
+   * unsatisfiable or a valid are rewritten to false or true respectively.
+   */
+  Node rewrite(TNode n);
+
+  /**
+   * Plug in old rewrite to the new (pre,post)rewrite interface.
+   */
+  RewriteResponse postRewrite(TNode n, bool topLevel) {
+    return RewriteComplete(topLevel ? rewrite(n) : Node(n));
+  }
+
+  /**
+   * Propagates theory literals. Currently does nothing.
+   *
+   * Overloads void propagate(Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void propagate(Effort level) {}
+
+  /**
+   * Explains a previously reported conflict. Currently does nothing.
+   *
+   * Overloads void explain(TNode n, Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void explain(TNode n, Effort level) {}
+
+  std::string identify() const { return std::string("TheoryUFTim"); }
+
+private:
+  /**
+   * Checks whether 2 nodes are already in the same equivalence class tree.
+   * This should only be used internally, and it should only be called 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(TNode x, TNode 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();
+
+  /** Constructs a conflict from an inconsistent disequality. */
+  Node constructConflict(TNode diseq);
+
+};/* class TheoryUFTim */
+
+
+/**
+ * Cleanup function for ECData. This will be used for called whenever
+ * a ECAttr is being destructed.
+ */
+struct ECCleanupStrategy {
+  static void cleanup(ECData* ec) {
+    Debug("ufgc") << "cleaning up ECData " << ec << "\n";
+    ec->deleteSelf();
+  }
+};/* struct ECCleanupStrategy */
+
+/** Unique name to use for constructing ECAttr. */
+struct ECAttrTag {};
+
+/**
+ * ECAttr is the attribute that maps a node to an equivalence class.
+ */
+typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
+
+}/* CVC4::theory::uf::tim namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */