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, 44 insertions, 3 deletions

diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 9d03560b71..40aeef3959 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -19,11 +19,31 @@
 (*                                                                      *)
 (************************************************************************)
 
-let rec pp_list f o l =
+
+module ISet = Set.Make(Int)
+
+module IMap =
+  struct
+    include Map.Make(Int)
+
+    let from k m =
+      let (_,_,r) = split (k-1) m in
+      r
+  end
+
+(*let output_int o i = output_string o (string_of_int i)*)
+
+let iset_pp o s =
+  Printf.fprintf o "{ %a }"
+    (fun o s ->  ISet.iter (fun i -> Printf.fprintf o "%i " i) s) s
+
+let rec pp_list s f o l =
   match l with
     | [] -> ()
-    | e::l -> f o e ; output_string o ";" ; pp_list f o l
+    | [e] -> f o e
+    | e::l -> f o e ; output_string o s ; pp_list s f o l
 
+let output_bigint o bi = output_string o (Big_int.string_of_big_int bi)
 
 let finally f rst =
   try
@@ -79,6 +99,12 @@ let extract pred l =
 		    |  _   -> (fd, e::sys)
 		 ) (None,[]) l
 
+let extract_all pred l  =
+  List.fold_left (fun (s1,s2) e ->
+      match pred e with
+      | None -> s1,e::s2
+      | Some v -> (v,e)::s1 , s2) ([],[]) l
+
 open Num
 open Big_int
 
@@ -117,7 +143,22 @@ let rats_to_ints l =
   List.map (fun x ->  (div_big_int (mult_big_int (numerator x) c)
 			(denominator x))) l
 
-(* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *)
+let iterate_until_stable f x =
+ let rec iter x =
+  match f x with
+  | None -> x
+  | Some x' -> iter x' in
+ iter x
+
+let rec app_funs l x =
+ match l with
+ | [] -> None
+ | f::fl ->
+  match f x with
+  | None    -> app_funs fl x
+  | Some x' -> Some x'
+
+
 (**
   * MODULE: Coq to Caml data-structure mappings
   *)