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.

3 files changed, 151 insertions, 0 deletions

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