X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=a1414de795bb1311145c22cf3bedbcd71aff9d72;hb=ab0954eab207a70e6ad5f2991cc117608deff55b;hp=b77fe955f7e25d10bb652d668e08b25469b8d0a4;hpb=04fcadbd9e194847138d97a0a9892a475bc21c88;p=helm.git 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