From db7f6d6b32515c091e0f338dd4903624f35f27ac Mon Sep 17 00:00:00 2001 From: denes Date: Mon, 13 Jul 2009 10:03:23 +0000 Subject: [PATCH] Added statistics printings --- .../binaries/matitaprover/matitaprover.ml | 17 +++++++++++++++-- .../components/binaries/matitaprover/stats.ml | 1 + .../components/binaries/matitaprover/stats.mli | 1 + 3 files changed, 17 insertions(+), 2 deletions(-) create mode 120000 helm/software/components/binaries/matitaprover/stats.ml create mode 120000 helm/software/components/binaries/matitaprover/stats.mli diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index f516552bc..cfa82da98 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -113,9 +113,9 @@ let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) oname let report_error s = prerr_endline (string_of_int (Unix.getpid())^": "^s);; module Main(P : Paramod.Paramod with type t = leaf) = struct - + let run bag g_passives passives pp_unit_clause name = - match + match P.paramod ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with @@ -137,6 +137,7 @@ let worker order goal hypotheses = let module Pp = Pp.Pp(B) in let module O = Orderings.NRKBO(B) in (* just for processing the clauses *) let module P = Paramod.Paramod(O) in + let module Stats = Stats.Stats(O) in let bag = Terms.empty_bag, 0 in let bag, g_passives = P.mk_goal bag goal in let bag, passives = @@ -146,6 +147,18 @@ let worker order goal hypotheses = * C and then B * TODO: rebuild clauses, since the ordering has to * change after the stats are computed *) + let symb_list = Stats.parse_symbols passives g_passives in + prerr_endline "Hypotheses statistics :"; + List.iter (fun (t,occ,ar,g_occ) -> prerr_endline + (Printf.sprintf "%s %d %d %d %s" + (B.pp t) ar occ g_occ + (String.concat "," + (List.map B.pp (Stats.dependencies t passives)))); + if List.exists + (fun (u,occ2,ar2,g_occ2) -> not (B.eq t u) && occ = occ2 + && ar = ar2 && g_occ = g_occ2) symb_list + then prerr_endline ((B.pp t) ^ " clashes") + ) symb_list; let module C = C in let module B = MakeBlob(C) in match order with diff --git a/helm/software/components/binaries/matitaprover/stats.ml b/helm/software/components/binaries/matitaprover/stats.ml new file mode 120000 index 000000000..ea1f8e1a2 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/stats.ml @@ -0,0 +1 @@ +../../ng_paramodulation/stats.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/stats.mli b/helm/software/components/binaries/matitaprover/stats.mli new file mode 120000 index 000000000..af0920c0c --- /dev/null +++ b/helm/software/components/binaries/matitaprover/stats.mli @@ -0,0 +1 @@ +../../ng_paramodulation/stats.mli \ No newline at end of file -- 2.39.2