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, 24 insertions, 4 deletions

diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index 13d50d1eee..e925f1bc5e 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -10,13 +10,33 @@
 
 module Mc = Micromega
 
-type 'a number_spec
 
+(** [use_simplex] is bound to the Coq option Simplex.
+    If set, use the Simplex method, otherwise use Fourier *)
+val use_simplex : bool ref
+
+(** [dump_file] is bound to the Coq option Dump Arith.
+    If set to some [file], arithmetic goals are dumped in filexxx.v *)
+val dump_file : string option ref
+
+(** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *)
 val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
+
+(** [z_cert_of_pos prf] converts a Sos proof into an integer Coq proof *)
 val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz
+
+(** [lia enum depth sys] generates an unsat proof for the linear constraints in [sys].
+    If the Simplex option is set, any failure to find a proof should be considered as a bug. *)
 val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> Mc.zArithProof option
+
+(** [nlia enum depth sys] generates an unsat proof for the non-linear constraints in [sys].
+    The solver is incomplete -- the problem is undecidable *)
 val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> Mc.zArithProof option
+
+(** [linear_prover_with_cert depth sys] generates an unsat proof for the linear constraints in [sys].
+    Over the rationals, the solver is complete. *)
+val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> Mc.q Micromega.psatz option
+
+(** [nlinear depth sys] generates an unsat proof for the non-linear constraints in [sys].
+    The solver is incompete -- the problem is decidable. *)
 val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> Mc.q Mc.psatz option
-val linear_prover_with_cert : int -> 'a number_spec ->
-  ('a Mc.pExpr * Mc.op1) list -> 'a Mc.psatz option
-val q_spec : Mc.q number_spec