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, 80 insertions, 0 deletions

diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml
new file mode 100644
index 0000000000..dc1df7ec9f
--- /dev/null
+++ b/plugins/micromega/itv.ml
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Intervals (extracted from mfourier.ml) *)
+
+open Num
+  (** The type of intervals is *)
+  type interval = num option * num option
+      (** None models the absence of bound i.e. infinity *)
+      (** As a result,
+          - None , None   -> \]-oo,+oo\[
+          - None , Some v -> \]-oo,v\]
+          - Some v, None  -> \[v,+oo\[
+          - Some v, Some v' -> \[v,v'\]
+      Intervals needs to be explicitly normalised.
+      *)
+
+  let pp o (n1,n2) =
+      (match n1 with
+       | None -> output_string o "]-oo"
+       | Some n  -> Printf.fprintf o "[%s" (string_of_num n)
+      );
+      output_string o ",";
+      (match n2 with
+       | None -> output_string o "+oo["
+       | Some n -> Printf.fprintf o "%s]" (string_of_num n)
+      )
+
+
+
+  (** if then interval [itv] is empty, [norm_itv itv] returns [None]
+      otherwise, it returns [Some itv] *)
+
+  let norm_itv itv =
+    match itv with
+      | Some a , Some b -> if a <=/ b then Some itv else None
+      |   _             -> Some itv
+
+(** [inter i1 i2 = None] if the intersection of intervals is empty
+    [inter i1 i2 = Some i] if [i] is the intersection of the intervals [i1] and [i2] *)
+  let inter i1 i2 =
+    let (l1,r1) = i1
+    and (l2,r2) = i2 in
+
+    let inter f o1 o2 =
+      match o1 , o2 with
+        | None , None -> None
+        | Some _ , None -> o1
+        | None  , Some _ -> o2
+        | Some n1 , Some n2 -> Some (f n1 n2) in
+
+    norm_itv (inter max_num l1 l2 , inter min_num r1 r2)
+
+  let range = function
+    | None,_ | _,None -> None
+    | Some i,Some j -> Some (floor_num j -/ceiling_num i +/ (Int 1))
+
+
+  let smaller_itv i1 i2 =
+    match  range i1 ,  range i2  with
+      | None , _ -> false
+      |  _   , None -> true
+      | Some i , Some j -> i <=/ j
+
+
+(** [in_bound bnd v] checks whether [v] is within the bounds [bnd] *)
+let in_bound bnd v =
+  let (l,r) = bnd in
+  match l , r with
+    | None , None -> true
+    | None , Some a -> v <=/ a
+    | Some a , None -> a <=/ v
+    | Some a , Some b -> a <=/ v && v <=/ b