Commit 78732fc4 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Remove non-linear benchmarks.

parent 1ebfe2bf
(set-info :smt-lib-version 2.6)
(set-logic UFFPDTLIRA)
(set-info :source |
Generated by: AdaCore
Generated on: 2020-03-06
Generator: SPARK
Application: Program verification for Ada
Target solver: CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-sort us_private 0)
(declare-fun private__bool_eq (us_private us_private) Bool)
(declare-const us_null_ext__ us_private)
(declare-sort us_type_of_heap 0)
(declare-datatypes ((us_type_of_heap__ref 0))
(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
(declare-sort us_image 0)
(declare-datatypes ((int__ref 0))
(((int__refqtmk (int__content Int)))))
(declare-datatypes ((bool__ref 0))
(((bool__refqtmk (bool__content Bool)))))
(declare-datatypes ((us_fixed__ref 0))
(((us_fixed__refqtmk (us_fixed__content Int)))))
(declare-datatypes ((real__ref 0))
(((real__refqtmk (real__content Real)))))
(declare-datatypes ((us_private__ref 0))
(((us_private__refqtmk (us_private__content us_private)))))
(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
a))
(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
(define-fun us_private__ref___projection ((a us_private__ref)) us_private
(us_private__content a))
(declare-fun power (Int Int) Int)
;; Power_0
(assert (forall ((x Int)) (= (power x 0) 1)))
;; Power_s
(assert
(forall ((x Int) (n Int))
(=> (<= 0 n) (= (power x (+ n 1)) (* x (power x n))))))
;; Power_s_alt
(assert
(forall ((x Int) (n Int))
(=> (< 0 n) (= (power x n) (* x (power x (- n 1)))))))
;; Power_1
(assert (forall ((x Int)) (= (power x 1) x)))
;; Power_sum
(assert
(forall ((x Int) (n Int) (m Int))
(=> (<= 0 n)
(=> (<= 0 m) (= (power x (+ n m)) (* (power x n) (power x m)))))))
;; Power_mult
(assert
(forall ((x Int) (n Int) (m Int))
(=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m))))))
;; Power_comm1
(assert
(forall ((x Int) (y Int))
(=> (= (* x y) (* y x))
(forall ((n Int)) (=> (<= 0 n) (= (* (power x n) y) (* y (power x n))))))))
;; Power_comm2
(assert
(forall ((x Int) (y Int))
(=> (= (* x y) (* y x))
(forall ((n Int))
(=> (<= 0 n) (= (power (* x y) n) (* (power x n) (power y n))))))))
;; Power_non_neg
(assert
(forall ((x Int) (y Int)) (=> (and (<= 0 x) (<= 0 y)) (<= 0 (power x y)))))
;; Power_pos
(assert
(forall ((x Int) (y Int)) (=> (and (< 0 x) (<= 0 y)) (< 0 (power x y)))))
;; Power_monotonic
(assert
(forall ((x Int) (n Int) (m Int))
(=> (and (< 0 x) (and (<= 0 n) (<= n m))) (<= (power x n) (power x m)))))
(declare-fun pow2 (Int) Int)
(define-fun is_plus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isPositive x)))
(define-fun is_minus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isNegative x)))
(define-fun is_plus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isPositive x)))
(define-fun is_minus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isNegative x)))
(declare-const max_int Int)
(define-fun in_int_range ((i Int)) Bool (and (<= (- max_int) i)
(<= i max_int)))
(define-fun in_safe_int_range ((i Int)) Bool (and (<= (- 16777216) i)
(<= i 16777216)))
(define-fun same_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isPositive y))
(and (fp.isNegative x) (fp.isNegative y))))
(define-fun diff_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isNegative y))
(and (fp.isNegative x) (fp.isPositive y))))
(define-fun product_sign ((z Float32) (x Float32)
(y Float32)) Bool (and (=> (same_sign x y) (fp.isPositive z))
(=> (diff_sign x y) (fp.isNegative z))))
(define-fun sqr ((x Real)) Real (* x x))
(declare-fun sqrt1 (Real) Real)
(define-fun same_sign_real ((x Float32)
(r Real)) Bool (or (and (fp.isPositive x) (< 0.0 r))
(and (fp.isNegative x) (< r 0.0))))
(declare-datatypes ((t__ref 0))
(((t__refqtmk (t__content Float32)))))
(declare-sort integer 0)
(declare-fun integerqtint (integer) Int)
;; integer'axiom
(assert
(forall ((i integer))
(and (<= (- 2147483648) (integerqtint i)) (<= (integerqtint i) 2147483647))))
(define-fun in_range ((x Int)) Bool (and (<= (- 2147483648) x)
(<= x 2147483647)))
(declare-fun attr__ATTRIBUTE_IMAGE (Int) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE (us_image) Int)
(declare-fun user_eq (integer integer) Bool)
(declare-const dummy integer)
(declare-datatypes ((integer__ref 0))
(((integer__refqtmk (integer__content integer)))))
(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer
(integer__content a))
(define-fun dynamic_invariant ((temp___expr_18 Int) (temp___is_init_14 Bool)
(temp___skip_constant_15 Bool) (temp___do_toplevel_16 Bool)
(temp___do_typ_inv_17 Bool)) Bool (=>
(or (= temp___is_init_14 true)
(<= (- 2147483648) 2147483647)) (in_range
temp___expr_18)))
(declare-sort natural 0)
(declare-fun naturalqtint (natural) Int)
;; natural'axiom
(assert
(forall ((i natural))
(and (<= 0 (naturalqtint i)) (<= (naturalqtint i) 2147483647))))
(define-fun in_range1 ((x Int)) Bool (and (<= 0 x) (<= x 2147483647)))
(declare-fun attr__ATTRIBUTE_IMAGE1 (Int) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Int)
(declare-fun user_eq1 (natural natural) Bool)
(declare-const dummy1 natural)
(declare-datatypes ((natural__ref 0))
(((natural__refqtmk (natural__content natural)))))
(define-fun natural__ref_natural__content__projection ((a natural__ref)) natural
(natural__content a))
(declare-sort float__ 0)
(declare-fun user_eq2 (float__ float__) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE2 (Float32) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Float32)
(declare-const dummy2 float__)
(declare-datatypes ((float____ref 0))
(((float____refqtmk (float____content float__)))))
(define-fun float____ref_float____content__projection ((a float____ref)) float__
(float____content a))
(define-fun dynamic_invariant1 ((temp___expr_60 Float32)
(temp___is_init_56 Bool) (temp___skip_constant_57 Bool)
(temp___do_toplevel_58 Bool)
(temp___do_typ_inv_59 Bool)) Bool (=>
(or (= temp___is_init_56 true)
(fp.leq (fp.neg (fp #b0 #b11111110 #b11111111111111111111111)) (fp #b0 #b11111110 #b11111111111111111111111)))
(fp.isFinite32 temp___expr_60)))
(declare-const x Int)
(declare-const attr__ATTRIBUTE_ADDRESS Int)
(declare-const y Float32)
(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
(declare-const attr__ATTRIBUTE_ADDRESS2 Int)
(declare-const attr__ATTRIBUTE_ADDRESS3 Int)
(define-fun dynamic_invariant2 ((temp___expr_39 Int) (temp___is_init_35 Bool)
(temp___skip_constant_36 Bool) (temp___do_toplevel_37 Bool)
(temp___do_typ_inv_38 Bool)) Bool (=>
(or (= temp___is_init_35 true)
(<= 0 2147483647)) (in_range1
temp___expr_39)))
(assert
;; defqtvc
;; File "gp_exp.adb", line 1, characters 0-0
(not
(forall ((a Int) (b Float32))
(=> (dynamic_invariant x true false true true)
(=> (dynamic_invariant1 y true false true true)
(=> (dynamic_invariant a false false true true)
(=> (dynamic_invariant1 b false false true true)
(let ((o x)) (=> (in_range1 o) (in_range (power 2 o)))))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic UFFPDTLIRA)
(set-info :source |
Generated by: AdaCore
Generated on: 2020-03-06
Generator: SPARK
Application: Program verification for Ada
Target solver: CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
(define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-sort us_private 0)
(declare-fun private__bool_eq (us_private us_private) Bool)
(declare-const us_null_ext__ us_private)
(declare-sort us_type_of_heap 0)
(declare-datatypes ((us_type_of_heap__ref 0))
(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
(declare-sort us_image 0)
(declare-datatypes ((int__ref 0))
(((int__refqtmk (int__content Int)))))
(declare-datatypes ((bool__ref 0))
(((bool__refqtmk (bool__content Bool)))))
(declare-datatypes ((us_fixed__ref 0))
(((us_fixed__refqtmk (us_fixed__content Int)))))
(declare-datatypes ((real__ref 0))
(((real__refqtmk (real__content Real)))))
(declare-datatypes ((us_private__ref 0))
(((us_private__refqtmk (us_private__content us_private)))))
(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
a))
(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
(define-fun us_private__ref___projection ((a us_private__ref)) us_private
(us_private__content a))
(declare-fun pow2 (Int) Int)
(define-fun is_plus_infinity ((x Float64)) Bool (and (fp.isInfinite x)
(fp.isPositive x)))
(define-fun is_minus_infinity ((x Float64)) Bool (and (fp.isInfinite x)
(fp.isNegative x)))
(define-fun is_plus_zero ((x Float64)) Bool (and (fp.isZero x)
(fp.isPositive x)))
(define-fun is_minus_zero ((x Float64)) Bool (and (fp.isZero x)
(fp.isNegative x)))
(declare-const max_int Int)
(define-fun in_int_range ((i Int)) Bool (and (<= (- max_int) i)
(<= i max_int)))
(define-fun in_safe_int_range ((i Int)) Bool (and (<= (- 9007199254740992) i)
(<= i 9007199254740992)))
(define-fun same_sign ((x Float64)
(y Float64)) Bool (or (and (fp.isPositive x) (fp.isPositive y))
(and (fp.isNegative x) (fp.isNegative y))))
(define-fun diff_sign ((x Float64)
(y Float64)) Bool (or (and (fp.isPositive x) (fp.isNegative y))
(and (fp.isNegative x) (fp.isPositive y))))
(define-fun product_sign ((z Float64) (x Float64)
(y Float64)) Bool (and (=> (same_sign x y) (fp.isPositive z))
(=> (diff_sign x y) (fp.isNegative z))))
(define-fun sqr ((x Real)) Real (* x x))
(declare-fun sqrt1 (Real) Real)
(define-fun same_sign_real ((x Float64)
(r Real)) Bool (or (and (fp.isPositive x) (< 0.0 r))
(and (fp.isNegative x) (< r 0.0))))
(declare-datatypes ((t__ref 0))
(((t__refqtmk (t__content Float64)))))
(declare-fun invariant__ (Int Float64) Bool)
(declare-fun invariant____function_guard (Bool Int Float64) Bool)
(declare-fun low_bound (Int) Float64)
(declare-fun low_bound__function_guard (Float64 Int) Bool)
(declare-fun high_bound (Int) Float64)
(declare-fun high_bound__function_guard (Float64 Int) Bool)
(declare-sort float64 0)
(declare-fun user_eq (float64 float64) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE (Float64) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE (us_image) Float64)
(declare-const dummy float64)
(declare-datatypes ((float64__ref 0))
(((float64__refqtmk (float64__content float64)))))
(define-fun float64__ref_float64__content__projection ((a float64__ref)) float64
(float64__content a))
(define-fun dynamic_invariant ((temp___expr_161 Float64)
(temp___is_init_157 Bool) (temp___skip_constant_158 Bool)
(temp___do_toplevel_159 Bool)
(temp___do_typ_inv_160 Bool)) Bool (=>
(or (= temp___is_init_157 true)
(fp.leq (fp.neg (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)) (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
(fp.isFinite64 temp___expr_161)))
(declare-sort frame 0)
(declare-fun frameqtint (frame) Int)
;; frame'axiom
(assert
(forall ((i frame)) (and (<= 0 (frameqtint i)) (<= (frameqtint i) 25000))))
(define-fun in_range ((x Int)) Bool (and (<= 0 x) (<= x 25000)))
(declare-fun attr__ATTRIBUTE_IMAGE1 (Int) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Int)
(declare-fun user_eq1 (frame frame) Bool)
(declare-const dummy1 frame)
(declare-datatypes ((frame__ref 0))
(((frame__refqtmk (frame__content frame)))))
(define-fun frame__ref_frame__content__projection ((a frame__ref)) frame
(frame__content a))
(define-fun dynamic_invariant1 ((temp___expr_168 Int)
(temp___is_init_164 Bool) (temp___skip_constant_165 Bool)
(temp___do_toplevel_166 Bool)
(temp___do_typ_inv_167 Bool)) Bool (=>
(or (= temp___is_init_164 true)
(<= 0 25000)) (in_range
temp___expr_168)))
;; invariant____post_axiom
(assert true)
;; invariant____def_axiom
(assert
(forall ((n Int))
(forall ((speed Float64))
(! (and (forall ((n1 Int)) (low_bound__function_guard (low_bound n1) n1))
(and (forall ((n1 Int)) (high_bound__function_guard (high_bound n1) n1))
(= (= (invariant__ n speed) true)
(and (fp.leq (low_bound n) speed) (fp.leq speed (high_bound n)))))) :pattern (
(invariant__ n speed)) ))))
(declare-const n Int)
(declare-const attr__ATTRIBUTE_ADDRESS Int)
(declare-const factor Float64)
(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
(declare-const old_speed Float64)
(declare-const attr__ATTRIBUTE_ADDRESS2 Int)
(declare-const attr__ATTRIBUTE_ADDRESS3 Int)
(declare-const attr__ATTRIBUTE_ADDRESS4 Int)
(declare-sort tfloat64B 0)
(declare-fun user_eq2 (tfloat64B tfloat64B) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE2 (Float64) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Float64)
(declare-const dummy2 tfloat64B)
(declare-datatypes ((tfloat64B__ref 0))
(((tfloat64B__refqtmk (tfloat64B__content tfloat64B)))))
(define-fun tfloat64B__ref_tfloat64B__content__projection ((a tfloat64B__ref)) tfloat64B
(tfloat64B__content a))
(declare-sort ratio_t 0)
(define-fun in_range1 ((x Float64)) Bool (and (fp.isFinite64 x)
(and
(fp.leq (fp.neg (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) x)
(fp.leq x (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))))
(declare-fun user_eq3 (ratio_t ratio_t) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE3 (Float64) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Float64)
(declare-const dummy3 ratio_t)
(declare-datatypes ((ratio_t__ref 0))
(((ratio_t__refqtmk (ratio_t__content ratio_t)))))
(define-fun ratio_t__ref_ratio_t__content__projection ((a ratio_t__ref)) ratio_t
(ratio_t__content a))
(define-fun dynamic_invariant2 ((temp___expr_175 Float64)
(temp___is_init_171 Bool) (temp___skip_constant_172 Bool)
(temp___do_toplevel_173 Bool)
(temp___do_typ_inv_174 Bool)) Bool (=>
(or (= temp___is_init_171 true)
(fp.leq (fp.neg (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))
(in_range1 temp___expr_175)))
;; low_bound__post_axiom
(assert
(forall ((n1 Int))
(! (=> (dynamic_invariant1 n1 true true true true)
(let ((result (low_bound n1)))
(=> (low_bound__function_guard result n1) (dynamic_invariant result true
false true true)))) :pattern ((low_bound n1)) )))
;; low_bound__def_axiom
(assert
(forall ((n1 Int))
(! (=> (dynamic_invariant1 n1 true true true true)
(= (low_bound n1) (fp.sub RNE (fp.mul RNE ((_ to_fp 11 53) RNE (to_real (* n1 n1))) (fp.neg (fp #b0 #b10000000101 #b0000000000000000000000000000000000000000000000000000))) (fp #b0 #b01111111010 #b1111101010101100110110011110100000111110010000100110)))) :pattern (
(low_bound n1)) )))
;; high_bound__post_axiom
(assert
(forall ((n1 Int))
(! (=> (dynamic_invariant1 n1 true true true true)
(let ((result (high_bound n1)))
(=> (high_bound__function_guard result n1) (dynamic_invariant result
true false true true)))) :pattern ((high_bound n1)) )))
;; high_bound__def_axiom
(assert
(forall ((n1 Int))
(! (=> (dynamic_invariant1 n1 true true true true)
(= (high_bound n1) (fp.add RNE (fp.mul RNE ((_ to_fp 11 53) RNE (to_real (* n1 n1))) (fp #b0 #b10000000101 #b0000000000000000000000000000000000000000000000000000)) (fp #b0 #b01111111010 #b1111101010101100110110011110100000111110010000100110)))) :pattern (
(high_bound n1)) )))
(assert
;; defqtvc
;; File "attempt_2.adb", line 24, characters 0-0
(not
(forall ((new_speed Float64) (average Float64))
(=> (dynamic_invariant1 n true false true true)
(=> (dynamic_invariant2 factor true false true true)
(=> (dynamic_invariant old_speed true false true true)
(=> (dynamic_invariant new_speed false false true true)
(=> (dynamic_invariant average false false true true)
(=> (< n 25000)
(=> (invariant____function_guard (invariant__ n old_speed) n old_speed)
(=> (= (invariant__ n old_speed) true)
(let ((o (fp.add RNE old_speed (fp.mul RNE (fp.mul RNE factor (fp #b0 #b10000000000 #b1101101100000010000011000100100110111010010111100011)) (fp #b0 #b01111111001 #b0001000100010001000100010001000100010001000100010001)))))
(=> (fp.isFinite64 o)
(forall ((new_speed1 Float64))
(=> (= new_speed1 o)
(=> (fp.isFinite64 (fp.add RNE old_speed new_speed1))
(=>
(forall ((new_speed2 Float64)) (invariant____function_guard
(invariant__ (+ n 1) new_speed2) (+ n 1) new_speed2))
(= (invariant__ (+ n 1) new_speed1) true))))))))))))))))))
(check-sat)
(exit)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment