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/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index e35393b5e8..a1c6586d8a 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -122,7 +122,7 @@ run: $(SUBSYSTEMS)
 bugs: $(BUGS)
 
 clean:
-	rm -f trace .lia.cache output/MExtraction.out
+	rm -f trace .nia.cache .lia.cache output/MExtraction.out
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
 	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
-- 
cgit v1.2.3