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