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