why3/bench/encoding at fsf - why3

ada/why3

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

Files

Jacques-Henri Jourdan 3f2f3138c0 Discriminate algebraic types.

That is, duplicate lemmas making use of an algebraic type (either by using a projection, a constructor or a pattern matching) which is tagged by the new meta alginst.

Also:
- Add new select metas for automatically tagging types with alginst
- edit relevent drivers so that discrimination happens before eliminate_algebraic:
    - CVC5
    - Z3 > 4.8.7
    - Vampire 4.5.1
    - why3-smt

2023-01-31 01:46:10 +01:00

why2

bench encoding

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

why3

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

Discriminate algebraic types.

2023-01-31 01:46:10 +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