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/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8db81902d..47d823009 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -52,19 +52,20 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
 //     }
   }
   else if (fact.getKind() == kind::EQUAL) {
+    // FIXME: kind::IFF as well ?
     // Automatically track all asserted equalities in the shared term manager
     d_engine->getSharedTermManager()->addEq(fact);
   }
   if(! fact.getAttribute(RegisteredAttr())) {
-    std::list<TNode> toReg;
+    list<TNode> toReg;
     toReg.push_back(fact);
 
-    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+    Debug("theory") << "Theory::get(): registering new atom" << endl;
 
     /* Essentially this is doing a breadth-first numbering of
      * non-registered subterms with children.  Any non-registered
      * leaves are immediately registered. */
-    for(std::list<TNode>::iterator workp = toReg.begin();
+    for(list<TNode>::iterator workp = toReg.begin();
         workp != toReg.end();
         ++workp) {
 
@@ -108,7 +109,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
      * and the above registration of leaves, this should ensure that
      * all subterms in the entire tree were registered in
      * reverse-topological order. */
-    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+    for(list<TNode>::reverse_iterator i = toReg.rbegin();
         i != toReg.rend();
         ++i) {
 
@@ -234,6 +235,7 @@ Node TheoryEngine::removeITEs(TNode node) {
   Node cachedRewrite;
   NodeManager *nodeManager = NodeManager::currentNM();
   if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) {
+    Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
     return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
   }
 
@@ -353,6 +355,9 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
   Node noItes = removeITEs(in);
   Node out;
 
+  Debug("theory-rewrite") << "removeITEs of: " << in << endl
+                          << "           is: " << noItes << endl;
+
   // descend top-down into the theory rewriters
   vector<RewriteStackElement> stack;
   stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel));
@@ -523,7 +528,6 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) {
                rse.d_node.toString().c_str(),
                rewrittenAgain.toString().c_str());
       }
-
       setPostRewriteCache(original, wasTopLevel, rse.d_node);
 
       out = rse.d_node;