From: Alberto Griggio Date: Thu, 23 Jun 2005 17:15:16 +0000 (+0000) Subject: added various profiling statistics... X-Git-Tag: INDEXING_NO_PROOFS~89 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97b887beb8b28738303ae32bcd5bd5c9c87eb606;p=helm.git added various profiling statistics... --- diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index b5a2d7274..443c5c63b 100644 --- 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 bbd3c4844..0193b781b 100644 --- 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 bc9bc01f1..9212f0ac8 100644 --- 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 b77fe955f..a1414de79 100644 --- 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