addition of lia.cache - csdp.cache is now handled by micromega not csdpcert

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 37 insertions, 94 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 66fe5335c..286e866fd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2009                             *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -1199,10 +1199,10 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
 	end ;
       let res = try prover.compact prf remap with x ->
 	if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; 
- 
+	(* This should not happen -- this is the recovery plan... *)
 	match prover.prover (List.map fst new_cl) with 
 	  | None -> failwith "proof compaction error"
-	  | Some p -> p 
+	  | Some p ->  p 
       in
       if debug then 
 	begin
@@ -1334,10 +1334,7 @@ module Cache = PHashtable(struct
   let hash  = Hashtbl.hash
 end)
 
-let cache_name = "csdp.cache" 
-
-let cache = lazy (Cache.open_in cache_name)
-
+let csdp_cache = "csdp.cache" 
 
 let really_call_csdpcert : provername -> micromega_polys -> csdpcert =
   fun provername poly -> 
@@ -1350,26 +1347,11 @@ let really_call_csdpcert : provername -> micromega_polys -> csdpcert =
 
 
 
-let call_csdpcert prover pb =
-
-  let cache = Lazy.force cache in
-    try 
-      Cache.find cache (prover,pb) 
-    with Not_found -> 
-      let cert = really_call_csdpcert prover pb in
-	Cache.add cache (prover,pb) cert ; 
-	cert
-
-
-
-
-  
-
-
-
-
+let xcall_csdpcert =
+  Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb)
 
 
+let call_csdpcert prover pb = xcall_csdpcert (prover,pb)
 
 let rec z_to_q_pol e = 
  match e with
@@ -1520,12 +1502,18 @@ let non_linear_prover_Z str o  = {
   pp_f    =  fun o x -> pp_pol pp_z o (fst x)
 }
 
+module CacheZ = PHashtable(struct 
+  type t = (Mc.z Mc.pol * Mc.op1) list
+  let equal = (=)
+  let hash  = Hashtbl.hash
+end)
 
+let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)
 
 
 let linear_Z =   {
   name = "lia";
-  prover = lift_pexpr_prover Certificate.zlinear_prover ; 
+  prover = memo_zlinear_prover ; 
   hyps   = hyps_of_pt;
   compact = compact_pt;
   pp_prf      = pp_proof_term;
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 272cc8931..cbacc48e4 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -40,6 +40,10 @@ module type PHashtable =
 	Once closed, a table cannot be used.
 	i.e, copy, find,add will raise UnboundTable *)
 
+    val memo : string -> (key -> 'a) -> (key -> 'a)
+      (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
+	  Note that the cache is just loaded when needed *)
+
   end
 
 open Hashtbl
@@ -86,15 +90,12 @@ let finally f rst =
 
 
 (** [from_file f] returns a hashtable by parsing records from file [f].
-    The structure of the file is
-    (KEY NL ELEM NL)* 
-    where 
-    NL is the character '\n'
-    KEY and ELEM are strings (without NL) parsed 
-    by the functions Key.parse and Elem.parse
+    Elements of the file are marshelled pairs of Caml structures.
+    (To ensure portability across platforms, closures are not allowed.)
 
     Raises Sys_error if the file cannot be open
-    Raises InvalidTableFormat if the file does not conform to the format,
+    Raises InvalidTableFormat if the file does not conform to the format
+    i.e, Marshal.from_channel fails
 *)
 
 
@@ -167,6 +168,18 @@ let find t k =
       let res = Table.find tbl k in
 	res 
 
+let memo cache f = 
+  let tbl = lazy (open_in cache) in
+    fun x -> 
+      let tbl = Lazy.force tbl in
+	try 
+	  find tbl x
+	with
+	    Not_found -> 
+	      let res = f x in
+		add tbl x res ;
+		res
+
 end
 
 
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 4085eb069..ee9fa35f1 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -4,7 +4,6 @@
 (* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL              *)
 (*   independent bits                                                        *)
 (* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
-(* - Addition of a csdp cache by the Coq development team                    *)
 (* ========================================================================= *)
 
 (* ========================================================================= *)
@@ -1109,7 +1108,6 @@ let csdp_params = csdp_default_parameters;;
 
 (* ------------------------------------------------------------------------- *)
 (* The same thing with CSDP.                                                 *)
-(* Modified by the Coq development team to use a cache                       *)
 (* ------------------------------------------------------------------------- *)
 
 let buffer_add_line buff line =
@@ -1125,63 +1123,10 @@ let file_of_string filename s =
   let fd = Pervasives.open_out filename in
   output_string fd s; close_out fd
 
-(*
-let request_mark = "*** REQUEST ***"
-let answer_mark  = "*** ANSWER ***"
-let end_mark     = "*** END ***"
-let infeasible_mark = "Infeasible\n"
-let failure_mark    = "Failure\n"
-
-let cache_name = "csdp.cache"
-
-let look_in_cache string_problem =
-  let n = String.length string_problem in
-  try
-    let inch = open_in cache_name in
-    let rec search () =
-      while input_line inch <> request_mark do () done;
-      let i = ref 0 in
-      while !i < n & string_problem.[!i] = input_char inch do incr i done;
-      if !i < n or input_line inch <> answer_mark then
-	search ()
-      else begin
-	let buff = Buffer.create 16 in
-	let line = ref (input_line inch) in
-	while (!line <> end_mark) do
-	  buffer_add_line buff !line; line := input_line inch
-	done;
-	close_in inch;
-	Buffer.contents buff
-      end in
-    try search () with End_of_file -> close_in inch; raise Not_found
-  with Sys_error _ -> raise Not_found
-
-let flush_to_cache string_problem string_result =
-  try
-    let flags = [Open_append;Open_text;Open_creat] in
-    let outch = open_out_gen flags 0o666 cache_name in
-    begin 
-    try
-      Printf.fprintf outch "%s\n" request_mark;
-      Printf.fprintf outch "%s" string_problem;
-      Printf.fprintf outch "%s\n" answer_mark;
-      Printf.fprintf outch "%s" string_result;
-      Printf.fprintf outch "%s\n" end_mark;
-    with Sys_error _ as e -> close_out outch; raise e
-    end;
-    close_out outch
-  with Sys_error _ -> 
-    print_endline "Warning: Could not open or write to csdp cache"
-*)
+
 exception CsdpInfeasible
 
 let run_csdp dbg string_problem =
-(*  try
-   let res = look_in_cache string_problem in
-   if res = infeasible_mark then raise CsdpInfeasible;
-   if res = failure_mark then failwith "csdp error";
-   res
-  with Not_found -> *)
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file = Filename.temp_file "sos" ".dat-s" in
   let temp_path = Filename.dirname input_file in
@@ -1190,15 +1135,12 @@ let run_csdp dbg string_problem =
   file_of_string params_file csdp_params;
   let rv = Sys.command("cd "^temp_path^"; csdp "^input_file^" "^output_file^
                        (if dbg then "" else "> /dev/null")) in
-    if rv = 1 or rv = 2 then 
-      ((*flush_to_cache string_problem infeasible_mark;*) raise CsdpInfeasible); 
+    if rv = 1 or rv = 2 then raise CsdpInfeasible; 
   if rv = 127 then
      (print_string "csdp not found, exiting..."; exit 1);
   if rv <> 0 & rv <> 3 (* reduced accuracy *) then
-    ((*flush_to_cache string_problem failure_mark;*)
-     failwith("csdp: error "^string_of_int rv));
+     failwith("csdp: error "^string_of_int rv);
   let string_result = string_of_file output_file in
-(*  flush_to_cache string_problem string_result;*)
   if not dbg then
     (Sys.remove input_file; Sys.remove output_file; Sys.remove params_file);
   string_result