reorganized guiven_clause to work with the on_the_fly simplification of goals during...

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 050ab49ebb490525fa01309f749399bce7a67e4c..be59003756df16a5b7cc1cb0e769fde101a89128 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1090,51 +1090,54 @@ 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
               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