X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fstats.ml;h=fd68f0fe765cd7cd75be5805dac8c516a0f623fb;hb=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;hp=90d6ccf0b8197b9f25276130be3b27dd0594f112;hpb=6f2f9693db45a2ef905123bc48cde9f04ddff54f;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index 90d6ccf0b..fd68f0fe7 100644
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -55,15 +55,43 @@ module Stats (B : Terms.Blob) =
 		| Terms.Predicate _ -> assert false;
     ;;
 
+    let goal_pos t goal =
+      let rec aux path = function
+       | Terms.Var _ -> [] 
+       | Terms.Leaf x ->
+           if B.eq t x then path else []
+       | Terms.Node l ->
+           match 
+             HExtlib.list_findopt
+               (fun x i -> 
+                  let p = aux (i::path) x in
+                  if p = [] then None else Some p)
+               l
+           with
+           | None -> []
+           | Some p -> p
+      in 
+        aux [] 
+          (match goal with
+          | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+	  | _,Terms.Predicate p,_,_ -> p)
+    ;;
+
     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 []
+			(t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
+    ;;
+
+    let rec leaf_count = function
+      | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
+      | Terms.Leaf _ -> 1
+      | _ -> 0
     ;;
 
     let rec dependencies op clauses acc =
       match clauses with
-	| [] -> []
+	| [] -> acc
 	| (_,lit,_,_)::tl ->
 	    match lit with
 	      | Terms.Predicate _ -> assert false
@@ -87,10 +115,21 @@ module Stats (B : Terms.Blob) =
 			    else
 			      dependencies op tl acc
 			else dependencies op tl acc
-		    | _ -> acc
+                    | ((Terms.Node (Terms.Leaf op1::t) as x),y)
+                    | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+                         let rec term_leaves = function
+                           | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
+                           | Terms.Leaf x -> [x]
+                           | _ -> []
+                         in
+                         if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then 
+                           dependencies op tl (op1::acc)
+                         else
+                           dependencies op tl acc
+		    | _ -> dependencies op tl acc
     ;;
 
-    let dependencies op clauses = dependencies op clauses [];;
+    let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
 
     (* let max_weight_hyp = *)