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.
---
 test-suite/output/MExtraction.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 352e422cf7..36992e4dda 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -7,6 +7,6 @@ Require Import QMicromega.
 Require Import RMicromega.
 
 Recursive Extraction
-  List.map RingMicromega.simpl_cone (*map_cone  indexes*)
-  denorm Qpower vm_add
-  n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+   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.
-- 
cgit v1.2.3