X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=25314a100794c5fda5094dabd49c6d432f6ca309;hb=c1edc2a802659d79c41590f1edb29845f4bcb63c;hp=e30b1545ff7cfd467b6eb8d82bf2782763727945;hpb=50b01988edd12788a59aea3fb0f6704d5fd2bb69;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index e30b1545f..25314a100 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -264,7 +264,8 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = | _::tl -> find_duplicate sign current tl in let demodulate table current = - let newmeta, newcurrent = Indexing.demodulate !maxmeta env table current in + let newmeta, newcurrent = + Indexing.demodulation !maxmeta env table current in maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) else None @@ -294,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 @@ -306,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.demodulate !maxmeta env table target in + 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 @@ -320,16 +351,23 @@ 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 -> EqualitySet.add e s) EqualitySet.empty new_pos + List.fold_left + (fun s e -> + if not (Inference.is_identity env e) then EqualitySet.add e s else s) + 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 *) ;; @@ -418,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 @@ -440,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) -> @@ -536,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 @@ -547,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 @@ -650,8 +713,16 @@ let main () = | Failure -> Printf.printf "NO proof found! :-(\n\n" | Success (Some proof, env) -> - Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof) + 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 -> @@ -668,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"; @@ -682,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;