Matteo Manighetti
dabd0d669c
Merge attemp
2023-05-17 11:15:20 +02:00
BONNOT Paul
8c839099bb
max_int and max_real values not defined as an axiom
...
Transform eliminate_big_constant for dReal prover
2023-04-04 13:00:22 +00:00
MARCHE Claude
113366e478
add metas for remove_unused:dep for bv relations ult ugt slt ugt
2023-04-03 15:23:00 +00:00
Johannes Kanig
41eac08831
Merging upstream Why3 into AdaCore master
2023-03-28 10:24:25 +09:00
Guillaume Melquiond
e278f4f8d5
Fix documentation typo.
2023-03-17 11:06:39 +01:00
MARCHE Claude
49bc8beb00
Changed the unsecure trusted_wf attribute mechanism into a more secure one
2023-02-22 13:50:29 +00:00
Johannes Kanig
c2d19bee32
W120-033 add rewriting of to_int/of_int pairs
...
We add of_int markers to the stdlib (the of_int markers are in gnat2why
library) and add rewriting code acting upon those markers.
* bv.mlw
add rewrite markers to the of_int function
* gnat_rewrite.ml
add rules for of_int/to_int and to_int/of_int
2023-01-30 08:40:03 +09:00
Solène Moreau
be1023970d
(W112-001) Merge Why3/master into SPARK
...
Change-Id: Iefffe9ad9367fbc1c590efdca96cf6311a02481d
Depends-On: If1f1bbd27aeeee421c8c6adb86fef670a924907a
Depends-On: I6be95441469218c8f9dfef8934764b92453c1727
2023-01-13 14:55:39 +01:00
MARCHE Claude
3718457464
Merge branch 'dreal' into 'master'
...
Support for dreal prover
See merge request why3/why3!749
2022-11-17 15:24:52 +00:00
Jean-Christophe Filliatre
bf06311f78
micro-Python: add_list can be used in logic
2022-11-14 14:58:24 +01:00
Claude Marche
16495323fc
Turn def of max_int, max_real into lemmas, fix bench-ce oracles
2022-11-03 10:55:25 +01:00
Paul Bonnot
05a7bc865d
Corrected some problems that caused crash of dreal
2022-10-20 16:04:23 +02:00
MARCHE Claude
9d25c57276
Add more meta for explicit dependencies in the bitvector library
2022-09-22 13:40:12 +00:00
David Ewert
5f54fca95f
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
Jean-Paul Bodeveix
11e9c87dc5
Improved micro Python
2022-09-08 16:00:22 +02:00
Claude Marche
4ce1079155
New attribute [@vc:trusted_wf]
...
It allows one to declare a relation well-founded without need to prove it
As a side-effect, it does not require to import `relations.WellFounded`
See issue #626
2022-07-22 16:49:21 +02:00
Solène Moreau
74914e7651
(V719-014) Merging Inria/master into SPARK/master
...
Change-Id: I2144736b2dbb76966fbe4eae6238a8751799a3d2
Depends-On: I5a522521b64c6e676113695f30625b9618461867
Depends-On: I51bf388c10a7d73401ebb48c7c3c07828da4af12
2022-07-19 14:57:03 +02:00
MARCHE Claude
99b3693442
Resolve "Constant max_int of ieee_float.GenericFloat should be given a value in its clones"
2022-07-08 17:18:36 +00:00
Claude Marche
c8614700f3
Reimplement the transf in two phases and tail recursive functions
2022-07-07 12:24:42 +02:00
Claude Marche
549f987180
fix elimination of constants.
...
Update oracles
Add elimination also in Alt-Ergo >= 2.4.0 and Z3 >= 4.4.0
2022-06-02 12:37:23 +02:00
Claude Marche
5f830d7c5e
more dependency metas
2022-06-02 09:44:06 +02:00
Claude Marche
abe993e76a
Use the new meta for eliminating int.abs when not needed
2022-06-02 08:36:36 +02:00
Solène Moreau
a29b8b930c
V325-031 Merging Why3/Inria master into Why3/SPARK master
...
Change-Id: Ib12de95cfa922bd1b8c1f5ad1ba269de9c90894c
Depends-On: I3c3e37849899e4436210701c67ddf0049aa08204
Depends-On: I28a9ef2ea1b11448bea50d1f4c4c799e8255fda8
2022-04-26 09:17:30 +02:00
MARCHE Claude
bcfef9818c
Resolve "Fix drivers for SMT-LIB strings"
2022-04-06 14:29:41 +00:00
Solène Moreau
524b938a9d
V325-031 Merge with upstream Why3
...
Change-Id: I2e98bd5ec8c138751713811f4dad164be6a4463a
2022-03-29 10:47:33 +02:00
