From: François Bobot Date: Fri, 30 Nov 2012 11:35:02 +0000 (+0000) Subject: fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first X-Git-Tag: cvc5-1.0.0~7524 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4643949ff4f1586935dfc2607931f26604422b50;p=cvc5.git fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first just after the bindings Do it before the release in order to not break user files later --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 39149ec89..87cf2083d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -532,9 +532,9 @@ rewriterulesCommand[CVC4::Command*& cmd] } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK term[head, expr2] term[body, expr2] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK { args.clear(); args.push_back(head); @@ -573,10 +573,10 @@ rewriterulesCommand[CVC4::Command*& cmd] } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK LPAREN_TOK (termList[heads,expr])? RPAREN_TOK term[body, expr2] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK { args.clear(); /* heads */ diff --git a/test/regress/regress0/rewriterules/datatypes2.smt2 b/test/regress/regress0/rewriterules/datatypes2.smt2 index 993cd2002..277ddc3ae 100644 --- a/test/regress/regress0/rewriterules/datatypes2.smt2 +++ b/test/regress/regress0/rewriterules/datatypes2.smt2 @@ -14,21 +14,21 @@ ;;;;;;;;;;;;;;;;;;;; ;; injective -(declare-fun inj1 (list) elt) +(declare-fun inj11 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj12 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj1 (list) elt) +(declare-fun inj21 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj22 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) ;;;;;;;;;;;;;;;;;;;; diff --git a/test/regress/regress0/rewriterules/datatypes3.smt2 b/test/regress/regress0/rewriterules/datatypes3.smt2 index dc3c8e20c..1ec5dcbc4 100644 --- a/test/regress/regress0/rewriterules/datatypes3.smt2 +++ b/test/regress/regress0/rewriterules/datatypes3.smt2 @@ -14,21 +14,21 @@ ;;;;;;;;;;;;;;;;;;;; ;; injective -(declare-fun inj1 (list) elt) +(declare-fun inj11 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj12 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj1 (list) elt) +(declare-fun inj21 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj22 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) ;;;;;;;;;;;;;;;;;;;; diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2 index f1e61a901..19163f49d 100644 --- a/test/regress/regress0/rewriterules/datatypes_clark.smt2 +++ b/test/regress/regress0/rewriterules/datatypes_clark.smt2 @@ -18,13 +18,13 @@ (declare-fun inj1 (nat) nat) (assert-propagation((?x1 nat)) - () () (= (inj1 (succ ?x1)) ?x1) (((succ ?x1))) ) + (((succ ?x1))) () () (= (inj1 (succ ?x1)) ?x1) ) ;;;;;;;;;;;;;;;;;;;; ;; projection (declare-fun pred (nat) nat) -(assert-rewrite ((?x1 nat)) () (pred (succ ?x1)) ?x1 () ) +(assert-rewrite ((?x1 nat)) () () (pred (succ ?x1)) ?x1 ) (assert (= (pred zero) zero)) @@ -32,34 +32,34 @@ ;; test (declare-fun is_succ (nat) Bool) (assert (= (is_succ zero) false)) -(assert-propagation ((?x1 nat)) () () (= (is_succ (succ ?x1)) true) (((succ ?x1))) ) +(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (= (is_succ (succ ?x1)) true) ) -(assert-propagation ((?x1 nat)) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1))) (((pred ?x1)))) +(assert-propagation ((?x1 nat)) (((pred ?x1))) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1)))) (declare-fun is_zero (nat) Bool) (assert (= (is_zero zero) true)) -(assert-propagation ((?x1 nat)) () ((is_zero ?x1)) (= ?x1 zero) ()) +(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (= ?x1 zero)) ;;; directrr -(assert-rewrite ((?x1 nat)) () (is_succ (succ ?x1)) true () ) -(assert-rewrite ((?x1 nat)) () (is_zero (succ ?x1)) false () ) +(assert-rewrite ((?x1 nat)) () () (is_succ (succ ?x1)) true ) +(assert-rewrite ((?x1 nat)) () () (is_zero (succ ?x1)) false ) ;;;;;;;;;;;;;;;;;;;; ;; distinct -(assert-propagation ((?x1 nat)) () ((is_zero ?x1)) (not (is_succ ?x1)) () ) -(assert-propagation ((?x1 nat)) () ((is_succ ?x1)) (not (is_zero ?x1)) () ) -(assert-propagation ((?x1 nat)) () ((not (is_zero ?x1))) (is_succ ?x1) () ) -(assert-propagation ((?x1 nat)) () ((not (is_succ ?x1))) (is_zero ?x1) () ) +(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (not (is_succ ?x1)) ) +(assert-propagation ((?x1 nat)) () () ((is_succ ?x1)) (not (is_zero ?x1)) ) +(assert-propagation ((?x1 nat)) () () ((not (is_zero ?x1))) (is_succ ?x1) ) +(assert-propagation ((?x1 nat)) () () ((not (is_succ ?x1))) (is_zero ?x1) ) ;;;;;;;;;;;;;;;;;;; ;; case-split -(assert-propagation ((?x1 nat)) () () (or (is_zero ?x1) (is_succ ?x1)) (((pred ?x1))) ) +(assert-propagation ((?x1 nat)) (((pred ?x1))) () () (or (is_zero ?x1) (is_succ ?x1)) ) ;;;;;;;;;;;;;;;;;;; ;; non-cyclic (declare-fun size_nat (nat) Real) -(assert-propagation ((?x1 nat)) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) (((succ ?x1))) ) +(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) ) @@ -83,22 +83,22 @@ ;; injective (declare-fun inj2 (list) tree) -(assert-propagation ((?x1 tree) (?x2 list)) () () (= (inj2 (cons ?x1 ?x2)) ?x1) (((cons ?x1 ?x2))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj2 (cons ?x1 ?x2)) ?x1) ) (declare-fun inj3 (list) list) -(assert-propagation ((?x1 tree) (?x2 list)) () () (= (inj3 (cons ?x1 ?x2)) ?x2) (((cons ?x1 ?x2))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj3 (cons ?x1 ?x2)) ?x2) ) ;;;;;;;;;;;;;;;;;;;; ;; projection (declare-fun car (list) tree) -(assert-rewrite ((?x1 tree) (?x2 list)) () (car (cons ?x1 ?x2)) ?x1 ()) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (car (cons ?x1 ?x2)) ?x1) (assert (= (car null) (node null))) (declare-fun cdr (list) list) -(assert-rewrite ((?x1 tree) (?x2 list)) () (cdr (cons ?x1 ?x2)) ?x2 ()) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (cdr (cons ?x1 ?x2)) ?x2) (assert (= (cdr null) null)) @@ -106,36 +106,36 @@ ;; test (declare-fun is_cons (list) Bool) (assert (= (is_cons null) false)) -(assert-propagation ((?x1 tree) (?x2 list)) () () (= (is_cons (cons ?x1 ?x2)) true) (((cons ?x1 ?x2))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (is_cons (cons ?x1 ?x2)) true) ) -(assert-propagation ((?x1 list)) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) (((car ?x1))) ) -(assert-propagation ((?x1 list)) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) (((cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) ) (declare-fun is_null (list) Bool) (assert (= (is_null null) true)) -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= (car ?x1) (node null)) (((car ?x1))) ) -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= (cdr ?x1) null) (((cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_null ?x1)) (= (car ?x1) (node null)) ) +(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_null ?x1)) (= (cdr ?x1) null) ) -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= ?x1 null) ()) +(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (= ?x1 null)) ;;; directrr -(assert-rewrite ((?x1 tree) (?x2 list)) () (is_cons (cons ?x1 ?x2)) true ()) -(assert-rewrite ((?x1 tree) (?x2 list)) () (is_null (cons ?x1 ?x2)) false ()) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_cons (cons ?x1 ?x2)) true) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_null (cons ?x1 ?x2)) false) ;;;;;;;;;;;;;;;;;;;; ;; distinct -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (not (is_cons ?x1)) () ) -(assert-propagation ((?x1 list)) () ((is_cons ?x1)) (not (is_null ?x1)) () ) -(assert-propagation ((?x1 list)) () ((not (is_null ?x1))) (is_cons ?x1) () ) -(assert-propagation ((?x1 list)) () ((not (is_cons ?x1))) (is_null ?x1) () ) +(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (not (is_cons ?x1)) ) +(assert-propagation ((?x1 list)) () () ((is_cons ?x1)) (not (is_null ?x1)) ) +(assert-propagation ((?x1 list)) () () ((not (is_null ?x1))) (is_cons ?x1) ) +(assert-propagation ((?x1 list)) () () ((not (is_cons ?x1))) (is_null ?x1) ) ;;;;;;;;;;;;;;;;;;; ;; case-split -(assert-propagation ((?x1 list)) () () (or (is_null ?x1) (is_cons ?x1)) (((car ?x1))) ) -(assert-propagation ((?x1 list)) () () (or (is_null ?x1) (is_cons ?x1)) (((cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((car ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) ) +(assert-propagation ((?x1 list)) (((cdr ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) ) ;;;;;;;;;;;;;;; ;; tree @@ -144,61 +144,61 @@ ;; injective (declare-fun inj4 (tree) list) -(assert-propagation ((?x1 list)) () () (= (inj4 (node ?x1)) ?x1) (((node ?x1))) ) +(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (inj4 (node ?x1)) ?x1) ) (declare-fun inj5 (tree) nat) -(assert-propagation ((?x1 nat)) () () (= (inj5 (leaf ?x1)) ?x1) (((leaf ?x1))) ) +(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (inj5 (leaf ?x1)) ?x1) ) ;;;;;;;;;;;;;;;;;;;; ;; projection (declare-fun children (tree) list) -(assert-rewrite ((?x1 list)) () (children (node ?x1)) ?x1 () ) -(assert-rewrite ((?x1 nat)) () (children (leaf ?x1)) null () ) +(assert-rewrite ((?x1 list)) () () (children (node ?x1)) ?x1 ) +(assert-rewrite ((?x1 nat)) () () (children (leaf ?x1)) null ) (declare-fun data (tree) nat) -(assert-rewrite ((?x1 nat)) () (data (leaf ?x1)) ?x1 () ) -(assert-rewrite ((?x1 list)) () (data (node ?x1)) zero () ) +(assert-rewrite ((?x1 nat)) () () (data (leaf ?x1)) ?x1 ) +(assert-rewrite ((?x1 list)) () () (data (node ?x1)) zero ) ;;;;;;;;;;;;;;;;;;; ;; test (declare-fun is_node (tree) Bool) -(assert-propagation ((?x1 list)) () () (= (is_node (node ?x1)) true) (((node ?x1))) ) +(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (is_node (node ?x1)) true) ) -(assert-propagation ((?x1 tree)) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) (((children ?x1))) ) -(assert-propagation ((?x1 tree)) () ((is_node ?x1)) (= (data ?x1) zero) (((data ?x1))) ) +(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) ) +(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_node ?x1)) (= (data ?x1) zero) ) (declare-fun is_leaf (tree) Bool) -(assert-propagation ((?x1 nat)) () () (= (is_leaf (leaf ?x1)) true) (((leaf ?x1))) ) -(assert-propagation ((?x1 tree)) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) (((data ?x1))) ) -(assert-propagation ((?x1 tree)) () ((is_leaf ?x1)) (= (children ?x1) null) (((children ?x1))) ) +(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (is_leaf (leaf ?x1)) true) ) +(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) ) +(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_leaf ?x1)) (= (children ?x1) null) ) ;;; directrr -(assert-rewrite ((?x1 list)) () (is_node (node ?x1)) true () ) -(assert-rewrite ((?x1 list)) () (is_leaf (node ?x1)) false () ) -(assert-rewrite ((?x1 nat)) () (is_leaf (leaf ?x1)) true () ) -(assert-rewrite ((?x1 nat)) () (is_node (leaf ?x1)) false () ) +(assert-rewrite ((?x1 list)) () () (is_node (node ?x1)) true ) +(assert-rewrite ((?x1 list)) () () (is_leaf (node ?x1)) false ) +(assert-rewrite ((?x1 nat)) () () (is_leaf (leaf ?x1)) true ) +(assert-rewrite ((?x1 nat)) () () (is_node (leaf ?x1)) false ) ;;;;;;;;;;;;;;;;;;;; ;; distinct -(assert-propagation ((?x1 tree)) () ((is_node ?x1)) (not (is_leaf ?x1)) () ) -(assert-propagation ((?x1 tree)) () ((is_leaf ?x1)) (not (is_node ?x1)) () ) -(assert-propagation ((?x1 tree)) () ((not (is_node ?x1))) (is_leaf ?x1) () ) -(assert-propagation ((?x1 tree)) () ((not (is_leaf ?x1))) (is_node ?x1) () ) +(assert-propagation ((?x1 tree)) () () ((is_node ?x1)) (not (is_leaf ?x1)) ) +(assert-propagation ((?x1 tree)) () () ((is_leaf ?x1)) (not (is_node ?x1)) ) +(assert-propagation ((?x1 tree)) () () ((not (is_node ?x1))) (is_leaf ?x1) ) +(assert-propagation ((?x1 tree)) () () ((not (is_leaf ?x1))) (is_node ?x1) ) ;;;;;;;;;;;;;;;;;;; ;; case-split -(assert-propagation ((?x1 tree)) () () (or (is_node ?x1) (is_leaf ?x1)) (((children ?x1))) ) -(assert-propagation ((?x1 tree)) () () (or (is_node ?x1) (is_leaf ?x1)) (((data ?x1))) ) +(assert-propagation ((?x1 tree)) (((children ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) ) +(assert-propagation ((?x1 tree)) (((data ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) ) ;;;;;;;;;;;;;;;;;; ;; non-cyclic (declare-fun size_list (list) Real) (declare-fun size_tree (tree) Real) -(assert-propagation ((?x1 tree) (?x2 list)) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) (((cons ?x1 ?x2))) ) -(assert-propagation ((?x1 list)) () () (> (size_tree (node ?x1)) (size_list ?x1)) (((node ?x1))) ) -(assert-propagation ((?x1 nat)) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) (((leaf ?x1))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) ) +(assert-propagation ((?x1 list)) (((node ?x1))) () () (> (size_tree (node ?x1)) (size_list ?x1)) ) +(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) ) diff --git a/test/regress/regress0/rewriterules/length_gen_010.smt2 b/test/regress/regress0/rewriterules/length_gen_010.smt2 index 41cc61c9e..052f5905b 100644 --- a/test/regress/regress0/rewriterules/length_gen_010.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_010.smt2 @@ -18,14 +18,14 @@ ;; (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)) ()) +(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) (?l)) -(assert-rewrite ((?n Int) (?l list)) (> ?n 0) (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)) ()) +(assert-rewrite ((?n Int) (?l list)) () (> ?n 0) (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l))) (declare-fun n () Int) diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2 index 1be13167d..b7d19b612 100644 --- a/test/regress/regress0/rewriterules/native_arrays.smt2 +++ b/test/regress/regress0/rewriterules/native_arrays.smt2 @@ -10,8 +10,8 @@ ;;A dumb predicate for a simple example (declare-fun P (Element) Bool) -(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () - (P (select (store ?a ?i1 ?e) ?i2)) true () ) +(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () () + (P (select (store ?a ?i1 ?e) ?i2)) true ) (declare-fun a1 () (Array Index Element)) (declare-fun a2 () (Array Index Element)) diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 index 7cd61738b..13f7234e9 100644 --- a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 +++ b/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 @@ -8,32 +8,32 @@ (declare-fun Rf (elt elt elt) Bool) ;;eq -(assert-propagation ((?x elt)) () () (or (= ?x ?x) (not (= ?x ?x))) ((?x)) ) +(assert-propagation ((?x elt)) ((?x)) () () (or (= ?x ?x) (not (= ?x ?x))) ) ;; reflexive -(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) ) +(assert-propagation ((?x elt)) ((?x)) () () (Rf ?x ?x ?x) ) ;; step -(assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((f ?x))) ) +(assert-propagation ((?x elt)) (((f ?x))) () () (Rf ?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))) ) +(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) () ((Rf ?x1 ?x2 ?x2)) (or (= ?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))) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) ;; 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) ) ;; 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)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) + (or (Rf ?x1 ?x2 ?x3) (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)) () ) +(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) () ) +(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)) () ) +(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)) () ) +(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) diff --git a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 index b7069536a..8f30f38a5 100644 --- a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 +++ b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 @@ -8,97 +8,97 @@ (declare-fun R (mem elt elt elt) Bool) ;; reflexive -(assert-propagation ((?m mem)(?x elt)) () () (R ?m ?x ?x ?x) ((?m ?x)) ) +(assert-propagation ((?m mem)(?x elt)) ((?m ?x)) () () (R ?m ?x ?x ?x) ) ;; step -(assert-propagation ((?m mem)(?x elt)) () () (R ?m ?x (select ?m ?x) (select ?m ?x)) (((select ?m ?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))) ) +(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)) () ((R ?m ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (R ?m ?x1 (select ?m ?x1) ?x2)) (((select ?m ?x1))) ) +(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)) ((not (= ?x1 ?x2))(Rf ?x1 ?x2 ?x2)) () (Rf ?x1 (f ?x1) ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) +;; (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)) ((not (Rf ?x1 (f ?x1) ?x2))(Rf ?x1 ?x2 ?x2)) () (= ?x1 ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) +;; (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) ?x1)) ((R ?m ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((select ?m ?x1))) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) () ) +(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)) () () (=> (and (= (f ?x1) ?x1) (Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x2)(f ?x1))) ) +;; (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) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x1))) ) +(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 ((?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)) () () -;; (=> (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))) ) +;; (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 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x3))) ) +;; (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 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x3 ?x2))) ) +;; (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 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x3 ?x2))) ) +;; (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 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x2 ?x3))) ) +;; (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)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) +;; (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)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) +;; (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)) () ) +(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) () ) +(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)) () ) +;; (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)) () ) +;; (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 ((?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)) () () +;; (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))) -;; (((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))) ) +;; (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 ?x0 ?x1 ?x2)(not (Rf ?x0 ?x1 ?x3))) -;; (not (Rf ?x1 ?x3 ?x2)) (((Rf ?x1 ?x3 ?x2))) ) +;; (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)) () ((not (Rf ?x0 ?x3 ?x2))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) (((Rf ?x0 ?x1 ?x2))) ) +;; (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 ?x0 ?x1 ?x2)(not (Rf ?x0 ?x3 ?x2))) -;; (not (Rf ?x1 ?x3 ?x2)) (((Rf ?x1 ?x3 ?x2))) ) +;; (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 ((?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)) () () +;; (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))) (((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1))) ) +;; (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2))) ) (declare-fun next () mem) @@ -112,17 +112,16 @@ (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)))) () ) +(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) +(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) ) ) - () -) + ) @@ -131,14 +130,14 @@ (declare-fun null () elt) (assert (= (select next null) null)) -(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) () ((R ?m ?x ?z ?z)(R ?m ?y ?z ?z)) (R ?m ?x (join ?m ?x ?y) ?z) (((join ?m ?x ?y))) ) -(assert-propagation ((?m mem)(?x elt)(?y elt)) () () (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)) (((join ?m ?x ?y))) ) +(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 ((?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)) () () +(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) @@ -173,8 +172,7 @@ ) ) )) - (((join (store ?m ?p ?q) ?u ?v))) - ) + ) (declare-fun next2 () mem) diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2 index a327a90a4..e8c0139e8 100644 --- a/test/regress/regress0/rewriterules/relation.smt2 +++ b/test/regress/regress0/rewriterules/relation.smt2 @@ -7,13 +7,13 @@ (declare-fun R (elt elt) Bool) ;; reflexive -(assert-rewrite ((x elt)) () (R x x) true ()) +(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) ()) +(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) ()) +(assert-propagation ((x elt) (y elt)) () () ((R x y) (R y x)) (= x y)) (declare-fun e1 () elt) (declare-fun e2 () elt) 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 index 1b397ef5b..9bd49f714 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 @@ -12,98 +12,98 @@ ;; 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)) () () + ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((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)) () ) + () () ((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)) ()) + () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) (((inter ?t1 ?t2))) ) + (((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))) ()) + () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((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) ()) + () () ((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) ()) + () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))) (((union ?t1 ?t2)))) + (((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))) ()) + () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2)))) + (((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) ()) + () () ((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)) ()) + () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) (((diff ?t1 ?t2))) ) + (((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)) - () () (in ?s (sing ?s)) (((sing ?s))) ) + (((sing ?s))) () () (in ?s (sing ?s)) ) (assert-propagation ((?s elt) (?t1 elt)) - () ((in ?s (sing ?t1))) (= ?s ?t1) ()) + () () ((in ?s (sing ?t1))) (= ?s ?t1)) (assert-propagation ((?s elt) (?t1 elt)) - () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)) ()) + () () ((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))) ()) + () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))) (((inter ?t1 ?t2)))) + (((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)))) ()) + () () ((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) ()) + () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) (declare-fun e () elt) (declare-fun t1 () set) 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 index 55050ac1a..4d65ffac5 100644 --- 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 @@ -13,98 +13,98 @@ ;; 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)) () () + ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((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)) () ) + () () ((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)) ()) + () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) (((inter ?t1 ?t2))) ) + (((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))) ()) + () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((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) ()) + () () ((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) ()) + () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))) (((union ?t1 ?t2)))) + (((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))) ()) + () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2)))) + (((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) ()) + () () ((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)) ()) + () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) (((diff ?t1 ?t2))) ) + (((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)) - () () (in ?s (sing ?s)) (((sing ?s))) ) + (((sing ?s))) () () (in ?s (sing ?s)) ) (assert-propagation ((?s elt) (?t1 elt)) - () ((in ?s (sing ?t1))) (= ?s ?t1) ()) + () () ((in ?s (sing ?t1))) (= ?s ?t1)) (assert-propagation ((?s elt) (?t1 elt)) - () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)) ()) + () () ((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))) ()) + () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))) (((inter ?t1 ?t2)))) + (((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)))) ()) + () () ((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) ()) + () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) (declare-fun e () elt) (declare-fun t1 () set) diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt deleted file mode 100644 index 4d39e12bb..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt +++ /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.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 new file mode 100644 index 000000000..4d39e12bb --- /dev/null +++ b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 @@ -0,0 +1,492 @@ +;;; 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.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt deleted file mode 100644 index 686b9ff04..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt +++ /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_harness2_rr.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 new file mode 100644 index 000000000..686b9ff04 --- /dev/null +++ b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 @@ -0,0 +1,508 @@ +;;; 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.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt deleted file mode 100644 index e468128ac..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt +++ /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.smt2 b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 new file mode 100644 index 000000000..e468128ac --- /dev/null +++ b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 @@ -0,0 +1,492 @@ +;;; 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.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt deleted file mode 100644 index a6f4106e5..000000000 --- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt +++ /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) - 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 new file mode 100644 index 000000000..a6f4106e5 --- /dev/null +++ b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 @@ -0,0 +1,520 @@ +;;; 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) +