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;;
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
;;
let get_stats () =
- <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats ();;
+ <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
+ Equality.get_stats ();;