why3/bench/encoding at 23.2 - why3 - ProxGit

ada/why3

mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00

Files

History

Guillaume Melquiond efb51e7d43 Merge theories and modules into stdlib (fix issue #62 ).

2017-12-15 15:34:35 +01:00

..

bench encoding

2011-02-10 18:12:47 +01:00

typing of bench encoding

2011-07-01 17:29:29 +02:00

.gitignore

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

benchs

benchs encoding : misspelled bench name

2011-05-11 09:19:26 +02:00

benchs_yices

benchs encoding : misspelled bench name

2011-05-11 09:19:26 +02:00

bool_inf.why

typing of bench encoding

2011-07-01 17:29:29 +02:00

clean.sh

Split the bench in four

2011-02-11 17:46:39 +01:00

columns

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

compute_result.sh

bench : compute_result.sh spelling fix, pretty much the same results as before (+-2)

2011-05-16 16:04:47 +02:00

create_bench.sh

separate symbol discrimination from polymorphism encoding

2011-06-03 22:21:40 +02:00

create_diff.sh

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

diff_all2.sh

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

diff_all.sh

Split the bench in four

2011-02-11 17:46:39 +01:00

gen_allbench.sh

separate symbol discrimination from polymorphism encoding

2011-06-03 22:21:40 +02:00

lines

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

meta.why

do not put spaces around colon in metas and labels

2016-03-08 16:48:59 +01:00

README

update commit number

2011-05-11 09:21:26 +02:00

result

resultat bench encoding

2011-02-11 12:04:43 +01:00

run_bench.sh

relativize path for the benchs of frocos

2011-05-10 14:01:55 +02:00

see_result.sh

Split the bench in four

2011-02-11 17:46:39 +01:00

template_rc

separate symbol discrimination from polymorphism encoding

2011-06-03 22:21:40 +02:00

unit_inf.why

typing of bench encoding

2011-07-01 17:29:29 +02:00

why.conf

Merge theories and modules into stdlib (fix issue #62 ).

2017-12-15 15:34:35 +01:00

yices_columns

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

yices_lines

benchs for frocos paper exported

2011-05-09 22:00:41 +02:00

README

How to reproduce the bench for "Expressing Polymorphic Types in a Many-Sorted Language" of FROCOS'11

The result of this bench can be reproduce using Why3 in the following way:

- You need to come back to version 69dd88e5c34808de3905aa3e257288d19e3b643c with
  git checkout 69dd88e5c34808de3905aa3e257288d19e3b643c, and
- You need to configure with --enable-local and compile why3.
- After that you should set in ./why.conf in the
  section [main] the variable "running_provers_max" to your own
  number of core. You need CVC3, Z3 and Yices.
- Run ./gen_allbench.sh generates one file, bench, by possible set of parameters
- Run ./run_bench.sh  (it takes 10 hours with 7 core). It runs the benchs used in the paper
- Run ./compute_result.sh (it takes 10seconds) to compute the comparison tables. It needs csvtool.

nb: bool_inf and unit_inf are used in order to be able to use explicit