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 type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
  15
  16 module Orderings (B : Terms.Blob) = struct
  17
  18   module Pp = Pp.Pp(B)
  19
  20   type weight = int * (int * int) list;;
  21
  22 let rec eq_foterm x y =
  23     x == y ||
  24     match x, y with
  25     | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
  26     | Terms.Var i, Terms.Var j -> i = j
  27     | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2
  28     | _ -> false
  29   ;;
  30
  31   let string_of_weight (cw, mw) =
  32     let s =
  33       String.concat ", "
  34         (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
  35     in
  36     Printf.sprintf "[%d; %s]" cw s
  37   ;;
  38
  39   let weight_of_term term =
  40     let vars_dict = Hashtbl.create 5 in
  41     let rec aux = function
  42       | Terms.Var i ->
  43           (try
  44              let oldw = Hashtbl.find vars_dict i in
  45              Hashtbl.replace vars_dict i (oldw+1)
  46            with Not_found ->
  47              Hashtbl.add vars_dict i 1);
  48           0
  49       | Terms.Leaf _ -> 1
  50       | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
  51     in
  52     let w = aux term in
  53     let l =
  54       Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
  55     in
  56     let compare w1 w2 =
  57       match w1, w2 with
  58       | (m1, _), (m2, _) -> m1 - m2
  59     in
  60     (w, List.sort compare l) (* from the smallest meta to the bigest *)
  61   ;;
  62
  63   let compute_unit_clause_weight (_,l, _, _) =
  64     let weight_of_polynomial w m =
  65       let factor = 2 in
  66       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
  67     in
  68     match l with
  69     | Terms.Predicate t ->
  70         let w, m = weight_of_term t in
  71         weight_of_polynomial w m
  72     | Terms.Equation (_,x,_,Terms.Lt)
  73     | Terms.Equation (x,_,_,Terms.Gt) ->
  74         let w, m = weight_of_term x in
  75         weight_of_polynomial w m
  76     | Terms.Equation (l,r,_,Terms.Eq)
  77     | Terms.Equation (l,r,_,Terms.Incomparable) ->
  78         let wl, ml = weight_of_term l in
  79         let wr, mr = weight_of_term r in
  80         weight_of_polynomial (wl+wr) (ml@mr)
  81   ;;
  82
  83 let compute_goal_weight (_,l, _, _) =
  84     let weight_of_polynomial w m =
  85       let factor = 2 in
  86       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
  87     in
  88     match l with
  89     | Terms.Predicate t ->
  90         let w, m = weight_of_term t in
  91         weight_of_polynomial w m
  92     | Terms.Equation (l,r,_,_) ->
  93         let wl, ml = weight_of_term l in
  94         let wr, mr = weight_of_term r in
  95         let wl = weight_of_polynomial wl ml in
  96         let wr = weight_of_polynomial wr mr in
  97           - (abs (wl-wr))
  98   ;;
  99
 100   (* Riazanov: 3.1.5 pag 38 *)
 101 (* Compare weights normalized in a new way :
 102  * Variables should be sorted from the lowest index to the highest
 103  * Variables which do not occur in the term should not be present
 104  * in the normalized polynomial
 105  *)
 106   let compare_weights (h1, w1) (h2, w2) =
 107     let rec aux hdiff (lt, gt) diffs w1 w2 =
 108       match w1, w2 with
 109         | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
 110             if var1 = var2 then
 111               let diffs = (w1 - w2) + diffs in
 112               let r = compare w1 w2 in
 113               let lt = lt or (r < 0) in
 114               let gt = gt or (r > 0) in
 115                 if lt && gt then XINCOMPARABLE else
 116                   aux hdiff (lt, gt) diffs tl1 tl2
 117             else if var1 < var2 then
 118               if lt then XINCOMPARABLE else
 119                 aux hdiff (false,true) (diffs+w1) tl1 l2
 120             else
 121               if gt then XINCOMPARABLE else
 122                 aux hdiff (true,false) (diffs-w2) l1 tl2
 123         | [], (_,w2)::tl2 ->
 124             if gt then XINCOMPARABLE else
 125               aux hdiff (true,false) (diffs-w2) [] tl2
 126         | (_,w1)::tl1, [] ->
 127             if lt then XINCOMPARABLE else
 128               aux hdiff (false,true) (diffs+w1) tl1 []
 129         | [], [] ->
 130             if lt then
 131               if hdiff <= 0 then XLT
 132               else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
 133             else if gt then
 134               if hdiff >= 0 then XGT
 135               else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
 136             else
 137               if hdiff < 0 then XLT
 138               else if hdiff > 0 then XGT
 139               else XEQ
 140     in
 141       aux (h1-h2) (false,false) 0 w1 w2
 142   ;;
 143
 144   (* Riazanov: p. 40, relation >>>
 145    * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
 146   let rec aux_ordering ?(head_only=false) t1 t2 =
 147     match t1, t2 with
 148     (* We want to discard any identity equality. *
 149      * If we give back XEQ, no inference rule    *
 150      * will be applied on this equality          *)
 151     | Terms.Var i, Terms.Var j when i = j ->
 152         XEQ
 153     (* 1. *)
 154     | Terms.Var _, _
 155     | _, Terms.Var _ -> XINCOMPARABLE
 156     (* 2.a *)
 157     | Terms.Leaf a1, Terms.Leaf a2 ->
 158         let cmp = B.compare a1 a2 in
 159         if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
 160     | Terms.Leaf _, Terms.Node _ -> XLT
 161     | Terms.Node _, Terms.Leaf _ -> XGT
 162     (* 2.b *)
 163     | Terms.Node l1, Terms.Node l2 ->
 164         let rec cmp t1 t2 =
 165           match t1, t2 with
 166           | [], [] -> XEQ
 167           | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
 168           | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
 169           | hd1::tl1, hd2::tl2 ->
 170               let o = aux_ordering ~head_only hd1 hd2 in
 171               if o = XEQ && not head_only then cmp tl1 tl2 else o
 172         in
 173         cmp l1 l2
 174   ;;
 175
 176   (* Riazanov: p. 40, relation >_n *)
 177   let nonrec_kbo t1 t2 =
 178     let w1 = weight_of_term t1 in
 179     let w2 = weight_of_term t2 in
 180     match compare_weights w1 w2 with
 181     | XLE ->  (* this is .> *)
 182         if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
 183     | XGE ->
 184         if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
 185     | XEQ -> aux_ordering t1 t2
 186     | res -> res
 187   ;;
 188
 189   (* Riazanov: p. 38, relation > *)
 190   let rec kbo t1 t2 =
 191     let aux = aux_ordering ~head_only:true in
 192     let rec cmp t1 t2 =
 193       match t1, t2 with
 194       | [], [] -> XEQ
 195       | _, [] -> XGT
 196       | [], _ -> XLT
 197       | hd1::tl1, hd2::tl2 ->
 198           let o = kbo hd1 hd2 in
 199           if o = XEQ then cmp tl1 tl2
 200           else o
 201     in
 202     let w1 = weight_of_term t1 in
 203     let w2 = weight_of_term t2 in
 204     let comparison = compare_weights w1 w2 in
 205     match comparison with
 206     | XLE ->
 207         let r = aux t1 t2 in
 208         if r = XLT then XLT
 209         else if r = XEQ then (
 210           match t1, t2 with
 211           | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
 212               if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
 213           | _, _ -> assert false
 214         ) else XINCOMPARABLE
 215     | XGE ->
 216         let r = aux t1 t2 in
 217         if r = XGT then XGT
 218         else if r = XEQ then (
 219           match t1, t2 with
 220           | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
 221               if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
 222           | _, _ ->  assert false
 223         ) else XINCOMPARABLE
 224     | XEQ ->
 225         let r = aux t1 t2 in
 226         if r = XEQ then (
 227           match t1, t2 with
 228           | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
 229           | _, _ ->  XINCOMPARABLE
 230         ) else r
 231     | res -> res
 232   ;;
 233
 234   let rec lpo s t =
 235     match s,t with
 236       | s, t when eq_foterm s t ->
 237           XEQ
 238       | Terms.Var _, Terms.Var _ ->
 239           XINCOMPARABLE
 240       | _, Terms.Var i ->
 241           if (List.mem i (Terms.vars_of_term s)) then XGT
 242           else XINCOMPARABLE
 243       | Terms.Var i,_ ->
 244           if (List.mem i (Terms.vars_of_term t)) then XLT
 245           else XINCOMPARABLE
 246       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
 247           let rec ge_subterm t ol = function
 248             | [] -> (false, ol)
 249             | x::tl ->
 250                 let res = lpo x t in
 251                 match res with
 252                   | XGT | XEQ -> (true,res::ol)
 253                   | o -> ge_subterm t (o::ol) tl
 254           in
 255           let (res, l_ol) = ge_subterm t [] tl1 in
 256             if res then XGT
 257             else let (res, r_ol) = ge_subterm s [] tl2 in
 258               if res then XLT
 259               else begin
 260                 let rec check_subterms t = function
 261                   | _,[] -> true
 262                   | o::ol,_::tl ->
 263                       if o = XLT then check_subterms t (ol,tl)
 264                       else false
 265                   | [], x::tl ->
 266                       if lpo x t = XLT then check_subterms t ([],tl)
 267                       else false
 268                 in
 269                 match aux_ordering hd1 hd2 with
 270                   | XGT -> if check_subterms s (r_ol,tl2) then XGT
 271                     else XINCOMPARABLE
 272                   | XLT -> if check_subterms t (l_ol,tl1) then XLT
 273                     else XINCOMPARABLE
 274                   | XEQ ->
 275                       let lex = List.fold_left2
 276                         (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
 277                         XEQ tl1 tl2
 278                       in
 279                  (match lex with
 280                     | XGT ->
 281                         if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
 282                       else XINCOMPARABLE
 283                     | XLT ->
 284                         if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
 285                       else XINCOMPARABLE
 286                     | o -> o)
 287               | XINCOMPARABLE -> XINCOMPARABLE
 288               | _ -> assert false
 289           end
 290       | _,_ -> aux_ordering s t
 291
 292   ;;
 293
 294   let compare_terms x y =
 295       match nonrec_kbo x y with
 296         | XINCOMPARABLE -> Terms.Incomparable
 297         | XGT -> Terms.Gt
 298         | XLT -> Terms.Lt
 299         | XEQ -> Terms.Eq
 300         | _ -> assert false
 301   ;;
 302
 303   let profiler = HExtlib.profile ~enable:true "compare_terms";;
 304   let compare_terms x y =
 305     profiler.HExtlib.profile (compare_terms x) y
 306   ;;
 307
 308 end