From 7f445d1027cbcedf91f446bc86afea36840728ba Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 24 Aug 2018 23:10:55 +0200
Subject: 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.
---
 plugins/micromega/MExtraction.v | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'plugins/micromega/MExtraction.v')

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: *)
-- 
cgit v1.2.3