Improved handling of micromega caches

- Specialised hash and equality functions.
  Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.

fixes #10772

4 files changed, 260 insertions, 68 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ceb651abed..90c9f86b07 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -50,6 +50,13 @@ let get_lia_option () =
 let get_lra_option () =
  !lra_proof_depth
 
+(* Enable/disable caches *)
+
+let use_lia_cache = ref true
+let use_nia_cache = ref true
+let use_nra_cache = ref true
+let use_csdp_cache = ref true
+
 let () =
 
  let int_opt l vref =
@@ -88,8 +95,38 @@ let () =
      optwrite = (fun x -> Certificate.dump_file := x)
    } in
 
+ let lia_cache_opt =
+   {
+     optdepr = false;
+     optname = "cache of lia (.lia.cache)";
+     optkey  = ["Lia" ; "Cache"];
+     optread = (fun () -> !use_lia_cache);
+     optwrite = (fun x -> use_lia_cache := x)
+   } in
+
+ let nia_cache_opt =
+   {
+     optdepr = false;
+     optname = "cache of nia (.nia.cache)";
+     optkey  = ["Nia" ; "Cache"];
+     optread = (fun () -> !use_nia_cache);
+     optwrite = (fun x -> use_nia_cache := x)
+   } in
+
+ let nra_cache_opt =
+   {
+     optdepr = false;
+     optname = "cache of nra (.nra.cache)";
+     optkey  = ["Nra" ; "Cache"];
+     optread = (fun () -> !use_nra_cache);
+     optwrite = (fun x -> use_nra_cache := x)
+   } in
+
 
  let () = declare_bool_option solver_opt in
+ let () = declare_bool_option lia_cache_opt in
+ let () = declare_bool_option nia_cache_opt in
+ let () = declare_bool_option nra_cache_opt in
  let () = declare_stringopt_option dump_file_opt in
  let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
  let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in
@@ -1978,13 +2015,47 @@ type provername = string * int option
 
 open Persistent_cache
 
-module Cache = PHashtable(struct
-  type t = (provername * micromega_polys)
-  let equal = (=)
-  let hash  = Hashtbl.hash
-end)
 
-let csdp_cache = ".csdp.cache"
+module MakeCache(T : sig type prover_option
+                         type coeff
+                         val  hash_prover_option : int -> prover_option -> int
+                         val  hash_coeff : int -> coeff -> int
+                         val  eq_prover_option : prover_option -> prover_option -> bool
+                         val  eq_coeff   : coeff -> coeff -> bool
+
+                     end) =
+  struct
+    module E =
+      struct
+        type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
+
+        let equal = Hash.(eq_pair T.eq_prover_option (CList.equal (eq_pair (eq_pol T.eq_coeff) Hash.eq_op1)))
+
+        let hash  =
+          let hash_cstr  = Hash.(hash_pair (hash_pol T.hash_coeff) hash_op1) in
+          Hash.( (hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0)
+      end
+
+      include PHashtable(E)
+
+      let memo_opt use_cache cache_file f =
+        let memof = memo cache_file f in
+        fun x -> if !use_cache then memof x else f x
+
+  end
+
+
+
+module CacheCsdp = MakeCache(struct
+                   type prover_option = provername
+                   type coeff = Mc.q
+                   let hash_prover_option = Hash.(hash_pair hash_string
+                                                    (hash_elt (Option.hash (fun x -> x))))
+                   let eq_prover_option = Hash.(eq_pair String.equal
+                                                  (Option.equal Int.equal))
+                   let hash_coeff = Hash.hash_q
+                   let eq_coeff   = Hash.eq_q
+                     end)
 
 (**
   * Build the command to call csdpcert, and launch it. This in turn will call
@@ -2017,7 +2088,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste
   *)
 
 let xcall_csdpcert =
-  Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb)
+  CacheCsdp.memo_opt use_csdp_cache ".csdp.cache" (fun (prover,pb) -> really_call_csdpcert prover pb)
 
 (**
   * Prover callback functions.
@@ -2112,23 +2183,31 @@ let compact_pt pt f =
 
 let lift_pexpr_prover p l =  p (List.map (fun (e,o) -> Mc.denorm e , o) l)
 
-module CacheZ = PHashtable(struct
- type prover_option = bool * bool* int
 
- type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list)
-  let equal = (=)
-  let hash  = Hashtbl.hash
-end)
+module CacheZ = MakeCache(struct
+                    type prover_option = bool * bool* int
+                    type coeff = Mc.z
+                    let hash_prover_option : int -> prover_option -> int = Hash.hash_elt Hashtbl.hash
+                    let eq_prover_option   : prover_option -> prover_option -> bool = (=)
+                    let  eq_coeff   = Hash.eq_z
+                    let  hash_coeff = Hash.hash_z
+                  end)
 
-module CacheQ = PHashtable(struct
-  type t = int * ((Mc.q Mc.pol * Mc.op1) list)
-  let equal = (=)
-  let hash  = Hashtbl.hash
-end)
+module CacheQ = MakeCache(struct
+                    type prover_option = int
+                    type coeff = Mc.q
+                    let hash_prover_option : int -> int -> int = Hash.hash_elt Hashtbl.hash
+                    let eq_prover_option  = Int.equal
+                    let eq_coeff    = Hash.eq_q
+                    let hash_coeff  = Hash.hash_q
+                  end)
 
-let memo_zlinear_prover = CacheZ.memo ".lia.cache"  (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
-let memo_nlia = CacheZ.memo ".nia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
-let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+let memo_lia   = CacheZ.memo_opt use_lia_cache ".lia.cache"
+                   (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
+let memo_nlia  = CacheZ.memo_opt use_nia_cache ".nia.cache"
+                            (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
+let memo_nra   = CacheQ.memo_opt use_nra_cache ".nra.cache"
+                   (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
 
 
 
@@ -2154,63 +2233,63 @@ let linear_prover_R = {
 }
 
 let nlinear_prover_R = {
-  name    = "nra";
- get_option = get_lra_option;
- prover  = memo_nra ;
-  hyps    = hyps_of_cone ;
-  compact = compact_cone ;
-  pp_prf  = pp_psatz pp_q ;
-  pp_f    =  fun o x -> pp_pol pp_q o (fst x)
+  name       = "nra";
+  get_option = get_lra_option;
+  prover     = memo_nra ;
+  hyps       = hyps_of_cone ;
+  compact    = compact_cone ;
+  pp_prf     = pp_psatz pp_q ;
+  pp_f       =  fun o x -> pp_pol pp_q o (fst x)
 }
 
 let non_linear_prover_Q str o = {
-  name    = "real nonlinear prover";
+  name      = "real nonlinear prover";
  get_option = (fun () -> (str,o));
- prover  = (fun (o,l) -> call_csdpcert_q o l);
-  hyps    = hyps_of_cone;
-  compact = compact_cone ;
-  pp_prf  = pp_psatz pp_q ;
-  pp_f    = fun o x -> pp_pol pp_q o  (fst x)
+ prover     = (fun (o,l) -> call_csdpcert_q o l);
+  hyps      = hyps_of_cone;
+  compact   = compact_cone ;
+  pp_prf    = pp_psatz pp_q ;
+  pp_f      = fun o x -> pp_pol pp_q o  (fst x)
 }
 
 let non_linear_prover_R str o = {
-  name    = "real nonlinear prover";
- get_option = (fun () -> (str,o));
- prover  = (fun (o,l) -> call_csdpcert_q o l);
-  hyps    = hyps_of_cone;
-  compact = compact_cone;
-  pp_prf  = pp_psatz pp_q;
-  pp_f    = fun o x -> pp_pol pp_q o  (fst x)
+  name       = "real nonlinear prover";
+  get_option = (fun () -> (str,o));
+  prover     = (fun (o,l) -> call_csdpcert_q o l);
+  hyps       = hyps_of_cone;
+  compact    = compact_cone;
+  pp_prf     = pp_psatz pp_q;
+  pp_f       = fun o x -> pp_pol pp_q o  (fst x)
 }
 
 let non_linear_prover_Z str o  = {
-  name    = "real nonlinear prover";
+  name       = "real nonlinear prover";
   get_option = (fun () -> (str,o));
-  prover  = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l);
-  hyps    = hyps_of_pt;
-  compact = compact_pt;
-  pp_prf  = pp_proof_term;
-  pp_f    =  fun o x -> pp_pol pp_z o (fst x)
+  prover     = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l);
+  hyps       = hyps_of_pt;
+  compact    = compact_pt;
+  pp_prf     = pp_proof_term;
+  pp_f       = fun o x -> pp_pol pp_z o (fst x)
 }
 
 let linear_Z =   {
-  name    = "lia";
- get_option = get_lia_option;
- prover  = memo_zlinear_prover ;
-  hyps    = hyps_of_pt;
-  compact = compact_pt;
-  pp_prf  = pp_proof_term;
-  pp_f    = fun o x -> pp_pol pp_z o (fst x)
+    name       = "lia";
+    get_option = get_lia_option;
+    prover     = memo_lia ;
+    hyps       = hyps_of_pt;
+    compact    = compact_pt;
+    pp_prf     = pp_proof_term;
+    pp_f       = fun o x -> pp_pol pp_z o (fst x)
 }
 
 let nlinear_Z =   {
-  name    = "nlia";
- get_option = get_lia_option;
- prover  = memo_nlia ;
-  hyps    = hyps_of_pt;
-  compact = compact_pt;
-  pp_prf  = pp_proof_term;
-  pp_f    = fun o x -> pp_pol pp_z o (fst x)
+  name       = "nlia";
+  get_option = get_lia_option;
+  prover     = memo_nlia ;
+  hyps       = hyps_of_pt;
+  compact    = compact_pt;
+  pp_prf     = pp_proof_term;
+  pp_f       = fun o x -> pp_pol pp_z o (fst x)
 }
 
 (**
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 537b6175b4..39905f8c52 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -233,6 +233,13 @@ struct
    | Zpos p -> (positive_big_int p)
    | Zneg p -> minus_big_int (positive_big_int p)
 
+ let z x =
+  match x with
+   | Z0 -> 0
+   | Zpos p -> index p
+   | Zneg p -> - (index p)
+
+
  let q_to_num {qnum = x ; qden = y} =
   Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
 
@@ -420,6 +427,80 @@ let command exe_path args vl =
              stdout_read; stdout_write;
              stderr_read; stderr_write])
 
+(** Hashing utilities *)
+
+module Hash =
+  struct
+
+    module Mc = Micromega
+
+    open Hashset.Combine
+
+    let int_of_eq_op1 = Mc.(function
+      | Equal -> 0
+      | NonEqual -> 1
+      | Strict   -> 2
+      | NonStrict -> 3)
+
+    let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2
+
+    let hash_op1 h o = combine h (int_of_eq_op1 o)
+
+
+    let rec eq_positive p1 p2 =
+      match p1 , p2 with
+      | Mc.XH , Mc.XH -> true
+      | Mc.XI p1 , Mc.XI p2 -> eq_positive p1 p2
+      | Mc.XO p1 , Mc.XO p2 -> eq_positive p1 p2
+      |   _      , _        -> false
+
+    let eq_z z1 z2 =
+      match z1 , z2 with
+      | Mc.Z0 , Mc.Z0 -> true
+      | Mc.Zpos p1, Mc.Zpos p2
+        | Mc.Zneg p1, Mc.Zneg p2 -> eq_positive p1 p2
+      | _ , _ -> false
+
+    let eq_q {Mc.qnum = qn1 ; Mc.qden = qd1} {Mc.qnum = qn2 ; Mc.qden = qd2} =
+      eq_z qn1 qn2 && eq_positive qd1 qd2
+
+    let rec eq_pol  eq p1 p2 =
+      match p1 , p2 with
+      | Mc.Pc c1 , Mc.Pc c2 -> eq c1 c2
+      | Mc.Pinj(i1,p1) , Mc.Pinj(i2,p2) -> eq_positive i1 i2 && eq_pol eq p1 p2
+      | Mc.PX(p1,i1,p1') , Mc.PX(p2,i2,p2') ->
+         eq_pol eq p1 p2 && eq_positive i1 i2 && eq_pol eq p1' p2'
+      |  _ , _ -> false
+
+
+    let eq_pair eq1 eq2 (x1,y1) (x2,y2) =
+      eq1 x1 x2 && eq2 y1 y2
+
+
+    let hash_pol helt =
+      let rec hash acc = function
+        | Mc.Pc c -> helt (combine acc 1) c
+        | Mc.Pinj(p,c) -> hash (combine  (combine acc 1) (CoqToCaml.index p)) c
+        | Mc.PX(p1,i,p2) -> hash (hash (combine (combine acc 2) (CoqToCaml.index i)) p1) p2 in
+      hash
+
+
+    let hash_pair h1 h2 h (e1,e2) =
+      h2 (h1 h e1) e2
+
+    let hash_elt f h e = combine h (f e)
+
+    let hash_string h (e:string) = hash_elt Hashtbl.hash h e
+
+    let hash_z  = hash_elt CoqToCaml.z
+
+    let hash_q  = hash_elt (fun q -> Hashtbl.hash (CoqToCaml.q_to_num q))
+
+  end
+
+
+
+
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 8dbdea39e2..9692bc631b 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -67,14 +67,46 @@ end
 module CoqToCaml : sig
 
   val z_big_int : Micromega.z -> Big_int.big_int
-  val q_to_num : Micromega.q -> Num.num
-  val positive : Micromega.positive -> int
-  val n : Micromega.n -> int
-  val nat : Micromega.nat -> int
-  val index : Micromega.positive -> int
+  val z         : Micromega.z -> int
+  val q_to_num  : Micromega.q -> Num.num
+  val positive  : Micromega.positive -> int
+  val n         : Micromega.n -> int
+  val nat       : Micromega.nat -> int
+  val index     : Micromega.positive -> int
 
 end
 
+module Hash : sig
+
+  val eq_op1      : Micromega.op1 -> Micromega.op1 -> bool
+
+  val eq_positive : Micromega.positive -> Micromega.positive -> bool
+
+  val eq_z : Micromega.z -> Micromega.z -> bool
+
+  val eq_q : Micromega.q -> Micromega.q -> bool
+
+  val eq_pol  : ('a -> 'a -> bool) -> 'a Micromega.pol -> 'a Micromega.pol -> bool
+
+  val eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a * 'b -> 'a * 'b -> bool
+
+  val hash_op1 : int -> Micromega.op1 -> int
+
+  val hash_pol  : (int -> 'a -> int) -> int -> 'a Micromega.pol -> int
+
+  val hash_pair : (int -> 'a -> int) -> (int -> 'b -> int) -> int -> 'a * 'b -> int
+
+  val hash_z   : int -> Micromega.z -> int
+
+  val hash_q   : int -> Micromega.q -> int
+
+  val hash_string : int -> string -> int
+
+  val hash_elt : ('a -> int) -> int -> 'a -> int
+
+end
+
+
 val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int
 
 val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 14a1bc9712..14e2e40846 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -127,7 +127,7 @@ let open_in f =
     match read_key_elem inch with
       | None -> ()
       | Some (key,elem) ->
-          Table.replace htbl key elem ;
+          Table.add htbl key elem ;
 	  xload () in
     try
       (* Locking of the (whole) file while reading *)
@@ -164,7 +164,7 @@ let add t k e =
     else
       let fd = descr_of_out_channel outch in
       begin
-       Table.replace tbl k e ;
+       Table.add tbl k e ;
        do_under_lock Write fd 
         (fun _ -> 
          Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;