more tests, configuration for UF

diff --git a/src/util/options.h b/src/util/options.h
index c79bc93b1f2bcbc93108e5c4984a4de41bf4b943..c2ac7b2252c95f4c7618e857b713cdae5d981295 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -71,7 +71,7 @@ struct CVC4_PUBLIC Options {
               err(0),
               verbosity(0),
               lang(parser::LANG_AUTO),
-              uf_implementation(MORGAN),
+              uf_implementation(TIM),
               parseOnly(false),
               semanticChecks(true),
               memoryMap(false),

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 452024309468cca19f2877b6c413672576c17b26..105baad8639346e156c3be66bc5c8a4a43a904dd 100644 (file)
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -17,6 +17,8 @@ TESTS =       \
        euf_simp12.smt \
        euf_simp13.smt \
        eq_diamond1.smt \
+       eq_diamond14.smt \
+       eq_diamond14.reduced.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
new file mode 100644 (file)
index 0000000..b41e453
--- /dev/null
+++ b/test/regress/regress0/uf/eq_diamond14.reduced.smt
@@ -0,0 +1,88 @@
+(benchmark eq_diamond14_reduced
+:logic QF_UF
+:source { Reduced by delta debugger from eq_diamond14 to fix a UF bug. }
+:status unsat
+:extrasorts (V)
+:extrafuns ((x13 V))
+:extrafuns ((x0 V))
+:extrafuns ((y12 V))
+:extrafuns ((x12 V))
+:extrafuns ((z11 V))
+:extrafuns ((x11 V))
+:extrafuns ((y11 V))
+:extrafuns ((z10 V))
+:extrafuns ((x10 V))
+:extrafuns ((y10 V))
+:extrafuns ((y9 V))
+:extrafuns ((x9 V))
+:extrafuns ((y8 V))
+:extrafuns ((x8 V))
+:extrafuns ((y7 V))
+:extrafuns ((x7 V))
+:extrafuns ((y6 V))
+:extrafuns ((x6 V))
+:extrafuns ((y5 V))
+:extrafuns ((x5 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 unknown
+: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 (= x5 y5))
+(flet ($n17 (= y5 x6))
+(flet ($n18 (and $n16 $n17))
+(flet ($n19 (= x6 y6))
+(flet ($n20 (= y6 x7))
+(flet ($n21 (and $n19 $n20))
+(flet ($n22 (= x7 y7))
+(flet ($n23 (= y7 x8))
+(flet ($n24 (and $n22 $n23))
+(flet ($n25 (= x8 y8))
+(flet ($n26 (= y8 x9))
+(flet ($n27 (and $n25 $n26))
+(flet ($n28 (= x9 y9))
+(flet ($n29 (= y9 x10))
+(flet ($n30 (and $n28 $n29))
+(flet ($n31 false)
+(flet ($n32 (= y10 x11))
+(flet ($n33 (and $n31 $n32))
+(flet ($n34 (= x10 z10))
+(flet ($n35 (= x11 z10))
+(flet ($n36 (and $n34 $n35))
+(flet ($n37 (or $n33 $n36))
+(flet ($n38 (= x11 y11))
+(flet ($n39 (= y11 x12))
+(flet ($n40 (and $n38 $n39))
+(flet ($n41 (= x11 z11))
+(flet ($n42 (= x12 z11))
+(flet ($n43 (and $n41 $n42))
+(flet ($n44 (or $n40 $n43))
+(flet ($n45 (= x12 y12))
+(flet ($n46 (= y12 x13))
+(flet ($n47 (and $n45 $n46))
+(flet ($n48 (= x0 x13))
+(flet ($n49 (not $n48))
+(flet ($n50 (and $n3 $n6 $n9 $n12 $n15 $n18 $n21 $n24 $n27 $n30 $n37 $n44 $n47 $n49))
+$n50
+)))))))))))))))))))))))))))))))))))))))))))))))))))

diff --git a/test/regress/regress0/uf/eq_diamond14.smt b/test/regress/regress0/uf/eq_diamond14.smt
new file mode 100644 (file)
index 0000000..f89d0e3
--- /dev/null
+++ b/test/regress/regress0/uf/eq_diamond14.smt
@@ -0,0 +1,41 @@
+(benchmark eq_diamond14
+:source{
+Generating minimum transitivity constraints in P-time for deciding Equality Logic,
+Ofer Strichman and Mirron Rozanov,
+SMT Workshop 2005.
+
+Translator: Leonardo de Moura. }
+:status unsat
+:category { crafted }
+:logic QF_UF
+:difficulty { 0 }
+:extrafuns ((x0 U) (y0 U) (z0 U)
+(x1 U) (y1 U) (z1 U)
+(x2 U) (y2 U) (z2 U)
+(x3 U) (y3 U) (z3 U)
+(x4 U) (y4 U) (z4 U)
+(x5 U) (y5 U) (z5 U)
+(x6 U) (y6 U) (z6 U)
+(x7 U) (y7 U) (z7 U)
+(x8 U) (y8 U) (z8 U)
+(x9 U) (y9 U) (z9 U)
+(x10 U) (y10 U) (z10 U)
+(x11 U) (y11 U) (z11 U)
+(x12 U) (y12 U) (z12 U)
+(x13 U) (y13 U) (z13 U)
+)
+:formula (and 
+(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
+(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
+(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
+(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
+(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
+(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
+(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
+(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
+(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
+(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
+(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
+(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
+(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
+(not (= x0 x13))))