garbage collection of dead equalities implemented

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"
+;;

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 237045bec67722aa241333d0e6f0f9a644f90057..1182afee654d855ea8bda55f5a5914d1dd10cf5a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -108,3 +108,14 @@ val symmetric:
   Cic.term -> Cic.term -> int -> UriManager.uri ->
     Cic.metasenv -> proof
 
+(* takes 3 lists of alive ids (they are threated the same way, the type is
+ * funny just to not oblige you to concatenate them) and drops all the dead
+ * equalities *)
+val collect: int list -> int list -> int list -> unit
+
+(* given an equality, returns the numerical id *)
+val id_of: equality -> int
+
+(* profiling statistics *)
+val get_stats: unit -> string
+

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index be59003756df16a5b7cc1cb0e769fde101a89128..ca9dc194bd8f0af487c3c0faafb13e82080ec5ee 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1062,7 +1062,16 @@ let infer_goal_set_with_current env current goals =
     passive_goals active_goals
 ;;
 
+let ids_of_goal g = 
+  let p,_,_ = g in
+  let ids = List.map (fun _,_,i,_,_ -> i) p in
+  ids
+;;
 
+let ids_of_goal_set (ga,gp) =
+  List.flatten (List.map ids_of_goal ga) @
+  List.flatten (List.map ids_of_goal gp)
+;;
 
 let size_of_goal_set_a (l,_) = List.length l;;
 let size_of_goal_set_p (_,l) = List.length l;;
@@ -1128,6 +1137,14 @@ let given_clause
             ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
+              (* COLLECTION OF GARBAGED EQUALITIES *)
+              if iterno mod 40 = 0 then
+                begin
+                  let active = List.map Equality.id_of (fst active) in
+                  let passive = List.map Equality.id_of (fst (fst passive)) in
+                  let goal = ids_of_goal_set goals in
+                  Equality.collect active passive goal
+                end;
               let current, passive = select env goals passive in
               let _ = 
                 List.iter                 
@@ -1855,5 +1872,6 @@ let demodulate_tac ~dbd ~pattern =
 ;;
 
 let get_stats () = 
-  <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats ();;
+  <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
+  Equality.get_stats ();;