Added statistics module

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
new file mode 100644 (file)
index 0000000..90d6ccf
--- /dev/null
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -0,0 +1,97 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: stats.ml 9822 2009-06-03 15:37:06Z denes $ *)
+
+module Stats (B : Terms.Blob) = 
+  struct
+
+    module SymbMap = Map.Make(B)
+
+    let rec occ_nbr t acc = function
+       | Terms.Leaf u when B.eq t u -> 1+acc
+       | Terms.Node l -> List.fold_left (occ_nbr t) acc l
+       | _ -> acc
+    ;;
+
+    let occ_nbr t = occ_nbr t 0;;
+
+    let goal_occ_nbr t = function
+      | (_,Terms.Equation (l,r,_,_),_,_) ->
+         occ_nbr t l + occ_nbr t r
+      | _ -> assert false
+    ;;
+
+    let rec parse_symbols acc l =
+      let rec aux acc = function
+       | Terms.Leaf t ->
+           (try
+              let (occ,ar) = SymbMap.find t acc in
+                SymbMap.add t (occ+1,ar) acc
+            with Not_found -> SymbMap.add t (1,0) acc)
+       | Terms.Var _ -> acc
+       | Terms.Node (Terms.Leaf hd::tl) ->
+           let acc =
+             try let (occ,ar) = SymbMap.find hd acc in
+               SymbMap.add hd (occ+1,ar) acc
+             with Not_found -> SymbMap.add hd (1,List.length tl) acc
+             in List.fold_left aux acc tl
+       | _ -> assert false
+      in
+       match l with
+         | [] -> acc
+         | (_,hd,_,_)::tl ->
+             match hd with
+               | Terms.Equation (l,r,_,_) ->
+                   parse_symbols (aux (aux acc l) r) tl
+               | Terms.Predicate _ -> assert false;
+    ;;
+
+    let parse_symbols l goal = 
+      let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in
+       SymbMap.fold (fun t (occ,ar) acc ->
+                       (t,occ,ar,goal_occ_nbr t goal)::acc) res []
+    ;;
+
+    let rec dependencies op clauses acc =
+      match clauses with
+       | [] -> []
+       | (_,lit,_,_)::tl ->
+           match lit with
+             | Terms.Predicate _ -> assert false
+             | Terms.Equation (l,r,_,_) ->
+                 match l,r with
+                   | (Terms.Node (Terms.Leaf op1::_),Terms.Node
+                        (Terms.Leaf op2::_)) ->
+                       if (B.eq op1 op) && not (B.eq op2 op) then
+                         let already = List.exists (B.eq op2) acc in
+                         let occ_l = occ_nbr op l in
+                         let occ_r = occ_nbr op r in
+                           if not already && occ_r > occ_l then
+                             dependencies op tl (op2::acc)
+                           else dependencies op tl acc
+                       else if not (B.eq op1 op) && (B.eq op2 op) then
+                         let already = List.exists (B.eq op1) acc in
+                         let occ_l = occ_nbr op l in
+                         let occ_r = occ_nbr op r in
+                           if not already && occ_l > occ_r then
+                             dependencies op tl (op1::acc)
+                           else
+                             dependencies op tl acc
+                       else dependencies op tl acc
+                   | _ -> acc
+    ;;
+
+    let dependencies op clauses = dependencies op clauses [];;
+
+    (* let max_weight_hyp = *)
+
+  end

diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli
new file mode 100644 (file)
index 0000000..b9be729
--- /dev/null
+++ b/helm/software/components/ng_paramodulation/stats.mli
@@ -0,0 +1,26 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: stats.mli 9822 2009-06-03 15:37:06Z denes $ *)
+
+module Stats (B : Orderings.Blob) : 
+  sig
+
+    module SymbMap : Map.S with type key = B.t
+
+    val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *)
+                       B.t Terms.unit_clause -> (* goal *)
+                       (B.t * int * int * int) list
+
+    val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list
+
+
+  end