X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=ca9dc194bd8f0af487c3c0faafb13e82080ec5ee;hb=31513dcd96791a28cb0f7667c7bbdb172b33864e;hp=be59003756df16a5b7cc1cb0e769fde101a89128;hpb=0fe1347ecafd65a4be26f85595032653f81d1ab3;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index be5900375..ca9dc194b 100644
--- 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 ();;