First compiling version

[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 0f9f45d960e6c30aac980d5bde0f62950d7678a1..04aaa75f51fc05e92888e398b9032d172321f42b 100644 (file)
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -25,7 +25,7 @@ module Stats (B : Terms.Blob) =
     let occ_nbr t = occ_nbr t 0;;
 
     let goal_occ_nbr t = function
-      | (_,Terms.Equation (l,r,_,_),_,_) ->
+      | (_,[],[Terms.Equation (l,r,_,_),_],_,_) ->
          occ_nbr t l + occ_nbr t r
       | _ -> assert false
     ;;
@@ -48,11 +48,11 @@ module Stats (B : Terms.Blob) =
       in
        match l with
          | [] -> acc
-         | (_,hd,_,_)::tl ->
-             match hd with
-               | Terms.Equation (l,r,_,_) ->
+         | (_,nlit,plit,_,_)::tl ->
+             match nlit,plit with
+               | [],[Terms.Equation (l,r,_,_),_] ->
                    parse_symbols (aux (aux acc l) r) tl
-               | Terms.Predicate _ -> assert false;
+               | _ -> assert false;
     ;;
 
     let goal_pos t goal =
@@ -73,8 +73,9 @@ module Stats (B : Terms.Blob) =
       in 
         aux [] 
           (match goal with
-          | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
-         | _,Terms.Predicate p,_,_ -> p)
+          | _,[],[Terms.Equation (l,r,ty,_),_],_,_ ->
+               Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+         | _ -> assert false)
     ;;
 
     let parse_symbols l goal = 
@@ -83,14 +84,19 @@ module Stats (B : Terms.Blob) =
                        (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
-             | Terms.Equation (l,r,_,_) ->
-                 match l,r with
+       | (_,nlit,plit,_,_)::tl ->
+           match nlit,plit with
+             | [],[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
@@ -109,10 +115,22 @@ module Stats (B : Terms.Blob) =
                            else
                              dependencies op tl acc
                        else dependencies op tl acc
-                   | _ -> dependencies op tl 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)
+               | _ -> assert false
     ;;
 
-    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 = *)