diff options
author | Tim King <taking@cs.nyu.edu> | 2010-03-11 18:23:31 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-03-11 18:23:31 +0000 |
commit | 7cc72123f6b422a53c8840ca034cfdb353be59bf (patch) | |
tree | c37856ffb16ae071b1ee09416381fc86dc0acb9a /test/regress/regress0 | |
parent | c7ccddcad95d7b6534a83a873c522b115530a553 (diff) |
Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 12 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp01.smt | 23 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp02.smt | 29 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp03.smt | 26 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp04.smt | 25 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp05.smt | 11 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp06.smt | 11 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp08.smt | 13 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp09.smt | 11 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp10.smt | 12 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp11.smt | 17 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp12.smt | 12 | ||||
-rw-r--r-- | test/regress/regress0/uf/euf_simp13.smt | 12 |
13 files changed, 214 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index a4e08ff99..b456f2809 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -3,6 +3,18 @@ TESTS = simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ simple.04.cvc \ + euf_simp01.smt \ + euf_simp02.smt \ + euf_simp03.smt \ + euf_simp04.smt \ + euf_simp05.smt \ + euf_simp06.smt \ + euf_simp08.smt \ + euf_simp09.smt \ + euf_simp10.smt \ + euf_simp11.smt \ + euf_simp12.smt \ + euf_simp13.smt \ dead_dnd002.smt \ iso_brn001.smt \ SEQ032_size2.smt diff --git a/test/regress/regress0/uf/euf_simp01.smt b/test/regress/regress0/uf/euf_simp01.smt new file mode 100644 index 000000000..c121ae82e --- /dev/null +++ b/test/regress/regress0/uf/euf_simp01.smt @@ -0,0 +1,23 @@ + +(benchmark euf_simp1.smt +:status sat +:logic QF_UF +:category { crafted } + +:extrafuns ((x U)) +:extrafuns ((y U)) +:extrafuns ((z U)) +:extrafuns ((f U U)) +:extrafuns ((g U U)) +:extrafuns ((H U U U)) +:extrafuns ((J U U U)) + + + +:formula +(and + (= (f x) (f z)) + (= (g y) (g z)) + (or (not (= x z)) (not (= y z))) + ) +)
\ No newline at end of file diff --git a/test/regress/regress0/uf/euf_simp02.smt b/test/regress/regress0/uf/euf_simp02.smt new file mode 100644 index 000000000..9c7b03f6e --- /dev/null +++ b/test/regress/regress0/uf/euf_simp02.smt @@ -0,0 +1,29 @@ + +(benchmark euf_simp2.smt +:status unsat +:logic QF_UF +:category { crafted } + +:extrafuns ((x U)) +:extrafuns ((y U)) +:extrafuns ((z U)) +:extrafuns ((f U U)) +:extrafuns ((g U U)) +:extrafuns ((H U U U)) +:extrafuns ((J U U U)) + + + +:formula +(and + (not (= x y)) + (= (f x) (f z)) + (= (g y) (g z)) + (= (g y) (g z)) + (= (g y) y) + (= (f x) x) + (= (f z) z) + (= (g z) z) + (or (not (= x z)) (not (= y z))) + ) +)
\ No newline at end of file diff --git a/test/regress/regress0/uf/euf_simp03.smt b/test/regress/regress0/uf/euf_simp03.smt new file mode 100644 index 000000000..e0d6cc849 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp03.smt @@ -0,0 +1,26 @@ + +(benchmark euf_simp3.smt +:status unsat +:logic QF_UF +:category { crafted } + +:extrafuns ((x U)) +:extrafuns ((y U)) +:extrafuns ((z U)) +:extrafuns ((f U U)) +:extrafuns ((g U U)) +:extrafuns ((H U U U)) +:extrafuns ((J U U U)) + + + +:formula +(and + (not (= x y)) + (= (f (f x)) (f (f (f x)))) + (= (f (f x)) y) + (= (f (f (f (f x)))) z) + (= (f x) z) + (not (= (f x) y)) + ) +)
\ No newline at end of file diff --git a/test/regress/regress0/uf/euf_simp04.smt b/test/regress/regress0/uf/euf_simp04.smt new file mode 100644 index 000000000..7b15ad309 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp04.smt @@ -0,0 +1,25 @@ + +(benchmark euf_simp4.smt +:status unsat +:logic QF_UF +:category { crafted } + +:extrafuns ((x U)) +:extrafuns ((y U)) +:extrafuns ((z U)) +:extrafuns ((f U U)) +:extrafuns ((g U U)) +:extrafuns ((H U U U)) +:extrafuns ((J U U U)) + + + +:formula +(and + (= (H x y) (H y x)) + (or (= x (J z y)) (= y (J z y))) + (= (J z y) (f x)) + (or (= x (f x)) (not (= y (f x))) ) + (or (not (= x (f x))) (not (= (H x (f x)) (H (f x) x) )) ) + ) +)
\ No newline at end of file diff --git a/test/regress/regress0/uf/euf_simp05.smt b/test/regress/regress0/uf/euf_simp05.smt new file mode 100644 index 000000000..85089a92a --- /dev/null +++ b/test/regress/regress0/uf/euf_simp05.smt @@ -0,0 +1,11 @@ +(benchmark euf_simp5.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f ?cvc_1)) (not (implies (and (= ?cvc_0 x) (= (f ?cvc_0) x)) (= ?cvc_1 x))))) +) diff --git a/test/regress/regress0/uf/euf_simp06.smt b/test/regress/regress0/uf/euf_simp06.smt new file mode 100644 index 000000000..020bafdff --- /dev/null +++ b/test/regress/regress0/uf/euf_simp06.smt @@ -0,0 +1,11 @@ +(benchmark euf_simp6.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f ?cvc_1)) (not (implies (and (= ?cvc_0 x) (= (f (f (f ?cvc_0))) x)) (= ?cvc_1 x))))) +) diff --git a/test/regress/regress0/uf/euf_simp08.smt b/test/regress/regress0/uf/euf_simp08.smt new file mode 100644 index 000000000..0a89fe96a --- /dev/null +++ b/test/regress/regress0/uf/euf_simp08.smt @@ -0,0 +1,13 @@ +(benchmark euf_simp8.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + + :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) ?cvc_0)) (= ?cvc_1 x))))) + +) diff --git a/test/regress/regress0/uf/euf_simp09.smt b/test/regress/regress0/uf/euf_simp09.smt new file mode 100644 index 000000000..69ec0fff4 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp09.smt @@ -0,0 +1,11 @@ +(benchmark euf_simp9.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + :formula (let (?cvc_1 (f (f x))) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) x)) (= ?cvc_1 x))))) +) diff --git a/test/regress/regress0/uf/euf_simp10.smt b/test/regress/regress0/uf/euf_simp10.smt new file mode 100644 index 000000000..1b4b05854 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp10.smt @@ -0,0 +1,12 @@ +(benchmark euf_simp10.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + + :formula (let (?cvc_0 (f x)) (let (?cvc_1 (f (f ?cvc_0))) (flet ($cvc_2 (= ?cvc_1 ?cvc_0)) (not (implies (and $cvc_2 (= (f (f ?cvc_1)) ?cvc_0)) $cvc_2))))) +) diff --git a/test/regress/regress0/uf/euf_simp11.smt b/test/regress/regress0/uf/euf_simp11.smt new file mode 100644 index 000000000..164bd47e5 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp11.smt @@ -0,0 +1,17 @@ +(benchmark euf_simp11.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + + + + + + + :formula (let (?cvc_0 (f x)) (let (?cvc_2 (f ?cvc_0)) (let (?cvc_1 (f (f ?cvc_2))) (not (implies (and (= ?cvc_1 ?cvc_0) (= (f (f ?cvc_1)) ?cvc_0)) (= ?cvc_2 ?cvc_0)))))) +) diff --git a/test/regress/regress0/uf/euf_simp12.smt b/test/regress/regress0/uf/euf_simp12.smt new file mode 100644 index 000000000..aff94fff3 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp12.smt @@ -0,0 +1,12 @@ +(benchmark euf_simp12.smt + + :status unsat + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + + :formula (let (?cvc_0 (f (f x))) (let (?cvc_2 (f ?cvc_0)) (let (?cvc_3 (f ?cvc_2)) (let (?cvc_1 (f ?cvc_3)) (let (?cvc_4 (f ?cvc_1)) (not (implies (and (= ?cvc_4 ?cvc_0) (= ?cvc_1 ?cvc_2)) (and (= ?cvc_3 ?cvc_0) (= ?cvc_4 ?cvc_3))))))))) + +) diff --git a/test/regress/regress0/uf/euf_simp13.smt b/test/regress/regress0/uf/euf_simp13.smt new file mode 100644 index 000000000..7e7abb8f9 --- /dev/null +++ b/test/regress/regress0/uf/euf_simp13.smt @@ -0,0 +1,12 @@ +(benchmark euf_simp13.smt + + :status unsat + :difficulty { unknown } + :category { crafted } + :logic QF_UF + :extrasorts (A) + :extrafuns ((x A)) + :extrafuns ((f A A)) + :formula + (let (?cvc_6 (f x)) (let (?cvc_0 (f ?cvc_6)) (flet ($cvc_1 (= ?cvc_0 x)) (let (?cvc_2 (f ?cvc_0)) (flet ($cvc_3 (= ?cvc_2 x)) (let (?cvc_4 (f ?cvc_2)) (let (?cvc_5 (f ?cvc_4)) (not (implies (or (or (or (and $cvc_1 $cvc_3) (and $cvc_1 (= ?cvc_5 x))) (and $cvc_3 (= ?cvc_4 ?cvc_2))) (and $cvc_3 (= ?cvc_5 ?cvc_2))) (= ?cvc_6 x)))))))))) +) |