diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p | 56 | ||||
-rw-r--r-- | test/regress/regress0/ho/fta0210.smt2 | 64 | ||||
-rw-r--r-- | test/regress/regress0/ho/ho-exponential-model.smt2 | 40 | ||||
-rw-r--r-- | test/regress/regress0/ho/ho-matching-enum-2.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/ho/ho-std-fmf.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/ho/hoa0008.smt2 | 68 | ||||
-rw-r--r-- | test/regress/regress0/ho/match-middle.smt2 | 20 |
7 files changed, 284 insertions, 0 deletions
diff --git a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p new file mode 100644 index 000000000..0ed7fe44b --- /dev/null +++ b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p @@ -0,0 +1,56 @@ +% COMMAND-LINE: --uf-ho +% EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1 + +%------------------------------------------------------------------------------ +% File : SYO042^1 : TPTP v7.2.0. Released v4.0.0. +% Domain : Syntactic +% Problem : Unsatisfiable basic formula 4 +% Version : Especial. +% English : + +% Refs : [BS09a] Brown E. & Smolka (2009), Terminating Tableaux for the +% : [BS09b] Brown E. & Smolka (2009), Extended First-Order Logic +% Source : [BS09a] +% Names : + +% Status : Unsatisfiable +% Rating : 0.00 v5.4.0, 0.33 v5.3.0, 0.67 v5.0.0, 0.33 v4.1.0, 0.67 v4.0.1, 1.00 v4.0.0 +% Syntax : Number of formulae : 5 ( 0 unit; 4 type; 0 defn) +% Number of atoms : 15 ( 3 equality; 0 variable) +% Maximal formula depth : 7 ( 4 average) +% Number of connectives : 10 ( 2 ~; 0 |; 4 &; 4 @) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<) +% Number of symbols : 6 ( 4 :; 0 =) +% Number of variables : 0 ( 0 sgn; 0 !; 0 ?; 0 ^) +% ( 0 :; 0 !>; 0 ?*) +% ( 0 @-; 0 @+) +% SPC : TH0_UNS_EQU_NAR + +% Comments : The fragment of simple type theory that restricts equations to +% base types and disallows lambda abstraction and quantification is +% decidable. This is an example. +%------------------------------------------------------------------------------ +thf(g,type,( + g: $o > $o )). + +thf(p,type,( + p: ( $o > $o ) > $o )). + +thf(x,type,( + x: $o )). + +thf(y,type,( + y: $o )). + +thf(4,axiom, + ( ( x != y ) + & ( ( g @ x ) + = y ) + & ( ( g @ y ) + = x ) + & ( p @ g ) + & ~ ( p @ (~) ) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2 new file mode 100644 index 000000000..9f0a39f25 --- /dev/null +++ b/test/regress/regress0/ho/fta0210.smt2 @@ -0,0 +1,64 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(declare-sort A$ 0) +(declare-sort Nat$ 0) +(declare-sort A_poly$ 0) +(declare-sort Nat_poly$ 0) +(declare-sort A_poly_poly$ 0) +(declare-fun p$ () A_poly$) +(declare-fun uu$ (A_poly$ (-> A_poly$ A_poly$) A_poly$) A_poly$) +(declare-fun one$ () Nat$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun uua$ (A_poly$) A_poly$) +(declare-fun uub$ (A$ (-> A$ A$) A$) A$) +(declare-fun uuc$ (A$) A$) +(declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$) +(declare-fun uue$ (Nat$) Nat$) +(declare-fun one$a () Nat_poly$) +(declare-fun one$b () A$) +(declare-fun one$c () A_poly$) +(declare-fun plus$ (A_poly$ A_poly$) A_poly$) +(declare-fun poly$ (A_poly$ A$) A$) +(declare-fun zero$ () A_poly$) +(declare-fun pCons$ (A$ A_poly$) A_poly$) +(declare-fun plus$a (Nat$ Nat$) Nat$) +(declare-fun plus$b (A$ A$) A$) +(declare-fun plus$c (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun poly$a (Nat_poly$ Nat$) Nat$) +(declare-fun poly$b (A_poly_poly$ A_poly$) A_poly$) +(declare-fun power$ (A$ Nat$) A$) +(declare-fun psize$ (A_poly$) Nat$) +(declare-fun times$ (A_poly$ A_poly$) A_poly$) +(declare-fun zero$a () Nat$) +(declare-fun zero$b () A$) +(declare-fun zero$c () Nat_poly$) +(declare-fun zero$d () A_poly_poly$) +(declare-fun pCons$a (Nat$ Nat_poly$) Nat_poly$) +(declare-fun pCons$b (A_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun power$a (A_poly$ Nat$) A_poly$) +(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$) +(declare-fun power$c (Nat$ Nat$) Nat$) +(declare-fun psize$a (A_poly_poly$) Nat$) +(declare-fun times$a (Nat$ Nat$) Nat$) +(declare-fun times$b (A$ A$) A$) +(declare-fun times$c (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun times$d (A_poly_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun uminus$ (A_poly$) A_poly$) +(declare-fun uminus$a (A$) A$) +(declare-fun constant$ ((-> A$ A$)) Bool) +(declare-fun pcompose$ (A_poly$ A_poly$) A_poly$) +(declare-fun pcompose$a (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun pcompose$b (A_poly_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun poly_shift$ (Nat$ A_poly$) A_poly$) +(declare-fun fold_coeffs$ ((-> A_poly$ (-> (-> A_poly$ A_poly$) (-> A_poly$ A_poly$))) A_poly_poly$ (-> A_poly$ A_poly$)) (-> A_poly$ A_poly$)) +(declare-fun poly_cutoff$ (Nat$ A_poly$) A_poly$) +(declare-fun fold_coeffs$a ((-> A$ (-> (-> A$ A$) (-> A$ A$))) A_poly$ (-> A$ A$)) (-> A$ A$)) +(declare-fun fold_coeffs$b ((-> Nat$ (-> (-> Nat$ Nat$) (-> Nat$ Nat$))) Nat_poly$ (-> Nat$ Nat$)) (-> Nat$ Nat$)) + +(assert (! (forall ((?v0 A$)) (= (poly$ zero$ ?v0) zero$b)) :named a14)) +(assert (! (forall ((?v0 (-> A$ A$))) (= (constant$ ?v0) (forall ((?v1 A$) (?v2 A$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a69)) +(assert (! (not (constant$ (poly$ zero$))) :named a206)) + +(check-sat) +;(get-proof) diff --git a/test/regress/regress0/ho/ho-exponential-model.smt2 b/test/regress/regress0/ho/ho-exponential-model.smt2 new file mode 100644 index 000000000..3f0011828 --- /dev/null +++ b/test/regress/regress0/ho/ho-exponential-model.smt2 @@ -0,0 +1,40 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(declare-fun f1 (Int Int Int Int) Int) +(declare-fun f2 (Int Int Int) Int) +(declare-fun f3 (Int Int) Int) +(declare-fun f4 (Int) Int) +(declare-fun f5 (Int Int Int) Int) +(declare-fun f6 (Int Int) Int) +(declare-fun f7 (Int) Int) + + +(assert (= (f1 0) (f1 1))) +(assert (= (f1 1) f2)) + +(assert (= (f2 0) (f2 1))) +(assert (= (f2 1) f3)) + +(assert (= (f3 0) (f3 1))) +(assert (= (f3 1) f4)) + +(assert (= (f4 0) (f4 1))) +(assert (= (f4 1) 2)) + + +(assert (= (f1 3) (f1 4))) +(assert (= (f1 4) f5)) + +(assert (= (f5 3) (f5 4))) +(assert (= (f5 4) f6)) + +(assert (= (f6 3) (f6 4))) +(assert (= (f6 4) f7)) + +(assert (= (f7 3) (f7 4))) +(assert (= (f7 4) 5)) + +; this benchmark has a concise model representation for f1 if we use curried (tree-like) models for UF +(check-sat) diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2 new file mode 100644 index 000000000..9581e4c4f --- /dev/null +++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun p (Int) Bool) +(declare-fun q (Int) Bool) +(declare-fun k (Int Int) Int) + +(assert (q (k 0 1))) +(assert (not (p (k 0 0)))) + +(assert (forall ((f (-> Int Int Int)) (y Int) (z Int)) (or (p (f y z)) (not (q (f z y)))))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/ho/ho-std-fmf.smt2 b/test/regress/regress0/ho/ho-std-fmf.smt2 new file mode 100644 index 000000000..61d82d00c --- /dev/null +++ b/test/regress/regress0/ho/ho-std-fmf.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --uf-ho --finite-model-find +; EXPECT: sat +(set-logic UF) +(set-info :status sat) +(declare-sort U 0) +(declare-fun P (U U) Bool) +(declare-fun Q (U U) Bool) +(declare-fun R (U U) Bool) +(declare-fun a () U) +(declare-fun b () U) + +; can solve this using standard MBQI model for P = \ xy true +(assert (forall ((x U) (y U)) (or (P x y) (Q x y)))) +(assert (forall ((x U) (y U)) (or (P x y) (R x y)))) + +(assert (not (= a b))) +(assert (= (Q a) (R b))) +(check-sat) diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2 new file mode 100644 index 000000000..f4833aadf --- /dev/null +++ b/test/regress/regress0/ho/hoa0008.smt2 @@ -0,0 +1,68 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(declare-sort A$ 0) +(declare-sort Com$ 0) +(declare-sort Loc$ 0) +(declare-sort Nat$ 0) +(declare-sort Pname$ 0) +(declare-sort State$ 0) +(declare-sort Vname$ 0) +(declare-sort Literal$ 0) +(declare-sort Natural$ 0) +(declare-sort Typerep$ 0) +(declare-sort A_triple$ 0) +(declare-sort Com_option$ 0) +(declare-fun p$ () (-> A$ (-> State$ Bool))) +(declare-fun q$ () (-> A$ (-> State$ Bool))) +(declare-fun pn$ () Pname$) +(declare-fun wt$ (Com$) Bool) +(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun the$ (Com_option$) Com$) +(declare-fun body$ (Pname$) Com$) +(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$) +(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$) +(declare-fun none$ () Com_option$) +(declare-fun plus$ (Nat$ Nat$) Nat$) +(declare-fun semi$ (Com$ Com$) Com$) +(declare-fun size$ (A_triple$) Nat$) +(declare-fun skip$ () Com$) +(declare-fun some$ (Com$) Com_option$) +(declare-fun suc$a (Natural$) Natural$) +(declare-fun zero$ () Nat$) +(declare-fun body$a (Pname$) Com_option$) +(declare-fun evalc$ (Com$ State$ State$) Bool) +(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool) +(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$) +(declare-fun plus$a (Natural$ Natural$) Natural$) +(declare-fun size$a (Com$) Nat$) +(declare-fun size$b (Natural$) Nat$) +(declare-fun size$c (Bool) Nat$) +(declare-fun size$d (Com_option$) Nat$) +(declare-fun size$e (Typerep$) Nat$) +(declare-fun size$f (Literal$) Nat$) +(declare-fun while$ ((-> State$ Bool) Com$) Com$) +(declare-fun zero$a () Natural$) +(declare-fun triple$ ((-> A$ (-> State$ Bool)) Com$ (-> A$ (-> State$ Bool))) A_triple$) +(declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$)) +(declare-fun size_com$ (Com$) Nat$) +(declare-fun size_bool$ (Bool) Nat$) +(declare-fun wT_bodies$ () Bool) +(declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$)) +(declare-fun size_triple$ ((-> A$ Nat$) A_triple$) Nat$) +(declare-fun size_natural$ (Natural$) Nat$) +(declare-fun triple_valid$ (Nat$ A_triple$) Bool) +(assert (! (not (triple_valid$ zero$ (triple$ p$ (body$ pn$) q$))) :named a0)) + +(assert (! (forall ((?v0 Nat$) (?v1 (-> A$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> A$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 A$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a6)) + +(assert (! (= (size_bool$ true) zero$) :named a13)) +(assert (! (= size_bool$ (rec_bool$ zero$ zero$)) :named a14)) + +(assert (! (forall ((?v0 Nat$)) (not (= zero$ (suc$ ?v0)))) :named a37)) + +(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$ ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$a ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a204)) + +(check-sat) +;(get-proof) diff --git a/test/regress/regress0/ho/match-middle.smt2 b/test/regress/regress0/ho/match-middle.smt2 new file mode 100644 index 000000000..0485f9a6f --- /dev/null +++ b/test/regress/regress0/ho/match-middle.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun f (Int Int Int) Int) +(declare-fun h (Int Int Int) Int) +(declare-fun g (Int Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) + +(assert (or (= (f a) g) (= (h a) g))) + +(assert (= (f a b d) c)) +(assert (= (h a b d) c)) + +(assert (forall ((x Int) (y Int)) (not (= (g x y) c)))) + +(check-sat) |