[micromega] Sort constraints before performing `subst`

This will be more predictable. In case there are several possible
substitution, the "simplest" is prefered.

3 files changed, 21 insertions, 16 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index f1ae07892e..74d5374193 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -1061,20 +1061,6 @@ let elim_redundant sys = tr_sys "elim_redundant" elim_redundant sys
     A necessary condition is to take the variable with the smallest coefficient *)
 
 let fourier_small (sys : WithProof.t list) =
-  let size ((p, o), prf) =
-    let _, p' = Vect.decomp_cst p in
-    let (x, q), p' = Vect.decomp_fst p' in
-    Vect.fold
-      (fun (l, (q, x)) x' q' ->
-        let q' = Q.abs q' in
-        (l + 1, if q </ q then (q, x) else (q', x')))
-      (1, (Q.abs q, x))
-      p
-  in
-  let cmp ((l1, (q1, _)), ((_, o), _)) ((l2, (q2, _)), ((_, o'), _)) =
-    if l1 < l2 then -1 else if l1 = l2 then Q.compare q1 q2 else 1
-  in
-  let syss = List.sort cmp (List.rev_map (fun wp -> (size wp, wp)) sys) in
   let gen_pivot acc (q, x) wp l =
     List.fold_left
       (fun acc (s, wp') ->
@@ -1091,7 +1077,7 @@ let fourier_small (sys : WithProof.t list) =
     | [] -> acc
     | ((_, qx), wp) :: l' -> all_pivots (gen_pivot acc qx wp (acc @ l')) l'
   in
-  List.rev_map snd (all_pivots [] syss)
+  List.rev_map snd (all_pivots [] (WithProof.sort sys))
 
 let fourier_small = tr_sys "fourier_small" fourier_small
 
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 1462ade7fb..7b29aa15f9 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -1081,6 +1081,22 @@ module WithProof = struct
       | None -> sys0
       | Some sys' -> sys' )
 
+  let sort (sys : t list) =
+    let size ((p, o), prf) =
+      let _, p' = Vect.decomp_cst p in
+      let (x, q), p' = Vect.decomp_fst p' in
+      Vect.fold
+        (fun (l, (q, x)) x' q' ->
+          let q' = Q.abs q' in
+          (l + 1, if q </ q then (q, x) else (q', x')))
+        (1, (Q.abs q, x))
+        p
+    in
+    let cmp ((l1, (q1, _)), ((_, o), _)) ((l2, (q2, _)), ((_, o'), _)) =
+      if l1 < l2 then -1 else if l1 = l2 then Q.compare q1 q2 else 1
+    in
+    List.sort cmp (List.rev_map (fun wp -> (size wp, wp)) sys)
+
   let subst sys0 =
     let elim sys =
       let oeq, sys' = extract (is_substitution true) sys in
@@ -1088,7 +1104,7 @@ module WithProof = struct
       | None -> None
       | Some (v, pc) -> simplify (linear_pivot sys0 pc v) sys'
     in
-    iterate_until_stable elim sys0
+    iterate_until_stable elim (List.map snd (sort sys0))
 
   let saturate_subst b sys0 =
     let select = is_substitution b in
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index 4f59b76549..84b5421207 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -379,6 +379,9 @@ module WithProof : sig
       p = c+a1.x1+....+c.x+...an.xn and c <> 0 *)
   val simple_pivot : Q.t * var -> t -> t -> t option
 
+  (** [sort sys] sorts constraints according to the lexicographic order (number of variables, size of the smallest coefficient *)
+  val sort : t list -> ((int * (Q.t * var)) * t) list
+
   (** [subst sys] performs the equivalent of the 'subst' tactic of Coq.
     For every p=0 \in sys such that p is linear in x with coefficient +/- 1
                                i.e. p = 0 <-> x = e and x \notin e.