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
  19     let rec occ_nbr t acc = function
  20         | Terms.Leaf u when B.eq t u -> 1+acc
  21         | Terms.Node l -> List.fold_left (occ_nbr t) acc l
  22         | _ -> acc
  23     ;;
  24
  25     let occ_nbr t = occ_nbr t 0;;
  26
  27     let goal_occ_nbr t = function
  28       | (_,Terms.Equation (l,r,_,_),_,_) ->
  29           occ_nbr t l + occ_nbr t r
  30       | _ -> assert false
  31     ;;
  32
  33     let rec parse_symbols acc l =
  34       let rec aux acc = function
  35         | Terms.Leaf t ->
  36             (try
  37                let (occ,ar) = SymbMap.find t acc in
  38                  SymbMap.add t (occ+1,ar) acc
  39              with Not_found -> SymbMap.add t (1,0) acc)
  40         | Terms.Var _ -> acc
  41         | Terms.Node (Terms.Leaf hd::tl) ->
  42             let acc =
  43               try let (occ,ar) = SymbMap.find hd acc in
  44                 SymbMap.add hd (occ+1,ar) acc
  45               with Not_found -> SymbMap.add hd (1,List.length tl) acc
  46               in List.fold_left aux acc tl
  47         | _ -> assert false
  48       in
  49         match l with
  50           | [] -> acc
  51           | (_,hd,_,_)::tl ->
  52               match hd with
  53                 | Terms.Equation (l,r,_,_) ->
  54                     parse_symbols (aux (aux acc l) r) tl
  55                 | Terms.Predicate _ -> assert false;
  56     ;;
  57
  58     let goal_pos t goal =
  59       let rec aux path = function
  60        | Terms.Var _ -> []
  61        | Terms.Leaf x ->
  62            if B.eq t x then path else []
  63        | Terms.Node l ->
  64            match
  65              HExtlib.list_findopt
  66                (fun x i ->
  67                   let p = aux (i::path) x in
  68                   if p = [] then None else Some p)
  69                l
  70            with
  71            | None -> []
  72            | Some p -> p
  73       in
  74         aux []
  75           (match goal with
  76           | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
  77           | _,Terms.Predicate p,_,_ -> p)
  78     ;;
  79
  80     let parse_symbols l goal =
  81       let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in
  82         SymbMap.fold (fun t (occ,ar) acc ->
  83                         (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
  84     ;;
  85
  86     let rec dependencies op clauses acc =
  87       match clauses with
  88         | [] -> acc
  89         | (_,lit,_,_)::tl ->
  90             match lit with
  91               | Terms.Predicate _ -> assert false
  92               | Terms.Equation (l,r,_,_) ->
  93                   match l,r with
  94                     | (Terms.Node (Terms.Leaf op1::_),Terms.Node
  95                          (Terms.Leaf op2::_)) ->
  96                         if (B.eq op1 op) && not (B.eq op2 op) then
  97                           let already = List.exists (B.eq op2) acc in
  98                           let occ_l = occ_nbr op l in
  99                           let occ_r = occ_nbr op r in
 100                             if not already && occ_r > occ_l then
 101                               dependencies op tl (op2::acc)
 102                             else dependencies op tl acc
 103                         else if not (B.eq op1 op) && (B.eq op2 op) then
 104                           let already = List.exists (B.eq op1) acc in
 105                           let occ_l = occ_nbr op l in
 106                           let occ_r = occ_nbr op r in
 107                             if not already && occ_l > occ_r then
 108                               dependencies op tl (op1::acc)
 109                             else
 110                               dependencies op tl acc
 111                         else dependencies op tl acc
 112                     | _ -> dependencies op tl acc
 113     ;;
 114
 115     let dependencies op clauses = dependencies op clauses [];;
 116
 117     (* let max_weight_hyp = *)
 118
 119   end