From 7cc72123f6b422a53c8840ca034cfdb353be59bf Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 11 Mar 2010 18:23:31 +0000 Subject: Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff. --- test/regress/regress0/uf/Makefile.am | 12 ++++++++++++ test/regress/regress0/uf/euf_simp01.smt | 23 +++++++++++++++++++++++ test/regress/regress0/uf/euf_simp02.smt | 29 +++++++++++++++++++++++++++++ test/regress/regress0/uf/euf_simp03.smt | 26 ++++++++++++++++++++++++++ test/regress/regress0/uf/euf_simp04.smt | 25 +++++++++++++++++++++++++ test/regress/regress0/uf/euf_simp05.smt | 11 +++++++++++ test/regress/regress0/uf/euf_simp06.smt | 11 +++++++++++ test/regress/regress0/uf/euf_simp08.smt | 13 +++++++++++++ test/regress/regress0/uf/euf_simp09.smt | 11 +++++++++++ test/regress/regress0/uf/euf_simp10.smt | 12 ++++++++++++ test/regress/regress0/uf/euf_simp11.smt | 17 +++++++++++++++++ test/regress/regress0/uf/euf_simp12.smt | 12 ++++++++++++ test/regress/regress0/uf/euf_simp13.smt | 12 ++++++++++++ 13 files changed, 214 insertions(+) create mode 100644 test/regress/regress0/uf/euf_simp01.smt create mode 100644 test/regress/regress0/uf/euf_simp02.smt create mode 100644 test/regress/regress0/uf/euf_simp03.smt create mode 100644 test/regress/regress0/uf/euf_simp04.smt create mode 100644 test/regress/regress0/uf/euf_simp05.smt create mode 100644 test/regress/regress0/uf/euf_simp06.smt create mode 100644 test/regress/regress0/uf/euf_simp08.smt create mode 100644 test/regress/regress0/uf/euf_simp09.smt create mode 100644 test/regress/regress0/uf/euf_simp10.smt create mode 100644 test/regress/regress0/uf/euf_simp11.smt create mode 100644 test/regress/regress0/uf/euf_simp12.smt create mode 100644 test/regress/regress0/uf/euf_simp13.smt (limited to 'test') 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)))))))))) +) -- cgit v1.2.3