4 files changed, 14 insertions, 39 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 9280141ea..8cbf975f2 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -4,4 +4,6 @@
 # src/expr/builtin_kinds.
 #
 
-parameterized APPLY "uninterpreted function application"
+theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
+
+parameterized APPLY_UF 1: "uninterpreted function application"
diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h
deleted file mode 100644
index b5cdda4ec..000000000
--- a/src/theory/uf/theory_def.h
+++ /dev/null
@@ -1,24 +0,0 @@
-/*********************                                                        */
-/** theory_def.h
- ** Original author: mdeters
- ** Major contributors: none
- ** 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.
- **
- ** Definition for TheoryUF (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__UF__THEORY_DEF_H
-#define __CVC4__THEORY__UF__THEORY_DEF_H
-
-#include "theory/uf/theory_uf.h"
-
-#endif /* __CVC4__THEORY__UF__THEORY_DEF_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index cd477a910..4f15cca75 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -107,15 +107,12 @@ void TheoryUF::registerTerm(TNode n){
     n.setAttribute(ECAttr(), ecN);
   }
 
-  /* If the node is an APPLY, we need to add it to the predecessor list
+  /* If the node is an APPLY_UF, we need to add it to the predecessor list
    * of its children.
    */
-  if(n.getKind() == APPLY){
+  if(n.getKind() == APPLY_UF){
     TNode::iterator cIter = n.begin();
 
-    //The first element of an apply is the function symbol which should not
-    //have an associated ECData, so it needs to be skipped.
-    ++cIter;
     for(; cIter != n.end(); ++cIter){
       TNode child = *cIter;
 
@@ -148,8 +145,8 @@ bool TheoryUF::sameCongruenceClass(TNode x, TNode y){
 }
 
 bool TheoryUF::equiv(TNode x, TNode y){
-  Assert(x.getKind() == kind::APPLY);
-  Assert(y.getKind() == kind::APPLY);
+  Assert(x.getKind() == kind::APPLY_UF);
+  Assert(y.getKind() == kind::APPLY_UF);
 
   if(x.getNumChildren() != y.getNumChildren())
     return false;
@@ -157,13 +154,11 @@ bool TheoryUF::equiv(TNode x, TNode y){
   if(x.getOperator() != y.getOperator())
     return false;
 
+  // intentionally don't look at operator
+
   TNode::iterator xIter = x.begin();
   TNode::iterator yIter = y.begin();
 
-  //Skip operator of the applies
-  ++xIter;
-  ++yIter;
-
   while(xIter != x.end()){
 
     if(!sameCongruenceClass(*xIter, *yIter)){
@@ -258,11 +253,12 @@ Node TheoryUF::constructConflict(TNode diseq){
 
   NodeBuilder<> nb(kind::AND);
   nb << diseq;
-  for(unsigned i=0; i<d_assertions.size(); ++i)
+  for(unsigned i = 0; i < d_assertions.size(); ++i) {
     nb << d_assertions[i];
+  }
 
-  Node conflict = nb;
-
+  Assert(nb.getNumChildren() > 0);
+  Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb;
 
   Debug("uf") << "conflict constructed : " << conflict << std::endl;
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 9e57311b5..87c33e958 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -30,6 +30,7 @@
 #include "theory/theory.h"
 
 #include "context/context.h"
+#include "context/cdo.h"
 #include "context/cdlist.h"
 #include "theory/uf/ecdata.h"