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, 21 insertions, 8 deletions

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){