- fwd concrete syntax fixed

[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 050ab49ebb490525fa01309f749399bce7a67e4c..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;;
@@ -1090,51 +1099,62 @@ let given_clause
     else if Unix.gettimeofday () > max_time then
       (ParamodulationFailure "No more time to spend")
     else
+(*
       let _ = prerr_endline "simpl goal with active" in
       let _ = <:start<simplify goal set active>> in
       let goals = simplify_goal_set env goals passive active in 
       let _ = <:stop<simplify goal set active>> in
+*)
+      let _ = 
+        prerr_endline 
+         (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
+           iterno (size_of_active active) (size_of_passive passive)
+           (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
+      in
+      (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
+      let passive =
+        let selection_estimate = iterations_left iterno in
+        let kept = size_of_passive passive in
+        if kept > selection_estimate then 
+          begin
+            (*Printf.eprintf "Too many passive equalities: pruning...";
+            prune_passive selection_estimate active*) passive
+          end
+        else
+          passive
+      in
+      kept_clauses := (size_of_passive passive) + (size_of_active active);
+      let goals = infer_goal_set env active goals in
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
           prerr_endline 
             (Printf.sprintf "Found a proof in: %f\n" 
               (Unix.gettimeofday() -. initial_time));
-(*          assert false;*)
           ParamodulationSuccess p
       | None -> 
-          prerr_endline 
-            (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
-            iterno (size_of_active active) (size_of_passive passive)
-            (size_of_goal_set_a goals) (size_of_goal_set_p goals));
-          (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
-          (*
-          let passive =
-            let selection_estimate = iterations_left iterno in
-            let kept = size_of_passive passive in
-            if kept > selection_estimate then 
-              begin
-                (*Printf.eprintf "Too many passive equalities: pruning...";
-                prune_passive selection_estimate active*) passive
-              end
-            else
-              passive
-          in
-          kept_clauses := (size_of_passive passive) + (size_of_active active);
-          *)
           (* SELECTION *)
           if passive_is_empty passive then
             ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
-              let goals = infer_goal_set env active goals in
+              (* 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 _,_,goaltype = List.hd (fst goals) in
-              List.iter                 
+              let _ = 
+                List.iter                 
                  (fun _,_,g -> 
-                    prerr_endline (Printf.sprintf  "Current goal = %s\n"
-                      (CicPp.pp g names))) (fst goals);
-              prerr_endline (Printf.sprintf  "Selected = %s\n"
-                (Equality.string_of_equality ~env current));
+                   prerr_endline (Printf.sprintf  "Current goal = %s\n"
+                    (CicPp.pp g names))) 
+                 (fst goals);
+                prerr_endline (Printf.sprintf  "Selected = %s\n"
+                  (Equality.string_of_equality ~env current))
+              in
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
                 forward_simplify eq_uri env (Positive, current) active 
@@ -1852,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 ();;