]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/orderings.ml
....
[helm.git] / 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 compare_terms x y = 
224     match nonrec_kbo x y with
225     | XINCOMPARABLE -> Terms.Incomparable
226     | XGT -> Terms.Gt
227     | XLT -> Terms.Lt
228     | XEQ -> Terms.Eq
229     | _ -> assert false
230   ;; 
231
232 end