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, 4 insertions, 2 deletions

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 0028aaad5..5d8e88db0 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -61,7 +61,8 @@ Context::~Context() throw(AssertionException) {
 
 
 void Context::push() {
-  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl;
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
+                   << getLevel() + 1 << "] {" << std::endl;
 
   // Create a new memory region
   d_pCMM->push();
@@ -100,7 +101,8 @@ void Context::pop() {
     pCNO = pCNO->d_pCNOnext;
   }
 
-  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl;
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
+                   << getLevel() << "]" << std::endl;
 }