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.

4 files changed, 121 insertions, 1 deletions

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 105baad86..f5c97241e 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -19,6 +19,7 @@ TESTS =	\
 	eq_diamond1.smt \
 	eq_diamond14.smt \
 	eq_diamond14.reduced.smt \
+	eq_diamond14.reduced2.smt \
 	dead_dnd002.smt \
 	iso_brn001.smt \
 	simple.01.cvc \
diff --git a/test/regress/regress0/uf/eq_diamond14.reduced.smt b/test/regress/regress0/uf/eq_diamond14.reduced.smt
index b41e4536d..6af6ac5be 100644
--- a/test/regress/regress0/uf/eq_diamond14.reduced.smt
+++ b/test/regress/regress0/uf/eq_diamond14.reduced.smt
@@ -32,7 +32,6 @@
 :extrafuns ((y1 V))
 :extrafuns ((x1 V))
 :extrafuns ((y0 V))
-:status unknown
 :formula
 (flet ($n1 (= x0 y0))
 (flet ($n2 (= y0 x1))
diff --git a/test/regress/regress0/uf/eq_diamond14.reduced2.smt b/test/regress/regress0/uf/eq_diamond14.reduced2.smt
new file mode 100644
index 000000000..019a935c4
--- /dev/null
+++ b/test/regress/regress0/uf/eq_diamond14.reduced2.smt
@@ -0,0 +1,102 @@
+(benchmark eq_diamond14
+:logic QF_UF
+:extrasorts (V)
+:extrafuns ((z9 V))
+:extrafuns ((x10 V))
+:extrafuns ((x9 V))
+:extrafuns ((x13 V))
+:extrafuns ((x0 V))
+:extrafuns ((z12 V))
+:extrafuns ((x12 V))
+:extrafuns ((y12 V))
+:extrafuns ((z11 V))
+:extrafuns ((x11 V))
+:extrafuns ((y11 V))
+:extrafuns ((z10 V))
+:extrafuns ((y10 V))
+:extrafuns ((y8 V))
+:extrafuns ((x8 V))
+:extrafuns ((y7 V))
+:extrafuns ((x7 V))
+:extrafuns ((z6 V))
+:extrafuns ((x6 V))
+:extrafuns ((y6 V))
+:extrafuns ((z5 V))
+:extrafuns ((x5 V))
+:extrafuns ((y5 V))
+:extrafuns ((y4 V))
+:extrafuns ((x4 V))
+:extrafuns ((y3 V))
+:extrafuns ((x3 V))
+:extrafuns ((y2 V))
+:extrafuns ((x2 V))
+:extrafuns ((y1 V))
+:extrafuns ((x1 V))
+:extrafuns ((y0 V))
+:status unsat
+:formula
+(flet ($n1 (= x0 y0))
+(flet ($n2 (= y0 x1))
+(flet ($n3 (and $n1 $n2))
+(flet ($n4 (= x1 y1))
+(flet ($n5 (= y1 x2))
+(flet ($n6 (and $n4 $n5))
+(flet ($n7 (= x2 y2))
+(flet ($n8 (= y2 x3))
+(flet ($n9 (and $n7 $n8))
+(flet ($n10 (= x3 y3))
+(flet ($n11 (= y3 x4))
+(flet ($n12 (and $n10 $n11))
+(flet ($n13 (= x4 y4))
+(flet ($n14 (= y4 x5))
+(flet ($n15 (and $n13 $n14))
+(flet ($n16 false)
+(flet ($n17 (= y5 x6))
+(flet ($n18 (and $n16 $n17))
+(flet ($n19 (= x5 z5))
+(flet ($n20 (= x6 z5))
+(flet ($n21 (and $n19 $n20))
+(flet ($n22 (or $n18 $n21))
+(flet ($n23 (= x6 y6))
+(flet ($n24 (= y6 x7))
+(flet ($n25 (and $n23 $n24))
+(flet ($n26 (= x6 z6))
+(flet ($n27 (= x7 z6))
+(flet ($n28 (and $n26 $n27))
+(flet ($n29 (or $n25 $n28))
+(flet ($n30 (= x7 y7))
+(flet ($n31 (= y7 x8))
+(flet ($n32 (and $n30 $n31))
+(flet ($n33 (= x8 y8))
+(flet ($n34 (= y8 x9))
+(flet ($n35 (and $n33 $n34))
+(flet ($n36 (= x10 y10))
+(flet ($n37 (= y10 x11))
+(flet ($n38 (and $n36 $n37))
+(flet ($n39 (= x10 z10))
+(flet ($n40 (= x11 z10))
+(flet ($n41 (and $n39 $n40))
+(flet ($n42 (or $n38 $n41))
+(flet ($n43 (= x11 y11))
+(flet ($n44 (= y11 x12))
+(flet ($n45 (and $n43 $n44))
+(flet ($n46 (= x11 z11))
+(flet ($n47 (= x12 z11))
+(flet ($n48 (and $n46 $n47))
+(flet ($n49 (or $n45 $n48))
+(flet ($n50 (= x12 y12))
+(flet ($n51 (= y12 x13))
+(flet ($n52 (and $n50 $n51))
+(flet ($n53 (= x12 z12))
+(flet ($n54 (= x13 z12))
+(flet ($n55 (and $n53 $n54))
+(flet ($n56 (or $n52 $n55))
+(flet ($n57 (= x0 x13))
+(flet ($n58 (not $n57))
+(flet ($n59 (= x9 z9))
+(flet ($n60 (= x10 z9))
+(flet ($n61 (and $n59 $n60))
+(flet ($n62 (or $n16 $n61))
+(flet ($n63 (and $n3 $n6 $n9 $n12 $n15 $n22 $n29 $n32 $n35 $n42 $n49 $n56 $n58 $n62))
+$n63
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/uf/pred.smt b/test/regress/regress0/uf/pred.smt
new file mode 100644
index 000000000..e6f82727e
--- /dev/null
+++ b/test/regress/regress0/uf/pred.smt
@@ -0,0 +1,18 @@
+(benchmark euf_simp1.smt
+:status sat
+:logic QF_UF
+:category { crafted }
+
+:extrafuns ((x U))
+:extrafuns ((y U))
+:extrapreds ((f U))
+
+
+
+:formula
+(and
+ (f x)
+ (iff (f x) (f y))
+ (not (f y))
+)
+)