From 29c72e0fd6d0161de275060bbd05370394f1f708 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 18 Aug 2010 03:59:26 +0000 Subject: [PATCH] more tests, configuration for UF --- src/util/options.h | 2 +- test/regress/regress0/uf/Makefile.am | 2 + .../regress0/uf/eq_diamond14.reduced.smt | 88 +++++++++++++++++++ test/regress/regress0/uf/eq_diamond14.smt | 41 +++++++++ 4 files changed, 132 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/uf/eq_diamond14.reduced.smt create mode 100644 test/regress/regress0/uf/eq_diamond14.smt diff --git a/src/util/options.h b/src/util/options.h index c79bc93b1..c2ac7b225 100644 --- 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 452024309..105baad86 100644 --- 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 index 000000000..b41e4536d --- /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 index 000000000..f89d0e3b7 --- /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)))) -- 2.30.2