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

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
index 000000000..90d6ccf0b
--- /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
index 000000000..b9be72907
--- /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