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 | XINVERTIBLE
  15
  16 module type Blob =
  17   sig
  18     include Terms.Blob
  19
  20     (* This order relation should be:
  21      * - stable for instantiation
  22      * - total on ground terms
  23      *
  24      *)
  25     val compare_terms :
  26           t Terms.foterm -> t Terms.foterm -> Terms.comparison
  27
  28     val compute_clause_weight : 't Terms.clause -> int
  29
  30     val name : string
  31
  32   end
  33
  34 type weight = int * (int * int) list;;
  35
  36 let rec eq_foterm f x y =
  37     x == y ||
  38     match x, y with
  39     | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
  40     | Terms.Var i, Terms.Var j -> i = j
  41     | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
  42     | _ -> false
  43 ;;
  44
  45 let string_of_weight (cw, mw) =
  46   let s =
  47     String.concat ", "
  48       (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
  49   in
  50   Printf.sprintf "[%d; %s]" cw s
  51 ;;
  52
  53 let weight_of_term term =
  54     let vars_dict = Hashtbl.create 5 in
  55     let rec aux = function
  56       | Terms.Var i ->
  57           (try
  58              let oldw = Hashtbl.find vars_dict i in
  59              Hashtbl.replace vars_dict i (oldw+1)
  60            with Not_found ->
  61              Hashtbl.add vars_dict i 1);
  62           0
  63       | Terms.Leaf _ -> 1
  64       | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
  65     in
  66     let w = aux term in
  67     let l =
  68       Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
  69     in
  70     let compare w1 w2 =
  71       match w1, w2 with
  72       | (m1, _), (m2, _) -> m1 - m2
  73     in
  74     (w, List.sort compare l) (* from the smallest meta to the bigest *)
  75 ;;
  76
  77 let compute_literal_weight l =
  78     let weight_of_polynomial w m =
  79       let factor = 2 in
  80       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
  81     in
  82     match l with
  83     | Terms.Predicate t ->
  84         let w, m = weight_of_term t in
  85         weight_of_polynomial w m
  86     | Terms.Equation (_,x,_,Terms.Lt)
  87     | Terms.Equation (x,_,_,Terms.Gt) ->
  88         let w, m = weight_of_term x in
  89         weight_of_polynomial w m
  90     | Terms.Equation (l,r,_,Terms.Eq)
  91     | Terms.Equation (l,r,_,Terms.Incomparable)
  92     | Terms.Equation (l,r,_,Terms.Invertible) ->
  93         let wl, ml = weight_of_term l in
  94         let wr, mr = weight_of_term r in
  95         weight_of_polynomial (wl+wr) (ml@mr)
  96 ;;
  97
  98 let compute_clause_weight (_,nl,pl,_,_) =
  99   List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
 100
 101 let compute_goal_weight = compute_clause_weight;;
 102
 103 (* Riazanov: 3.1.5 pag 38 *)
 104 (* Compare weights normalized in a new way :
 105  * Variables should be sorted from the lowest index to the highest
 106  * Variables which do not occur in the term should not be present
 107  * in the normalized polynomial
 108  *)
 109 let compare_weights (h1, w1) (h2, w2) =
 110   let rec aux hdiff (lt, gt) diffs w1 w2 =
 111     match w1, w2 with
 112       | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
 113           if var1 = var2 then
 114             let diffs = (w1 - w2) + diffs in
 115             let r = Pervasives.compare w1 w2 in
 116             let lt = lt or (r < 0) in
 117             let gt = gt or (r > 0) in
 118               if lt && gt then XINCOMPARABLE else
 119                 aux hdiff (lt, gt) diffs tl1 tl2
 120           else if var1 < var2 then
 121             if lt then XINCOMPARABLE else
 122               aux hdiff (false,true) (diffs+w1) tl1 l2
 123           else
 124             if gt then XINCOMPARABLE else
 125               aux hdiff (true,false) (diffs-w2) l1 tl2
 126       | [], (_,w2)::tl2 ->
 127           if gt then XINCOMPARABLE else
 128             aux hdiff (true,false) (diffs-w2) [] tl2
 129       | (_,w1)::tl1, [] ->
 130           if lt then XINCOMPARABLE else
 131             aux hdiff (false,true) (diffs+w1) tl1 []
 132       | [], [] ->
 133           if lt then
 134             if hdiff <= 0 then XLT
 135             else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
 136           else if gt then
 137             if hdiff >= 0 then XGT
 138             else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
 139           else
 140             if hdiff < 0 then XLT
 141             else if hdiff > 0 then XGT
 142             else XEQ
 143   in
 144     aux (h1-h2) (false,false) 0 w1 w2
 145 ;;
 146
 147 (* Riazanov: p. 40, relation >>>
 148  * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
 149 let rec aux_ordering b_compare ?(head_only=false) t1 t2 =
 150   match t1, t2 with
 151   (* We want to discard any identity equality. *
 152    * If we give back XEQ, no inference rule    *
 153    * will be applied on this equality          *)
 154   | Terms.Var i, Terms.Var j when i = j ->
 155       XEQ
 156   (* 1. *)
 157   | Terms.Var _, _
 158   | _, Terms.Var _ -> XINCOMPARABLE
 159   (* 2.a *)
 160   | Terms.Leaf a1, Terms.Leaf a2 ->
 161       let cmp = b_compare a1 a2 in
 162       if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
 163   | Terms.Leaf _, Terms.Node _ -> XLT
 164   | Terms.Node _, Terms.Leaf _ -> XGT
 165   (* 2.b *)
 166   | Terms.Node l1, Terms.Node l2 ->
 167       let rec cmp t1 t2 =
 168         match t1, t2 with
 169         | [], [] -> XEQ
 170         | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
 171         | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
 172         | hd1::tl1, hd2::tl2 ->
 173             let o = aux_ordering b_compare ~head_only hd1 hd2 in
 174             if o = XEQ && not head_only then cmp tl1 tl2 else o
 175       in
 176       cmp l1 l2
 177 ;;
 178
 179 let compare_terms o x y =
 180     match o x y with
 181       | XINCOMPARABLE -> Terms.Incomparable
 182       | XGT -> Terms.Gt
 183       | XLT -> Terms.Lt
 184       | XEQ -> Terms.Eq
 185       | XINVERTIBLE -> Terms.Invertible
 186       | _ -> assert false
 187 ;;
 188
 189 module NRKBO (B : Terms.Blob) = struct
 190   let name = "nrkbo"
 191   include B
 192
 193   module Pp = Pp.Pp(B)
 194
 195   let eq_foterm = eq_foterm B.eq;;
 196
 197 exception UnificationFailure of string Lazy.t;;
 198
 199
 200 (* DUPLICATE CODE FOR TESTS (see FoUnif)  *)
 201   let alpha_eq s t =
 202     let rec equiv subst s t =
 203       let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
 204       and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
 205
 206       in
 207       match s, t with
 208         | s, t when eq_foterm s t -> subst
 209         | Terms.Var i, Terms.Var j
 210             when (not (List.exists (fun (_,k) -> k=t) subst)) ->
 211             let subst = FoSubst.build_subst i t subst in
 212               subst
 213         | Terms.Node l1, Terms.Node l2 -> (
 214             try
 215               List.fold_left2
 216                 (fun subst' s t -> equiv subst' s t)
 217                 subst l1 l2
 218             with Invalid_argument _ ->
 219               raise (UnificationFailure (lazy "Inference.unification.unif"))
 220           )
 221         | _, _ ->
 222             raise (UnificationFailure (lazy "Inference.unification.unif"))
 223     in
 224       equiv FoSubst.id_subst s t
 225 ;;
 226
 227 let relocate maxvar varlist subst =
 228     List.fold_right
 229       (fun i (maxvar, varlist, s) ->
 230          maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
 231       varlist (maxvar+1, [], subst)
 232   ;;
 233
 234   let are_invertible l r =
 235     let varlist = Terms.vars_of_term l in
 236     let maxvar = List.fold_left max 0 varlist in
 237     let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
 238     let l = FoSubst.apply_subst subst l in
 239       try (ignore(alpha_eq l r);true) with
 240           UnificationFailure _ -> false
 241
 242   let compute_clause_weight = compute_clause_weight;;
 243
 244   (* Riazanov: p. 40, relation >_n *)
 245   let nonrec_kbo t1 t2 =
 246     let w1 = weight_of_term t1 in
 247     let w2 = weight_of_term t2 in
 248     match compare_weights w1 w2 with
 249     | XLE ->  (* this is .> *)
 250         if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
 251     | XGE ->
 252         if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
 253     | XEQ -> let res = aux_ordering B.compare t1 t2 in
 254         if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
 255         else res
 256     | res -> res
 257   ;;
 258
 259   let compare_terms = compare_terms nonrec_kbo;;
 260
 261   let profiler = HExtlib.profile ~enable:true "compare_terms(nrkbo)";;
 262   let compare_terms x y =
 263     profiler.HExtlib.profile (compare_terms x) y
 264   ;;
 265
 266 end
 267
 268 module KBO (B : Terms.Blob) = struct
 269   let name = "kbo"
 270   include B
 271
 272   module Pp = Pp.Pp(B)
 273
 274   let eq_foterm = eq_foterm B.eq;;
 275
 276   let compute_clause_weight = compute_clause_weight;;
 277   let compute_goal_weight = compute_goal_weight;;
 278
 279   (* Riazanov: p. 38, relation > *)
 280   let rec kbo t1 t2 =
 281     let aux = aux_ordering B.compare ~head_only:true in
 282     let rec cmp t1 t2 =
 283       match t1, t2 with
 284       | [], [] -> XEQ
 285       | _, [] -> XGT
 286       | [], _ -> XLT
 287       | hd1::tl1, hd2::tl2 ->
 288           let o = kbo hd1 hd2 in
 289           if o = XEQ then cmp tl1 tl2
 290           else o
 291     in
 292     let w1 = weight_of_term t1 in
 293     let w2 = weight_of_term t2 in
 294     let comparison = compare_weights w1 w2 in
 295     match comparison with
 296     | XLE ->
 297         let r = aux t1 t2 in
 298         if r = XLT then XLT
 299         else if r = XEQ then (
 300           match t1, t2 with
 301           | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
 302               if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
 303           | _, _ -> assert false
 304         ) else XINCOMPARABLE
 305     | XGE ->
 306         let r = aux t1 t2 in
 307         if r = XGT then XGT
 308         else if r = XEQ then (
 309           match t1, t2 with
 310           | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
 311               if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
 312           | _, _ ->  assert false
 313         ) else XINCOMPARABLE
 314     | XEQ ->
 315         let r = aux t1 t2 in
 316         if r = XEQ then (
 317           match t1, t2 with
 318           | Terms.Var i, Terms.Var j when i=j -> XEQ
 319           | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
 320           | _, _ ->  XINCOMPARABLE
 321         ) else r
 322     | res -> res
 323   ;;
 324
 325   let compare_terms = compare_terms kbo;;
 326
 327   let profiler = HExtlib.profile ~enable:true "compare_terms(kbo)";;
 328   let compare_terms x y =
 329     profiler.HExtlib.profile (compare_terms x) y
 330   ;;
 331
 332 end
 333
 334 module LPO (B : Terms.Blob) = struct
 335   let name = "lpo"
 336   include B
 337
 338   module Pp = Pp.Pp(B)
 339
 340   let eq_foterm = eq_foterm B.eq;;
 341
 342   let compute_clause_weight = compute_clause_weight;;
 343   let compute_goal_weight = compute_goal_weight;;
 344
 345   let rec lpo s t =
 346     match s,t with
 347       | s, t when eq_foterm s t ->
 348           XEQ
 349       | Terms.Var _, Terms.Var _ ->
 350           XINCOMPARABLE
 351       | _, Terms.Var i ->
 352           if (List.mem i (Terms.vars_of_term s)) then XGT
 353           else XINCOMPARABLE
 354       | Terms.Var i,_ ->
 355           if (List.mem i (Terms.vars_of_term t)) then XLT
 356           else XINCOMPARABLE
 357       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
 358           let rec ge_subterm t ol = function
 359             | [] -> (false, ol)
 360             | x::tl ->
 361                 let res = lpo x t in
 362                 match res with
 363                   | XGT | XEQ -> (true,res::ol)
 364                   | o -> ge_subterm t (o::ol) tl
 365           in
 366           let (res, l_ol) = ge_subterm t [] tl1 in
 367             if res then XGT
 368             else let (res, r_ol) = ge_subterm s [] tl2 in
 369               if res then XLT
 370               else begin
 371                 let rec check_subterms t = function
 372                   | _,[] -> true
 373                   | o::ol,_::tl ->
 374                       if o = XLT then check_subterms t (ol,tl)
 375                       else false
 376                   | [], x::tl ->
 377                       if lpo x t = XLT then check_subterms t ([],tl)
 378                       else false
 379                 in
 380                 match aux_ordering B.compare hd1 hd2 with
 381                   | XGT -> if check_subterms s (r_ol,tl2) then XGT
 382                     else XINCOMPARABLE
 383                   | XLT -> if check_subterms t (l_ol,tl1) then XLT
 384                     else XINCOMPARABLE
 385                   | XEQ ->
 386                       let lex = List.fold_left2
 387                         (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
 388                         XEQ tl1 tl2
 389                       in
 390                  (match lex with
 391                     | XGT ->
 392                         if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
 393                       else XINCOMPARABLE
 394                     | XLT ->
 395                         if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
 396                       else XINCOMPARABLE
 397                     | o -> o)
 398               | XINCOMPARABLE -> XINCOMPARABLE
 399               | _ -> assert false
 400           end
 401       | _,_ -> aux_ordering B.compare s t
 402
 403   ;;
 404
 405   let compare_terms = compare_terms lpo;;
 406
 407   let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;
 408   let compare_terms x y =
 409     profiler.HExtlib.profile (compare_terms x) y
 410   ;;
 411
 412 end
 413