}
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);
}
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 */
;;;;;;;;;;;;;;;;;;;;
;; 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) ))
;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;
;; 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) ))
;;;;;;;;;;;;;;;;;;;;
(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))
;; 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)) )
;; 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))
;; 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
;; 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)) )
;; (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)
;;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))
(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)
(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)
(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) ) )
- ()
-)
+ )
(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)
)
)
))
- (((join (store ?m ?p ?q) ?u ?v)))
- )
+ )
(declare-fun next2 () mem)
(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)
;; 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)
;; 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)
+++ /dev/null
-;;; 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)
-
--- /dev/null
+;;; 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)
+
+++ /dev/null
-;;; 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)
-
--- /dev/null
+;;; 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)
+
+++ /dev/null
-;;; 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)
-
--- /dev/null
+;;; 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)
+
+++ /dev/null
-;;; 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)
-
--- /dev/null
+;;; 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)
+
projects / cvc5.git / commitdiff