Merge PR #18228: Micromega: avoid generating duplicate pivots in four…

…ier_small

Reviewed-by: fajb
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

plugins/micromega/certificate.ml

@@ -916,24 +916,33 @@ let normalise = tr_sys "normalise" normalise
     When there are several variables, we hope to eliminate all the variables.
     A necessary condition is to take the variable with the smallest coefficient *)
 
+let try_pivot qx wp wp' =
+  match WithProof.simple_pivot qx wp wp' with
+  | None -> None
+  | Some wp2 ->
+    match WithProof.cutting_plane wp2 with
+    | Some wp2 -> Some wp2
+    | None -> None
+
 let fourier_small (sys : WithProof.t list) =
-  let gen_pivot acc (q, x) wp l =
-    List.fold_left
-      (fun acc (s, wp') ->
-        match WithProof.simple_pivot (q, x) wp wp' with
-        | None -> acc
-        | Some wp2 -> (
-          match WithProof.cutting_plane wp2 with
-          | Some wp2 -> (s, wp2) :: acc
-          | _ -> acc ))
-      acc l
+  let module WPset = Set.Make(WithProof) in
+  let gen_pivot acc qx wp l =
+    let fold acc wp' =
+      match try_pivot qx wp wp' with
+      | None -> acc
+      | Some wp2 -> WPset.add wp2 acc
+    in
+    let acc = WPset.fold (fun wp acc -> fold acc wp) acc acc in
+    List.fold_left (fun acc (_,wp') -> fold acc wp') acc l
   in
   let rec all_pivots acc l =
     match l with
     | [] -> acc
-    | ((_, qx), wp) :: l' -> all_pivots (gen_pivot acc qx wp (acc @ l')) l'
+    | ((_, qx), wp) :: l' -> all_pivots (gen_pivot acc qx wp l') l'
   in
-  List.rev_map snd (all_pivots [] (WithProof.sort sys))
+  let sys = WithProof.sort sys in
+  let res = all_pivots WPset.empty sys in
+  WPset.elements res
 
 let fourier_small = tr_sys "fourier_small" fourier_small
 

test-suite/bugs/bug_17960.v

@@ -0,0 +1,67 @@
+Require Import ZArith.
+Require Import Lia.
+
+Open Scope Z_scope.
+
+Parameter Znth : Z -> list Z -> Z.
+Parameter Zlength : list Z -> Z.
+Parameter max_unsigned : Z.
+
+Goal forall j r N M row_ptr,
+  Zlength row_ptr = N + 1 ->
+  0 <= r ->
+  r <= Znth 0 row_ptr ->
+  Znth (N + 1 - 1) row_ptr <= max_unsigned ->
+  0 <= j < N ->
+  0 <= M ->
+  0 <= N + 1 ->
+  0 <= j + 1 < N + 1 ->
+  0 <= j + 1 < N + 1 ->
+  j + 1 <= j + 1 + 0 ->
+  Znth (j + 1) row_ptr <= Znth (j + 1) row_ptr ->
+  0 <= j + 1 < N + 1 ->
+  0 <= j < N + 1 ->
+  j + 0 < j + 1 ->
+  0 <= j + 1 < N + 1 ->
+  0 <= N < N + 1 ->
+  j + 1 <= N + 0 -> Znth (j + 1) row_ptr <= M -> 0 <= j + 1 < N + 1 ->
+  0 <= 0 < N + 1 ->
+  0 + 0 < j + 1 ->
+  0 <= j + 1 < N + 1 ->
+  0 <= N + 1 - 1 < N + 1 ->
+  j + 1 <= N + 1 - 1 + 0 ->
+  Znth (j + 1) row_ptr <= Znth (N + 1 - 1) row_ptr ->
+  0 <= j < N + 1 ->
+  0 <= j < N + 1 ->
+  j <= j + 0 ->
+  Znth j row_ptr <= Znth j row_ptr ->
+  0 <= j < N + 1 ->
+  0 <= N < N + 1 ->
+  j <= N + 0 ->
+  Znth j row_ptr <= M ->
+  0 <= j < N + 1 ->
+  0 <= 0 < N + 1 ->
+  j <= 0 + 0 ->
+  Znth j row_ptr <= Znth 0 row_ptr -> 0 <= j < N + 1 -> 0 <= N + 1 - 1 < N + 1 ->
+  j <= N + 1 - 1 + 0 ->
+  Znth j row_ptr <= Znth (N + 1 - 1) row_ptr ->
+  0 <= j < N + 1 ->
+  0 <= j + 1 < N + 1 ->
+  j <= j + 1 + 0 ->
+  Znth j row_ptr <= Znth (j + 1) row_ptr ->
+  0 <= N < N + 1 ->
+  0 <= N < N + 1 ->
+  N <= N + 0 ->
+  M <= M ->
+  0 <= N < N + 1 ->
+  0 <= 0 < N + 1 ->
+  0 + 0 < N ->
+  0 <= N < N + 1 ->
+  0 <= N + 1 - 1 < N + 1 ->
+  N <= N + 1 - 1 + 0 ->
+  M <= Znth (N + 1 - 1) row_ptr ->
+  0 <= N < N + 1 -> 0 <= j + 1 < N + 1 -> j + 1 + 0 < N ->
+  False.
+Proof.
+  Timeout 1 Fail lia. (* lia crashes. *)
+Abort.