From 6f2f9693db45a2ef905123bc48cde9f04ddff54f Mon Sep 17 00:00:00 2001 From: denes Date: Mon, 13 Jul 2009 10:02:10 +0000 Subject: [PATCH] Added statistics module --- .../components/ng_paramodulation/stats.ml | 97 +++++++++++++++++++ .../components/ng_paramodulation/stats.mli | 26 +++++ 2 files changed, 123 insertions(+) create mode 100644 helm/software/components/ng_paramodulation/stats.ml create mode 100644 helm/software/components/ng_paramodulation/stats.mli diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml new file mode 100644 index 000000000..90d6ccf0b --- /dev/null +++ b/helm/software/components/ng_paramodulation/stats.ml @@ -0,0 +1,97 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: stats.ml 9822 2009-06-03 15:37:06Z denes $ *) + +module Stats (B : Terms.Blob) = + struct + + module SymbMap = Map.Make(B) + + let rec occ_nbr t acc = function + | Terms.Leaf u when B.eq t u -> 1+acc + | Terms.Node l -> List.fold_left (occ_nbr t) acc l + | _ -> acc + ;; + + let occ_nbr t = occ_nbr t 0;; + + let goal_occ_nbr t = function + | (_,Terms.Equation (l,r,_,_),_,_) -> + occ_nbr t l + occ_nbr t r + | _ -> assert false + ;; + + let rec parse_symbols acc l = + let rec aux acc = function + | Terms.Leaf t -> + (try + let (occ,ar) = SymbMap.find t acc in + SymbMap.add t (occ+1,ar) acc + with Not_found -> SymbMap.add t (1,0) acc) + | Terms.Var _ -> acc + | Terms.Node (Terms.Leaf hd::tl) -> + let acc = + try let (occ,ar) = SymbMap.find hd acc in + SymbMap.add hd (occ+1,ar) acc + with Not_found -> SymbMap.add hd (1,List.length tl) acc + in List.fold_left aux acc tl + | _ -> assert false + in + match l with + | [] -> acc + | (_,hd,_,_)::tl -> + match hd with + | Terms.Equation (l,r,_,_) -> + parse_symbols (aux (aux acc l) r) tl + | Terms.Predicate _ -> assert false; + ;; + + let parse_symbols l goal = + let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in + SymbMap.fold (fun t (occ,ar) acc -> + (t,occ,ar,goal_occ_nbr t goal)::acc) res [] + ;; + + let rec dependencies op clauses acc = + match clauses with + | [] -> [] + | (_,lit,_,_)::tl -> + match lit with + | Terms.Predicate _ -> assert false + | 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 + let already = List.exists (B.eq op2) acc in + let occ_l = occ_nbr op l in + let occ_r = occ_nbr op r in + if not already && occ_r > occ_l then + dependencies op tl (op2::acc) + else dependencies op tl acc + else if not (B.eq op1 op) && (B.eq op2 op) then + let already = List.exists (B.eq op1) acc in + let occ_l = occ_nbr op l in + let occ_r = occ_nbr op r in + if not already && occ_l > occ_r then + dependencies op tl (op1::acc) + else + dependencies op tl acc + else dependencies op tl acc + | _ -> acc + ;; + + let dependencies op clauses = dependencies op clauses [];; + + (* let max_weight_hyp = *) + + end diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli new file mode 100644 index 000000000..b9be72907 --- /dev/null +++ b/helm/software/components/ng_paramodulation/stats.mli @@ -0,0 +1,26 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: stats.mli 9822 2009-06-03 15:37:06Z denes $ *) + +module Stats (B : Orderings.Blob) : + sig + + module SymbMap : Map.S with type key = B.t + + val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *) + B.t Terms.unit_clause -> (* goal *) + (B.t * int * int * int) list + + val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list + + + end -- 2.39.2