From: Alberto Griggio Date: Fri, 17 Jun 2005 13:28:27 +0000 (+0000) Subject: profiling experiments... X-Git-Tag: INDEXING_NO_PROOFS~124 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c1edc2a802659d79c41590f1edb29845f4bcb63c;p=helm.git profiling experiments... --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index c45e19ab0..055314676 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -1,6 +1,6 @@ -(* type naif_indexing = - (Cic.term * ((bool * Inference.equality) list)) list -;; *) +(** settable by the command line (-i switch) *) +let use_index = ref true;; + type pos = Left | Right ;; @@ -47,7 +47,7 @@ let remove_index table eq = ;; -let rec find_matches unif_fun metasenv context ugraph lift_amount term = +let rec find_matches metasenv context ugraph lift_amount term = let module C = Cic in let module U = Utils in let module S = CicSubstitution in @@ -74,7 +74,7 @@ let rec find_matches unif_fun metasenv context ugraph lift_amount term = let subst', metasenv', ugraph' = (* Inference.matching (metasenv @ metas) context term *) (* (S.lift lift_amount c) ugraph *) - unif_fun (metasenv @ metas) context + Inference.matching (metasenv @ metas) context term (S.lift lift_amount c) ugraph in (* let names = U.names_of_context context in *) @@ -96,7 +96,7 @@ let rec find_matches unif_fun metasenv context ugraph lift_amount term = res with e -> (* Printf.printf "ERRORE!: %s\n" (Printexc.to_string e); *) - find_matches unif_fun metasenv context ugraph lift_amount term tl + find_matches metasenv context ugraph lift_amount term tl else let res = try do_match c other eq_URI with e -> None in match res with @@ -112,10 +112,17 @@ let rec find_matches unif_fun metasenv context ugraph lift_amount term = if order = U.Gt then res else - find_matches unif_fun metasenv context ugraph - lift_amount term tl + find_matches metasenv context ugraph lift_amount term tl | None -> - find_matches unif_fun metasenv context ugraph lift_amount term tl + find_matches metasenv context ugraph lift_amount term tl +;; + + +let get_candidates table term = + if !use_index then + try Hashtbl.find table (head_of_term term) with Not_found -> [] + else + Hashtbl.fold (fun k v l -> v @ l) table [] ;; @@ -124,14 +131,12 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let hd_term = head_of_term term in - let candidates = try Hashtbl.find table hd_term with Not_found -> [] in + let candidates = get_candidates table term in match term with | C.Meta _ -> None | term -> let res = - find_matches Inference.matching metasenv context ugraph - lift_amount term candidates + find_matches metasenv context ugraph lift_amount term candidates in if res <> None then res @@ -233,13 +238,8 @@ let rec demodulation newmeta env table target = if (Inference.is_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget - else ( -(* Printf.printf "Going on 1:\ntarget: %s\nnewtarget: %s\n%s\n\n" *) -(* (Inference.string_of_equality ~env target) *) -(* (Inference.string_of_equality ~env newtarget) *) -(* (string_of_bool (target = newtarget)); *) + else demodulation newmeta env table newtarget - ) | None -> let res = demodulate_term metasenv' context ugraph table 0 right in match res with @@ -248,12 +248,8 @@ let rec demodulation newmeta env table target = if (Inference.is_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget - else ( -(* Printf.printf "Going on 2:\ntarget: %s\nnewtarget: %s\n\n" *) -(* (Inference.string_of_equality ~env target) *) -(* (Inference.string_of_equality ~env newtarget); *) + else demodulation newmeta env table newtarget - ) | None -> newmeta, target ;; @@ -313,8 +309,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let hd_term = head_of_term term in - let candidates = try Hashtbl.find table hd_term with Not_found -> [] in + let candidates = get_candidates table term in let res, lifted_term = match term with | C.Meta (i, l) -> diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 372127b48..25314a100 100644 --- 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;