helm/software/components/ng_paramodulation/stats.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: stats.ml 9822 2009-06-03 15:37:06Z denes $ *)
  13
  14 module Stats (B : Terms.Blob) =
  15   struct
  16
  17     module SymbMap = Map.Make(B)
  18     module Pp = Pp.Pp(B)
  19
  20     let rec occ_nbr t acc = function
  21         | Terms.Leaf u when B.eq t u -> 1+acc
  22         | Terms.Node l -> List.fold_left (occ_nbr t) acc l
  23         | _ -> acc
  24     ;;
  25
  26     let occ_nbr t = occ_nbr t 0;;
  27
  28     let goal_occ_nbr t = function
  29       | (_,[],[Terms.Equation (l,r,_,_),_],_,_) ->
  30           occ_nbr t l + occ_nbr t r
  31       | _ -> assert false
  32     ;;
  33
  34     let rec parse_symbols acc l =
  35       let rec aux acc = function
  36         | Terms.Leaf t ->
  37             (try
  38                let (occ,ar) = SymbMap.find t acc in
  39                  SymbMap.add t (occ+1,ar) acc
  40              with Not_found -> SymbMap.add t (1,0) acc)
  41         | Terms.Var _ -> acc
  42         | Terms.Node (Terms.Leaf hd::tl) ->
  43             let acc =
  44               try let (occ,ar) = SymbMap.find hd acc in
  45                 SymbMap.add hd (occ+1,ar) acc
  46               with Not_found -> SymbMap.add hd (1,List.length tl) acc
  47               in List.fold_left aux acc tl
  48         | _ -> assert false
  49       in
  50         match l with
  51           | [] -> acc
  52           | (_,nlit,plit,_,_)::tl ->
  53               let acc = List.fold_left (fun acc t ->
  54                                       match t with
  55                                         | Terms.Equation (l,r,_,_),_ ->
  56                                             (aux (aux acc l) r)
  57                                         | _ -> assert false) acc (nlit@plit)
  58               in
  59                  parse_symbols acc tl
  60     ;;
  61
  62     let goal_pos t goal =
  63       let rec aux path = function
  64        | Terms.Var _ -> []
  65        | Terms.Leaf x ->
  66            if B.eq t x then path else []
  67        | Terms.Node l ->
  68            match
  69              HExtlib.list_findopt
  70                (fun x i ->
  71                   let p = aux (i::path) x in
  72                   if p = [] then None else Some p)
  73                l
  74            with
  75            | None -> []
  76            | Some p -> p
  77       in
  78         aux []
  79           (match goal with
  80           | _,[],[Terms.Equation (l,r,ty,_),_],_,_ ->
  81                Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
  82           | _ -> assert false)
  83     ;;
  84
  85     let parse_symbols l goal =
  86       let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in
  87         SymbMap.fold (fun t (occ,ar) acc ->
  88                         (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
  89     ;;
  90
  91     let rec leaf_count = function
  92       | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
  93       | Terms.Leaf _ -> 1
  94       | _ -> 0
  95     ;;
  96
  97     let rec dependencies op clauses acc =
  98       match clauses with
  99         | [] -> acc
 100         | (_,nlit,plit,_,_)::tl ->
 101             match nlit,plit with
 102               | [],[Terms.Equation (l,r,_,_),_] ->
 103                   (match l,r with
 104                     | (Terms.Node (Terms.Leaf op1::_),Terms.Node
 105                          (Terms.Leaf op2::_)) ->
 106                         if (B.eq op1 op) && not (B.eq op2 op) then
 107                           let already = List.exists (B.eq op2) acc in
 108                           let occ_l = occ_nbr op l in
 109                           let occ_r = occ_nbr op r in
 110                             if not already && occ_r > occ_l then
 111                               dependencies op tl (op2::acc)
 112                             else dependencies op tl acc
 113                         else if not (B.eq op1 op) && (B.eq op2 op) then
 114                           let already = List.exists (B.eq op1) acc in
 115                           let occ_l = occ_nbr op l in
 116                           let occ_r = occ_nbr op r in
 117                             if not already && occ_l > occ_r then
 118                               dependencies op tl (op1::acc)
 119                             else
 120                               dependencies op tl acc
 121                         else dependencies op tl acc
 122                     | ((Terms.Node (Terms.Leaf op1::t) as x),y)
 123                     | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
 124                          let rec term_leaves = function
 125                            | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
 126                            | Terms.Leaf x -> [x]
 127                            | _ -> []
 128                          in
 129                          if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then
 130                            dependencies op tl (op1::acc)
 131                          else
 132                            dependencies op tl acc
 133                     | _ -> dependencies op tl acc)
 134                 | _ -> [] (* TODO : compute dependencies for clauses *)
 135     ;;
 136
 137     let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
 138
 139     (* let max_weight_hyp = *)
 140
 141   end