diff options
| author | Frédéric Besson | 2019-03-08 09:56:49 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2019-04-01 12:08:45 +0200 |
| commit | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (patch) | |
| tree | 2f09d223261f45a527b36231a4f74c803ccf8fa6 /doc/stdlib | |
| parent | 4c3f4d105a32cc7661ae714fe4e25619e32bc84c (diff) | |
Several improvements and fixes of Lia
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/hidden-files | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b58148ffff..b25104ddb9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -22,6 +22,7 @@ plugins/extraction/Extraction.v plugins/funind/FunInd.v plugins/funind/Recdef.v plugins/ltac/Ltac.v +plugins/micromega/DeclConstant.v plugins/micromega/Env.v plugins/micromega/EnvRing.v plugins/micromega/Fourier.v |