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, 13 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 64a3b8f06..1cce09439 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -313,6 +313,19 @@ public:
    * rewrite a term to a strictly larger term that contains itself, as
    * this will cause a loop of hard Node links in the cache (and thus
    * memory leakage).
+   *
+   * Be careful with the return value.  If a preRewrite() can return a
+   * sub-expression, and that sub-expression can be a member of the
+   * same theory and could be rewritten, make sure to return
+   * RewriteAgain instead of RewriteComplete.  This is an easy mistake
+   * to make, as preRewrite() is often a short-circuiting version of
+   * the same rewrites that occur in postRewrite(); however, in the
+   * postRewrite() case, the subexpressions have all been
+   * post-rewritten.  In the preRewrite() case, they have NOT yet been
+   * pre-rewritten.  For example, (ITE true (ITE true x y) z) should
+   * pre-rewrite to x; but if the outer preRewrite() returns
+   * RewriteComplete, the result of the pre-rewrite will be
+   * (ITE true x y).
    */
   virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
     Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;