Added statistics printings

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index f516552bc795b19a3ec250edd96c37519a1f3cdf..cfa82da98b6fa826c86113f631e9d6f07ee2bdee 100644 (file)
--- 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 (symlink)
index 0000000..ea1f8e1
--- /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 (symlink)
index 0000000..af0920c
--- /dev/null
+++ b/helm/software/components/binaries/matitaprover/stats.mli
@@ -0,0 +1 @@
+../../ng_paramodulation/stats.mli
\ No newline at end of file