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 parse_symbols l goal =
  59       let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in
  60         SymbMap.fold (fun t (occ,ar) acc ->
  61                         (t,occ,ar,goal_occ_nbr t goal)::acc) res []
  62     ;;
  63
  64     let rec dependencies op clauses acc =
  65       match clauses with
  66         | [] -> []
  67         | (_,lit,_,_)::tl ->
  68             match lit with
  69               | Terms.Predicate _ -> assert false
  70               | Terms.Equation (l,r,_,_) ->
  71                   match l,r with
  72                     | (Terms.Node (Terms.Leaf op1::_),Terms.Node
  73                          (Terms.Leaf op2::_)) ->
  74                         if (B.eq op1 op) && not (B.eq op2 op) then
  75                           let already = List.exists (B.eq op2) acc in
  76                           let occ_l = occ_nbr op l in
  77                           let occ_r = occ_nbr op r in
  78                             if not already && occ_r > occ_l then
  79                               dependencies op tl (op2::acc)
  80                             else dependencies op tl acc
  81                         else if not (B.eq op1 op) && (B.eq op2 op) then
  82                           let already = List.exists (B.eq op1) acc in
  83                           let occ_l = occ_nbr op l in
  84                           let occ_r = occ_nbr op r in
  85                             if not already && occ_l > occ_r then
  86                               dependencies op tl (op1::acc)
  87                             else
  88                               dependencies op tl acc
  89                         else dependencies op tl acc
  90                     | _ -> acc
  91     ;;
  92
  93     let dependencies op clauses = dependencies op clauses [];;
  94
  95     (* let max_weight_hyp = *)
  96
  97   end