profiling experiments...

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 372127b48d9b234c97b8d009aeccf10fe0655dca..25314a100794c5fda5094dabd49c6d432f6ca309 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -295,8 +295,18 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
         else res
 ;;
 
+type fs_time_info_t = {
+  mutable build_all: float;
+  mutable demodulate: float;
+  mutable subsumption: float;
+};;
+
+let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
+
 
 let forward_simplify_new env (new_neg, new_pos) ?passive active =
+  let t1 = Unix.gettimeofday () in
+
   let active_list, active_table = active in
   let pl, passive_table =
     match passive with
@@ -307,11 +317,31 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
         pn @ pp, Some pt
   in
   let all = active_list @ pl in
+  
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
+  
   let demodulate table target =
     let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
     maxmeta := newmeta;
     newtarget
   in
+  let f sign' target (sign, eq) =
+    if sign <> sign' then false
+    else subsumption env target eq 
+  in
+
+  let t1 = Unix.gettimeofday () in
+
+  let new_neg, new_pos = 
+    (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
+     List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
+  in
+
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
+  let t1 = Unix.gettimeofday () in
+
   let new_neg, new_pos =
     let new_neg = List.map (demodulate active_table) new_neg
     and new_pos = List.map (demodulate active_table) new_pos in
@@ -321,6 +351,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
         List.map (demodulate passive_table) new_neg,
         List.map (demodulate passive_table) new_pos
   in
+
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
+
   let new_pos_set =
     List.fold_left
       (fun s e ->
@@ -328,12 +362,12 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
       EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
-  let f sign' target (sign, eq) =
-    if sign <> sign' then false
-    else subsumption env target eq 
-  in
-  (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
-   List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
+  new_neg, new_pos
+(*   let res = *)
+(*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
+(*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
+(*   in *)
+(*   res *)
 ;;
 
 
@@ -422,6 +456,11 @@ let backward_simplify env new' ?passive active =
       active, passive, newa, newp
 ;;
 
+
+let infer_time = ref 0.;;
+let forward_simpl_time = ref 0.;;
+let backward_simpl_time = ref 0.;;
+
   
 let rec given_clause env passive active =
   match passive_is_empty passive with
@@ -444,19 +483,31 @@ let rec given_clause env passive active =
               (string_of_sign sign) (string_of_equality ~env current);
             print_newline ();
 
+            let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
+            let t2 = Unix.gettimeofday () in
+            infer_time := !infer_time +. (t2 -. t1);
+            
             let res, proof = contains_empty env new' in
             if res then
               Success (proof, env)
-            else
+            else 
+              let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' active in
+              let t2 = Unix.gettimeofday () in
+              let _ =
+                forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
+              in
               let active =
                 match sign with
                 | Negative -> active
                 | Positive ->
+                    let t1 = Unix.gettimeofday () in
                     let active, _, newa, _ =
                       backward_simplify env ([], [current]) active
                     in
+                    let t2 = Unix.gettimeofday () in
+                    backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
                     match newa with
                     | None -> active
                     | Some (n, p) ->
@@ -540,7 +591,10 @@ let rec given_clause_fullred env passive active =
               (string_of_sign sign) (string_of_equality ~env current);
             print_newline ();
 
+            let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
+            let t2 = Unix.gettimeofday () in
+            infer_time := !infer_time +. (t2 -. t1);
 
             let active =
               if is_identity env current then active
@@ -551,10 +605,15 @@ let rec given_clause_fullred env passive active =
                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
             in
             let rec simplify new' active passive =
+              let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' ~passive active in
+              let t2 = Unix.gettimeofday () in
+              forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
+              let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained =
-                backward_simplify env new' ~passive active
-              in
+                backward_simplify env new' ~passive active in
+              let t2 = Unix.gettimeofday () in
+              backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
               | None, None -> active, passive, new'
               | Some (n, p), None
@@ -657,6 +716,13 @@ let main () =
         Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
           (PP.pp proof (names_of_context context))
           (finish -. start);
+        Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+                         "backward_simpl_time: %.9f\n")
+          !infer_time !forward_simpl_time !backward_simpl_time;
+        Printf.printf ("forward_simpl_details:\n  build_all: %.9f\n" ^^
+                         "  demodulate: %.9f\n  subsumption: %.9f\n")
+          fs_time_info.build_all fs_time_info.demodulate
+          fs_time_info.subsumption;
     | Success (None, env) ->
         Printf.printf "Success, but no proof?!?\n\n"
   with exc ->
@@ -673,6 +739,7 @@ let _ =
   and set_lpo () = Utils.compare_terms := lpo
   and set_kbo () = Utils.compare_terms := nonrec_kbo
   and set_fullred () = given_clause_ref := given_clause_fullred
+  and set_use_index v = Indexing.use_index := v
   in
   Arg.parse [
     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
@@ -687,6 +754,8 @@ let _ =
     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 
     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
+
+    "-i", Arg.Bool set_use_index, "Use indexing yes/no (default: yes)";
   ] (fun a -> ()) "Usage:"
 in
 Helm_registry.load_from !configuration_file;