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.

2 files changed, 103 insertions, 29 deletions

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 */