From ad24cbdb3462b2b2dd312aab2f1f33d9bbcac00e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 19 Aug 2010 23:49:58 +0000 Subject: 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. --- test/regress/regress0/uf/Makefile.am | 1 + test/regress/regress0/uf/eq_diamond14.reduced.smt | 1 - test/regress/regress0/uf/eq_diamond14.reduced2.smt | 102 +++++++++++++++++++++ test/regress/regress0/uf/pred.smt | 18 ++++ 4 files changed, 121 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/uf/eq_diamond14.reduced2.smt create mode 100644 test/regress/regress0/uf/pred.smt (limited to 'test/regress/regress0') 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)) +) +) -- cgit v1.2.3