Fixed conflicts due to problem when merging with UEQ implementation

[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..fd68f0fe765cd7cd75be5805dac8c516a0f623fb 100644 (file)
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -83,6 +83,12 @@ 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
@@ -109,10 +115,21 @@ module Stats (B : Terms.Blob) =
                            else
                              dependencies op tl acc
                        else 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
     ;;
 
-    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 = *)