added various profiling statistics...

diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml
index b5a2d727472799c4991a9a50702047ad9e37dcc0..443c5c63bc043d12a61d4ff67f881611120a7307 100644 (file)
--- a/helm/ocaml/paramodulation/discrimination_tree.ml
+++ b/helm/ocaml/paramodulation/discrimination_tree.ml
@@ -39,9 +39,10 @@ end
 module PosEqSet = Set.Make(OrderedPosEquality);;
 
 
-(* module DiscriminationTree = Trie.Make(PSMap);; *)
+module DiscriminationTree = Trie.Make(PSMap);;
 
 
+(*
 module DiscriminationTree = struct
   type key = path_string
   type t = Node of PosEqSet.t option * (t PSMap.t)
@@ -91,6 +92,7 @@ module DiscriminationTree = struct
     traverse [] t acc
 
 end
+*)
 
   
 let string_of_discrimination_tree tree =

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index bbd3c484446d4d727fd2a928cad8c1c336b6fd65..0193b781b2e87de32665093a4960d82527ef0b91 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -18,7 +18,10 @@ let print_candidates mode term res =
                (Inference.string_of_equality e))
           res));
   print_endline "|";
-;;  
+;;
+
+
+let indexing_retrieval_time = ref 0.;;
 
 
 let empty_table () =
@@ -30,12 +33,20 @@ and remove_index = Path_indexing.remove_index
 and in_index = Path_indexing.in_index;;
   
 let get_candidates mode trie term =
-  let s = 
-    match mode with
-    | Matching -> Path_indexing.retrieve_generalizations trie term
-    | Unification -> Path_indexing.retrieve_unifiables trie term
+  let t1 = Unix.gettimeofday () in
+  let res = 
+    let s = 
+      match mode with
+      | Matching -> Path_indexing.retrieve_generalizations trie term
+      | Unification -> Path_indexing.retrieve_unifiables trie term
+(*       Path_indexing.retrieve_all trie term *)
+    in
+    Path_indexing.PosEqSet.elements s
   in
-  Path_indexing.PosEqSet.elements s
+(*   print_candidates mode term res; *)
+  let t2 = Unix.gettimeofday () in
+  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
+  res
 ;;
 
 
@@ -62,6 +73,9 @@ let get_candidates mode tree term =
 ;;
 *)
 
+let match_unif_time_ok = ref 0.;;
+let match_unif_time_no = ref 0.;;
+
 
 let rec find_matches metasenv context ugraph lift_amount term =
   let module C = Cic in
@@ -77,11 +91,21 @@ let rec find_matches metasenv context ugraph lift_amount term =
         let pos, (proof, (ty, left, right, o), metas, args) = candidate in
         let do_match c other eq_URI =
           let subst', metasenv', ugraph' =
-            Inference.matching (metasenv @ metas) context
-              term (S.lift lift_amount c) ugraph
+            let t1 = Unix.gettimeofday () in
+            try
+              let r = 
+                Inference.matching (metasenv @ metas) context
+                  term (S.lift lift_amount c) ugraph in
+              let t2 = Unix.gettimeofday () in
+              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+              r
+            with e ->
+              let t2 = Unix.gettimeofday () in
+              match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+              raise e
           in
-          Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
-                (candidate, eq_URI))
+            Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+                  (candidate, eq_URI))
         in
         let c, other, eq_URI =
           if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
@@ -124,8 +148,18 @@ let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
         let pos, (proof, (ty, left, right, o), metas, args) = candidate in
         let do_match c other eq_URI =
           let subst', metasenv', ugraph' =
-            unif_fun (metasenv @ metas) context
-              term (S.lift lift_amount c) ugraph
+            let t1 = Unix.gettimeofday () in
+            try
+              let r = 
+                unif_fun (metasenv @ metas) context
+                  term (S.lift lift_amount c) ugraph in
+              let t2 = Unix.gettimeofday () in
+              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+              r
+            with e ->
+              let t2 = Unix.gettimeofday () in
+              match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+              raise e
           in
           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
            (candidate, eq_URI))
@@ -190,7 +224,18 @@ let subsumption env table target =
       try
         let other = if pos = Utils.Left then r else l in
         let subst', menv', ug' =
-          Inference.matching metasenv context what other ugraph in
+          let t1 = Unix.gettimeofday () in
+          try
+            let r = 
+              Inference.matching metasenv context what other ugraph in
+            let t2 = Unix.gettimeofday () in
+            match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+            r
+          with e ->
+            let t2 = Unix.gettimeofday () in
+            match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+            raise e
+        in
         samesubst subst subst'
       with e ->
         false

diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml
index bc9bc01f1608fa42d36c369a57808496364a6b08..9212f0ac857ca868141c2dc154a85e5ea2a50b3a 100644 (file)
--- a/helm/ocaml/paramodulation/path_indexing.ml
+++ b/helm/ocaml/paramodulation/path_indexing.ml
@@ -49,8 +49,6 @@ end
 
 module PSMap = Map.Make(OrderedPathStringElement);;
 
-(* module PSTrie = Trie.Make(PathStringElementMap);; *)
-
 module OrderedPosEquality = struct
   type t = Utils.pos * Inference.equality
 
@@ -59,6 +57,10 @@ end
 
 module PosEqSet = Set.Make(OrderedPosEquality);;
 
+
+module PSTrie = Trie.Make(PSMap);;
+
+(*
 (*
  * Trie: maps over lists.
  * Copyright (C) 2000 Jean-Christophe FILLIATRE
@@ -111,6 +113,7 @@ module PSTrie = struct
     traverse [] t acc
 
 end
+*)
 
 
 let index trie equality =
@@ -289,6 +292,12 @@ let rec retrieve_unifiables trie term =
 ;;
 
 
+let retrieve_all trie term =
+  PSTrie.fold
+    (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty
+;;
+
+
 let string_of_pstrie trie =
   let rec to_string level = function
     | PSTrie.Node (v, map) ->

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index b77fe955f7e25d10bb652d668e08b25469b8d0a4..a1414de795bb1311145c22cf3bedbcd71aff9d72 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -12,7 +12,8 @@ let processed_clauses = ref 0;; (* number of equalities selected so far... *)
 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
 let start_time = ref 0.;; (* time at which the execution started *)
 let elapsed_time = ref 0.;;
-let maximal_retained_equality = ref None;;
+let maximal_weight = ref None;;
+(* let maximal_retained_equality = ref None;; *)
 
 (* equality-selection related globals *)
 let use_fullred = ref false;;
@@ -21,6 +22,10 @@ let weight_age_counter = ref !weight_age_ratio;;
 let symbols_ratio = ref 0;;
 let symbols_counter = ref 0;;
 
+(* statistics... *)
+let derived_clauses = ref 0;;
+let kept_clauses = ref 0;;
+
 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
 let maxmeta = ref 0;;
 
@@ -57,6 +62,12 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
 ;;
 
 
+let weight_of_equality (_, (ty, left, right, _), _, _) =
+  let weight_of t = fst (weight_of_term ~consider_metas:false t) in
+  (weight_of ty) + (weight_of left) + (weight_of right)
+;;
+
+
 module OrderedEquality = struct
   type t = Inference.equality
 
@@ -69,6 +80,8 @@ module OrderedEquality = struct
         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+(*         let w1 = weight_of_equality eq1 *)
+(*         and w2 = weight_of_equality eq2 in *)
         match Pervasives.compare w1 w2 with
         | 0 -> Pervasives.compare eq1 eq2
         | res -> res
@@ -243,6 +256,11 @@ let size_of_passive ((_, ns), (_, ps), _) =
 ;;
 
 
+let size_of_active (active_list, _) =
+  List.length active_list
+;;
+
+
 let prune_passive howmany (active, _) passive =
   let (nl, ns), (pl, ps), tbl = passive in
   let howmany = float_of_int howmany
@@ -329,7 +347,8 @@ let prune_passive howmany (active, _) passive =
   let in_age, ns, nl = picka in_age ns nl in
   let _, ps, pl = picka in_age ps pl in
   if not (EqualitySet.is_empty ps) then
-    maximal_retained_equality := Some (EqualitySet.max_elt ps);
+    maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps));
+(*     maximal_retained_equality := Some (EqualitySet.max_elt ps); *)
   let tbl =
     EqualitySet.fold
       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
@@ -369,11 +388,13 @@ let infer env sign current (active_list, active_table) =
         let neg, pos = infer_positive curr_table active_list in
         neg, res @ pos
   in
-  match !maximal_retained_equality with
+  derived_clauses := !derived_clauses + (List.length new_neg) +
+    (List.length new_pos);
+  match !maximal_weight(* !maximal_retained_equality *) with
   | None -> new_neg, new_pos
-  | Some eq ->
+  | Some w (* eq *) ->
       let new_pos =
-        List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos in
+        List.filter (fun e -> (weight_of_equality e) <= w (* OrderedEquality.compare e eq <= 0 *)) new_pos in
       new_neg, new_pos
 ;;
 
@@ -665,7 +686,7 @@ let get_selection_estimate () =
 (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
   int_of_float (
     ceil ((float_of_int !processed_clauses) *.
-            (!time_limit /. !elapsed_time -. 1.)))
+            ((!time_limit *. 2.) /. !elapsed_time -. 1.)))
 ;;
 
   
@@ -686,6 +707,8 @@ let rec given_clause env passive active =
     ) else
       passive
   in
+
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
     
   match passive_is_empty passive with
   | true -> Failure
@@ -746,27 +769,27 @@ let rec given_clause env passive active =
                         in
                         nn @ al @ pp, tbl
               in
-              let _ =
-                Printf.printf "active:\n%s\n"
-                  (String.concat "\n"
-                     ((List.map
-                         (fun (s, e) -> (string_of_sign s) ^ " " ^
-                            (string_of_equality ~env e)) (fst active))));
-                print_newline ();
-              in
-              let _ =
-                match new' with
-                | neg, pos ->
-                    Printf.printf "new':\n%s\n"
-                      (String.concat "\n"
-                         ((List.map
-                             (fun e -> "Negative " ^
-                                (string_of_equality ~env e)) neg) @
-                            (List.map
-                               (fun e -> "Positive " ^
-                                  (string_of_equality ~env e)) pos)));
-                    print_newline ();
-              in
+(*               let _ = *)
+(*                 Printf.printf "active:\n%s\n" *)
+(*                   (String.concat "\n" *)
+(*                      ((List.map *)
+(*                          (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
+(*                             (string_of_equality ~env e)) (fst active)))); *)
+(*                 print_newline (); *)
+(*               in *)
+(*               let _ = *)
+(*                 match new' with *)
+(*                 | neg, pos -> *)
+(*                     Printf.printf "new':\n%s\n" *)
+(*                       (String.concat "\n" *)
+(*                          ((List.map *)
+(*                              (fun e -> "Negative " ^ *)
+(*                                 (string_of_equality ~env e)) neg) @ *)
+(*                             (List.map *)
+(*                                (fun e -> "Positive " ^ *)
+(*                                   (string_of_equality ~env e)) pos))); *)
+(*                     print_newline (); *)
+(*               in *)
               match contains_empty env new' with
               | false, _ -> 
                   let active =
@@ -777,16 +800,16 @@ let rec given_clause env passive active =
                         al @ [(sign, current)], Indexing.index tbl current
                   in
                   let passive = add_to_passive passive new' in
-                  let (_, ns), (_, ps), _ = passive in
-                  Printf.printf "passive:\n%s\n"
-                    (String.concat "\n"
-                       ((List.map (fun e -> "Negative " ^
-                                     (string_of_equality ~env e))
-                           (EqualitySet.elements ns)) @
-                          (List.map (fun e -> "Positive " ^
-                                       (string_of_equality ~env e))
-                             (EqualitySet.elements ps))));
-                  print_newline ();
+(*                   let (_, ns), (_, ps), _ = passive in *)
+(*                   Printf.printf "passive:\n%s\n" *)
+(*                     (String.concat "\n" *)
+(*                        ((List.map (fun e -> "Negative " ^ *)
+(*                                      (string_of_equality ~env e)) *)
+(*                            (EqualitySet.elements ns)) @ *)
+(*                           (List.map (fun e -> "Positive " ^ *)
+(*                                        (string_of_equality ~env e)) *)
+(*                              (EqualitySet.elements ps)))); *)
+(*                   print_newline (); *)
                   given_clause env passive active
               | true, proof ->
                   Success (proof, env)
@@ -959,22 +982,32 @@ let main () =
         env passive active
     in
     let finish = Unix.gettimeofday () in
-    match res with
-    | Failure ->
-        Printf.printf "NO proof found! :-(\n\n"
-    | Success (Some proof, env) ->
-        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;
+    let _ =
+      match res with
+      | Failure ->
+          Printf.printf "NO proof found! :-(\n\n"
+      | Success (Some proof, env) ->
+          Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
+            (PP.pp proof (names_of_context context))
+            (finish -. start);
 (*         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"
+      | Success (None, env) ->
+          Printf.printf "Success, but no proof?!?\n\n"
+    in
+    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 "successful unification/matching time: %.9f\n"
+      !Indexing.match_unif_time_ok;
+    Printf.printf "failed unification/matching time: %.9f\n"
+      !Indexing.match_unif_time_no;
+    Printf.printf "indexing retrieval time: %.9f\n"
+      !Indexing.indexing_retrieval_time;
+    Printf.printf "derived %d clauses, kept %d clauses.\n"
+      !derived_clauses !kept_clauses;
   with exc ->
     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
     raise exc