UF theory bug fixes, code cleanup, and extra debugging output.

Enabled new UF theory by default.

Added some UF regressions.

Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing.  (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)

Added pre-rewriting to TheoryBool which rewrites:

  * (IFF true x)          =>  x
  * (IFF false x)         =>  (NOT x)
  * (IFF x true)          =>  x
  * (IFF x false)         =>  (NOT x)
  * (IFF x x)             =>  true
  * (IFF x (NOT x))       =>  false
  * (IFF (NOT x) x)       =>  false

  * (ITE true x y)        =>  x
  * (ITE false x y)       =>  y
  * (ITE cond x x)        =>  x

Added post-rewriting that does all of the above, plus normalize IFF and ITE:

  * (IFF x y)             =>  (IFF y x), if y < x
  * (ITE (NOT cond) x y)  =>  (ITE cond y x)

(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)

A little more debugging output from CNF stream, context pushes/pops,
ITE removal.

Some more documentation.

Fixed some typos.

15 files changed, 352 insertions, 72 deletions

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 0028aaad5..5d8e88db0 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -61,7 +61,8 @@ Context::~Context() throw(AssertionException) {
 
 
 void Context::push() {
-  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl;
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
+                   << getLevel() + 1 << "] {" << std::endl;
 
   // Create a new memory region
   d_pCMM->push();
@@ -100,7 +101,8 @@ void Context::pop() {
     pCNO = pCNO->d_pCNOnext;
   }
 
-  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl;
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
+                   << getLevel() << "]" << std::endl;
 }
 
 
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index b15f4ae66..08bcbaa7c 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -262,7 +262,7 @@ throw(OptionException) {
           printf("morgan\n");
           exit(1);
         } else {
-          throw OptionException(string("unknown language for --uf: `") +
+          throw OptionException(string("unknown option for --uf: `") +
                                 optarg + "'.  Try --uf help.");
         }
       }
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 5f8eb12b9..c719c66da 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -100,10 +100,10 @@ Node CnfStream::getNode(const SatLiteral& literal) {
 }
 
 SatLiteral CnfStream::convertAtom(TNode node) {
-  Assert(!isCached(node), "atom already mapped!");
-
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
+  Assert(!isCached(node), "atom already mapped!");
+
   bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
 
@@ -245,6 +245,8 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
   Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
+  Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
+
   // Convert the children to CNF
   SatLiteral a = toCNF(iffNode[0]);
   SatLiteral b = toCNF(iffNode[1]);
@@ -287,7 +289,7 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   Assert(iteNode.getKind() == ITE);
   Assert(iteNode.getNumChildren() == 3);
 
-  Debug("cnf") << "handlIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
+  Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
 
   SatLiteral condLit = toCNF(iteNode[0]);
   SatLiteral thenLit = toCNF(iteNode[1]);
@@ -353,8 +355,10 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
       nodeLit = handleAnd(node);
       break;
     case EQUAL:
-      if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) {
-        nodeLit = handleIff(node[0].iffNode(node[1]));
+      if(node[0].getType().isBoolean()) {
+        // should have an IFF instead
+        Unreachable("= Bool Bool  shouldn't be possible ?!");
+        //nodeLit = handleIff(node[0].iffNode(node[1]));
       } else {
         nodeLit = convertAtom(node);
       }
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 9b10f5a62..ba1445df8 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -43,7 +43,7 @@ Kind multKind(Kind k, int sgn);
  * Also writes relations with constants on both sides to TRUE or FALSE.
  * If it can, it returns true and sets res to this value.
  *
- * This is for optimizing rewriteAtom() to avoid the more compuationally
+ * This is for optimizing rewriteAtom() to avoid the more computationally
  * expensive general rewriting procedure.
  *
  * If simplification is not done, it returns Node::null()
@@ -476,8 +476,7 @@ Node ArithRewriter::rewriteTerm(TNode t){
     Node sub = makeUnaryMinusNode(t[0]);
     return rewrite(sub);
   }else{
-    Unreachable();
-    return Node::null();
+    Unhandled(t);
   }
 }
 
@@ -533,7 +532,7 @@ Kind multKind(Kind k, int sgn){
     case GEQ: return LEQ;
     case GT: return LT;
     default:
-      Unhandled();
+      Unhandled(k);
     }
     return NULL_EXPR;
   }else{
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ab8884228..157c45160 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -316,6 +316,9 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
 }
 
 RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
+  // ensure a hard link to the node we're returning
+  Node out;
+
   // Look for multiplications with a 0 argument and rewrite the whole
   // thing as 0
   if(n.getKind() == MULT) {
@@ -324,23 +327,34 @@ RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
     for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
       if((*i).getKind() == CONST_RATIONAL) {
         if((*i).getConst<Rational>() == ratZero) {
-          n = NodeManager::currentNM()->mkConst(ratZero);
+          out = NodeManager::currentNM()->mkConst(ratZero);
           break;
         }
       } else if((*i).getKind() == CONST_INTEGER) {
         if((*i).getConst<Integer>() == intZero) {
           if(n.getType().isInteger()) {
-            n = NodeManager::currentNM()->mkConst(intZero);
+            out = NodeManager::currentNM()->mkConst(intZero);
             break;
           } else {
-            n = NodeManager::currentNM()->mkConst(ratZero);
+            out = NodeManager::currentNM()->mkConst(ratZero);
             break;
           }
         }
       }
     }
+  } else if(n.getKind() == EQUAL) {
+    if(n[0] == n[1]) {
+      out = NodeManager::currentNM()->mkConst(true);
+    }
+  }
+
+  if(out.isNull()) {
+    // no preRewrite to perform
+    return RewriteComplete(Node(n));
+  } else {
+    // out is always a constant, so doesn't need to be rewritten again
+    return RewriteComplete(out);
   }
-  return RewriteComplete(Node(n));
 }
 
 Node TheoryArith::rewrite(TNode n){
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 3bd8b5a39..c8a9b4dbd 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libbooleans.la
 
 libbooleans_la_SOURCES = \
 	theory_bool.h \
+	theory_bool.cpp \
 	theory_bool_type_rules.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
new file mode 100644
index 000000000..a7e343fdc
--- /dev/null
+++ b/src/theory/booleans/theory_bool.cpp
@@ -0,0 +1,146 @@
+/*********************                                                        */
+/*! \file theory_bool.cpp
+ ** \verbatim
+ ** 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.\endverbatim
+ **
+ ** \brief The theory of booleans.
+ **
+ ** The theory of booleans.
+ **/
+
+#include "theory/theory.h"
+#include "theory/booleans/theory_bool.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+
+RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) {
+  if(n.getKind() == kind::IFF) {
+    NodeManager* nodeManager = NodeManager::currentNM();
+    Node tt = nodeManager->mkConst(true);
+    Node ff = nodeManager->mkConst(false);
+
+    // rewrite simple cases of IFF
+    if(n[0] == tt) {
+      // IFF true x
+      return RewriteAgain(n[1]);
+    } else if(n[1] == tt) {
+      // IFF x true
+      return RewriteAgain(n[0]);
+    } else if(n[0] == ff) {
+      // IFF false x
+      return RewriteAgain(n[1].notNode());
+    } else if(n[1] == ff) {
+      // IFF x false
+      return RewriteAgain(n[0].notNode());
+    } else if(n[0] == n[1]) {
+      // IFF x x
+      return RewriteComplete(tt);
+    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+      // IFF (NOT x) x
+      return RewriteComplete(ff);
+    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+      // IFF x (NOT x)
+      return RewriteComplete(ff);
+    }
+  } else if(n.getKind() == kind::ITE) {
+    // non-Boolean-valued ITEs should have been removed in place of
+    // a variable
+    Assert(n.getType().isBoolean());
+
+    NodeManager* nodeManager = NodeManager::currentNM();
+
+    // rewrite simple cases of ITE
+    if(n[0] == nodeManager->mkConst(true)) {
+      // ITE true x y
+      return RewriteAgain(n[1]);
+    } else if(n[0] == nodeManager->mkConst(false)) {
+      // ITE false x y
+      return RewriteAgain(n[2]);
+    } else if(n[1] == n[2]) {
+      // ITE c x x
+      return RewriteAgain(n[1]);
+    }
+  }
+
+  return RewriteComplete(n);
+}
+
+
+RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) {
+  if(n.getKind() == kind::IFF) {
+    NodeManager* nodeManager = NodeManager::currentNM();
+    Node tt = nodeManager->mkConst(true);
+    Node ff = nodeManager->mkConst(false);
+
+    // rewrite simple cases of IFF
+    if(n[0] == tt) {
+      // IFF true x
+      return RewriteComplete(n[1]);
+    } else if(n[1] == tt) {
+      // IFF x true
+      return RewriteComplete(n[0]);
+    } else if(n[0] == ff) {
+      // IFF false x
+      return RewriteAgain(n[1].notNode());
+    } else if(n[1] == ff) {
+      // IFF x false
+      return RewriteAgain(n[0].notNode());
+    } else if(n[0] == n[1]) {
+      // IFF x x
+      return RewriteComplete(tt);
+    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+      // IFF (NOT x) x
+      return RewriteComplete(ff);
+    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+      // IFF x (NOT x)
+      return RewriteComplete(ff);
+    }
+
+    if(n[1] < n[0]) {
+      // normalize (IFF x y) ==> (IFF y x), if y < x
+      return RewriteComplete(n[1].iffNode(n[0]));
+    }
+  } else if(n.getKind() == kind::ITE) {
+    // non-Boolean-valued ITEs should have been removed in place of
+    // a variable
+    Assert(n.getType().isBoolean());
+
+    NodeManager* nodeManager = NodeManager::currentNM();
+
+    // rewrite simple cases of ITE
+    if(n[0] == nodeManager->mkConst(true)) {
+      // ITE true x y
+      return RewriteComplete(n[1]);
+    } else if(n[0] == nodeManager->mkConst(false)) {
+      // ITE false x y
+      return RewriteComplete(n[2]);
+    } else if(n[1] == n[2]) {
+      // ITE c x x
+      return RewriteComplete(n[1]);
+    }
+
+    if(n[0].getKind() == kind::NOT) {
+      // rewrite  (ITE (NOT c) x y)  to  (ITE c y x)
+      Node out = nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]);
+      return RewriteComplete(out);
+    }
+  }
+
+  return RewriteComplete(n);
+}
+
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 4d8620146..f492041b8 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -45,6 +45,10 @@ public:
   void check(Effort e) { Unimplemented(); }
   void propagate(Effort e) { Unimplemented(); }
   void explain(TNode n, Effort e) { Unimplemented(); }
+
+  RewriteResponse preRewrite(TNode n, bool topLevel);
+  RewriteResponse postRewrite(TNode n, bool topLevel);
+
   std::string identify() const { return std::string("TheoryBool"); }
 };
 
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 174e10d2f..ba258aafd 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -20,8 +20,6 @@
 #include "expr/kind.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory::builtin;
 
 namespace CVC4 {
 namespace theory {
@@ -33,8 +31,10 @@ Node TheoryBuiltin::blastDistinct(TNode in) {
   if(in.getNumChildren() == 2) {
     // if this is the case exactly 1 != pair will be generated so the
     // AND is not required
-    Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]);
-    Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+    Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ?
+                                               kind::IFF : kind::EQUAL,
+                                               in[0], in[1]);
+    Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
     return neq;
   }
   // assume that in.getNumChildren() > 2 => diseqs.size() > 1
@@ -42,12 +42,14 @@ Node TheoryBuiltin::blastDistinct(TNode in) {
   for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
     TNode::iterator j = i;
     while(++j != in.end()) {
-      Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
-      Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+      Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ?
+                                                 kind::IFF : kind::EQUAL,
+                                                 *i, *j);
+      Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
       diseqs.push_back(neq);
     }
   }
-  Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
+  Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs);
   return out;
 }
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 64a3b8f06..1cce09439 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -313,6 +313,19 @@ public:
    * rewrite a term to a strictly larger term that contains itself, as
    * this will cause a loop of hard Node links in the cache (and thus
    * memory leakage).
+   *
+   * Be careful with the return value.  If a preRewrite() can return a
+   * sub-expression, and that sub-expression can be a member of the
+   * same theory and could be rewritten, make sure to return
+   * RewriteAgain instead of RewriteComplete.  This is an easy mistake
+   * to make, as preRewrite() is often a short-circuiting version of
+   * the same rewrites that occur in postRewrite(); however, in the
+   * postRewrite() case, the subexpressions have all been
+   * post-rewritten.  In the preRewrite() case, they have NOT yet been
+   * pre-rewritten.  For example, (ITE true (ITE true x y) z) should
+   * pre-rewrite to x; but if the outer preRewrite() returns
+   * RewriteComplete, the result of the pre-rewrite will be
+   * (ITE true x y).
    */
   virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
     Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8db81902d..47d823009 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -52,19 +52,20 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
 //     }
   }
   else if (fact.getKind() == kind::EQUAL) {
+    // FIXME: kind::IFF as well ?
     // Automatically track all asserted equalities in the shared term manager
     d_engine->getSharedTermManager()->addEq(fact);
   }
   if(! fact.getAttribute(RegisteredAttr())) {
-    std::list<TNode> toReg;
+    list<TNode> toReg;
     toReg.push_back(fact);
 
-    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+    Debug("theory") << "Theory::get(): registering new atom" << endl;
 
     /* Essentially this is doing a breadth-first numbering of
      * non-registered subterms with children.  Any non-registered
      * leaves are immediately registered. */
-    for(std::list<TNode>::iterator workp = toReg.begin();
+    for(list<TNode>::iterator workp = toReg.begin();
         workp != toReg.end();
         ++workp) {
 
@@ -108,7 +109,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
      * and the above registration of leaves, this should ensure that
      * all subterms in the entire tree were registered in
      * reverse-topological order. */
-    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+    for(list<TNode>::reverse_iterator i = toReg.rbegin();
         i != toReg.rend();
         ++i) {
 
@@ -234,6 +235,7 @@ Node TheoryEngine::removeITEs(TNode node) {
   Node cachedRewrite;
   NodeManager *nodeManager = NodeManager::currentNM();
   if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) {
+    Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
     return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
   }
 
@@ -353,6 +355,9 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
   Node noItes = removeITEs(in);
   Node out;
 
+  Debug("theory-rewrite") << "removeITEs of: " << in << endl
+                          << "           is: " << noItes << endl;
+
   // descend top-down into the theory rewriters
   vector<RewriteStackElement> stack;
   stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel));
@@ -523,7 +528,6 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
                rse.d_node.toString().c_str(),
                rewrittenAgain.toString().c_str());
       }
-
       setPostRewriteCache(original, wasTopLevel, rse.d_node);
 
       out = rse.d_node;
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index a480a4d21..f3c16e515 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -21,7 +21,6 @@
 #include "util/congruence_closure.h"
 
 using namespace CVC4;
-using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
@@ -37,7 +36,8 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
   d_disequality(ctxt),
   d_conflict(),
   d_trueNode(),
-  d_falseNode() {
+  d_falseNode(),
+  d_activeAssertions(ctxt) {
   TypeNode boolType = NodeManager::currentNM()->booleanType();
   d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType);
   d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType);
@@ -52,7 +52,8 @@ RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
   if(topLevel) {
     Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
     Node ret(n);
-    if(n.getKind() == EQUAL) {
+    if(n.getKind() == kind::EQUAL ||
+       n.getKind() == kind::IFF) {
       if(n[0] == n[1]) {
         ret = NodeManager::currentNM()->mkConst(true);
       }
@@ -86,7 +87,8 @@ Node TheoryUFMorgan::constructConflict(TNode diseq) {
       nb << *i;
     }
   } else {
-    Assert(explanation.getKind() == kind::EQUAL);
+    Assert(explanation.getKind() == kind::EQUAL ||
+           explanation.getKind() == kind::IFF);
     nb << explanation;
   }
   nb << diseq.notNode();
@@ -121,15 +123,6 @@ TNode TheoryUFMorgan::debugFind(TNode a) const {
   }
 }
 
-void TheoryUFMorgan::unionClasses(TNode a, TNode b) {
-  if(a == b) {
-    return;
-  }
-  Assert(d_unionFind.find(a) == d_unionFind.end());
-  Assert(d_unionFind.find(b) == d_unionFind.end());
-  d_unionFind[a] = b;
-}
-
 void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
   Debug("uf") << "uf: notified of merge " << a << std::endl
               << "                  and " << b << std::endl;
@@ -138,6 +131,12 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
     return;
   }
 
+  merge(a, b);
+}
+
+void TheoryUFMorgan::merge(TNode a, TNode b) {
+  Assert(d_conflict.isNull());
+
   // make "a" the one with shorter diseqList
   DiseqLists::iterator deq_ia = d_disequalities.find(a);
   DiseqLists::iterator deq_ib = d_disequalities.find(b);
@@ -154,7 +153,12 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
   b = find(b);
   Debug("uf") << "uf: uf reps are " << a << std::endl
               << "            and " << b << std::endl;
-  unionClasses(a, b);
+
+  if(a == b) {
+    return;
+  }
+
+  d_unionFind[a] = b;
 
   DiseqLists::iterator deq_i = d_disequalities.find(a);
   if(deq_i != d_disequalities.end()) {
@@ -163,7 +167,7 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
     std::set<TNode> alreadyDiseqs;
     DiseqLists::iterator deq_ib = d_disequalities.find(b);
     if(deq_ib != d_disequalities.end()) {
-      DiseqList* deq = (*deq_i).second;
+      DiseqList* deq = (*deq_ib).second;
       for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
         TNode deqn = *j;
         TNode s = deqn[0];
@@ -185,7 +189,8 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
     for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
       Debug("uf") << "  deq(a) ==> " << *j << std::endl;
       TNode deqn = *j;
-      Assert(deqn.getKind() == kind::EQUAL);
+      Assert(deqn.getKind() == kind::EQUAL ||
+             deqn.getKind() == kind::IFF);
       TNode s = deqn[0];
       TNode t = deqn[1];
       Debug("uf") << "       s  ==> " << s << std::endl
@@ -219,7 +224,8 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
 void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
   Debug("uf") << "appending " << eq << std::endl
               << "  to diseq list of " << of << std::endl;
-  Assert(eq.getKind() == kind::EQUAL);
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
   Assert(of == debugFind(of));
   DiseqLists::iterator deq_i = d_disequalities.find(of);
   DiseqList* deq;
@@ -234,10 +240,11 @@ void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
 }
 
 void TheoryUFMorgan::addDisequality(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL);
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
 
-  Node a = eq[0];
-  Node b = eq[1];
+  TNode a = eq[0];
+  TNode b = eq[1];
 
   appendToDiseqList(find(a), eq);
   appendToDiseqList(find(b), eq);
@@ -249,10 +256,13 @@ void TheoryUFMorgan::check(Effort level) {
   while(!done()) {
     Node assertion = get();
 
+    d_activeAssertions.push_back(assertion);
+
     Debug("uf") << "uf check(): " << assertion << std::endl;
 
     switch(assertion.getKind()) {
-    case EQUAL:
+    case kind::EQUAL:
+    case kind::IFF:
       d_cc.addEquality(assertion);
       if(!d_conflict.isNull()) {
         Node conflict = constructConflict(d_conflict);
@@ -260,18 +270,29 @@ void TheoryUFMorgan::check(Effort level) {
         d_out->conflict(conflict, false);
         return;
       }
+      merge(assertion[0], assertion[1]);
       break;
-    case APPLY_UF:
+    case kind::APPLY_UF:
       { // predicate
-        Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion, d_trueNode);
+
+        // assert it's a predicate
+        Assert(assertion.getOperator().getType().getRangeType().isBoolean());
+
+        Node eq = NodeManager::currentNM()->mkNode(kind::IFF,
+                                                   assertion, d_trueNode);
         d_cc.addTerm(assertion);
         d_cc.addEquality(eq);
-        Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+        Debug("uf") << "true == false ? "
+                    << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+
         Assert(find(d_trueNode) != find(d_falseNode));
+
+        merge(eq[0], eq[1]);
       }
       break;
-    case NOT:
-      if(assertion[0].getKind() == kind::EQUAL) {
+    case kind::NOT:
+      if(assertion[0].getKind() == kind::EQUAL ||
+         assertion[0].getKind() == kind::IFF) {
         Node a = assertion[0][0];
         Node b = assertion[0][1];
 
@@ -311,17 +332,31 @@ void TheoryUFMorgan::check(Effort level) {
         // to this disequality.
         Assert(!d_cc.areCongruent(a, b));
       } else {
+        // negation of a predicate
         Assert(assertion[0].getKind() == kind::APPLY_UF);
-        Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion[0], d_falseNode);
+
+        // assert it's a predicate
+        Assert(assertion[0].getOperator().getType().getRangeType().isBoolean());
+
+        Node eq = NodeManager::currentNM()->mkNode(kind::IFF, assertion[0], d_falseNode);
         d_cc.addTerm(assertion[0]);
         d_cc.addEquality(eq);
-        Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+
+        Debug("uf") << "true == false ? "
+                    << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+
         Assert(find(d_trueNode) != find(d_falseNode));
+
+        merge(eq[0], eq[1]);
       }
       break;
     default:
       Unhandled(assertion.getKind());
     }
+
+    if(Debug.isOn("uf")) {
+      dump();
+    }
   }
   Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl;
 
@@ -346,3 +381,32 @@ void TheoryUFMorgan::propagate(Effort level) {
   Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl;
   Debug("uf") << "uf: end propagate(" << level << ")" << std::endl;
 }
+
+void TheoryUFMorgan::dump() {
+  Debug("uf") << "============== THEORY_UF ==============" << std::endl;
+  Debug("uf") << "Active assertions list:" << std::endl;
+  for(context::CDList<Node>::const_iterator i = d_activeAssertions.begin();
+      i != d_activeAssertions.end();
+      ++i) {
+    Debug("uf") << "    " << *i << std::endl;
+  }
+  Debug("uf") << "Congruence union-find:" << std::endl;
+  for(UnionFind::const_iterator i = d_unionFind.begin();
+      i != d_unionFind.end();
+      ++i) {
+    Debug("uf") << "    " << (*i).first << "  ==>  " << (*i).second << std::endl;
+  }
+  Debug("uf") << "Disequality lists:" << std::endl;
+  for(DiseqLists::const_iterator i = d_disequalities.begin();
+      i != d_disequalities.end();
+      ++i) {
+    Debug("uf") << "    " << (*i).first << ":" << std::endl;
+    DiseqList* dl = (*i).second;
+    for(DiseqList::const_iterator j = dl->begin();
+        j != dl->end();
+        ++j) {
+      Debug("uf") << "        " << *j << std::endl;
+    }
+  }
+  Debug("uf") << "=======================================" << std::endl;
+}
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 1a1ade250..a00e7d15d 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -93,6 +93,8 @@ private:
 
   Node d_trueNode, d_falseNode;
 
+  context::CDList<Node> d_activeAssertions;
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
@@ -165,7 +167,6 @@ private:
 
   TNode find(TNode a);
   TNode debugFind(TNode a) const;
-  void unionClasses(TNode a, TNode b);
 
   void appendToDiseqList(TNode of, TNode eq);
   void addDisequality(TNode eq);
@@ -176,6 +177,15 @@ private:
    */
   void notifyCongruent(TNode a, TNode b);
 
+  /**
+   * Internally handle a congruence, whether generated by the CC
+   * module or from a theory check().  Merges the classes from a and b
+   * and looks for a conflict.  If there is one, sets d_conflict.
+   */
+  void merge(TNode a, TNode b);
+
+  void dump();
+
 };/* class TheoryUFMorgan */
 
 }/* CVC4::theory::uf::morgan namespace */
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index 058f9c193..7d7e26bbe 100644
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -159,8 +159,9 @@ public:
    */
   void addEquality(TNode inputEq) {
     Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl;
-    Assert(inputEq.getKind() == kind::EQUAL);
-    NodeBuilder<> eqb(kind::EQUAL);
+    Assert(inputEq.getKind() == kind::EQUAL ||
+           inputEq.getKind() == kind::IFF);
+    NodeBuilder<> eqb(inputEq.getKind());
     if(inputEq[1].getKind() == kind::APPLY_UF &&
        inputEq[0].getKind() != kind::APPLY_UF) {
       eqb << flatten(inputEq[1]) << inputEq[0];
@@ -190,7 +191,7 @@ public:
       EqMap::iterator i = d_eqMap.find(t);
       if(i == d_eqMap.end()) {
         Node v = NodeManager::currentNM()->mkSkolem(t.getType());
-        addEq(NodeManager::currentNM()->mkNode(kind::EQUAL, t, v), TNode::null());
+        addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null());
         d_eqMap.insert(t, v);
         return v;
       } else {
@@ -272,7 +273,8 @@ public:
    */
   inline Node explain(TNode eq)
     throw(CongruenceClosureException, AssertionException) {
-    Assert(eq.getKind() == kind::EQUAL);
+    Assert(eq.getKind() == kind::EQUAL ||
+           eq.getKind() == kind::IFF);
     return explain(eq[0], eq[1]);
   }
 
@@ -299,7 +301,8 @@ private:
       return TNode::null();
     } else {
       TNode l = (*i).second;
-      Assert(l.getKind() == kind::EQUAL);
+      Assert(l.getKind() == kind::EQUAL ||
+             l.getKind() == kind::IFF);
       return l;
     }
   }
@@ -309,7 +312,8 @@ private:
    */
   inline void setLookup(TNode a, TNode b) {
     Assert(a.getKind() == kind::TUPLE);
-    Assert(b.getKind() == kind::EQUAL);
+    Assert(b.getKind() == kind::EQUAL ||
+           b.getKind() == kind::IFF);
     d_lookup[a] = b;
   }
 
@@ -325,7 +329,8 @@ private:
    */
   inline void appendToUseList(TNode of, TNode eq) {
     Debug("cc") << "adding " << eq << " to use list of " << of << std::endl;
-    Assert(eq.getKind() == kind::EQUAL);
+    Assert(eq.getKind() == kind::EQUAL ||
+           eq.getKind() == kind::IFF);
     Assert(of == find(of));
     UseLists::iterator usei = d_useList.find(of);
     UseList* ul;
@@ -389,7 +394,8 @@ void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
   d_proofRewrite[eq] = inputEq;
 
   Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
-  Assert(eq.getKind() == kind::EQUAL);
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
   Assert(eq[1].getKind() != kind::APPLY_UF);
   if(areCongruent(eq[0], eq[1])) {
     Debug("cc") << "CC -- redundant, ignoring...\n";
@@ -466,7 +472,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
     Debug("cc") << "=== e is " << e << " ===" << std::endl;
 
     TNode a, b;
-    if(e.getKind() == kind::EQUAL) {
+    if(e.getKind() == kind::EQUAL ||
+       e.getKind() == kind::IFF) {
       // e is an equality a = b (a, b are constants)
 
       a = e[0];
@@ -481,8 +488,10 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
       Assert(e.getKind() == kind::TUPLE);
 
       Assert(e.getNumChildren() == 2);
-      Assert(e[0].getKind() == kind::EQUAL);
-      Assert(e[1].getKind() == kind::EQUAL);
+      Assert(e[0].getKind() == kind::EQUAL ||
+             e[0].getKind() == kind::IFF);
+      Assert(e[1].getKind() == kind::EQUAL ||
+             e[1].getKind() == kind::IFF);
 
       // tuple is (eq, lookup)
       a = e[0][1];
@@ -576,7 +585,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
               ++i) {
             TNode eq = *i;
             Debug("cc") << "CC  -- useList: " << eq << std::endl;
-            Assert(eq.getKind() == kind::EQUAL);
+            Assert(eq.getKind() == kind::EQUAL ||
+                   eq.getKind() == kind::IFF);
             // change from paper
             // use list elts can have form (apply c..) = x  OR  x = (apply c..)
             Assert(eq[0].getKind() == kind::APPLY_UF || eq[1].getKind() == kind::APPLY_UF);
@@ -730,7 +740,8 @@ Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
 
     Node theLookup = lookup(ap);
     if(allConstants && !theLookup.isNull()) {
-      Assert(theLookup.getKind() == kind::EQUAL);
+      Assert(theLookup.getKind() == kind::EQUAL ||
+             theLookup.getKind() == kind::IFF);
       Assert(theLookup[0].getKind() == kind::APPLY_UF);
       Assert(theLookup[1].getKind() != kind::APPLY_UF);
       return find(theLookup[1]);
@@ -769,7 +780,8 @@ void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, std::l
   while(a != c) {
     Node b = d_proof[a];
     Node e = d_proofLabel[a];
-    if(e.getKind() == kind::EQUAL) {
+    if(e.getKind() == kind::EQUAL ||
+       e.getKind() == kind::IFF) {
       pf.push_back(e);
     } else {
       Assert(e.getKind() == kind::TUPLE);
@@ -900,6 +912,11 @@ std::ostream& operator<<(std::ostream& out,
     out << "  " << (*i).first << " => " << n << std::endl;
   }
 
+  out << "Care set:" << std::endl;
+  for(typename CongruenceClosure<OutputChannel>::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) {
+    out << "  " << *i << std::endl;
+  }
+
   out << "==============================================" << std::endl;
 
   return out;
diff --git a/src/util/options.h b/src/util/options.h
index c2ac7b225..c79bc93b1 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -71,7 +71,7 @@ struct CVC4_PUBLIC Options {
               err(0),
               verbosity(0),
               lang(parser::LANG_AUTO),
-              uf_implementation(TIM),
+              uf_implementation(MORGAN),
               parseOnly(false),
               semanticChecks(true),
               memoryMap(false),