diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 13:00:43 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-23 13:00:43 -0500 |
commit | 085d6a91f0686d6680d15bb54f9435f30d53c331 (patch) | |
tree | a5ffe08fecdcd1a66b5b40623a5b514284857cbe /test/regress/regress1 | |
parent | 996de9116150fb7214b3b9a56995e2492d3e5668 (diff) |
Update dynamic splitting strategy for quantifiers (#3162)
Diffstat (limited to 'test/regress/regress1')
-rw-r--r-- | test/regress/regress1/quantifiers/f993-loss-easy.smt2 | 73 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/issue993.smt2 | 108 |
2 files changed, 181 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/f993-loss-easy.smt2 b/test/regress/regress1/quantifiers/f993-loss-easy.smt2 new file mode 100644 index 000000000..775b63338 --- /dev/null +++ b/test/regress/regress1/quantifiers/f993-loss-easy.smt2 @@ -0,0 +1,73 @@ +(set-info :smt-lib-version 2.6) +(set-logic UFDT) +(set-info :status unsat) +(declare-sort A$ 0) +(declare-sort Nat$ 0) +(declare-sort Nat_nat_fun$ 0) +(declare-sort Enat_nat_fun$ 0) +(declare-sort Nat_bool_fun$ 0) +(declare-sort Nat_enat_fun$ 0) +(declare-sort Bool_bool_fun$ 0) +(declare-sort Enat_bool_fun$ 0) +(declare-sort Enat_enat_fun$ 0) +(declare-sort A_stream_bool_fun$ 0) +(declare-sort Nat_bool_fun_nat_fun$ 0) +(declare-sort Nat_nat_bool_fun_fun$ 0) +(declare-sort Bool_enat_bool_fun_fun$ 0) +(declare-sort Enat_enat_bool_fun_fun$ 0) +(declare-sort Nat_bool_fun_nat_bool_fun_fun$ 0) +(declare-datatypes ((Nat_option$ 0)(Enat$ 0)) (((none$) (some$ (the$ Nat$))) +((abs_enat$ (rep_enat$ Nat_option$))) +)) +(declare-sort A_stream$ 0) +(declare-fun shd$ (A_stream$) A$) +(declare-fun stl$ (A_stream$) A_stream$) +(declare-fun sCons$ (A$ A_stream$) A_stream$) +(declare-fun i$ () Nat$) +(declare-fun p$ () A_stream_bool_fun$) +(declare-fun ia$ () Nat$) +(declare-fun uu$ (Nat$) Nat_bool_fun$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun uua$ (Enat$) Nat_bool_fun$) +(declare-fun uub$ (Bool_bool_fun$) Nat_bool_fun_nat_bool_fun_fun$) +(declare-fun uuc$ (Enat$) Nat_bool_fun$) +(declare-fun uud$ () Nat_nat_fun$) +(declare-fun eSuc$ (Enat$) Enat$) +(declare-fun enat$ (Nat$) Enat$) +(declare-fun less$ (Nat$) Nat_bool_fun$) +(declare-fun plus$ (Enat$) Enat_enat_fun$) +(declare-fun less$a (Enat$) Enat_bool_fun$) +(declare-fun omega$ () A_stream$) +(declare-fun plus$a (Nat$) Nat_nat_fun$) +(declare-fun sdrop$ (Nat$ A_stream$) A_stream$) +(declare-fun omega$a () A_stream$) +(declare-fun sfirst$ (A_stream_bool_fun$ A_stream$) Enat$) +(declare-fun fun_app$ (Nat_bool_fun$ Nat$) Bool) +(declare-fun less_eq$ (Nat$) Nat_bool_fun$) +(declare-fun case_nat$ (Bool) Nat_bool_fun_nat_bool_fun_fun$) +(declare-fun fun_app$a (Enat_bool_fun$ Enat$) Bool) +(declare-fun fun_app$b (Bool_enat_bool_fun_fun$ Bool) Enat_bool_fun$) +(declare-fun fun_app$c (Nat_bool_fun_nat_bool_fun_fun$ Nat_bool_fun$) Nat_bool_fun$) +(declare-fun fun_app$d (Bool_bool_fun$ Bool) Bool) +(declare-fun fun_app$e (Nat_nat_fun$ Nat$) Nat$) +(declare-fun fun_app$f (A_stream_bool_fun$ A_stream$) Bool) +(declare-fun fun_app$g (Nat_enat_fun$ Nat$) Enat$) +(declare-fun fun_app$h (Enat_enat_fun$ Enat$) Enat$) +(declare-fun fun_app$i (Enat_nat_fun$ Enat$) Nat$) +(declare-fun fun_app$j (Enat_enat_bool_fun_fun$ Enat$) Enat_bool_fun$) +(declare-fun fun_app$k (Nat_nat_bool_fun_fun$ Nat$) Nat_bool_fun$) +(declare-fun fun_app$l (Nat_bool_fun_nat_fun$ Nat_bool_fun$) Nat$) +(declare-fun greatest$ (Enat_bool_fun$) Enat$) +(declare-fun less_eq$a (Enat$) Enat_bool_fun$) +(declare-fun rec_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$) +(declare-fun case_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$) +(declare-fun greatest$a () Nat_bool_fun_nat_fun$) +(declare-fun greatestM$ (Nat_nat_fun$) Nat_bool_fun_nat_fun$) +(assert (and +(forall ((?v0 Nat$) (?v1 A_stream_bool_fun$) (?v2 A_stream$)) (=> (fun_app$a (less$a (enat$ ?v0)) (sfirst$ ?v1 ?v2)) (not (fun_app$f ?v1 (sdrop$ ?v0 ?v2)))) ) +(not (fun_app$a (less_eq$a (sfirst$ p$ omega$)) (enat$ (suc$ ia$)))) +(fun_app$f p$ (sdrop$ (suc$ ia$) omega$)) +(forall ((?v0 Enat$) (?v1 Enat$)) (=> (not (fun_app$a (less$a ?v0) ?v1)) (fun_app$a (less_eq$a ?v1) ?v0)) ) +)) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/issue993.smt2 b/test/regress/regress1/quantifiers/issue993.smt2 new file mode 100644 index 000000000..40c5538de --- /dev/null +++ b/test/regress/regress1/quantifiers/issue993.smt2 @@ -0,0 +1,108 @@ +(set-logic AUFBVDTNIRA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-sort us_private 0) + +(declare-sort integer 0) + +(declare-fun to_rep1 (integer) Int) + +(declare-datatypes () +((us_split_fields + (mk___split_fields (rec__unit1__t1__c1 integer)(rec__ext__ us_private))))) + +(declare-datatypes () +((us_split_fields__ref + (mk___split_fields__ref (us_split_fields__content us_split_fields))))) +(define-fun us_split_fields__ref___projection ((a us_split_fields__ref)) us_split_fields + (us_split_fields__content a)) + +(declare-datatypes () +((us_rep (mk___rep (us_split_fields1 us_split_fields)(attr__tag Int))))) +(define-fun us_rep___projection ((a us_rep)) us_split_fields (us_split_fields1 + a)) + +(declare-fun is_zero (us_rep) Bool) + +(declare-fun is_zero__post_predicate (Bool us_rep) Bool) + +;; is_zero__def_axiom + (assert + (forall ((x us_rep)) + (! (=> (is_zero__post_predicate (is_zero x) x) + (= (= (is_zero x) true) + (= (to_rep1 (rec__unit1__t1__c1 (us_split_fields1 x))) 0))) :pattern ( + (is_zero x)) ))) + +(declare-datatypes () +((us_split_fields2 + (mk___split_fields1 + (rec__unit2__t2__c2 integer)(rec__unit1__t1__c11 integer)(rec__ext__1 us_private))))) + +(declare-datatypes () +((us_split_fields__ref1 + (mk___split_fields__ref1 (us_split_fields__content1 us_split_fields2))))) +(define-fun us_split_fields__ref_2__projection ((a us_split_fields__ref1)) us_split_fields2 + (us_split_fields__content1 a)) + +(declare-datatypes () +((us_rep1 (mk___rep1 (us_split_fields3 us_split_fields2)(attr__tag1 Int))))) +(define-fun us_rep_3__projection ((a us_rep1)) us_split_fields2 (us_split_fields3 + a)) + +(declare-fun hide_ext__ (integer us_private) us_private) + +(define-fun to_base ((a us_rep1)) us_rep (mk___rep + (mk___split_fields + (rec__unit1__t1__c11 + (us_split_fields3 a)) + (hide_ext__ + (rec__unit2__t2__c2 + (us_split_fields3 a)) + (rec__ext__1 (us_split_fields3 a)))) + (attr__tag1 a))) + +(declare-fun is_zero2 (us_rep1) Bool) + +(declare-fun is_zero__post_predicate2 (Bool us_rep1) Bool) + +;; is_zero__def_axiom + (assert + (forall ((x us_rep1)) + (! (=> (is_zero__post_predicate2 (is_zero2 x) x) + (= (= (is_zero2 x) true) + (and (= (is_zero (to_base x)) true) + (= (to_rep1 (rec__unit2__t2__c2 (us_split_fields3 x))) 0)))) :pattern ( + (is_zero2 x)) ))) + +(declare-fun x2__attr__tag () Int) + +(declare-fun x2__split_fields () integer) + +(declare-fun x2__split_fields1 () integer) + +(declare-fun x2__split_fields2 () us_private) + +;; H + (assert + (forall ((x2__split_fields3 us_split_fields2)) (is_zero__post_predicate2 + (is_zero2 (mk___rep1 x2__split_fields3 x2__attr__tag)) + (mk___rep1 x2__split_fields3 x2__attr__tag)))) + +;; H + (assert + (and (= (to_rep1 x2__split_fields1) 0) (= (to_rep1 x2__split_fields) 0))) + +;; Should be enough to imply following hypothesis + (assert + (forall ((x us_rep1)) (is_zero__post_predicate (is_zero (to_base x)) + (to_base x)))) + +(assert +;; WP_parameter_def + ;; File "main.adb", line 5, characters 0-0 + (not + (= (is_zero (to_base (mk___rep1 + (mk___split_fields1 x2__split_fields x2__split_fields1 + x2__split_fields2) x2__attr__tag))) true))) +(check-sat) |