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