Commit b8ce06ce authored by François Bobot's avatar François Bobot
Browse files

bench encoding

parent 39f3a317
[tools twin_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Twin"
use = "meta.Deco"
[tools partial_deco]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Deco"
[tools twin_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Explicit"
use = "meta.Twin"
[tools partial_explicit]
prover = "cvc3"
prover = "z3"
prover = "yices"
timelimit = 30
memlimit = 2048
loadpath = "."
use = "meta.Partial"
use = "meta.Explicit"
[probs caduceus]
file = "why3/caduceus/abs_why.why"
file = "why3/caduceus/alloca_why.why"
file = "why3/caduceus/alloc_why.why"
file = "why3/caduceus/all_why.why"
file = "why3/caduceus/all_zeros_why.why"
file = "why3/caduceus/arith_why.why"
file = "why3/caduceus/array_why.why"
file = "why3/caduceus/assigns2_why.why"
file = "why3/caduceus/assigns_range_right_why.why"
file = "why3/caduceus/assigns_why.why"
file = "why3/caduceus/band_why.why"
file = "why3/caduceus/binary_search_overflows_why.why"
file = "why3/caduceus/binary_search_safety_why.why"
file = "why3/caduceus/binary_search_why.why"
file = "why3/caduceus/blit_why.why"
file = "why3/caduceus/break_why.why"
file = "why3/caduceus/bresenham_why.why"
file = "why3/caduceus/bug_why.why"
file = "why3/caduceus/calloc_why.why"
file = "why3/caduceus/call_why.why"
file = "why3/caduceus/clash_why.why"
file = "why3/caduceus/consts_why.why"
file = "why3/caduceus/const_why.why"
file = "why3/caduceus/continue_why.why"
file = "why3/caduceus/coord_why.why"
file = "why3/caduceus/copy_why.why"
file = "why3/caduceus/count_bits_2_why.why"
file = "why3/caduceus/count_bits_why.why"
file = "why3/caduceus/dassault_1_why.why"
file = "why3/caduceus/Dillon_why.why"
file = "why3/caduceus/division_why.why"
file = "why3/caduceus/dowhile_why.why"
file = "why3/caduceus/enum_why.why"
file = "why3/caduceus/e_why.why"
file = "why3/caduceus/extern_why.why"
file = "why3/caduceus/fact_why.why"
file = "why3/caduceus/false2_why.why"
file = "why3/caduceus/false_why.why"
file = "why3/caduceus/fib_why.why"
file = "why3/caduceus/flag_checkenum_why.why"
file = "why3/caduceus/flag_why.why"
file = "why3/caduceus/float_why.why"
file = "why3/caduceus/gappa_why.why"
file = "why3/caduceus/ghost2_why.why"
file = "why3/caduceus/ghost_why.why"
file = "why3/caduceus/goto_why.why"
file = "why3/caduceus/heapsort_swap_safety_why.why"
file = "why3/caduceus/heapsort_swap_why.why"
file = "why3/caduceus/heapsort_why.why"
file = "why3/caduceus/heap_why.why"
file = "why3/caduceus/ifs_why.why"
file = "why3/caduceus/incr_why.why"
file = "why3/caduceus/init2_why.why"
file = "why3/caduceus/init_why.why"
file = "why3/caduceus/insertion_safety_why.why"
file = "why3/caduceus/insertion_why.why"
file = "why3/caduceus/invariants_why.why"
file = "why3/caduceus/keiko1_why.why"
file = "why3/caduceus/labels_why.why"
file = "why3/caduceus/latespec_why.why"
file = "why3/caduceus/lexico_why.why"
file = "why3/caduceus/linked-list_why.why"
file = "why3/caduceus/logic_cast_why.why"
file = "why3/caduceus/logic_why.why"
file = "why3/caduceus/loop_assigns_why.why"
file = "why3/caduceus/loop_inv_why.why"
file = "why3/caduceus/loops_why.why"
file = "why3/caduceus/malloc_why.why"
file = "why3/caduceus/math_mod_why.why"
file = "why3/caduceus/matrix_why.why"
file = "why3/caduceus/mean_why.why"
file = "why3/caduceus/muller_why.why"
file = "why3/caduceus/negate_why.why"
file = "why3/caduceus/not_assigns_why.why"
file = "why3/caduceus/null_why.why"
file = "why3/caduceus/overflows_why.why"
file = "why3/caduceus/param_why.why"
file = "why3/caduceus/passing_why.why"
file = "why3/caduceus/pi_again_why.why"
file = "why3/caduceus/pi_why.why"
file = "why3/caduceus/pointer_why.why"
file = "why3/caduceus/purse_why.why"
file = "why3/caduceus/queue_jr_why.why"
file = "why3/caduceus/queue_why.why"
file = "why3/caduceus/rc4_why.why"
file = "why3/caduceus/rec2_why.why"
file = "why3/caduceus/rec_why.why"
file = "why3/caduceus/ref_glob_why.why"
file = "why3/caduceus/ref_why.why"
file = "why3/caduceus/russian_why.why"
file = "why3/caduceus/search_why.why"
file = "why3/caduceus/see_why.why"
file = "why3/caduceus/selection_safety_why.why"
file = "why3/caduceus/selection_why.why"
file = "why3/caduceus/separation1_why.why"
file = "why3/caduceus/separation2_why.why"
file = "why3/caduceus/separation3_why.why"
file = "why3/caduceus/separation4_why.why"
file = "why3/caduceus/separation_why.why"
file = "why3/caduceus/shift_why.why"
file = "why3/caduceus/sort_why.why"
file = "why3/caduceus/sqrt_why.why"
file = "why3/caduceus/strcpy_why.why"
file = "why3/caduceus/string_why.why"
file = "why3/caduceus/struct2_why.why"
file = "why3/caduceus/struct3_why.why"
file = "why3/caduceus/struct4_why.why"
file = "why3/caduceus/struct_why.why"
file = "why3/caduceus/sum1_why.why"
file = "why3/caduceus/sum2_why.why"
file = "why3/caduceus/switch_why.why"
file = "why3/caduceus/tracability_why.why"
file = "why3/caduceus/trop_why.why"
file = "why3/caduceus/unsafe_why.why"
file = "why3/caduceus/zones2_why.why"
file = "why3/caduceus/zones_why.why"
[probs caduceus_why]
file = "why3/caduceus_why/algo64_why.why"
file = "why3/caduceus_why/algo65_why.why"
file = "why3/caduceus_why/all_why.why"
file = "why3/caduceus_why/arith_why.why"
file = "why3/caduceus_why/bresenham_why.why"
file = "why3/caduceus_why/bsearch_why.why"
file = "why3/caduceus_why/dijkstra_why.why"
file = "why3/caduceus_why/exns_why.why"
file = "why3/caduceus_why/fib_why.why"
file = "why3/caduceus_why/find_why.why"
file = "why3/caduceus_why/gcd_why.why"
file = "why3/caduceus_why/heapsort_why.why"
file = "why3/caduceus_why/inductive_why.why"
file = "why3/caduceus_why/loop0_why.why"
file = "why3/caduceus_why/loops_why.why"
file = "why3/caduceus_why/mac_carthy_why.why"
file = "why3/caduceus_why/maximumsort_why.why"
file = "why3/caduceus_why/max_why.why"
file = "why3/caduceus_why/mergesort_why.why"
file = "why3/caduceus_why/oldify_why.why"
file = "why3/caduceus_why/opaque_why.why"
file = "why3/caduceus_why/peano_why.why"
file = "why3/caduceus_why/poly_why.why"
file = "why3/caduceus_why/power_why.why"
file = "why3/caduceus_why/po_why.why"
file = "why3/caduceus_why/queens_why.why"
file = "why3/caduceus_why/quicksort2_why.why"
file = "why3/caduceus_why/quicksort_why.why"
file = "why3/caduceus_why/recfun_why.why"
file = "why3/caduceus_why/return_why.why"
file = "why3/caduceus_why/search_why.why"
file = "why3/caduceus_why/see_why.why"
file = "why3/caduceus_why/selection_why.why"
file = "why3/caduceus_why/set_why.why"
file = "why3/caduceus_why/sqrt_dicho_why.why"
file = "why3/caduceus_why/sqrt_why.why"
file = "why3/caduceus_why/swap0_why.why"
file = "why3/caduceus_why/wpcalls_why.why"
[probs dancing_rev]
file = "why3/dancing/bug2_why.why"
file = "why3/dancing/i_behavior.myset_why.why"
file = "why3/dancing/i_behavior_oracle.myset_why.why"
file = "why3/dancing/i_dancing.myset_why.why"
file = "why3/dancing/i_safety_frame_jessie_why.why"
file = "why3/dancing/i_safety.myset_why.why"
file = "why3/dancing/i_safety.notinft2_why.why"
file = "why3/dancing/i_safety.notinft_why.why"
file = "why3/rev/notinc_disj_FT.ft_is_a_pred_why.why"
file = "why3/rev/notinc_disj_FT.with_notin___why.why"
file = "why3/rev/notinc_disj_FT.without_inductive_FT_why.why"
file = "why3/rev/notin.jessie_frame_why.why"
[bench twin_deco]
tools = twin_deco
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "twin_deco.time"
average = "twin_deco.avg"
csv = "twin_deco.csv"
[bench partial_deco]
tools = partial_deco
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "partial_deco.time"
average = "partial_deco.avg"
csv = "partial_deco.csv"
[bench twin_explicit]
tools = twin_explicit
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "twin_explicit.time"
average = "twin_explicit.avg"
csv = "twin_explicit.csv"
[bench partial_explicit]
tools = partial_explicit
probs = caduceus
probs = caduceus_why
probs = dancing_rev
timeline = "partial_explicit.time"
average = "partial_explicit.avg"
csv = "partial_explicit.csv"
theory Partial
meta "enco_kept" "instantiate"
end
theory Twin
meta "enco_kept" "bridge"
end
theory Partial_incomplete
meta "enco_kept" "instantiate"
meta "encoding_instantiate : complete" "no"
end
theory Explicit
meta "enco_poly" "explicit"
end
theory Deco
meta "enco_poly" "decorate"
end
theory Goal
meta "enco_select" "goal"
end
\ No newline at end of file
#!/bin/sh
why3bench -B bench.rc "$@"
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
logic eq_unit : unit, unit -> prop
logic neq_unit : unit, unit -> prop
logic eq_bool : bool, bool -> prop
logic neq_bool : bool, bool -> prop
logic lt_int : int, int -> prop
logic le_int : int, int -> prop
logic gt_int : int, int -> prop
logic ge_int : int, int -> prop
logic eq_int : int, int -> prop
logic neq_int : int, int -> prop
logic add_int : int, int -> int
logic sub_int : int, int -> int
logic mul_int : int, int -> int
logic div_int : int, int -> int
logic mod_int : int, int -> int
logic neg_int : int -> int
predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
logic bw_compl : int -> int
logic bw_and : int, int -> int
logic bw_xor : int, int -> int
logic bw_or : int, int -> int
logic lsl : int, int -> int
logic lsr : int, int -> int
type 'z pointer
type 'z addr
type alloc_table
logic block_length : alloc_table, 'a1 pointer -> int
logic base_addr : 'a1 pointer -> 'a1 addr
logic offset : 'a1 pointer -> int
logic shift : 'a1 pointer, int -> 'a1 pointer
logic sub_pointer : 'a1 pointer, 'a1 pointer -> int
predicate lt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
((base_addr(p1) = base_addr(p2)) and (offset(p1) < offset(p2)))
predicate le_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
((base_addr(p1) = base_addr(p2)) and (offset(p1) <= offset(p2)))
predicate gt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
((base_addr(p1) = base_addr(p2)) and (offset(p1) > offset(p2)))
predicate ge_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
((base_addr(p1) = base_addr(p2)) and (offset(p1) >= offset(p2)))
predicate valid(a: alloc_table, p: 'a1 pointer) =
((0 <= offset(p)) and (offset(p) < block_length(a, p)))
predicate valid_index(a: alloc_table, p: 'a1 pointer, i: int) =
((0 <= (offset(p) + i)) and ((offset(p) + i) < block_length(a, p)))
predicate valid_range(a: alloc_table, p: 'a1 pointer, i: int, j: int) =
((0 <= (offset(p) + i)) and ((offset(p) + j) < block_length(a, p)))
axiom offset_shift:
(forall p:'a1 pointer.
(forall i:int [offset(shift(p, i))]. (offset(shift(p,
i)) = (offset(p) + i))))
axiom shift_zero: (forall p:'a1 pointer [shift(p, 0)]. (shift(p, 0) = p))
axiom shift_shift:
(forall p:'a1 pointer.
(forall i:int.
(forall j:int [shift(shift(p, i), j)]. (shift(shift(p, i),
j) = shift(p, (i + j))))))
axiom base_addr_shift:
(forall p:'a1 pointer.
(forall i:int [base_addr(shift(p, i))]. (base_addr(shift(p,
i)) = base_addr(p))))
axiom block_length_shift:
(forall a:alloc_table.
(forall p:'a1 pointer.
(forall i:int [block_length(a, shift(p, i))]. (block_length(a, shift(p,
i)) = block_length(a, p)))))
axiom base_addr_block_length:
(forall a:alloc_table.
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
((base_addr(p1) = base_addr(p2)) -> (block_length(a,
p1) = block_length(a, p2))))))
axiom pointer_pair_1:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
(((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))) ->
(p1 = p2))))
axiom pointer_pair_2:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
((p1 = p2) ->
((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))))))
axiom neq_base_addr_neq_shift:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
(forall i:int.
(forall j:int.
((base_addr(p1) <> base_addr(p2)) -> (shift(p1, i) <> shift(p2, j)))))))
axiom neq_offset_neq_shift:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
(forall i:int.
(forall j:int.
(((offset(p1) + i) <> (offset(p2) + j)) -> (shift(p1,
i) <> shift(p2, j)))))))
axiom eq_offset_eq_shift:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
(forall i:int.
(forall j:int.
((base_addr(p1) = base_addr(p2)) ->
(((offset(p1) + i) = (offset(p2) + j)) -> (shift(p1,
i) = shift(p2, j))))))))
axiom valid_index_valid_shift:
(forall a:alloc_table.
(forall p:'a1 pointer.
(forall i:int. (valid_index(a, p, i) -> valid(a, shift(p, i))))))
axiom valid_range_valid_shift:
(forall a:alloc_table.
(forall p:'a1 pointer.
(forall i:int.
(forall j:int.
(forall k:int.
(valid_range(a, p, i, j) ->
(((i <= k) and (k <= j)) -> valid(a, shift(p, k)))))))))
axiom valid_range_valid:
(forall a:alloc_table.
(forall p:'a1 pointer.
(forall i:int.
(forall j:int.
(valid_range(a, p, i, j) ->
(((i <= 0) and (0 <= j)) -> valid(a, p)))))))
axiom valid_range_valid_index:
(forall a:alloc_table.
(forall p:'a1 pointer.
(forall i:int.
(forall j:int.
(forall k:int.
(valid_range(a, p, i, j) ->
(((i <= k) and (k <= j)) -> valid_index(a, p, k))))))))
axiom sub_pointer_def:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer.
((base_addr(p1) = base_addr(p2)) -> (sub_pointer(p1,
p2) = (offset(p1) - offset(p2))))))
type ('a, 'z) memory
logic acc : ('a1, 'a2) memory, 'a2 pointer -> 'a1
logic upd : ('a1, 'a2) memory, 'a2 pointer, 'a1 -> ('a1, 'a2) memory
axiom acc_upd:
(forall m:('a1, 'a2) memory.
(forall p:'a2 pointer.
(forall a:'a1 [acc(upd(m, p, a), p)]. (acc(upd(m, p, a), p) = a))))
axiom acc_upd_neq:
(forall m:('a1, 'a2) memory.
(forall p1:'a2 pointer.
(forall p2:'a2 pointer.
(forall a:'a1 [acc(upd(m, p1, a), p2)].
((p1 <> p2) -> (acc(upd(m, p1, a), p2) = acc(m, p2)))))))
axiom false_not_true: (false <> true)
type 'z pset
logic pset_empty : 'a1 pset
logic pset_singleton : 'a1 pointer -> 'a1 pset
logic pset_star : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
logic pset_all : 'a1 pset -> 'a1 pset
logic pset_range : 'a1 pset, int, int -> 'a1 pset
logic pset_range_left : 'a1 pset, int -> 'a1 pset
logic pset_range_right : 'a1 pset, int -> 'a1 pset
logic pset_acc_all : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
logic pset_acc_range : 'a2 pset, ('a1 pointer, 'a2) memory, int,
int -> 'a1 pset
logic pset_acc_range_left : 'a2 pset, ('a1 pointer, 'a2) memory,
int -> 'a1 pset
logic pset_acc_range_right : 'a2 pset, ('a1 pointer, 'a2) memory,
int -> 'a1 pset
logic pset_union : 'a1 pset, 'a1 pset -> 'a1 pset
logic not_in_pset : 'a1 pointer, 'a1 pset -> prop
predicate not_assigns(a: alloc_table, m1: ('a1, 'a2) memory, m2: ('a1,
'a2) memory, l: 'a2 pset) =
(forall p:'a2 pointer.
(valid(a, p) -> (not_in_pset(p, l) -> (acc(m2, p) = acc(m1, p)))))
axiom pset_empty_intro: (forall p:'a1 pointer. not_in_pset(p, pset_empty))
axiom pset_singleton_intro:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
((p1 <> p2) -> not_in_pset(p1, pset_singleton(p2)))))
axiom pset_singleton_elim:
(forall p1:'a1 pointer.
(forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
(not_in_pset(p1, pset_singleton(p2)) -> (p1 <> p2))))
axiom not_not_in_singleton:
(forall p:'a1 pointer. (not not_in_pset(p, pset_singleton(p))))
axiom pset_union_intro:
(forall l1:'a1 pset.
(forall l2:'a1 pset.
(forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
((not_in_pset(p, l1) and not_in_pset(p, l2)) -> not_in_pset(p,
pset_union(l1, l2))))))
axiom pset_union_elim1:
(forall l1:'a1 pset.
(forall l2:'a1 pset.
(forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
(not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l1)))))
axiom pset_union_elim2:
(forall l1:'a1 pset.
(forall l2:'a1 pset.
(forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
(not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l2)))))
axiom pset_star_intro:
(forall l:'a1 pset.
(forall m:('a2 pointer, 'a1) memory.
(forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
((forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l))) ->
not_in_pset(p, pset_star(l, m))))))
axiom pset_star_elim:
(forall l:'a1 pset.
(forall m:('a2 pointer, 'a1) memory.
(forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
(not_in_pset(p, pset_star(l, m)) ->
(forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l)))))))
axiom pset_all_intro:
(forall p:'a1 pointer.
(forall l:'a1 pset [not_in_pset(p, pset_all(l))].
((forall p1:'a1 pointer.
((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))) ->
not_in_pset(p, pset_all(l)))))
axiom pset_all_elim:
(forall p:'a1 pointer.
(forall l:'a1 pset [not_in_pset(p, pset_all(l))].
(not_in_pset(p, pset_all(l)) ->
(forall p1:'a1 pointer.
((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))))))
axiom pset_range_intro:
(forall p:'a1 pointer.
(forall l:'a1 pset.
(forall a:int.
(forall b:int [not_in_pset(p, pset_range(l, a, b))].
((forall p1:'a1 pointer.
(not_in_pset(p1, l) or
(forall i:int.
(((a <= i) and (i <= b)) -> (p <> shift(p1, i)))))) ->
not_in_pset(p, pset_range(l, a, b)))))))
axiom pset_range_elim:
(forall p:'a1 pointer.
(forall l:'a1 pset.
(forall a:int.
(forall b:int [not_in_pset(p, pset_range(l, a, b))].
(not_in_pset(p, pset_range(l, a, b)) ->
(forall p1:'a1 pointer.
((not not_in_pset(p1, l)) ->
(forall i:int.
(((a <= i) and (i <= b)) -> (shift(p1, i) <> p))))))))))
axiom pset_range_left_intro:
(forall p:'a1 pointer.
(forall l:'a1 pset.
(forall a:int [not_in_pset(p, pset_range_left(l, a))].
((forall p1:'a1 pointer.
(not_in_pset(p1, l) or
(forall i:int. ((i <= a) -> (p <> shift(p1, i)))))) ->
not_in_pset(p, pset_range_left(l, a))))))
axiom pset_range_left_elim:
(forall p:'a1 pointer.
(forall l:'a1 pset.
(forall a:int [not_in_pset(p, pset_range_left(l, a))].
(not_in_pset(p, pset_range_left(l, a)) ->
(forall p1:'a1 pointer.
((not not_in_pset(p1, l)) ->
(forall i:int. ((i <= a) -> (shift(p1, i) <> p)))))))))
axiom pset_range_right_intro:
(forall p:'a1 pointer.
(forall l:'a1 pset.
(forall a:int [not_in_pset(p, pset_range_right(l, a))].
((forall p1:'a1 pointer.
(not_in_pset(p1, l) or
(forall i:int. ((a <= i) -> (p <> shift(p1, i)))))) ->