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.

1 files changed, 9 insertions, 7 deletions

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;
 }