ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/bench/infer
History
Claude Marche 8b3fe28b23 improved efficiency of BDD-infer 
also use "if c then e1 else e2" in generated formulas instead of
(c /\ e1) \/ (not c /\ e2)
2023-04-28 09:58:02 +02:00
..
bddinfer-oracles
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
infer-oracles
support for logic defs + decompile translations bool <-> prop
2023-01-16 14:22:06 +00:00
aliasing.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
assign_bool.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
assign_cond.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
auto_array1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_array_false.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_cst1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_ref0.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_ref1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_ref2.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_ref3.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
auto_ref_false.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
binary_search1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
binary_search2.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
binary_search.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
bool_bw_and.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
bool_cond.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
bool_ops.mlw
support for Boolean variable directly as a condition
2022-07-20 12:55:44 +02:00
bools.mlw
support for logic defs + decompile translations bool <-> prop
2023-01-16 14:22:06 +00:00
call_inside_expr.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
call_val_in_loop.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
counter_andb.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
counter_break.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
counter.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
disjunction1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
divmod.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
double_count_bool.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
double_count_vars.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
double_count.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
example_ternary.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
exec_of_andb.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
if.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
iff.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
ifint.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
incr.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
junjie.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
logic_def.mlw
support for logic defs + decompile translations bool <-> prop
2023-01-16 14:22:06 +00:00
mccarthy.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
merge_sort.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
minus1.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
mult.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
neg1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
pbinfer2_simplified.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
pbinfer2.mlw
fix translation of function calls to AST
2022-07-19 19:05:11 +02:00
precision0.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
precision1.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
precision2.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
precision3.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
precision4.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
precision5.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
ref3.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
return_function.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
sttt.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00
support1.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
support2.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
support3.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
support4.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
support5.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
try1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
try3.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
tuple1.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
tuple2.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
twoway.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
uf6.mlw
activate all tests, a bunch of unsupported feature identified
2022-07-20 12:19:11 +02:00
val_call_unit_arg.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
val_call.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
val_writes_param.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
while1.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while2.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while3.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while4.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while5.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while6.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while7.mlw
run infer bench with the new BDD inference engine
2022-07-19 15:35:55 +02:00
while_and_int.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
while_break_bool.mlw
Support for break in BDDinfer
2022-11-17 17:13:21 +01:00
while_break.mlw
Support for break in BDDinfer
2022-11-17 17:13:21 +01:00
while_inv_loc_var.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
while_loop_bis.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
while_loop_bool.mlw
move oracles in a separate subdir
2022-07-19 16:41:36 +02:00
while_loop_count.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
while_loop_ref.mlw
complements on BDDinfer
2023-01-20 17:38:10 +01:00
while_loop.mlw
move oracles in a separate subdir
2022-07-19 16:41:36 +02:00
widening_demo.mlw
improved efficiency of BDD-infer
2023-04-28 09:58:02 +02:00