diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
| commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
| tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress0/rewriterules | |
| parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) | |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress0/rewriterules')
41 files changed, 1 insertions, 4481 deletions
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index fcaa9dc2b..5df254bad 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -23,14 +23,12 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 \ - length_gen_020.smt2 \ datatypes.smt2 \ - datatypes_sat.smt2 \ relation.smt2 \ simulate_rewriting.smt2 \ native_arrays.smt2 -# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 +# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/datatypes2.smt2 b/test/regress/regress0/rewriterules/datatypes2.smt2 deleted file mode 100644 index 277ddc3ae..000000000 --- a/test/regress/regress0/rewriterules/datatypes2.smt2 +++ /dev/null @@ -1,150 +0,0 @@ -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status unsat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons1 (elt list) list) -(declare-fun cons2 (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) )) - - -(declare-fun proj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons1 (list) Bool) -(assert (= (iscons1 nil1) false)) -(assert (= (iscons1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons1 (cons2 ?e ?l)) false))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) - - -(declare-fun iscons2 (list) Bool) -(assert (= (iscons2 nil1) false)) -(assert (= (iscons2 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons2 (cons1 ?e ?l)) false))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) -(assert (= (isnil1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons1 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons2 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil1) false)) -(assert (= (isnil2 nil2) true)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons1 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons2 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - - (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2))))))) - -;;(assert (= (cons1 l1 l2) (cons2 l1 l2))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/datatypes3.smt2 b/test/regress/regress0/rewriterules/datatypes3.smt2 deleted file mode 100644 index 1ec5dcbc4..000000000 --- a/test/regress/regress0/rewriterules/datatypes3.smt2 +++ /dev/null @@ -1,137 +0,0 @@ -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status unsat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons1 (elt list) list) -(declare-fun cons2 (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) )) - -(assert (= (proj11 nil1) nil1)) -(assert (= (proj12 nil1) nil1)) -(assert (= (proj11 nil2) nil2)) -(assert (= (proj12 nil2) nil2)) - -(declare-fun proj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) )) - -(assert (= (proj21 nil1) nil1)) -(assert (= (proj22 nil1) nil1)) -(assert (= (proj21 nil2) nil2)) -(assert (= (proj22 nil2) nil2)) - - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons1 (list) Bool) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) - - -(declare-fun iscons2 (list) Bool) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil2) true)) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - -;; (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2))))))) - -(assert (= (cons1 l1 l2) (cons2 l1 l2))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2 b/test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2 deleted file mode 100644 index 6e22816d7..000000000 --- a/test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2 +++ /dev/null @@ -1,264 +0,0 @@ -(set-logic AUFLIRA) - -;; DATATYPE -;; nat = succ(pred : nat) | zero, -;; list = cons(car : tree, cdr : list) | null, -;; tree = node(children : list) | leaf(data : nat) -;; END; - -;;;;;;;;;;; -;; nat ;; -;;;;;;;;;;; -(declare-sort nat 0) -(declare-fun zero () nat) -(declare-fun succ (nat) nat) - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj1 (nat) nat) -(assert (forall ((?x1 nat)) - (! (= (inj1 (succ ?x1)) ?x1) :pattern ((succ ?x1)) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun pred (nat) nat) -(assert (forall ((?x1 nat)) - (! (= (pred (succ ?x1)) ?x1) :pattern ((pred (succ ?x1))) ) )) - -(assert (= (pred zero) zero)) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_succ (nat) Bool) -(assert (= (is_succ zero) false)) -(assert (forall ((?x1 nat)) - (! (= (is_succ (succ ?x1)) true) :pattern ((succ ?x1)) ) )) - -(assert (forall ((?x1 nat)) - (! (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1)))) :pattern ((is_succ ?x1) (pred ?x1)) ) )) - -(declare-fun is_zero (nat) Bool) -(assert (= (is_zero zero) true)) -(assert (forall ((?x1 nat)) - (! (=> (is_zero ?x1) (= ?x1 zero)) :pattern ((is_zero ?x1)) ) )) - -;;; directrr -(assert (forall ((?x1 nat)) - (! (= (is_succ (succ ?x1)) true) :pattern ((is_succ (succ ?x1))) ) )) -(assert (forall ((?x1 nat)) - (! (= (is_zero (succ ?x1)) false) :pattern ((is_zero (succ ?x1))) ))) - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert (forall ((?x1 nat)) - (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :pattern ((is_zero ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :pattern ((is_succ ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :pattern ((is_zero ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :pattern ((is_succ ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?x1 nat)) - (! (or (is_zero ?x1) (is_succ ?x1)) :pattern ((pred ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; non-cyclic -(declare-fun size_nat (nat) Real) -(assert (forall ((?x1 nat)) - (! (> (size_nat (succ ?x1)) (size_nat ?x1)) :pattern ((succ ?x1)) ) )) - - - -;;;;;;;;;;;;;;;;;;;;; -;; list and tree - -(declare-sort list 0) -(declare-sort tree 0) - -;;;;;;;;;;; -;; list ;; -;;;;;;;;;;; - -(declare-fun null () list) -(declare-fun cons (tree list) list) - -(declare-fun node (list) tree) -(declare-fun leaf (nat) tree) - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj2 (list) tree) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (inj2 (cons ?x1 ?x2)) ?x1) :pattern ((cons ?x1 ?x2)) ) )) - -(declare-fun inj3 (list) list) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (inj3 (cons ?x1 ?x2)) ?x2) :pattern ((cons ?x1 ?x2)) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun car (list) tree) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (car (cons ?x1 ?x2)) ?x1) :pattern ((car (cons ?x1 ?x2))) ) )) - -(assert (= (car null) (node null))) - -(declare-fun cdr (list) list) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (cdr (cons ?x1 ?x2)) ?x2) :pattern ((cdr (cons ?x1 ?x2))) ) )) - -(assert (= (cdr null) null)) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_cons (list) Bool) -(assert (= (is_cons null) false)) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((cons ?x1 ?x2)) ) )) - -(assert (forall ((?x1 list)) - (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(car ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(cdr ?x1)) ) )) - -(declare-fun is_null (list) Bool) -(assert (= (is_null null) true)) - -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (= (car ?x1) (node null))) :pattern ((is_null ?x1)(car ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (= (cdr ?x1) null)) :pattern ((is_null ?x1)(cdr ?x1)) ) )) - -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (= ?x1 null)) :pattern ((is_null ?x1)) ) )) - -;;; directrr -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((is_cons (cons ?x1 ?x2))) ) )) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (is_null (cons ?x1 ?x2)) false) :pattern ((is_null (cons ?x1 ?x2))) ) )) - - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :pattern ((is_null ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :pattern ((is_cons ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :pattern ((is_null ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :pattern ((is_cons ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?x1 list)) - (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((car ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((cdr ?x1)) ) )) - -;;;;;;;;;;;;;;; -;; tree - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj4 (tree) list) -(assert (forall ((?x1 list)) - (! (= (inj4 (node ?x1)) ?x1) :pattern ((node ?x1)) ) )) - -(declare-fun inj5 (tree) nat) -(assert (forall ((?x1 nat)) - (! (= (inj5 (leaf ?x1)) ?x1) :pattern ((leaf ?x1)) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun children (tree) list) -(assert (forall ((?x1 list)) - (! (= (children (node ?x1)) ?x1) :pattern ((children (node ?x1))) ) )) -(assert (forall ((?x1 nat)) - (! (= (children (leaf ?x1)) null) :pattern ((children (leaf ?x1))) ) )) - - -(declare-fun data (tree) nat) -(assert (forall ((?x1 nat)) - (! (= (data (leaf ?x1)) ?x1) :pattern ((data (leaf ?x1))) ) )) -(assert (forall ((?x1 list)) - (! (= (data (node ?x1)) zero) :pattern ((data (node ?x1))) ) )) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_node (tree) Bool) -(assert (forall ((?x1 list)) - (! (= (is_node (node ?x1)) true) :pattern ((node ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (=> (is_node ?x1) (= ?x1 (node (children ?x1)))) :pattern ((is_node ?x1)(children ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (=> (is_node ?x1) (= (data ?x1) zero)) :pattern ((is_node ?x1)(data ?x1)) ) )) - - -(declare-fun is_leaf (tree) Bool) -(assert (forall ((?x1 nat)) - (! (=> true (= (is_leaf (leaf ?x1)) true)) :pattern ((leaf ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1)))) :pattern ((is_leaf ?x1)(data ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (is_leaf ?x1) (= (children ?x1) null)) :pattern ((is_leaf ?x1)(children ?x1)) ) )) - -;;; directrr -(assert (forall ((?x1 list)) - (! (= (is_node (node ?x1)) true) :pattern ((is_node (node ?x1))) ) )) -(assert (forall ((?x1 list)) - (! (= (is_leaf (node ?x1)) false) :pattern ((is_leaf (node ?x1))) ) )) -(assert (forall ((?x1 nat)) - (! (= (is_leaf (leaf ?x1)) true) :pattern (is_leaf (leaf ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (= (is_node (leaf ?x1)) false) :pattern ((is_node (leaf ?x1))) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert (forall ((?x1 tree)) - (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :pattern ((is_node ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :pattern ((is_leaf ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :pattern ((is_node ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :pattern ((is_leaf ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?x1 tree)) - (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((children ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((data ?x1)) ) )) - - -;;;;;;;;;;;;;;;;;; -;; non-cyclic -(declare-fun size_list (list) Real) -(declare-fun size_tree (tree) Real) -(assert (forall ((?x1 tree) (?x2 list)) - (! (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) :pattern ((cons ?x1 ?x2)) ) )) -(assert (forall ((?x1 list)) - (! (> (size_tree (node ?x1)) (size_list ?x1)) :pattern ((node ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (> (size_tree (leaf ?x1)) (size_nat ?x1)) :pattern ((leaf ?x1)) ) )) diff --git a/test/regress/regress0/rewriterules/datatypes_sat.smt2 b/test/regress/regress0/rewriterules/datatypes_sat.smt2 deleted file mode 100644 index 92576f976..000000000 --- a/test/regress/regress0/rewriterules/datatypes_sat.smt2 +++ /dev/null @@ -1,101 +0,0 @@ -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status sat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj1 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj2 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj1 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj2 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons (list) Bool) -(assert (= (iscons nil1) false)) -(assert (= (iscons nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) -(assert (= (isnil1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil1) false)) -(assert (= (isnil2 nil2) true)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - -(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l2) (proj2 l2))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen.smt2 b/test/regress/regress0/rewriterules/length_gen.smt2 deleted file mode 100644 index dda478357..000000000 --- a/test/regress/regress0/rewriterules/length_gen.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 42 nil)) 42))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_010.smt2 b/test/regress/regress0/rewriterules/length_gen_010.smt2 deleted file mode 100644 index 052f5905b..000000000 --- a/test/regress/regress0/rewriterules/length_gen_010.smt2 +++ /dev/null @@ -1,36 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -;; (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(assert-rewrite ((?e Int) (?l list)) () () (length (cons ?e ?l)) (+ 1 (length ?l))) - -(declare-fun gen_cons (Int list) list) - -(assert-rewrite ((?n Int) (?l list)) () (= ?n 0) (gen_cons ?n ?l) (?l)) - -(assert-rewrite ((?n Int) (?l list)) () (> ?n 0) (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 10 nil)) 10))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 deleted file mode 100644 index 02bc877fc..000000000 --- a/test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 10 nil)) 10))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_020.smt2 b/test/regress/regress0/rewriterules/length_gen_020.smt2 deleted file mode 100644 index 8e0021175..000000000 --- a/test/regress/regress0/rewriterules/length_gen_020.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 20 nil)) 20))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_020_sat.smt2 deleted file mode 100644 index cc75eb85a..000000000 --- a/test/regress/regress0/rewriterules/length_gen_020_sat.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status sat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 20 nil)) 200))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_040.smt2 b/test/regress/regress0/rewriterules/length_gen_040.smt2 deleted file mode 100644 index 687422223..000000000 --- a/test/regress/regress0/rewriterules/length_gen_040.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 40 nil)) 40))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 deleted file mode 100644 index 293ea147b..000000000 --- a/test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 40 nil)) 40))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 b/test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 deleted file mode 100644 index 69f9f97be..000000000 --- a/test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) - :pattern ((gen_cons ?n ?l)) ))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 40 nil)) 40))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_080.smt2 b/test/regress/regress0/rewriterules/length_gen_080.smt2 deleted file mode 100644 index 061042be3..000000000 --- a/test/regress/regress0/rewriterules/length_gen_080.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 80 nil)) 80))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_1280.smt2 b/test/regress/regress0/rewriterules/length_gen_1280.smt2 deleted file mode 100644 index b613844ce..000000000 --- a/test/regress/regress0/rewriterules/length_gen_1280.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 1280 nil)) 1280))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 b/test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 deleted file mode 100644 index 7d1cf3203..000000000 --- a/test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) - :pattern ((gen_cons ?n ?l)) ))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 1280 nil)) 1280))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160.smt2 b/test/regress/regress0/rewriterules/length_gen_160.smt2 deleted file mode 100644 index 339c70bb5..000000000 --- a/test/regress/regress0/rewriterules/length_gen_160.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 160))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 deleted file mode 100644 index 28b58183e..000000000 --- a/test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 160))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 b/test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 deleted file mode 100644 index 65d0c9570..000000000 --- a/test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) - :pattern ((gen_cons ?n ?l)) ))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 160))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_160_sat.smt2 deleted file mode 100644 index e2ed52faf..000000000 --- a/test/regress/regress0/rewriterules/length_gen_160_sat.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status sat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 1600))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_2560.smt2 b/test/regress/regress0/rewriterules/length_gen_2560.smt2 deleted file mode 100644 index 2aff61656..000000000 --- a/test/regress/regress0/rewriterules/length_gen_2560.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 2560 nil)) 2560))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 deleted file mode 100644 index 3e88e781f..000000000 --- a/test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 2560 nil)) 25600))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_640.smt2 b/test/regress/regress0/rewriterules/length_gen_640.smt2 deleted file mode 100644 index f1dc6bbf2..000000000 --- a/test/regress/regress0/rewriterules/length_gen_640.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 640 nil)) 640))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 deleted file mode 100644 index 29d0f1aca..000000000 --- a/test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 640 nil)) 640))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_640_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_640_sat.smt2 deleted file mode 100644 index 958c2c730..000000000 --- a/test/regress/regress0/rewriterules/length_gen_640_sat.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 640 nil)) 6400))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 b/test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 deleted file mode 100644 index 30e3bc864..000000000 --- a/test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (cons 1 (gen_cons (- ?n 1) ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 1280 nil)) 1280))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_inv_160.smt2 b/test/regress/regress0/rewriterules/length_gen_inv_160.smt2 deleted file mode 100644 index 9c2a5c307..000000000 --- a/test/regress/regress0/rewriterules/length_gen_inv_160.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (cons 1 (gen_cons (- ?n 1) ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 160))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_trick3.smt2 b/test/regress/regress0/rewriterules/length_trick3.smt2 deleted file mode 100644 index f6899541b..000000000 --- a/test/regress/regress0/rewriterules/length_trick3.smt2 +++ /dev/null @@ -1,36 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) -;; don't use arith -(declare-sort mynat 0) -(declare-fun zero () mynat) -(declare-fun succ (mynat) mynat) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) mynat) - -(assert (= (length nil) zero)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) - -(declare-fun ten_one_cons (list) list) - -(assert (forall ((?l list)) (! (= (ten_one_cons ?l) - (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) - ) :rewrite-rule))) - -(assert (not (= (length (ten_one_cons nil)) - (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero))))))))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_trick3_int.smt2 b/test/regress/regress0/rewriterules/length_trick3_int.smt2 deleted file mode 100644 index d58bf55fe..000000000 --- a/test/regress/regress0/rewriterules/length_trick3_int.smt2 +++ /dev/null @@ -1,44 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun ten_one_cons (list) list) - -(assert (forall ((?l list)) (! (= (ten_one_cons ?l) - (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) - ) :rewrite-rule))) - -(assert (not (= (length (ten_one_cons nil)) - 10))) - -(check-sat) - -(declare-fun ten_one_ten (list) list) - -(assert (forall ((?l list)) (! (= (ten_one_ten ?l) - (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons ?l) ))))))))) - ) :rewrite-rule))) - -(declare-fun two_one_ten (list) list) - -(assert (forall ((?l list)) (! (= (two_one_ten ?l) - (ten_one_cons (ten_one_cons ?l)) - ) :rewrite-rule))) - -(exit) diff --git a/test/regress/regress0/rewriterules/native_datatypes2.smt2 b/test/regress/regress0/rewriterules/native_datatypes2.smt2 deleted file mode 100644 index f19e5097b..000000000 --- a/test/regress/regress0/rewriterules/native_datatypes2.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-info :status unsat) - -(declare-datatypes ((nat 0) (list 0)) ( -((succ (pred nat)) (zero ) ) -((cons (car nat)(cdr list)) (nil ) ) - -)) - - -;;define length -(declare-fun length (list) nat) - -(assert (= (length nil) zero)) - -(assert-rewrite ((?e nat) (?l list)) () (length (cons ?e ?l)) (succ (length ?l)) () ) -(assert-propagation ((?l list)) ((= (length ?l) zero)) () (= ?l nil) (((length ?l))) ) -;(assert-propagation ((?l list)) () () (= ?l nil) (((= (length ?l) 0))) ) - -(declare-fun gen_cons (nat list) list) - -(assert-rewrite ((?l list)) () (gen_cons zero ?l) ?l () ) - -(assert-rewrite ((?n nat) (?l list)) () (gen_cons (succ ?n) ?l) (gen_cons ?n (cons zero ?l)) () ) - -(declare-fun l1 () list) -(declare-fun l2 () list) - -(assert (not (=> (= (length l1) zero) (= l1 nil)))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2 b/test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2 deleted file mode 100644 index 955c810aa..000000000 --- a/test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2 +++ /dev/null @@ -1,72 +0,0 @@ -;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer -(set-logic AUFLIA) -(set-info :status unsat) - -(declare-sort elt 0) - -(declare-fun f (elt) elt) -(declare-fun Rf (elt elt elt) Bool) - -;;eq -(assert-propagation ((?x elt)) () () (or (= ?x ?x) (not (= ?x ?x))) ((?x)) ) -;; reflexive -(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) ) -;; step -(assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((f ?x))) ) - -;; reach -(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) (((f ?x1))) ) -;; reach extended -(assert-propagation ((?x1 elt)(?x2 elt)) ((not (= ?x1 ?x2))(Rf ?x1 ?x2 ?x2)) () (Rf ?x1 (f ?x1) ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) -;; reach extended -(assert-propagation ((?x1 elt)(?x2 elt)) ((not (Rf ?x1 (f ?x1) ?x2))(Rf ?x1 ?x2 ?x2)) () (= ?x1 ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) - -;; cycle -(assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((f ?x1))) ) -;; sandwich -(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) () ) -;; order1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) - (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) () ) -;; order1 extended -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () - (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x3))) ) -;; order1 extended -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () - (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x3 ?x2))) ) - -;; order2 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x3)) - (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) () ) -;; transitive1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3)) - (Rf ?x1 ?x3 ?x3) () ) -;; transitive2 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) - (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) () ) -;;transitive3 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) - (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) () ) - -(declare-fun e1 () elt) -(declare-fun e2 () elt) -(declare-fun e3 () elt) -(declare-fun e4 () elt) - - -(assert (and (hack e1) (hack e2) (hack e3) (hack e4) (hack (f e1)))) - - -;; (assert (=> (Rf e1 e2 e3) (Rf e1 (f e1) (f e1)) )) - -;; (assert (=> (Rf e1 e2 e3) (Rf e1 e3 e3) )) - -;; (assert (=> (Rf e1 e2 e3) (or (= e1 e3) (Rf e1 (f e1) e3)) )) - -;;(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3) ))) - -(assert (and (not (= e1 e2)) (Rf e1 e2 e3) (not (Rf e1 (f e1) e3)) )) - - -(check-sat) -(exit)
\ No newline at end of file diff --git a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 deleted file mode 100644 index 8f30f38a5..000000000 --- a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 +++ /dev/null @@ -1,330 +0,0 @@ -;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer -(set-logic AUFLIA) -(set-info :status unsat) - -(declare-sort elt 0) -(define-sort mem () (Array elt elt)) - -(declare-fun R (mem elt elt elt) Bool) - -;; reflexive -(assert-propagation ((?m mem)(?x elt)) ((?m ?x)) () () (R ?m ?x ?x ?x) ) -;; step -(assert-propagation ((?m mem)(?x elt)) (((select ?m ?x))) () () (R ?m ?x (select ?m ?x) (select ?m ?x)) ) -;; (assert-propagation ((?x elt)) (f ?x)))) () () (Rf ?x (f ?x) (f ?x)) (((Rf ?x (f ?x) ) -;; (assert-propagation ((?x elt)) (((f ?x))) () () (=> true (Rf ?x (f ?x) (f ?x))) ) - -;; reach -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) (((select ?m ?x1))) () ((R ?m ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (R ?m ?x1 (select ?m ?x1) ?x2)) ) -;; ;; reach extended -;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 (f ?x1) ?x2))) ((not (= ?x1 ?x2))(Rf ?x1 ?x2 ?x2)) () (Rf ?x1 (f ?x1) ?x2) ) -;; ;; reach extended -;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 (f ?x1) ?x2))) ((not (Rf ?x1 (f ?x1) ?x2))(Rf ?x1 ?x2 ?x2)) () (= ?x1 ?x2) ) - -;; cycle -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) (((select ?m ?x1))) ((= (select ?m ?x1) ?x1)) ((R ?m ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) () ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) - -;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 ?x2 ?x2)(f ?x1))) () () (=> (and (= (f ?x1) ?x1) (Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2)) ) - -;; sandwich -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) () () ((R ?m ?x1 ?x2 ?x1)) (= ?x1 ?x2) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 ?x2 ?x1))) () () (=> (Rf ?x1 ?x2 ?x1) (= ?x1 ?x2)) ) - -;; order1 -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () () - ((R ?m ?x1 ?x2 ?x2)(R ?m ?x1 ?x3 ?x3)) (or (R ?m ?x1 ?x2 ?x3) (R ?m ?x1 ?x3 ?x2)) ) - -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) () () -;; (=> (and (Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2))) ) - -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) ) - -;; order2 -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x1 ?x2 ?x3)) - (and (R ?m ?x1 ?x2 ?x2) (R ?m ?x2 ?x3 ?x3)) ) -;; transitive1 -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x1 ?x2 ?x2)(R ?m ?x2 ?x3 ?x3)) - (R ?m ?x1 ?x3 ?x3) ) -;; ;; transitive1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((not (Rf ?x1 ?x3 ?x3))(Rf ?x2 ?x3 ?x3)) -;; (not (Rf ?x1 ?x2 ?x2)) ) -;; ;; transitive1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(not (Rf ?x1 ?x3 ?x3))) -;; (not (Rf ?x2 ?x3 ?x3)) ) - -;;transitive2 -(assert-propagation ((?m mem)(?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x0 ?x1 ?x2)(R ?m ?x1 ?x3 ?x2)) - (and (R ?m ?x0 ?x1 ?x3) (R ?m ?x0 ?x3 ?x2)) ) - -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2))) () () -;; (=> (and (Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) -;; (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2))) -;; ) - -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2))) () ((not (Rf ?x0 ?x1 ?x3))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) ) -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x1 ?x3))) -;; (not (Rf ?x1 ?x3 ?x2)) ) -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2))) () ((not (Rf ?x0 ?x3 ?x2))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) ) -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x3 ?x2))) -;; (not (Rf ?x1 ?x3 ?x2)) ) - -;; ;;transitive3 -(assert-propagation ((?m mem)(?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x0 ?x1 ?x2)(R ?m ?x0 ?x3 ?x1)) - (and (R ?m ?x0 ?x3 ?x2) (R ?m ?x3 ?x1 ?x2)) ) - -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1))) () () -;; (=> (and (Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) -;; (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2))) ) - - -(declare-fun next () mem) - -(declare-fun e1 () elt) -(declare-fun e2 () elt) -(declare-fun e3 () elt) -(declare-fun e4 () elt) - - - -(declare-fun R_avoid (mem elt elt elt) Bool) - -(assert-rewrite ((?m mem)(?x0 elt)(?x1 elt)(?exc elt)) () () (R_avoid ?m ?x0 ?x1 ?exc) - (or (R ?m ?x0 ?x1 ?exc) (and (R ?m ?x0 ?x1 ?x1) (not (R ?m ?x0 ?exc ?exc)))) ) - - -;; Identity of Back to the future p175 -(assert-rewrite ((?p elt)(?q elt)(?u elt)(?v elt)(?w elt)(?m mem)) () () (R (store ?m ?p ?q) ?u ?v ?w) - (or (and (R ?m ?u ?v ?w) (R_avoid ?m ?u ?w ?p) ) - (and (not (= ?p ?w)) (R_avoid ?m ?u ?p ?w) (R ?m ?u ?v ?p) (R_avoid ?m ?q ?w ?p) ) - (and (not (= ?p ?w)) (R_avoid ?m ?u ?p ?w) (R ?m ?q ?v ?w) (R_avoid ?m ?q ?w ?p) ) ) - ) - - - -(declare-fun join (mem elt elt) elt) - -(declare-fun null () elt) -(assert (= (select next null) null)) - -(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) (((join ?m ?x ?y))) () ((R ?m ?x ?z ?z)(R ?m ?y ?z ?z)) (R ?m ?x (join ?m ?x ?y) ?z) ) -(assert-propagation ((?m mem)(?x elt)(?y elt)) (((join ?m ?x ?y))) () () (or (and (R ?m ?x (join ?m ?x ?y) (join ?m ?x ?y)) (R ?m ?y (join ?m ?x ?y) (join ?m ?x ?y))) (= (join ?m ?x ?y) null)) ) - -;;extended join -(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) () () ((R ?m ?x ?z (join ?m ?x ?y))(R ?m ?y ?z (join ?m ?x ?y))) (= ?z (join ?m ?x ?y)) ) - - -(assert-propagation ((?p elt)(?q elt)(?m mem)(?u elt)(?v elt)) (((join (store ?m ?p ?q) ?u ?v))) () () - (= (join (store ?m ?p ?q) ?u ?v) - (let ((jp (join ?m ?u ?v))) - ;; In ?m: ?u ?v have a nearest point of junction (join ?m ?u ?v) - (ite (and (R ?m ?u jp jp) (R ?m ?v jp jp)) - ;; The modification is in the ?u branch - (ite (R ?m ?u ?p jp) - ;; we can go by the new path and the new path doesn't cycle - (ite (and (R (store ?m ?p ?q) ?u ?p ?q) (R (store ?m ?p ?q) ?q (join ?m ?q ?v) (join ?m ?q ?v))) - (join ?m ?q ?v) - ;; we can't - null - ) - ;; The modification is in the ?v branch - (ite (R ?m ?v ?p jp) - ;; we can go by the new path and the new path doesn't cycle - (ite (and (R (store ?m ?p ?q) ?v ?p ?q) (R (store ?m ?p ?q) ?q (join ?m ?u ?q) (join ?m ?u ?q))) - (join ?m ?u ?q) - ;; we can't - null - ) - ;; The modification is not before the point of junction - (join ?m ?u ?v) - )) - ;; In ?m: ?u ?v doens't have a point of junction - ;;The modification is accesible from ?u - (ite (R ?m ?u ?p ?p) (join ?m ?q ?v) - ;;The modification is accesible from ?v - (ite (R ?m ?v ?p ?p) (join ?m ?u ?q) - ;;The modification is accesible neither from ?u neither from ?v - (join ?m ?u ?v) - ) - ) - ) - )) - ) - -(declare-fun next2 () mem) - -;; === Example 0 === -;; (assert (not (=> -;; (and (not (= e1 e2)) -;; (R next e1 e2 e3)) -;; (R next e1 (select next e1) e3)) -;; )) - -;;================ -;;Thomas' example1 x,e1 y,e2 z,e3 y',e4 -;;================ -;; (assert (not (=> -;; (and (R next e1 e2 e3) -;; (not (= e2 e3)) -;; (= e4 (select next e2))) -;; (R next e1 e4 e3)) -;; )) - - -;;=================== -;; ;;Thomas' example2 -;;=================== - -;; (assert (not (=> -;; (and (R next e1 null null) -;; (= (join next e1 e2) null) -;; (= next2 (store next e2 e1)) -;; ) -;; (R next2 e1 null null) -;; ) -;; ) -;; ) - - -;;================ -;;Thomas' example3 -;;================ -(assert (not (=> (and (= (join next e1 e2) null) - (R next e2 null null) - (not (= e2 null)) - (= next2 (store next e2 e1)) - (= e3 e2) - (= e4 (select next e2)) - ) - (= (join next2 e3 e4) null) - ) - ) - ) - -;; ==== for debugging example 3 ==== -;; ;;case to consider -;; ;;(assert (or (not (R next e1 null null)) (R next e1 null null))) - -;; ;;first case to consider -;; ;;(assert (R next e1 null null)) - -;; ;;second case to consider -;; ;; (assert (not (R next e1 null null))) - - -;; ;;hyp -;; (assert (= (join next e1 e2) null)) -;; (assert (R next e2 null null)) -;; (assert (not (= e2 null))) -;; (assert (= next2 (store next e2 e1))) -;; (assert (= e3 e2)) -;; (assert (= e4 (select next e2))) - -;; ;; help -;; ;; have a join point -;; ;; (assert (R next e2 e4 e4)) -;; ;; (assert (R next e4 e4 e4)) - -;; ;; (assert (R next e2 (join next e2 e4) e4)) -;; ;; (assert (not (R next e4 e2 e2))) - -;; ;; (assert (not (= e2 (join next e2 e4))));; slow with efficient (/axioms) - -;; ;; (assert (= e4 (join next e2 e4))) ;; unprovable with efficient (/axioms) -;; ;; in e2 branch -;; ;; (assert (not (R next e4 e2 null))) ;; -;; ;; the auxillary join -;; ;; (assert (= (join next2 e1 e4) null)) - - -;; ;;to prove -;; (assert (not (= (join next2 e3 e4) null))) - - -;;==================== -;; ;;Thomas' example wrong sat? -;;==================== - -;; (assert (not (=> (and -;; (= (join next e1 e2) null) -;; (R next e2 null null) -;; (not (= e2 null)) -;; (= next2 (store next e2 e1)) -;; ) -;; (= (join next2 e1 e2) null) -;; ) -;; ) -;; ) - -;;==================== -;; ;;example4 sat -;;==================== - -;; (assert (not (=> (and -;; (= (join next e1 e2) null) -;; (R next e2 null null) (not (= e2 null)) -;; ) -;; (not (R next e2 e2 e2)) -;; ))) - - -;;==================== -;;example5 unsat -;;==================== - -;; (assert (and -;; ;; (= (join e1 e2) null) -;; (= (select next (select next e1)) e1) -;; (R next e1 e2 e2) -;; (not (= e2 e1)) -;; (not (= e2 (select next e1))) -;; ) -;; ) - -;;==================== -;; ;; example 6 unsat -;;==================== - -;; ;; join is the nearest junction point -;; (assert (and (not (= e3 (join next e1 e2))) -;; (R next e1 e3 (join next e1 e2)) -;; (R next e2 e3 (join next e1 e2)) -;; )) - - -;;==================== -;; example7 unsat -;;==================== - -;; (assert (R next e1 e2 (select next e1))) -;; (assert (not (= e1 e2))) -;; (assert (not (= e2 (select next e1)))) - - - -(check-sat) -(exit) - diff --git a/test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2 b/test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2 deleted file mode 100644 index 92103238c..000000000 --- a/test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2 +++ /dev/null @@ -1,211 +0,0 @@ -;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer -(set-logic AUFLIA) -(set-info :status unsat) - -(declare-sort elt 0) - -(declare-fun f (elt) elt) -(declare-fun Rf (elt elt elt) Bool) - -;; reflexive -;;(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) ) -;; step -(assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((f ?x))) ) -;; (assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((Rf ?x (f ?x) (f ?x)))) ) -;; (assert-propagation ((?x elt)) () () (=> true (Rf ?x (f ?x) (f ?x))) (((f ?x))) ) - -;; reach -(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) (((f ?x1))) ) -;; ;; reach extended -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((not (= ?x1 ?x2))(Rf ?x1 ?x2 ?x2)) () (Rf ?x1 (f ?x1) ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) -;; ;; reach extended -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((not (Rf ?x1 (f ?x1) ?x2))(Rf ?x1 ?x2 ?x2)) () (= ?x1 ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) - -;; cycle -(assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((f ?x1))) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) () ) - -;; (assert-propagation ((?x1 elt)(?x2 elt)) () () (=> (and (= (f ?x1) ?x1) (Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x2)(f ?x1))) ) - -;; sandwich -(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) () ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) () () (=> (Rf ?x1 ?x2 ?x1) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x1))) ) - -;; order1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () - ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) () ) - -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () -;; (=> (and (Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2))) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) - -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x3))) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x3 ?x2))) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x3 ?x2))) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x2 ?x3))) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) -;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) - -;; order2 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x3)) - (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) () ) -;; transitive1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3)) - (Rf ?x1 ?x3 ?x3) () ) -;; ;; transitive1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((not (Rf ?x1 ?x3 ?x3))(Rf ?x2 ?x3 ?x3)) -;; (not (Rf ?x1 ?x2 ?x2)) () ) -;; ;; transitive1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(not (Rf ?x1 ?x3 ?x3))) -;; (not (Rf ?x2 ?x3 ?x3)) () ) - -;;transitive2 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) - (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) () ) - -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () -;; (=> (and (Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) -;; (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2))) -;; (((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2))) ) - -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((not (Rf ?x0 ?x1 ?x3))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) (((Rf ?x0 ?x1 ?x2))) ) -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x1 ?x3))) -;; (not (Rf ?x1 ?x3 ?x2)) (((Rf ?x1 ?x3 ?x2))) ) -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((not (Rf ?x0 ?x3 ?x2))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) (((Rf ?x0 ?x1 ?x2))) ) -;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x3 ?x2))) -;; (not (Rf ?x1 ?x3 ?x2)) (((Rf ?x1 ?x3 ?x2))) ) - -;; ;;transitive3 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) - (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) () ) - -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () -;; (=> (and (Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) -;; (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2))) (((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1))) ) - - -(declare-fun e1 () elt) -(declare-fun e2 () elt) -(declare-fun e3 () elt) -(declare-fun e4 () elt) - - -;;Example0 -;;(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3))) ) - -;;Thomas' example1 x,e1 y,e2 z,e3 y',e4 -;;(assert (not (=> (and (Rf e1 e2 e3) (not (= e2 e3)) (= e4 (f e2))) (Rf e1 e4 e3)))) - -(declare-fun Rf_avoid (elt elt elt) Bool) - -;; (assert-rewrite ((?x0 elt)(?x1 elt)(?exc elt)) () (Rf_avoid ?x0 ?x1 ?exc) -;; (or (Rf ?x0 ?x1 ?exc) (and (Rf ?x0 ?x1 ?x1) (not (Rf ?x0 ?exc ?exc)))) () ) - -(declare-fun null () elt) -(assert (= (f null) null)) - -(declare-fun join (elt elt) elt) - -;; (assert-propagation ((?x elt)(?y elt)(?z elt)) () ((Rf ?x ?z ?z)(Rf ?y ?z ?z)) (Rf ?x (join ?x ?y) ?z) (((join ?x ?y))) ) -;; (assert-propagation ((?x elt)(?y elt)) () () (or (and (Rf ?x (join ?x ?y) (join ?x ?y)) (Rf ?y (join ?x ?y) (join ?x ?y))) (= (join ?x ?y) null)) (((join ?x ?y))) ) - -;;Thomas' example2 -;; (assert (not (=> (and (Rf e1 null null) (= (join e1 e2) null) -;; ;; (next' == upd(next, e, e1) -;; ) -;; ;; (reach(next', e1, null) ) -;; (or (and (Rf e1 null null) (Rf_avoid e1 null e2) ) -;; (and (not (= e2 null)) (Rf_avoid e1 e2 null) (Rf e1 null e2) (Rf_avoid e1 null e2) ) -;; (and (not (= e2 null)) (Rf_avoid e1 e2 null) (Rf e1 null null) (Rf_avoid e1 null e2) ) ) -;; ))) - - -;;Thomas' example3 -;; join(next, first, e) == null && -;; reach(next, e, null) && -;; e != null && -;; next' == upd(next, e, first) && -;; first' == e && -;; e' == sel (next, e) -;; ==> -;; join(next', first', e') == null - - -;;Thomas' example3 -(assert(not - (=> - (and - ;; (= (join e1 e2) null) - (Rf e2 null null) - (not (= e2 null))) - ;; (next' == upd(next, e2, e1) - ;;join(next',e1,e2) == null -(or (and (not (Rf (f e2) e2 e2)) (not (Rf e1 e2 e2) )) -;; (and (Rf (f e2) e2 e2) (not (Rf e1 e1 e1) )) - (and (Rf e1 e2 e2) (not (Rf (f e2) e1 e1)) ) -) -;; (or -;; (and (not (Rf e1 e2 e2)) (not (Rf e2 e2 e2))) -;; (and (Rf e1 e2 e2) (not (Rf e2 e1 e1))) -;; (and (Rf e2 e2 e2) (not (Rf e1 e1 e1))) -;; ) -))) - - - -;; ;;Thomas' example wrong sat? -;; (assert (not (=> (and -;; (= (join e1 e2) null) -;; (Rf e2 null null) (not (= e2 null))) -;; ;; (next' == upd(next, e2, e1) -;; ;;join(next',e1,e2) == null -;; (not (Rf e2 e2 e2)) -;; ;; (or -;; ;; (and (not (Rf e1 e2 e2)) (not (Rf e2 e2 e2))) -;; ;; (and (Rf e1 e2 e2) (not (Rf e2 e1 e1))) -;; ;; (and (Rf e2 e2 e2) (not (Rf e1 e1 e1))) -;; ;; ) -;; ))) - -;; ;;example4 -;; (assert (not (=> (and -;; (= (join e1 e2) null) -;; (Rf e2 null null) (not (= e2 null)) -;; ) -;; (not (Rf e2 e2 e2)) -;; ))) - - -;; ;;example5 -;; (assert (and -;; ;; (= (join e1 e2) null) -;; (= (f (f e1)) e1) -;; (Rf e1 e2 e2) -;; (not (= e2 e1)) -;; (not (= e2 (f e1))) -;; ) -;; ) - - - - -(check-sat) -(exit) - diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 deleted file mode 100644 index 9bd49f714..000000000 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 +++ /dev/null @@ -1,126 +0,0 @@ -;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort elt 0) -(declare-sort set 0) - -(declare-fun in (elt set) Bool) - -;;;;;;;;;;;;;;;;;;;; -;; inter - -(declare-fun inter (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) - - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;;; -;; union - -(declare-fun union (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) - -;;;;;;;;;;;;;;;;;;;; -;; diff - -(declare-fun diff (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;; -;;sing - -(declare-fun sing (elt) set) -(assert-propagation ((?s elt)) - (((sing ?s))) () () (in ?s (sing ?s)) ) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((in ?s (sing ?t1))) (= ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) - -;;;;;;;;;;;;;;;;;;; -;; fullfiling runned at Full effort -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) - -(assert-propagation ((?t1 set) (?t2 set)) - () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) - -;;;;;;;;;;;;;;;;;;; -;; shortcut -(declare-fun subset (set set) Bool) -(assert-reduction ((?t1 set) (?t2 set)) - () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) - -(declare-fun e () elt) -(declare-fun t1 () set) -(declare-fun t2 () set) -(declare-fun t3 () set) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) -;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) - -;; hyp -;;(assert (=> (in e (union t1 t1)) (in e t1))) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) - -;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) ) -(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) ) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 deleted file mode 100644 index 4d65ffac5..000000000 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ /dev/null @@ -1,127 +0,0 @@ -;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba -(set-logic AUFLIA) -(set-info :status sat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort elt 0) -(declare-sort set 0) - -(declare-fun in (elt set) Bool) - - -;;;;;;;;;;;;;;;;;;;; -;; inter - -(declare-fun inter (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) - - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;;; -;; union - -(declare-fun union (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) - -;;;;;;;;;;;;;;;;;;;; -;; diff - -(declare-fun diff (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;; -;;sing - -(declare-fun sing (elt) set) -(assert-propagation ((?s elt)) - (((sing ?s))) () () (in ?s (sing ?s)) ) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((in ?s (sing ?t1))) (= ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) - -;;;;;;;;;;;;;;;;;;; -;; fullfiling runned at Full effort -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) - -(assert-propagation ((?t1 set) (?t2 set)) - () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) - -;;;;;;;;;;;;;;;;;;; -;; shortcut -(declare-fun subset (set set) Bool) -(assert-reduction ((?t1 set) (?t2 set)) - () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) - -(declare-fun e () elt) -(declare-fun t1 () set) -(declare-fun t2 () set) -(declare-fun t3 () set) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) -;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) - -;; hyp -;;(assert (=> (in e (union t1 t1)) (in e t1))) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) - -(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) ) - - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/test_efficient_ematching.smt2 b/test/regress/regress0/rewriterules/test_efficient_ematching.smt2 deleted file mode 100644 index e91ef36c2..000000000 --- a/test/regress/regress0/rewriterules/test_efficient_ematching.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort elt 0) - -(declare-fun R (elt elt) Bool) - -;; reflexive -(assert-rewrite ((x elt)) () (R x x) true ()) - -;; transitive -(assert-propagation ((x elt) (y elt) (z elt)) () ((R x y) (R y z)) (R x z) ()) - -;; anti-symmetric -(assert-propagation ((x elt) (y elt)) () ((R x y) (R y x)) (= x y) ()) - -(declare-fun f (elt) elt) -(assert-propagation ((x elt)(y elt)) () ((R (f x) (f y))) (R x y) ()) - - -(declare-fun e1 () elt) -(declare-fun e2 () elt) -(declare-fun e3 () elt) -(declare-fun e4 () elt) -(declare-fun e5 () elt) - -(assert (not (=> (and (R e1 e2) (R e3 (f e4)) (R e4 e5) - (or (and (= e3 (f e2)) (= e4 e1)) - (and (= e4 e2) (= e5 e1)) ) - ) (= e1 e2)))) - -(check-sat) - -(exit)
\ No newline at end of file diff --git a/test/regress/regress0/rewriterules/test_guards.smt2 b/test/regress/regress0/rewriterules/test_guards.smt2 deleted file mode 100644 index 98c845fb5..000000000 --- a/test/regress/regress0/rewriterules/test_guards.smt2 +++ /dev/null @@ -1,45 +0,0 @@ -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) -;; don't use arith -(declare-sort mynat 0) -(declare-fun zero () mynat) -(declare-fun succ (mynat) mynat) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) -(declare-fun p (list) Bool) - - -;;define length -(declare-fun length (list) mynat) - -(assert (= (length nil) zero)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) - -(declare-fun ten_one_cons (list) list) - -(assert (forall ((?l list)) (! (=> (p ?l) (= (ten_one_cons ?l) - (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) - )) :rewrite-rule))) - -(declare-fun a () Bool) -(declare-fun b () Bool) -(declare-fun c () Bool) - -(assert (=> a (p nil)) ) -(assert (=> b (p nil)) ) -(assert (or a b)) - -(assert (not (= (length (ten_one_cons nil)) - (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero))))))))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 deleted file mode 100644 index 4d39e12bb..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 +++ /dev/null @@ -1,492 +0,0 @@ -;;; From a verification condition generated by why3. The original program -;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . -;; The problem has been modified by doubling the size of the arrays -;; (* **) -;; VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html **) -;; Problem 1: maximum /\ sum of an array **) - -;; Author: Jean-Christophe Filliatre (CNRS) **) -;; Tool: Why3 (see http://why3.lri.fr/) **) -;; *\) **) - -;; Particularly the assertion in the test case that the sum s = 90 - -;;; this is a prelude for CVC4 -(set-logic AUFNIRA) -;;; this is a prelude for CVC4 integer arithmetic -(declare-sort uni 0) - -(declare-sort deco 0) - -(declare-sort ty 0) - -(declare-fun sort (ty uni) deco) - -(declare-fun int () ty) - -(declare-fun real () ty) - -(declare-fun bool () ty) - -(declare-fun True () uni) - -(declare-fun False () uni) - -(declare-fun match_bool (deco deco deco) uni) - -;; match_bool_True - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool True) (sort a z) (sort a z1))) (sort a z))))) - -;; match_bool_False - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool False) (sort a z) (sort a z1))) (sort a - z1))))) - -(declare-fun index_bool (deco) Int) - -;; index_bool_True - (assert (= (index_bool (sort bool True)) 0)) - -;; index_bool_False - (assert (= (index_bool (sort bool False)) 1)) - -;; bool_inversion - (assert - (forall ((u uni)) - (or (= (sort bool u) (sort bool True)) (= (sort bool u) (sort bool False))))) - -(declare-fun tuple0 () ty) - -(declare-fun Tuple0 () uni) - -;; tuple0_inversion - (assert (forall ((u uni)) (= (sort tuple0 u) (sort tuple0 Tuple0)))) - -;; CompatOrderMult - (assert - (forall ((x Int) (y Int) (z Int)) - (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z)))))) - -(declare-fun ref (ty) ty) - -(declare-fun mk_ref (deco) uni) - -(declare-fun contents (deco) uni) - -;; contents_def - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort a (contents (sort (ref a) (mk_ref (sort a u))))) (sort a u))))) - -;; ref_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (ref a) u) (sort (ref a) - (mk_ref (sort a (contents (sort (ref a) u))))))))) - -(declare-fun map (ty ty) ty) - -(declare-fun get (deco deco) uni) - -(declare-fun set (deco deco deco) uni) - -;; Select_eq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (= a1 a2) (= (select (store m a1 b) a2) b)) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_eq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (= (sort a a1) (sort a a2)) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b b1))) :pattern ((sort b - (get - (sort (map a b) - (set (sort (map a b) m) - (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -;; Select_neq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (not (= a1 a2)) (= (select (store m a1 b) a2) (select m a2))) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_neq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (not (= (sort a a1) (sort a a2))) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b (get (sort (map a b) m) (sort a a2))))) :pattern ( - (sort b - (get (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -(declare-fun const1 (deco) uni) - -(declare-fun const2 (Int) (Array Int Int)) - -;; Const - (assert (forall ((b Int) (a Int)) (= (select (const2 b) a) b))) - -;; Const - (assert - (forall ((a ty) (b ty)) - (forall ((b1 uni) (a1 uni)) - (= (sort b (get (sort (map a b) (const1 (sort b b1))) (sort a a1))) - (sort b b1))))) - -(declare-sort array 1) - -(declare-fun array1 (ty) ty) - -(declare-fun mk_array (Int deco) uni) - -(declare-fun mk_array1 (Int (Array Int Int)) (array Int)) - -(declare-fun length (deco) Int) - -(declare-fun t2tb ((array Int)) uni) - -(declare-fun tb2t (deco) (array Int)) - -;; BridgeL - (assert - (forall ((i (array Int))) - (! (= (tb2t (sort (array1 int) (t2tb i))) i) :pattern ((sort (array1 int) - (t2tb i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (array1 int) (t2tb (tb2t (sort (array1 int) j)))) (sort - (array1 int) - j)) :pattern ( - (sort (array1 int) (t2tb (tb2t (sort (array1 int) j))))) ))) - -;; length_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (length (sort (array1 int) (t2tb (mk_array1 u u1)))) u))) - -;; length_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (length (sort (array1 a) (mk_array u (sort (map int a) u1)))) u)))) - -(declare-fun elts (deco) uni) - -(declare-fun t2tb1 ((Array Int Int)) uni) - -(declare-fun tb2t1 (deco) (Array Int Int)) - -;; BridgeL - (assert - (forall ((i (Array Int Int))) - (! (= (tb2t1 (sort (map int int) (t2tb1 i))) i) :pattern ((sort - (map int int) - (t2tb1 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j)))) (sort - (map - int - int) j)) :pattern ( - (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j))))) ))) - -;; elts_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb (mk_array1 u u1)))))) u1))) - -;; elts_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (sort (map int a) - (elts (sort (array1 a) (mk_array u (sort (map int a) u1))))) (sort - (map int a) - u1))))) - -;; array_inversion - (assert - (forall ((u (array Int))) - (= u (mk_array1 (length (sort (array1 int) (t2tb u))) - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb u))))))))) - -;; array_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (array1 a) u) (sort (array1 a) - (mk_array (length (sort (array1 a) u)) - (sort (map int a) (elts (sort (array1 a) u))))))))) - -(declare-fun get1 (deco Int) uni) - -(declare-fun t2tb2 (Int) uni) - -(declare-fun tb2t2 (deco) Int) - -;; BridgeL - (assert - (forall ((i Int)) - (! (= (tb2t2 (sort int (t2tb2 i))) i) :pattern ((sort int (t2tb2 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort int (t2tb2 (tb2t2 (sort int j)))) (sort int j)) :pattern ( - (sort int (t2tb2 (tb2t2 (sort int j))))) ))) - -;; get_def - (assert - (forall ((a (array Int)) (i Int)) - (= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) i))) (select - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb a))))) i)))) - -;; get_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int)) - (= (sort a (get1 (sort (array1 a) a1) i)) (sort a - (get - (sort (map int a) - (elts (sort (array1 a) a1))) - (sort int (t2tb2 i)))))))) - -(declare-fun set1 (deco Int deco) uni) - -;; set_def - (assert - (forall ((a (array Int)) (i Int) (v Int)) - (= (tb2t - (sort (array1 int) - (set1 (sort (array1 int) (t2tb a)) i (sort int (t2tb2 v))))) (mk_array1 - (length - (sort - (array1 - int) - (t2tb a))) - (store - (tb2t1 - (sort - (map - int - int) - (elts - (sort - (array1 - int) - (t2tb a))))) i v))))) - -;; set_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int) (v uni)) - (= (sort (array1 a) (set1 (sort (array1 a) a1) i (sort a v))) (sort - (array1 a) - (mk_array - (length - (sort - (array1 a) - a1)) - (sort - (map int a) - (set - (sort - (map int a) - (elts - (sort - (array1 a) - a1))) - (sort - int - (t2tb2 i)) - (sort a v))))))))) - -(declare-fun make (Int deco) uni) - -;; make_def - (assert - (forall ((n Int) (v Int)) - (= (tb2t (sort (array1 int) (make n (sort int (t2tb2 v))))) (mk_array1 n - (const2 v))))) - -;; make_def - (assert - (forall ((a ty)) - (forall ((n Int) (v uni)) - (= (sort (array1 a) (make n (sort a v))) (sort (array1 a) - (mk_array n - (sort (map int a) - (const1 (sort a v))))))))) - -(declare-fun sum ((Array Int Int) Int Int) Int) - -;; Sum_def_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (<= j i) (= (sum c i j) 0)))) - -;; Sum_def_non_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (select c i) (sum c (+ i 1) j)))))) - -;; Sum_right_extension - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1))))))) - -;; Sum_transitivity - (assert - (forall ((c (Array Int Int)) (i Int) (k Int) (j Int)) - (=> (and (<= i k) (<= k j)) (= (sum c i j) (+ (sum c i k) (sum c k j)))))) - -;; Sum_eq - (assert - (forall ((c1 (Array Int Int)) (c2 (Array Int Int)) (i Int) (j Int)) - (=> - (forall ((k Int)) - (=> (and (<= i k) (< k j)) (= (select c1 k) (select c2 k)))) - (= (sum c1 i j) (sum c2 i j))))) - -(declare-fun sum1 ((array Int) Int Int) Int) - -;; sum_def - (assert - (forall ((a (array Int)) (l Int) (h Int)) - (= (sum1 a l h) (sum - (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb a))))) l - h)))) - -(declare-fun is_max ((array Int) Int Int Int) Bool) - -;; is_max_def - (assert - (forall ((a (array Int)) (l Int) (h Int) (m Int)) - (and - (=> (is_max a l h m) - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k)))))))))) - (=> - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))) (is_max - a l h m))))) - -(assert -;; WP_parameter_test_case - ;; File "vstte10_max_sum/../vstte10_max_sum.mlw", line 63, characters 6-15 - (not - (=> (<= 0 20) - (=> (and (<= 0 0) (< 0 20)) - (forall ((a (Array Int Int))) - (=> (= a (store (const2 0) 0 9)) - (=> (and (<= 0 1) (< 1 20)) - (forall ((a1 (Array Int Int))) - (=> (= a1 (store a 1 5)) - (=> (and (<= 0 2) (< 2 20)) - (forall ((a2 (Array Int Int))) - (=> (= a2 (store a1 2 0)) - (=> (and (<= 0 3) (< 3 20)) - (forall ((a3 (Array Int Int))) - (=> (= a3 (store a2 3 2)) - (=> (and (<= 0 4) (< 4 20)) - (forall ((a4 (Array Int Int))) - (=> (= a4 (store a3 4 7)) - (=> (and (<= 0 5) (< 5 20)) - (forall ((a5 (Array Int Int))) - (=> (= a5 (store a4 5 3)) - (=> (and (<= 0 6) (< 6 20)) - (forall ((a6 (Array Int Int))) - (=> (= a6 (store a5 6 2)) - (=> (and (<= 0 7) (< 7 20)) - (forall ((a7 (Array Int Int))) - (=> (= a7 (store a6 7 1)) - (=> (and (<= 0 8) (< 8 20)) - (forall ((a8 (Array Int Int))) - (=> (= a8 (store a7 8 10)) - (=> (and (<= 0 9) (< 9 20)) - (forall ((a9 (Array Int Int))) - (=> (= a9 (store a8 9 6)) - (=> (and (<= 0 10) (< 10 20)) - (forall ((a10 (Array Int Int))) - (=> (= a10 (store a9 10 9)) - (=> (and (<= 0 11) (< 11 20)) - (forall ((a11 (Array Int Int))) - (=> (= a11 (store a10 11 5)) - (=> (and (<= 0 12) (< 12 20)) - (forall ((a12 (Array Int Int))) - (=> (= a12 (store a11 12 0)) - (=> (and (<= 0 13) (< 13 20)) - (forall ((a13 (Array Int Int))) - (=> (= a13 (store a12 13 2)) - (=> (and (<= 0 14) (< 14 20)) - (forall ((a14 (Array Int Int))) - (=> (= a14 (store a13 14 7)) - (=> (and (<= 0 15) (< 15 20)) - (forall ((a15 (Array Int Int))) - (=> (= a15 (store a14 15 3)) - (=> (and (<= 0 16) (< 16 20)) - (forall ((a16 (Array Int Int))) - (=> (= a16 (store a15 16 2)) - (=> (and (<= 0 17) (< 17 20)) - (forall ((a17 (Array Int Int))) - (=> (= a17 (store a16 17 1)) - (=> (and (<= 0 18) (< 18 20)) - (forall ((a18 (Array Int Int))) - (=> (= a18 (store a17 18 10)) - (=> (and (<= 0 19) (< 19 20)) - (forall ((a19 (Array Int Int))) - (=> (= a19 (store a18 19 6)) - (=> - (and (<= 0 20) - (forall ((i Int)) (=> (and (<= 0 i) (< i 20)) (<= 0 (select a19 i))))) - (forall ((result Int) (result1 Int)) - (=> - (and (= result (sum a19 0 20)) - (and (is_max (mk_array1 20 a19) 0 20 result1) (<= result (* 20 result1)))) - (= result 90))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -(check-sat) - diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 deleted file mode 100644 index 686b9ff04..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 +++ /dev/null @@ -1,508 +0,0 @@ -;;; From a verification condition generated by why3. The original program -;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . -;; The problem has been modified by doubling the size of the arrays -;; (* **) -;; VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html **) -;; Problem 1: maximum /\ sum of an array **) - -;; Author: Jean-Christophe Filliatre (CNRS) **) -;; Tool: Why3 (see http://why3.lri.fr/) **) -;; *\) **) - -;; Particularly the assertion in the test case that the sum s = 90 - -;; Added rewriterules: - -;; (assert-propagation ((c (Array Int Int)) (i Int) (j Int)) ((>= i j)) -;; () (= (sum c i j) 0) (((sum c i j)))) - -;; (assert-propagation ((c (Array Int Int)) (i Int) (j Int)) ((< i j)) -;; () (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1)))) (((sum c i j)))) - - - -;;; this is a prelude for CVC4 -(set-logic AUFNIRA) -;;; this is a prelude for CVC4 integer arithmetic -(declare-sort uni 0) - -(declare-sort deco 0) - -(declare-sort ty 0) - -(declare-fun sort (ty uni) deco) - -(declare-fun int () ty) - -(declare-fun real () ty) - -(declare-fun bool () ty) - -(declare-fun True () uni) - -(declare-fun False () uni) - -(declare-fun match_bool (deco deco deco) uni) - -;; match_bool_True - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool True) (sort a z) (sort a z1))) (sort a z))))) - -;; match_bool_False - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool False) (sort a z) (sort a z1))) (sort a - z1))))) - -(declare-fun index_bool (deco) Int) - -;; index_bool_True - (assert (= (index_bool (sort bool True)) 0)) - -;; index_bool_False - (assert (= (index_bool (sort bool False)) 1)) - -;; bool_inversion - (assert - (forall ((u uni)) - (or (= (sort bool u) (sort bool True)) (= (sort bool u) (sort bool False))))) - -(declare-fun tuple0 () ty) - -(declare-fun Tuple0 () uni) - -;; tuple0_inversion - (assert (forall ((u uni)) (= (sort tuple0 u) (sort tuple0 Tuple0)))) - -;; CompatOrderMult - (assert - (forall ((x Int) (y Int) (z Int)) - (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z)))))) - -(declare-fun ref (ty) ty) - -(declare-fun mk_ref (deco) uni) - -(declare-fun contents (deco) uni) - -;; contents_def - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort a (contents (sort (ref a) (mk_ref (sort a u))))) (sort a u))))) - -;; ref_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (ref a) u) (sort (ref a) - (mk_ref (sort a (contents (sort (ref a) u))))))))) - -(declare-fun map (ty ty) ty) - -(declare-fun get (deco deco) uni) - -(declare-fun set (deco deco deco) uni) - -;; Select_eq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (= a1 a2) (= (select (store m a1 b) a2) b)) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_eq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (= (sort a a1) (sort a a2)) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b b1))) :pattern ((sort b - (get - (sort (map a b) - (set (sort (map a b) m) - (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -;; Select_neq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (not (= a1 a2)) (= (select (store m a1 b) a2) (select m a2))) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_neq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (not (= (sort a a1) (sort a a2))) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b (get (sort (map a b) m) (sort a a2))))) :pattern ( - (sort b - (get (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -(declare-fun const1 (deco) uni) - -(declare-fun const2 (Int) (Array Int Int)) - -;; Const - (assert (forall ((b Int) (a Int)) (= (select (const2 b) a) b))) - -;; Const - (assert - (forall ((a ty) (b ty)) - (forall ((b1 uni) (a1 uni)) - (= (sort b (get (sort (map a b) (const1 (sort b b1))) (sort a a1))) - (sort b b1))))) - -(declare-sort array 1) - -(declare-fun array1 (ty) ty) - -(declare-fun mk_array (Int deco) uni) - -(declare-fun mk_array1 (Int (Array Int Int)) (array Int)) - -(declare-fun length (deco) Int) - -(declare-fun t2tb ((array Int)) uni) - -(declare-fun tb2t (deco) (array Int)) - -;; BridgeL - (assert - (forall ((i (array Int))) - (! (= (tb2t (sort (array1 int) (t2tb i))) i) :pattern ((sort (array1 int) - (t2tb i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (array1 int) (t2tb (tb2t (sort (array1 int) j)))) (sort - (array1 int) - j)) :pattern ( - (sort (array1 int) (t2tb (tb2t (sort (array1 int) j))))) ))) - -;; length_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (length (sort (array1 int) (t2tb (mk_array1 u u1)))) u))) - -;; length_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (length (sort (array1 a) (mk_array u (sort (map int a) u1)))) u)))) - -(declare-fun elts (deco) uni) - -(declare-fun t2tb1 ((Array Int Int)) uni) - -(declare-fun tb2t1 (deco) (Array Int Int)) - -;; BridgeL - (assert - (forall ((i (Array Int Int))) - (! (= (tb2t1 (sort (map int int) (t2tb1 i))) i) :pattern ((sort - (map int int) - (t2tb1 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j)))) (sort - (map - int - int) j)) :pattern ( - (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j))))) ))) - -;; elts_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb (mk_array1 u u1)))))) u1))) - -;; elts_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (sort (map int a) - (elts (sort (array1 a) (mk_array u (sort (map int a) u1))))) (sort - (map int a) - u1))))) - -;; array_inversion - (assert - (forall ((u (array Int))) - (= u (mk_array1 (length (sort (array1 int) (t2tb u))) - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb u))))))))) - -;; array_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (array1 a) u) (sort (array1 a) - (mk_array (length (sort (array1 a) u)) - (sort (map int a) (elts (sort (array1 a) u))))))))) - -(declare-fun get1 (deco Int) uni) - -(declare-fun t2tb2 (Int) uni) - -(declare-fun tb2t2 (deco) Int) - -;; BridgeL - (assert - (forall ((i Int)) - (! (= (tb2t2 (sort int (t2tb2 i))) i) :pattern ((sort int (t2tb2 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort int (t2tb2 (tb2t2 (sort int j)))) (sort int j)) :pattern ( - (sort int (t2tb2 (tb2t2 (sort int j))))) ))) - -;; get_def - (assert - (forall ((a (array Int)) (i Int)) - (= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) i))) (select - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb a))))) i)))) - -;; get_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int)) - (= (sort a (get1 (sort (array1 a) a1) i)) (sort a - (get - (sort (map int a) - (elts (sort (array1 a) a1))) - (sort int (t2tb2 i)))))))) - -(declare-fun set1 (deco Int deco) uni) - -;; set_def - (assert - (forall ((a (array Int)) (i Int) (v Int)) - (= (tb2t - (sort (array1 int) - (set1 (sort (array1 int) (t2tb a)) i (sort int (t2tb2 v))))) (mk_array1 - (length - (sort - (array1 - int) - (t2tb a))) - (store - (tb2t1 - (sort - (map - int - int) - (elts - (sort - (array1 - int) - (t2tb a))))) i v))))) - -;; set_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int) (v uni)) - (= (sort (array1 a) (set1 (sort (array1 a) a1) i (sort a v))) (sort - (array1 a) - (mk_array - (length - (sort - (array1 a) - a1)) - (sort - (map int a) - (set - (sort - (map int a) - (elts - (sort - (array1 a) - a1))) - (sort - int - (t2tb2 i)) - (sort a v))))))))) - -(declare-fun make (Int deco) uni) - -;; make_def - (assert - (forall ((n Int) (v Int)) - (= (tb2t (sort (array1 int) (make n (sort int (t2tb2 v))))) (mk_array1 n - (const2 v))))) - -;; make_def - (assert - (forall ((a ty)) - (forall ((n Int) (v uni)) - (= (sort (array1 a) (make n (sort a v))) (sort (array1 a) - (mk_array n - (sort (map int a) - (const1 (sort a v))))))))) - -(declare-fun sum ((Array Int Int) Int Int) Int) - -;; Sum_def_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (<= j i) (= (sum c i j) 0)))) - -;; Sum_def_non_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (select c i) (sum c (+ i 1) j)))))) - -;; Sum_right_extension - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1))))))) - -;; Sum_transitivity - (assert - (forall ((c (Array Int Int)) (i Int) (k Int) (j Int)) - (=> (and (<= i k) (<= k j)) (= (sum c i j) (+ (sum c i k) (sum c k j)))))) - -;; Sum_eq - (assert - (forall ((c1 (Array Int Int)) (c2 (Array Int Int)) (i Int) (j Int)) - (=> - (forall ((k Int)) - (=> (and (<= i k) (< k j)) (= (select c1 k) (select c2 k)))) - (= (sum c1 i j) (sum c2 i j))))) - - (assert-propagation ((c (Array Int Int)) (i Int) (j Int)) ((>= i j)) - () (= (sum c i j) 0) (((sum c i j)))) - - (assert-propagation ((c (Array Int Int)) (i Int) (j Int)) ((< i j)) - () (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1)))) (((sum c i j)))) - -(declare-fun sum1 ((array Int) Int Int) Int) - -;; sum_def - (assert - (forall ((a (array Int)) (l Int) (h Int)) - (= (sum1 a l h) (sum - (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb a))))) l - h)))) - -(declare-fun is_max ((array Int) Int Int Int) Bool) - -;; is_max_def - (assert - (forall ((a (array Int)) (l Int) (h Int) (m Int)) - (and - (=> (is_max a l h m) - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k)))))))))) - (=> - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))) (is_max - a l h m))))) - -(assert -;; WP_parameter_test_case - ;; File "vstte10_max_sum/../vstte10_max_sum.mlw", line 63, characters 6-15 - (not - (=> (<= 0 20) - (=> (and (<= 0 0) (< 0 20)) - (forall ((a (Array Int Int))) - (=> (= a (store (const2 0) 0 9)) - (=> (and (<= 0 1) (< 1 20)) - (forall ((a1 (Array Int Int))) - (=> (= a1 (store a 1 5)) - (=> (and (<= 0 2) (< 2 20)) - (forall ((a2 (Array Int Int))) - (=> (= a2 (store a1 2 0)) - (=> (and (<= 0 3) (< 3 20)) - (forall ((a3 (Array Int Int))) - (=> (= a3 (store a2 3 2)) - (=> (and (<= 0 4) (< 4 20)) - (forall ((a4 (Array Int Int))) - (=> (= a4 (store a3 4 7)) - (=> (and (<= 0 5) (< 5 20)) - (forall ((a5 (Array Int Int))) - (=> (= a5 (store a4 5 3)) - (=> (and (<= 0 6) (< 6 20)) - (forall ((a6 (Array Int Int))) - (=> (= a6 (store a5 6 2)) - (=> (and (<= 0 7) (< 7 20)) - (forall ((a7 (Array Int Int))) - (=> (= a7 (store a6 7 1)) - (=> (and (<= 0 8) (< 8 20)) - (forall ((a8 (Array Int Int))) - (=> (= a8 (store a7 8 10)) - (=> (and (<= 0 9) (< 9 20)) - (forall ((a9 (Array Int Int))) - (=> (= a9 (store a8 9 6)) - (=> (and (<= 0 10) (< 10 20)) - (forall ((a10 (Array Int Int))) - (=> (= a10 (store a9 10 9)) - (=> (and (<= 0 11) (< 11 20)) - (forall ((a11 (Array Int Int))) - (=> (= a11 (store a10 11 5)) - (=> (and (<= 0 12) (< 12 20)) - (forall ((a12 (Array Int Int))) - (=> (= a12 (store a11 12 0)) - (=> (and (<= 0 13) (< 13 20)) - (forall ((a13 (Array Int Int))) - (=> (= a13 (store a12 13 2)) - (=> (and (<= 0 14) (< 14 20)) - (forall ((a14 (Array Int Int))) - (=> (= a14 (store a13 14 7)) - (=> (and (<= 0 15) (< 15 20)) - (forall ((a15 (Array Int Int))) - (=> (= a15 (store a14 15 3)) - (=> (and (<= 0 16) (< 16 20)) - (forall ((a16 (Array Int Int))) - (=> (= a16 (store a15 16 2)) - (=> (and (<= 0 17) (< 17 20)) - (forall ((a17 (Array Int Int))) - (=> (= a17 (store a16 17 1)) - (=> (and (<= 0 18) (< 18 20)) - (forall ((a18 (Array Int Int))) - (=> (= a18 (store a17 18 10)) - (=> (and (<= 0 19) (< 19 20)) - (forall ((a19 (Array Int Int))) - (=> (= a19 (store a18 19 6)) - (=> - (and (<= 0 20) - (forall ((i Int)) (=> (and (<= 0 i) (< i 20)) (<= 0 (select a19 i))))) - (forall ((result Int) (result1 Int)) - (=> - (and (= result (sum a19 0 20)) - (and (is_max (mk_array1 20 a19) 0 20 result1) (<= result (* 20 result1)))) - (= result 90))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -(check-sat) - diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 deleted file mode 100644 index e468128ac..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 +++ /dev/null @@ -1,492 +0,0 @@ -;;; From a verification condition generated by why3. The original program -;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . -;; The problem has been modified by doubling the size of the arrays -;; (* **) -;; VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html **) -;; Problem 1: maximum /\ sum of an array **) - -;; Author: Jean-Christophe Filliatre (CNRS) **) -;; Tool: Why3 (see http://why3.lri.fr/) **) -;; *\) **) - -;; Particularly the assertion in the test case that the max m = 10 - -;;; this is a prelude for CVC4 -(set-logic AUFNIRA) -;;; this is a prelude for CVC4 integer arithmetic -(declare-sort uni 0) - -(declare-sort deco 0) - -(declare-sort ty 0) - -(declare-fun sort (ty uni) deco) - -(declare-fun int () ty) - -(declare-fun real () ty) - -(declare-fun bool () ty) - -(declare-fun True () uni) - -(declare-fun False () uni) - -(declare-fun match_bool (deco deco deco) uni) - -;; match_bool_True - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool True) (sort a z) (sort a z1))) (sort a z))))) - -;; match_bool_False - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool False) (sort a z) (sort a z1))) (sort a - z1))))) - -(declare-fun index_bool (deco) Int) - -;; index_bool_True - (assert (= (index_bool (sort bool True)) 0)) - -;; index_bool_False - (assert (= (index_bool (sort bool False)) 1)) - -;; bool_inversion - (assert - (forall ((u uni)) - (or (= (sort bool u) (sort bool True)) (= (sort bool u) (sort bool False))))) - -(declare-fun tuple0 () ty) - -(declare-fun Tuple0 () uni) - -;; tuple0_inversion - (assert (forall ((u uni)) (= (sort tuple0 u) (sort tuple0 Tuple0)))) - -;; CompatOrderMult - (assert - (forall ((x Int) (y Int) (z Int)) - (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z)))))) - -(declare-fun ref (ty) ty) - -(declare-fun mk_ref (deco) uni) - -(declare-fun contents (deco) uni) - -;; contents_def - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort a (contents (sort (ref a) (mk_ref (sort a u))))) (sort a u))))) - -;; ref_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (ref a) u) (sort (ref a) - (mk_ref (sort a (contents (sort (ref a) u))))))))) - -(declare-fun map (ty ty) ty) - -(declare-fun get (deco deco) uni) - -(declare-fun set (deco deco deco) uni) - -;; Select_eq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (= a1 a2) (= (select (store m a1 b) a2) b)) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_eq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (= (sort a a1) (sort a a2)) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b b1))) :pattern ((sort b - (get - (sort (map a b) - (set (sort (map a b) m) - (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -;; Select_neq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (not (= a1 a2)) (= (select (store m a1 b) a2) (select m a2))) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_neq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (not (= (sort a a1) (sort a a2))) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b (get (sort (map a b) m) (sort a a2))))) :pattern ( - (sort b - (get (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -(declare-fun const1 (deco) uni) - -(declare-fun const2 (Int) (Array Int Int)) - -;; Const - (assert (forall ((b Int) (a Int)) (= (select (const2 b) a) b))) - -;; Const - (assert - (forall ((a ty) (b ty)) - (forall ((b1 uni) (a1 uni)) - (= (sort b (get (sort (map a b) (const1 (sort b b1))) (sort a a1))) - (sort b b1))))) - -(declare-sort array 1) - -(declare-fun array1 (ty) ty) - -(declare-fun mk_array (Int deco) uni) - -(declare-fun mk_array1 (Int (Array Int Int)) (array Int)) - -(declare-fun length (deco) Int) - -(declare-fun t2tb ((array Int)) uni) - -(declare-fun tb2t (deco) (array Int)) - -;; BridgeL - (assert - (forall ((i (array Int))) - (! (= (tb2t (sort (array1 int) (t2tb i))) i) :pattern ((sort (array1 int) - (t2tb i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (array1 int) (t2tb (tb2t (sort (array1 int) j)))) (sort - (array1 int) - j)) :pattern ( - (sort (array1 int) (t2tb (tb2t (sort (array1 int) j))))) ))) - -;; length_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (length (sort (array1 int) (t2tb (mk_array1 u u1)))) u))) - -;; length_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (length (sort (array1 a) (mk_array u (sort (map int a) u1)))) u)))) - -(declare-fun elts (deco) uni) - -(declare-fun t2tb1 ((Array Int Int)) uni) - -(declare-fun tb2t1 (deco) (Array Int Int)) - -;; BridgeL - (assert - (forall ((i (Array Int Int))) - (! (= (tb2t1 (sort (map int int) (t2tb1 i))) i) :pattern ((sort - (map int int) - (t2tb1 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j)))) (sort - (map - int - int) j)) :pattern ( - (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j))))) ))) - -;; elts_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb (mk_array1 u u1)))))) u1))) - -;; elts_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (sort (map int a) - (elts (sort (array1 a) (mk_array u (sort (map int a) u1))))) (sort - (map int a) - u1))))) - -;; array_inversion - (assert - (forall ((u (array Int))) - (= u (mk_array1 (length (sort (array1 int) (t2tb u))) - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb u))))))))) - -;; array_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (array1 a) u) (sort (array1 a) - (mk_array (length (sort (array1 a) u)) - (sort (map int a) (elts (sort (array1 a) u))))))))) - -(declare-fun get1 (deco Int) uni) - -(declare-fun t2tb2 (Int) uni) - -(declare-fun tb2t2 (deco) Int) - -;; BridgeL - (assert - (forall ((i Int)) - (! (= (tb2t2 (sort int (t2tb2 i))) i) :pattern ((sort int (t2tb2 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort int (t2tb2 (tb2t2 (sort int j)))) (sort int j)) :pattern ( - (sort int (t2tb2 (tb2t2 (sort int j))))) ))) - -;; get_def - (assert - (forall ((a (array Int)) (i Int)) - (= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) i))) (select - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb a))))) i)))) - -;; get_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int)) - (= (sort a (get1 (sort (array1 a) a1) i)) (sort a - (get - (sort (map int a) - (elts (sort (array1 a) a1))) - (sort int (t2tb2 i)))))))) - -(declare-fun set1 (deco Int deco) uni) - -;; set_def - (assert - (forall ((a (array Int)) (i Int) (v Int)) - (= (tb2t - (sort (array1 int) - (set1 (sort (array1 int) (t2tb a)) i (sort int (t2tb2 v))))) (mk_array1 - (length - (sort - (array1 - int) - (t2tb a))) - (store - (tb2t1 - (sort - (map - int - int) - (elts - (sort - (array1 - int) - (t2tb a))))) i v))))) - -;; set_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int) (v uni)) - (= (sort (array1 a) (set1 (sort (array1 a) a1) i (sort a v))) (sort - (array1 a) - (mk_array - (length - (sort - (array1 a) - a1)) - (sort - (map int a) - (set - (sort - (map int a) - (elts - (sort - (array1 a) - a1))) - (sort - int - (t2tb2 i)) - (sort a v))))))))) - -(declare-fun make (Int deco) uni) - -;; make_def - (assert - (forall ((n Int) (v Int)) - (= (tb2t (sort (array1 int) (make n (sort int (t2tb2 v))))) (mk_array1 n - (const2 v))))) - -;; make_def - (assert - (forall ((a ty)) - (forall ((n Int) (v uni)) - (= (sort (array1 a) (make n (sort a v))) (sort (array1 a) - (mk_array n - (sort (map int a) - (const1 (sort a v))))))))) - -(declare-fun sum ((Array Int Int) Int Int) Int) - -;; Sum_def_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (<= j i) (= (sum c i j) 0)))) - -;; Sum_def_non_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (select c i) (sum c (+ i 1) j)))))) - -;; Sum_right_extension - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1))))))) - -;; Sum_transitivity - (assert - (forall ((c (Array Int Int)) (i Int) (k Int) (j Int)) - (=> (and (<= i k) (<= k j)) (= (sum c i j) (+ (sum c i k) (sum c k j)))))) - -;; Sum_eq - (assert - (forall ((c1 (Array Int Int)) (c2 (Array Int Int)) (i Int) (j Int)) - (=> - (forall ((k Int)) - (=> (and (<= i k) (< k j)) (= (select c1 k) (select c2 k)))) - (= (sum c1 i j) (sum c2 i j))))) - -(declare-fun sum1 ((array Int) Int Int) Int) - -;; sum_def - (assert - (forall ((a (array Int)) (l Int) (h Int)) - (= (sum1 a l h) (sum - (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb a))))) l - h)))) - -(declare-fun is_max ((array Int) Int Int Int) Bool) - -;; is_max_def - (assert - (forall ((a (array Int)) (l Int) (h Int) (m Int)) - (and - (=> (is_max a l h m) - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k)))))))))) - (=> - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))) (is_max - a l h m))))) - -(assert -;; WP_parameter_test_case - ;; File "vstte10_max_sum/../vstte10_max_sum.mlw", line 63, characters 6-15 - (not - (=> (<= 0 20) - (=> (and (<= 0 0) (< 0 20)) - (forall ((a (Array Int Int))) - (=> (= a (store (const2 0) 0 9)) - (=> (and (<= 0 1) (< 1 20)) - (forall ((a1 (Array Int Int))) - (=> (= a1 (store a 1 5)) - (=> (and (<= 0 2) (< 2 20)) - (forall ((a2 (Array Int Int))) - (=> (= a2 (store a1 2 0)) - (=> (and (<= 0 3) (< 3 20)) - (forall ((a3 (Array Int Int))) - (=> (= a3 (store a2 3 2)) - (=> (and (<= 0 4) (< 4 20)) - (forall ((a4 (Array Int Int))) - (=> (= a4 (store a3 4 7)) - (=> (and (<= 0 5) (< 5 20)) - (forall ((a5 (Array Int Int))) - (=> (= a5 (store a4 5 3)) - (=> (and (<= 0 6) (< 6 20)) - (forall ((a6 (Array Int Int))) - (=> (= a6 (store a5 6 2)) - (=> (and (<= 0 7) (< 7 20)) - (forall ((a7 (Array Int Int))) - (=> (= a7 (store a6 7 1)) - (=> (and (<= 0 8) (< 8 20)) - (forall ((a8 (Array Int Int))) - (=> (= a8 (store a7 8 10)) - (=> (and (<= 0 9) (< 9 20)) - (forall ((a9 (Array Int Int))) - (=> (= a9 (store a8 9 6)) - (=> (and (<= 0 10) (< 10 20)) - (forall ((a10 (Array Int Int))) - (=> (= a10 (store a9 10 9)) - (=> (and (<= 0 11) (< 11 20)) - (forall ((a11 (Array Int Int))) - (=> (= a11 (store a10 11 5)) - (=> (and (<= 0 12) (< 12 20)) - (forall ((a12 (Array Int Int))) - (=> (= a12 (store a11 12 0)) - (=> (and (<= 0 13) (< 13 20)) - (forall ((a13 (Array Int Int))) - (=> (= a13 (store a12 13 2)) - (=> (and (<= 0 14) (< 14 20)) - (forall ((a14 (Array Int Int))) - (=> (= a14 (store a13 14 7)) - (=> (and (<= 0 15) (< 15 20)) - (forall ((a15 (Array Int Int))) - (=> (= a15 (store a14 15 3)) - (=> (and (<= 0 16) (< 16 20)) - (forall ((a16 (Array Int Int))) - (=> (= a16 (store a15 16 2)) - (=> (and (<= 0 17) (< 17 20)) - (forall ((a17 (Array Int Int))) - (=> (= a17 (store a16 17 1)) - (=> (and (<= 0 18) (< 18 20)) - (forall ((a18 (Array Int Int))) - (=> (= a18 (store a17 18 10)) - (=> (and (<= 0 19) (< 19 20)) - (forall ((a19 (Array Int Int))) - (=> (= a19 (store a18 19 6)) - (=> - (and (<= 0 20) - (forall ((i Int)) (=> (and (<= 0 i) (< i 20)) (<= 0 (select a19 i))))) - (forall ((result Int) (result1 Int)) - (=> - (and (= result (sum a19 0 20)) - (and (is_max (mk_array1 20 a19) 0 20 result1) (<= result (* 20 result1)))) - (=> (= result 90) (= result1 10)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -(check-sat) - diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 deleted file mode 100644 index a6f4106e5..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 +++ /dev/null @@ -1,520 +0,0 @@ -;;; From a verification condition generated by why3. The original program -;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . -;; The problem has been modified by doubling the size of the arrays. -;; (* **) -;; VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html **) -;; Problem 1: maximum /\ sum of an array **) - -;; Author: Jean-Christophe Filliatre (CNRS) **) -;; Tool: Why3 (see http://why3.lri.fr/) **) -;; *\) **) - -;; Particularly the assertion in the test case that the max m = 10 - -;; Added rewriterules: -;; (assert-propagation ((c (array Int)) (l Int) (h Int) (m Int)) () -;; ((is_max c l h m)) (= m (comp_max c l h)) ()) - -;; (assert-rewrite ((c (array Int)) (l Int) (h Int)) ((<= h l)) -;; (comp_max c l h) 0 ()) - -;; (assert-rewrite ((c (array Int)) (l Int) (h Int)) ((< l h)(< (comp_max c l (- h 1)) (tb2t2 (sort int (get1 (sort (array1 int) (t2tb c)) h)))) ) -;; (comp_max c l h) (tb2t2 (sort int (get1 (sort (array1 int) (t2tb c)) h))) ()) - -;; (assert-rewrite ((c (array Int)) (l Int) (h Int)) ((< l h)(>= (comp_max c l (- h 1)) (tb2t2 (sort int (get1 (sort (array1 int) (t2tb c)) h)))) ) -;; (comp_max c l h) (comp_max c l (- h 1)) ()) - - -;;; this is a prelude for CVC4 -(set-logic AUFNIRA) -;;; this is a prelude for CVC4 integer arithmetic -(declare-sort uni 0) - -(declare-sort deco 0) - -(declare-sort ty 0) - -(declare-fun sort (ty uni) deco) - -(declare-fun int () ty) - -(declare-fun real () ty) - -(declare-fun bool () ty) - -(declare-fun True () uni) - -(declare-fun False () uni) - -(declare-fun match_bool (deco deco deco) uni) - -;; match_bool_True - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool True) (sort a z) (sort a z1))) (sort a z))))) - -;; match_bool_False - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool False) (sort a z) (sort a z1))) (sort a - z1))))) - -(declare-fun index_bool (deco) Int) - -;; index_bool_True - (assert (= (index_bool (sort bool True)) 0)) - -;; index_bool_False - (assert (= (index_bool (sort bool False)) 1)) - -;; bool_inversion - (assert - (forall ((u uni)) - (or (= (sort bool u) (sort bool True)) (= (sort bool u) (sort bool False))))) - -(declare-fun tuple0 () ty) - -(declare-fun Tuple0 () uni) - -;; tuple0_inversion - (assert (forall ((u uni)) (= (sort tuple0 u) (sort tuple0 Tuple0)))) - -;; CompatOrderMult - (assert - (forall ((x Int) (y Int) (z Int)) - (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z)))))) - -(declare-fun ref (ty) ty) - -(declare-fun mk_ref (deco) uni) - -(declare-fun contents (deco) uni) - -;; contents_def - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort a (contents (sort (ref a) (mk_ref (sort a u))))) (sort a u))))) - -;; ref_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (ref a) u) (sort (ref a) - (mk_ref (sort a (contents (sort (ref a) u))))))))) - -(declare-fun map (ty ty) ty) - -(declare-fun get (deco deco) uni) - -(declare-fun set (deco deco deco) uni) - -;; Select_eq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (= a1 a2) (= (select (store m a1 b) a2) b)) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_eq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (= (sort a a1) (sort a a2)) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b b1))) :pattern ((sort b - (get - (sort (map a b) - (set (sort (map a b) m) - (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -;; Select_neq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (not (= a1 a2)) (= (select (store m a1 b) a2) (select m a2))) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_neq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (not (= (sort a a1) (sort a a2))) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b (get (sort (map a b) m) (sort a a2))))) :pattern ( - (sort b - (get (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -(declare-fun const1 (deco) uni) - -(declare-fun const2 (Int) (Array Int Int)) - -;; Const - (assert (forall ((b Int) (a Int)) (= (select (const2 b) a) b))) - -;; Const - (assert - (forall ((a ty) (b ty)) - (forall ((b1 uni) (a1 uni)) - (= (sort b (get (sort (map a b) (const1 (sort b b1))) (sort a a1))) - (sort b b1))))) - -(declare-sort array 1) - -(declare-fun array1 (ty) ty) - -(declare-fun mk_array (Int deco) uni) - -(declare-fun mk_array1 (Int (Array Int Int)) (array Int)) - -(declare-fun length (deco) Int) - -(declare-fun t2tb ((array Int)) uni) - -(declare-fun tb2t (deco) (array Int)) - -;; BridgeL - (assert - (forall ((i (array Int))) - (! (= (tb2t (sort (array1 int) (t2tb i))) i) :pattern ((sort (array1 int) - (t2tb i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (array1 int) (t2tb (tb2t (sort (array1 int) j)))) (sort - (array1 int) - j)) :pattern ( - (sort (array1 int) (t2tb (tb2t (sort (array1 int) j))))) ))) - -;; length_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (length (sort (array1 int) (t2tb (mk_array1 u u1)))) u))) - -;; length_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (length (sort (array1 a) (mk_array u (sort (map int a) u1)))) u)))) - -(declare-fun elts (deco) uni) - -(declare-fun t2tb1 ((Array Int Int)) uni) - -(declare-fun tb2t1 (deco) (Array Int Int)) - -;; BridgeL - (assert - (forall ((i (Array Int Int))) - (! (= (tb2t1 (sort (map int int) (t2tb1 i))) i) :pattern ((sort - (map int int) - (t2tb1 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j)))) (sort - (map - int - int) j)) :pattern ( - (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j))))) ))) - -;; elts_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb (mk_array1 u u1)))))) u1))) - -;; elts_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (sort (map int a) - (elts (sort (array1 a) (mk_array u (sort (map int a) u1))))) (sort - (map int a) - u1))))) - -;; array_inversion - (assert - (forall ((u (array Int))) - (= u (mk_array1 (length (sort (array1 int) (t2tb u))) - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb u))))))))) - -;; array_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (array1 a) u) (sort (array1 a) - (mk_array (length (sort (array1 a) u)) - (sort (map int a) (elts (sort (array1 a) u))))))))) - -(declare-fun get1 (deco Int) uni) - -(declare-fun t2tb2 (Int) uni) - -(declare-fun tb2t2 (deco) Int) - -;; BridgeL - (assert - (forall ((i Int)) - (! (= (tb2t2 (sort int (t2tb2 i))) i) :pattern ((sort int (t2tb2 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort int (t2tb2 (tb2t2 (sort int j)))) (sort int j)) :pattern ( - (sort int (t2tb2 (tb2t2 (sort int j))))) ))) - -;; get_def - (assert - (forall ((a (array Int)) (i Int)) - (= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) i))) (select - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb a))))) i)))) - -;; get_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int)) - (= (sort a (get1 (sort (array1 a) a1) i)) (sort a - (get - (sort (map int a) - (elts (sort (array1 a) a1))) - (sort int (t2tb2 i)))))))) - -(declare-fun set1 (deco Int deco) uni) - -;; set_def - (assert - (forall ((a (array Int)) (i Int) (v Int)) - (= (tb2t - (sort (array1 int) - (set1 (sort (array1 int) (t2tb a)) i (sort int (t2tb2 v))))) (mk_array1 - (length - (sort - (array1 - int) - (t2tb a))) - (store - (tb2t1 - (sort - (map - int - int) - (elts - (sort - (array1 - int) - (t2tb a))))) i v))))) - -;; set_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int) (v uni)) - (= (sort (array1 a) (set1 (sort (array1 a) a1) i (sort a v))) (sort - (array1 a) - (mk_array - (length - (sort - (array1 a) - a1)) - (sort - (map int a) - (set - (sort - (map int a) - (elts - (sort - (array1 a) - a1))) - (sort - int - (t2tb2 i)) - (sort a v))))))))) - -(declare-fun make (Int deco) uni) - -;; make_def - (assert - (forall ((n Int) (v Int)) - (= (tb2t (sort (array1 int) (make n (sort int (t2tb2 v))))) (mk_array1 n - (const2 v))))) - -;; make_def - (assert - (forall ((a ty)) - (forall ((n Int) (v uni)) - (= (sort (array1 a) (make n (sort a v))) (sort (array1 a) - (mk_array n - (sort (map int a) - (const1 (sort a v))))))))) - -(declare-fun sum ((Array Int Int) Int Int) Int) - -;; Sum_def_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (<= j i) (= (sum c i j) 0)))) - -;; Sum_def_non_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (select c i) (sum c (+ i 1) j)))))) - -;; Sum_right_extension - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1))))))) - -;; Sum_transitivity - (assert - (forall ((c (Array Int Int)) (i Int) (k Int) (j Int)) - (=> (and (<= i k) (<= k j)) (= (sum c i j) (+ (sum c i k) (sum c k j)))))) - -;; Sum_eq - (assert - (forall ((c1 (Array Int Int)) (c2 (Array Int Int)) (i Int) (j Int)) - (=> - (forall ((k Int)) - (=> (and (<= i k) (< k j)) (= (select c1 k) (select c2 k)))) - (= (sum c1 i j) (sum c2 i j))))) - -(declare-fun sum1 ((array Int) Int Int) Int) - -;; sum_def - (assert - (forall ((a (array Int)) (l Int) (h Int)) - (= (sum1 a l h) (sum - (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb a))))) l - h)))) - -(declare-fun is_max ((array Int) Int Int Int) Bool) - -;; is_max_def - (assert - (forall ((a (array Int)) (l Int) (h Int) (m Int)) - (and - (=> (is_max a l h m) - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k)))))))))) - (=> - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))) (is_max - a l h m))))) - -(declare-fun comp_max ((array Int) Int Int) Int) - -(assert-propagation ((c (array Int)) (l Int) (h Int) (m Int)) () - ((is_max c l h m)) (= m (comp_max c l h)) ()) - -(assert-rewrite ((c (array Int)) (l Int) (h Int)) ((<= h l)) - (comp_max c l h) 0 ()) - -(assert-rewrite ((c (array Int)) (l Int) (h Int)) ((< l h)(< (comp_max c l (- h 1)) (tb2t2 (sort int (get1 (sort (array1 int) (t2tb c)) h)))) ) - (comp_max c l h) (tb2t2 (sort int (get1 (sort (array1 int) (t2tb c)) h))) ()) - -(assert-rewrite ((c (array Int)) (l Int) (h Int)) ((< l h)(>= (comp_max c l (- h 1)) (tb2t2 (sort int (get1 (sort (array1 int) (t2tb c)) h)))) ) - (comp_max c l h) (comp_max c l (- h 1)) ()) - -(assert -;; WP_parameter_test_case - ;; File "vstte10_max_sum/../vstte10_max_sum.mlw", line 63, characters 6-15 - (not - (=> (<= 0 20) - (=> (and (<= 0 0) (< 0 20)) - (forall ((a (Array Int Int))) - (=> (= a (store (const2 0) 0 9)) - (=> (and (<= 0 1) (< 1 20)) - (forall ((a1 (Array Int Int))) - (=> (= a1 (store a 1 5)) - (=> (and (<= 0 2) (< 2 20)) - (forall ((a2 (Array Int Int))) - (=> (= a2 (store a1 2 0)) - (=> (and (<= 0 3) (< 3 20)) - (forall ((a3 (Array Int Int))) - (=> (= a3 (store a2 3 2)) - (=> (and (<= 0 4) (< 4 20)) - (forall ((a4 (Array Int Int))) - (=> (= a4 (store a3 4 7)) - (=> (and (<= 0 5) (< 5 20)) - (forall ((a5 (Array Int Int))) - (=> (= a5 (store a4 5 3)) - (=> (and (<= 0 6) (< 6 20)) - (forall ((a6 (Array Int Int))) - (=> (= a6 (store a5 6 2)) - (=> (and (<= 0 7) (< 7 20)) - (forall ((a7 (Array Int Int))) - (=> (= a7 (store a6 7 1)) - (=> (and (<= 0 8) (< 8 20)) - (forall ((a8 (Array Int Int))) - (=> (= a8 (store a7 8 10)) - (=> (and (<= 0 9) (< 9 20)) - (forall ((a9 (Array Int Int))) - (=> (= a9 (store a8 9 6)) - (=> (and (<= 0 10) (< 10 20)) - (forall ((a10 (Array Int Int))) - (=> (= a10 (store a9 10 9)) - (=> (and (<= 0 11) (< 11 20)) - (forall ((a11 (Array Int Int))) - (=> (= a11 (store a10 11 5)) - (=> (and (<= 0 12) (< 12 20)) - (forall ((a12 (Array Int Int))) - (=> (= a12 (store a11 12 0)) - (=> (and (<= 0 13) (< 13 20)) - (forall ((a13 (Array Int Int))) - (=> (= a13 (store a12 13 2)) - (=> (and (<= 0 14) (< 14 20)) - (forall ((a14 (Array Int Int))) - (=> (= a14 (store a13 14 7)) - (=> (and (<= 0 15) (< 15 20)) - (forall ((a15 (Array Int Int))) - (=> (= a15 (store a14 15 3)) - (=> (and (<= 0 16) (< 16 20)) - (forall ((a16 (Array Int Int))) - (=> (= a16 (store a15 16 2)) - (=> (and (<= 0 17) (< 17 20)) - (forall ((a17 (Array Int Int))) - (=> (= a17 (store a16 17 1)) - (=> (and (<= 0 18) (< 18 20)) - (forall ((a18 (Array Int Int))) - (=> (= a18 (store a17 18 10)) - (=> (and (<= 0 19) (< 19 20)) - (forall ((a19 (Array Int Int))) - (=> (= a19 (store a18 19 6)) - (=> - (and (<= 0 20) - (forall ((i Int)) (=> (and (<= 0 i) (< i 20)) (<= 0 (select a19 i))))) - (forall ((result Int) (result1 Int)) - (=> - (and (= result (sum a19 0 20)) - (and (is_max (mk_array1 20 a19) 0 20 result1) (<= result (* 20 result1)))) - (=> (= result 90) (= result1 10)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -(check-sat) - |