garbage collection of dead equalities implemented

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

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 ();;