helm/software/components/ng_paramodulation/orderings.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$ *)
  13
  14 module Orderings (B : Terms.Blob) = struct
  15
  16   type weight = int * (int * int) list;;
  17
  18   let string_of_weight (cw, mw) =
  19     let s =
  20       String.concat ", "
  21         (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
  22     in
  23     Printf.sprintf "[%d; %s]" cw s
  24   ;;
  25
  26   let weight_of_term term =
  27     let vars_dict = Hashtbl.create 5 in
  28     let rec aux = function
  29       | Terms.Var i ->
  30           (try
  31              let oldw = Hashtbl.find vars_dict i in
  32              Hashtbl.replace vars_dict i (oldw+1)
  33            with Not_found ->
  34              Hashtbl.add vars_dict i 1);
  35           0
  36       | Terms.Leaf _ -> 1
  37       | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
  38     in
  39     let w = aux term in
  40     let l =
  41       Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
  42     in
  43     let compare w1 w2 =
  44       match w1, w2 with
  45       | (m1, _), (m2, _) -> m2 - m1
  46     in
  47     (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
  48   ;;
  49
  50   let compute_clause_weight = assert false (*
  51     let factor = 2 in
  52     match o with
  53       | Terms.Lt ->
  54         let w, m = (weight_of_term
  55                ~consider_metas:true ~count_metas_occurrences:false right) in
  56           w + (factor * (List.length m)) ;
  57       | Terms.Le -> assert false
  58       | Terms.Gt ->
  59         let w, m = (weight_of_term
  60                ~consider_metas:true ~count_metas_occurrences:false left) in
  61           w + (factor * (List.length m)) ;
  62     | Terms.Ge -> assert false
  63     | Terms.Eq
  64     | Terms.Incomparable ->
  65         let w1, m1 = (weight_of_term
  66                ~consider_metas:true ~count_metas_occurrences:false right) in
  67         let w2, m2 = (weight_of_term
  68                ~consider_metas:true ~count_metas_occurrences:false left) in
  69         w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
  70   *)
  71   ;;
  72
  73   (* returns a "normalized" version of the polynomial weight wl (with type
  74    * weight list), i.e. a list sorted ascending by meta number,
  75    * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
  76    * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
  77    *      (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
  78   let normalize_weight maxmeta (cw, wl) =
  79     let rec aux = function
  80       | 0 -> []
  81       | m -> (m, 0)::(aux (m-1))
  82     in
  83     let tmpl = aux maxmeta in
  84     let wl =
  85       List.sort
  86         (fun (m, _) (n, _) -> Pervasives.compare m n)
  87         (List.fold_left
  88            (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
  89     in
  90     (cw, wl)
  91   ;;
  92
  93
  94   let normalize_weights (cw1, wl1) (cw2, wl2) =
  95     let rec aux wl1 wl2 =
  96       match wl1, wl2 with
  97       | [], [] -> [], []
  98       | (m, w)::tl1, (n, w')::tl2 when m = n ->
  99           let res1, res2 = aux tl1 tl2 in
 100           (m, w)::res1, (n, w')::res2
 101       | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
 102           let res1, res2 = aux tl1 wl2 in
 103           (m, w)::res1, (m, 0)::res2
 104       | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
 105           let res1, res2 = aux wl1 tl2 in
 106           (n, 0)::res1, (n, w')::res2
 107       | [], (n, w)::tl2 ->
 108           let res1, res2 = aux [] tl2 in
 109           (n, 0)::res1, (n, w)::res2
 110       | (m, w)::tl1, [] ->
 111           let res1, res2 = aux tl1 [] in
 112           (m, w)::res1, (m, 0)::res2
 113       | _, _ -> assert false
 114     in
 115     let cmp (m, _) (n, _) = compare m n in
 116     let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
 117     (cw1, wl1), (cw2, wl2)
 118   ;;
 119
 120   (* Riazanov: 3.1.5 pag 38 *)
 121   (* TODO: optimize early detection of Terms.Incomparable case *)
 122   let compare_weights (h1, w1) (h2, w2) =
 123     let res, diffs =
 124       try
 125         List.fold_left2
 126           (fun ((lt, eq, gt), diffs) w1 w2 ->
 127              match w1, w2 with
 128              | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
 129                  let diffs = (w1 - w2) + diffs in
 130                  let r = compare w1 w2 in
 131                  if r < 0 then (lt+1, eq, gt), diffs
 132                  else if r = 0 then (lt, eq+1, gt), diffs
 133                  else (lt, eq, gt+1), diffs
 134              | _ -> assert false)
 135           ((0, 0, 0), 0) w1 w2
 136       with Invalid_argument _ -> assert false
 137     in
 138     let hdiff = h1 - h2 in
 139     match res with
 140     | (0, _, 0) ->
 141         if hdiff < 0 then Terms.Lt
 142         else if hdiff > 0 then Terms.Gt
 143         else Terms.Eq
 144     | (m, _, 0) ->
 145         if hdiff <= 0 then Terms.Lt
 146         else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
 147     | (0, _, m) ->
 148         if hdiff >= 0 then Terms.Gt
 149         else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
 150     | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
 151     | _ -> assert false
 152   ;;
 153
 154
 155   let rec aux_ordering t1 t2 =
 156     match t1, t2 with
 157     | Terms.Var _, _
 158     | _, Terms.Var _ -> Terms.Incomparable
 159
 160     | Terms.Leaf a1, Terms.Leaf a2 ->
 161         let cmp = Pervasives.compare a1 a2 in
 162         if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
 163
 164     | Terms.Leaf _, Terms.Node _ -> Terms.Lt
 165     | Terms.Node _, Terms.Leaf _ -> Terms.Gt
 166
 167     | Terms.Node l1, Terms.Node l2 ->
 168         let rec cmp t1 t2 =
 169           match t1, t2 with
 170           | [], [] -> Terms.Eq
 171           | _, [] -> Terms.Gt
 172           | [], _ -> Terms.Lt
 173           | hd1::tl1, hd2::tl2 ->
 174               let o = aux_ordering hd1 hd2 in
 175               if o = Terms.Eq then cmp tl1 tl2
 176               else o
 177         in
 178         cmp l1 l2
 179   ;;
 180
 181   let nonrec_kbo t1 t2 =
 182     let w1 = weight_of_term t1 in
 183     let w2 = weight_of_term t2 in
 184     let w1, w2 = normalize_weights w1 w2 in
 185     match compare_weights w1 w2 with
 186     | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
 187     | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
 188     | Terms.Eq -> aux_ordering t1 t2
 189     | res -> res
 190   ;;
 191
 192   (*
 193   let rec kbo t1 t2 =
 194     let aux = aux_ordering ~recursion:false in
 195     let w1 = weight_of_term t1
 196     and w2 = weight_of_term t2 in
 197     let rec cmp t1 t2 =
 198       match t1, t2 with
 199       | [], [] -> Terms.Eq
 200       | _, [] -> Terms.Gt
 201       | [], _ -> Terms.Lt
 202       | hd1::tl1, hd2::tl2 ->
 203           let o =
 204             kbo hd1 hd2
 205           in
 206           if o = Terms.Eq then cmp tl1 tl2
 207           else o
 208     in
 209     let w1, w2 = normalize_weights w1 w2 in
 210     let comparison = compare_weights w1 w2 in
 211     match comparison with
 212     | Terms.Le ->
 213         let r = aux t1 t2 in
 214         if r = Terms.Lt then Terms.Lt
 215         else if r = Terms.Eq then (
 216           match t1, t2 with
 217           | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 218               if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
 219           | _, _ ->  Terms.Incomparable
 220         ) else Terms.Incomparable
 221     | Terms.Ge ->
 222         let r = aux t1 t2 in
 223         if r = Terms.Gt then Terms.Gt
 224         else if r = Terms.Eq then (
 225           match t1, t2 with
 226           | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 227               if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
 228           | _, _ ->  Terms.Incomparable
 229         ) else Terms.Incomparable
 230     | Terms.Eq ->
 231         let r = aux t1 t2 in
 232         if r = Terms.Eq then (
 233           match t1, t2 with
 234           | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 235               cmp tl1 tl2
 236           | _, _ ->  Terms.Incomparable
 237         ) else r
 238     | res -> res
 239   ;;
 240   *)
 241
 242   let compare_terms = nonrec_kbo;;
 243
 244 end