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 =
  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     function
  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   (* Riazanov: 3.1.5 pag 38 *)
  73 (* Compare weights normalized in a new way :
  74  * Variables should be sorted from the lowest index to the highest
  75  * Variables which do not occur in the term should not be present
  76  * in the normalized polynomial
  77  *)
  78   let compare_weights (h1, w1) (h2, w2) =
  79     let rec aux hdiff (lt, gt) diffs w1 w2 =
  80       match w1, w2 with
  81         | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
  82             if var1 = var2 then
  83               let diffs = (w1 - w2) + diffs in
  84               let r = compare w1 w2 in
  85               let lt = lt or (r < 0) in
  86               let gt = gt or (r > 0) in
  87                 if lt && gt then XINCOMPARABLE else
  88                   aux hdiff (lt, gt) diffs tl1 tl2
  89             else if var1 < var2 then
  90               if lt then XINCOMPARABLE else
  91                 aux hdiff (false,true) (diffs+w1) tl1 l2
  92             else
  93               if gt then XINCOMPARABLE else
  94                 aux hdiff (true,false) (diffs-w2) l1 tl2
  95         | [], (_,w2)::tl2 ->
  96             if gt then XINCOMPARABLE else
  97               aux hdiff (true,false) (diffs-w2) [] tl2
  98         | (_,w1)::tl1, [] ->
  99             if lt then XINCOMPARABLE else
 100               aux hdiff (false,true) (diffs+w1) tl1 []
 101         | [], [] ->
 102             if lt then
 103               if hdiff <= 0 then XLT
 104               else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
 105             else if gt then
 106               if hdiff >= 0 then XGT
 107               else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
 108             else
 109               if hdiff < 0 then XLT
 110               else if hdiff > 0 then XGT
 111               else XEQ
 112     in
 113       aux (h1-h2) (false,false) 0 w1 w2
 114   ;;
 115
 116   (* Riazanov: p. 40, relation >>>
 117    * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
 118   let rec aux_ordering ?(head_only=false) t1 t2 =
 119     match t1, t2 with
 120     (* We want to discard any identity equality. *
 121      * If we give back XEQ, no inference rule    *
 122      * will be applied on this equality          *)
 123     | Terms.Var i, Terms.Var j when i = j ->
 124         XEQ
 125     (* 1. *)
 126     | Terms.Var _, _
 127     | _, Terms.Var _ -> XINCOMPARABLE
 128     (* 2.a *)
 129     | Terms.Leaf a1, Terms.Leaf a2 ->
 130         let cmp = B.compare a1 a2 in
 131         if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
 132     | Terms.Leaf _, Terms.Node _ -> XLT
 133     | Terms.Node _, Terms.Leaf _ -> XGT
 134     (* 2.b *)
 135     | Terms.Node l1, Terms.Node l2 ->
 136         let rec cmp t1 t2 =
 137           match t1, t2 with
 138           | [], [] -> XEQ
 139           | _, [] -> XGT
 140           | [], _ -> XLT
 141           | hd1::tl1, hd2::tl2 ->
 142               let o = aux_ordering ~head_only hd1 hd2 in
 143               if o = XEQ && not head_only then cmp tl1 tl2 else o
 144         in
 145         cmp l1 l2
 146   ;;
 147
 148   (* Riazanov: p. 40, relation >_n *)
 149   let nonrec_kbo t1 t2 =
 150     let w1 = weight_of_term t1 in
 151     let w2 = weight_of_term t2 in
 152     match compare_weights w1 w2 with
 153     | XLE ->  (* this is .> *)
 154         if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
 155     | XGE ->
 156         if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
 157     | XEQ -> aux_ordering t1 t2
 158     | res -> res
 159   ;;
 160
 161   (* Riazanov: p. 38, relation > *)
 162   let rec kbo t1 t2 =
 163     let aux = aux_ordering ~head_only:true in
 164     let rec cmp t1 t2 =
 165       match t1, t2 with
 166       | [], [] -> XEQ
 167       | _, [] -> XGT
 168       | [], _ -> XLT
 169       | hd1::tl1, hd2::tl2 ->
 170           let o = kbo hd1 hd2 in
 171           if o = XEQ then cmp tl1 tl2
 172           else o
 173     in
 174     let w1 = weight_of_term t1 in
 175     let w2 = weight_of_term t2 in
 176     let comparison = compare_weights w1 w2 in
 177     match comparison with
 178     | XLE ->
 179         let r = aux t1 t2 in
 180         if r = XLT then XLT
 181         else if r = XEQ then (
 182           match t1, t2 with
 183           | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
 184               if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
 185           | _, _ -> assert false
 186         ) else XINCOMPARABLE
 187     | XGE ->
 188         let r = aux t1 t2 in
 189         if r = XGT then XGT
 190         else if r = XEQ then (
 191           match t1, t2 with
 192           | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
 193               if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
 194           | _, _ ->  assert false
 195         ) else XINCOMPARABLE
 196     | XEQ ->
 197         let r = aux t1 t2 in
 198         if r = XEQ then (
 199           match t1, t2 with
 200           | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
 201           | _, _ ->  XINCOMPARABLE
 202         ) else r
 203     | res -> res
 204   ;;
 205
 206   let compare_terms x y =
 207     match nonrec_kbo x y with
 208     | XINCOMPARABLE -> Terms.Incomparable
 209     | XGT -> Terms.Gt
 210     | XLT -> Terms.Lt
 211     | XEQ -> Terms.Eq
 212     | _ -> assert false
 213   ;;
 214
 215 end