Omega: avoiding distinct proof-terms on repeated identical runs

 Omega now reuse the same inner variable names (Zvar0, Zvar1, ...)
 at each run. This way, the obtained proof-terms on
 two identical omega runs should be the same.
 This wasn't always the case earlier:
  - the two proofs were almost always convertible, but with distinct
    variable names.
  - in very rare situations, the two proofs could even be non-convertible.
    Indeed, the omega engine use hash-tables which may be sensible to
    the names in the (in)equality system and hence lead to different
    solutions. Example of this behavior (with ocaml 4, whose default hash
    function is different from ocaml 3.12, leading to a different behavior
    here !) :

--------------------------------------------------------------------
Require Import Omega.
Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Check (eq_refl : test1 = test2). (* OK *)
Check (eq_refl : test1 = test3). (* OK *)
Check (eq_refl : test1 = test4). (* KO, test4 is different !! *)
--------------------------------------------------------------------

 The old behavior could be restored with "Unset Stable Omega".

 Thanks to Frédéric Loulergue for spotting this sensibility to
 the underlying ocaml versions...

1 files changed, 48 insertions, 12 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e4e3650c7..b61279cd5 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -47,6 +47,18 @@ let display_system_flag = ref false
 let display_action_flag = ref false
 let old_style_flag = ref false
 
+(* Should we reset all variable labels between two runs of omega ? *)
+
+let reset_flag = ref true
+
+(* Coq < 8.5 was not performing such resets, hence omega was slightly
+   non-deterministic: successive runs of omega on the same problem may
+   lead to distinct proof-terms.
+   At the very least, these terms differed on the inner
+   variable names, but they could even be non-convertible :
+   the OmegaSolver relies on Hashtbl.iter, it can hence find a different
+   solution when variable indices differ. *)
+
 let read f () = !f
 let write f x = f:=x
 
@@ -79,31 +91,44 @@ let _ =
       optread  = read old_style_flag;
       optwrite = write old_style_flag }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = true;
+      optname  = "Omega automatic reset of generated names";
+      optkey   = ["Stable";"Omega"];
+      optread  = read reset_flag;
+      optwrite = write reset_flag }
+
+let intref, reset_all_references =
+  let refs = ref [] in
+  (fun n -> let r = ref n in refs := (r,n) :: !refs; r),
+  (fun () -> List.iter (fun (r,n) -> r:=n) !refs)
 
 let new_identifier =
-  let cpt = ref 0 in
+  let cpt = intref 0 in
   (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
 let new_identifier_state =
-  let cpt = ref 0 in
+  let cpt = intref 0 in
   (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
 
 let new_identifier_var =
-  let cpt = ref 0 in
+  let cpt = intref 0 in
   (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
 let new_id =
-  let cpt = ref 0 in fun () -> incr cpt; !cpt
+  let cpt = intref 0 in fun () -> incr cpt; !cpt
 
 let new_var_num =
-  let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
+  let cpt = intref 1000 in (fun () -> incr cpt; !cpt)
 
 let new_var =
-  let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
+  let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
 
 let display_var i = Printf.sprintf "X%d" i
 
-let intern_id,unintern_id =
+let intern_id,unintern_id,reset_intern_tables =
   let cpt = ref 0 in
   let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
   (fun (name : Id.t) ->
@@ -115,7 +140,8 @@ let intern_id,unintern_id =
   (fun idx ->
      try Hashtbl.find co_table idx with Not_found ->
        let v = new_var () in
-       Hashtbl.add table v idx; Hashtbl.add co_table idx v; v)
+       Hashtbl.add table v idx; Hashtbl.add co_table idx v; v),
+  (fun () -> cpt := 0; Hashtbl.clear table)
 
 let mk_then = tclTHENLIST
 
@@ -134,13 +160,14 @@ let rev_assoc k =
   in
   loop
 
-let tag_hypothesis,tag_of_hyp, hyp_of_tag =
+let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags =
   let l = ref ([]:(Id.t * int) list) in
   (fun h id -> l := (h,id):: !l),
   (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
-  (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
+  (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"),
+  (fun () -> l := [])
 
-let hide_constr,find_constr,clear_tables,dump_tables =
+let hide_constr,find_constr,clear_constr_tables,dump_tables =
   let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
   (fun h ->
@@ -148,6 +175,14 @@ let hide_constr,find_constr,clear_tables,dump_tables =
   (fun () -> l := []),
   (fun () -> !l)
 
+let reset_all () =
+  if !reset_flag then begin
+    reset_all_references ();
+    reset_intern_tables ();
+    clear_tags ();
+    clear_constr_tables ()
+  end
+
 (* Lazy evaluation is used for Coq constants, because this code
  is evaluated before the compiled modules are loaded.
  To use the constant Zplus, one must type "Lazy.force coq_Zplus"
@@ -1381,7 +1416,7 @@ open Proofview.Notations
 
 let coq_omega =
   Proofview.Goal.enter begin fun gl ->
-  clear_tables ();
+  clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   let destructure_omega = Tacmach.New.of_old destructure_omega gl in
   let tactic_normalisation, system =
@@ -1828,4 +1863,5 @@ let destructure_goal = destructure_goal
 let omega_solver =
   Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
   Coqlib.check_required_library ["Coq";"omega";"Omega"];
+  reset_all ();
   destructure_goal