From: denes <??>
Date: Mon, 13 Jul 2009 10:03:23 +0000 (+0000)
Subject: Added statistics printings
X-Git-Tag: make_still_working~3689
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=db7f6d6b32515c091e0f338dd4903624f35f27ac

Added statistics printings
---

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