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 fd68f0fe765cd7cd75be5805dac8c516a0f623fb..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 = 
@@ -92,11 +93,10 @@ module Stats (B : Terms.Blob) =
     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
@@ -126,7 +126,8 @@ module Stats (B : Terms.Blob) =
                            dependencies op tl (op1::acc)
                          else
                            dependencies op tl acc
-                   | _ -> dependencies op tl acc
+                   | _ -> dependencies op tl acc)
+               | _ -> assert false
     ;;
 
     let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;