Refactoring of Micromega code using a Simplex linear solver

- Simplex based linear prover
  Unset Simplex to get Fourier elimination
  For lia and nia, do not enumerate but generate cutting planes.
- Better non-linear support
  Factorisation of the non-linear pre-processing
  Careful handling of equation x=e, x is only eliminated if x is used linearly
- More opaque interfaces
  (Linear solvers Simplex and Mfourier are independent)
- Set Dump Arith "file" so that lia,nia calls generate Coq goals
  in filexxx.v. Used to collect benchmarks and regressions.
- Rationalise the test-suite
  example.v only tests psatz Z
  example_nia.v only tests lia, nia
  In both files, the tests are in essence the same.
  In particular, if a test is solved by psatz but not by nia,
  we finish the goal by an explicit Abort.
  There are additional tests in example_nia.v which require specific
  integer reasoning out of scope of psatz.

1 files changed, 5 insertions, 6 deletions

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 158ddb589b..5f01f981ef 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -53,12 +53,11 @@ 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 "plugins/micromega/micromega.ml" *)
-(* Recursive Extraction *)
-(*   List.map simpl_cone (*map_cone  indexes*) *)
-(*   denorm Qpower vm_add *)
-(*   n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. *)
-
+(*Extraction "micromega.ml"
+(*Recursive Extraction*)   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: *)
 (* coding: utf-8 *)
 (* End: *)