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

1 files changed, 4 insertions, 2 deletions

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 5f01f981ef..6112eda200 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -54,8 +54,10 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 (** In order to avoid annoying build dependencies the actual
     extraction is only performed as a test in the test suite. *)
 (*Extraction "micromega.ml"
-(*Recursive Extraction*)   List.map simpl_cone (*map_cone  indexes*)
-   denorm Qpower vm_add
+           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ
+           List.map simpl_cone (*map_cone  indexes*)
+           denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 *)
 (* Local Variables: *)