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