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
Guillaume Melquiond
efb51e7d43
Merge theories and modules into stdlib (fix issue #62 ).
2017-12-15 15:34:35 +01:00
Andrei Paskevich
9fa6da6d2f
do not put spaces around colon in metas and labels
2016-03-08 16:48:59 +01:00
Andrei Paskevich
9f22cd9fdc
remove encoding_bridge, replace by encoding_twin
2011-09-02 13:26:33 +02:00
François Bobot
5f858062b4
typing of bench encoding
2011-07-01 17:29:29 +02:00
Andrei Paskevich
aa2c430e3b
several changes in syntax
...
- No more "and", "or", "implies", "iff", and "~".
Use "/\", "\/", "->", "<->", and "not" instead.
- No more "logic". Use "function" or "predicate".
2011-06-29 19:13:18 +02:00
Andrei Paskevich
35c0d32eab
separate symbol discrimination from polymorphism encoding
2011-06-03 22:21:40 +02:00
Andrei Paskevich
b71623a745
rename files in drivers/
2011-05-22 13:18:03 +02:00
François Bobot
fa6d7f41a9
bench : compute_result.sh spelling fix, pretty much the same results as before (+-2)
2011-05-16 16:04:47 +02:00
François Bobot
ec5701feb6
update commit number
2011-05-11 09:21:26 +02:00
François Bobot
69dd88e5c3
benchs encoding : misspelled bench name
2011-05-11 09:19:26 +02:00
François Bobot
a960dc7cf3
relativize path for the benchs of frocos
2011-05-10 14:01:55 +02:00
François Bobot
e8e0dc51b1
wrong files exported, use finite type (forbidden for explicit)
2011-05-10 13:56:20 +02:00
François Bobot
c84568d770
benchs for frocos paper exported
2011-05-09 22:00:41 +02:00
François Bobot
29bc534a56
Split the bench in four
2011-02-11 17:46:39 +01:00
François Bobot
988ea15a8c
resultat bench encoding
2011-02-11 12:04:43 +01:00
François Bobot
d5afe882b6
spass bench
2011-02-10 20:56:45 +01:00
François Bobot
b8ce06ce7d
bench encoding
2011-02-10 18:12:47 +01:00
