statistics are used, when possible, to sort

[helm.git] / helm / software / components / ng_paramodulation / stats.ml

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index 90d6ccf0b8197b9f25276130be3b27dd0594f112..a281ddc867a12ee8a21ab8f1ae17f629cf345e87 100644 (file)
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -55,10 +55,32 @@ 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 dependencies op clauses acc =