garbage collection of dead equalities implemented

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 10c0aa8d4c8dba048ffab45914698a775303d1c7..6b3a1e0efabc8ab8271532715d6a38003ae85593 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let _profiler = <:profiler<_profiler>>;;
+
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
@@ -997,3 +999,47 @@ let symmetric eq_ty l id uri m =
     (Demodulation,id1,(Utils.Left,id),pred))
 ;;
 
+module IntOT = struct
+  type t = int
+  let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make(IntOT);;
+
+let n_purged = ref 0;;
+
+let collect alive1 alive2 alive3 =
+  let _ = <:start<collect>> in
+  let deps_of id = 
+    let p,_,_ = proof_of_id id in  
+    match p with
+    | Exact _ -> IntSet.empty
+    | Step (_,(_,id1,(_,id2),_)) ->
+          IntSet.add id1 (IntSet.add id2 IntSet.empty)
+  in
+  let rec close s = 
+    let news = IntSet.fold (fun id s -> IntSet.union (deps_of id) s) s s in
+    if IntSet.equal news s then s else close news
+  in
+  let l_to_s s l = List.fold_left (fun s x -> IntSet.add x s) s l in
+  let alive_set = l_to_s (l_to_s (l_to_s IntSet.empty alive2) alive1) alive3 in
+  let closed_alive_set = close alive_set in
+  let to_purge = 
+    Hashtbl.fold 
+      (fun k _ s -> 
+        if not (IntSet.mem k closed_alive_set) then
+          k::s else s) id_to_eq []
+  in
+  n_purged := !n_purged + List.length to_purge;
+  List.iter (Hashtbl.remove id_to_eq) to_purge;
+  let _ = <:stop<collect>> in ()  
+;;
+
+let id_of e = 
+  let _,_,_,_,id = open_equality e in id
+;;
+
+let get_stats () = 
+  <:show<Equality.>> ^ 
+  "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n"
+;;