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, 5 deletions

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