]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/orderings.ml
commitcompleted: some files were missing :(
[helm.git] / 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   (*CSC: beware! Imperative cache! *)
367   let cache = Hashtbl.create 101
368
369   let rec lpo_le s t = 
370     eq_foterm s t || lpo_lt s t 
371   
372   and lpo_lt s t =
373     try Hashtbl.find cache (s,t)
374     with
375     Not_found -> let res =
376     match s,t with
377       | _, Terms.Var _ -> false
378       | Terms.Var i,_ ->
379           if (List.mem i (Terms.vars_of_term t)) then true
380           else false
381       | Terms.Leaf a, Terms.Leaf b -> B.compare a b < 0
382       | Terms.Leaf _, Terms.Node _  -> true (* we assume unary constants 
383                             are smaller than constants with higher arity *)
384       | Terms.Node _, Terms.Leaf _ -> false
385       | Terms.Node [],_
386       | _,Terms.Node [] -> assert false
387       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
388           if List.exists (lpo_le s) tl2 then true
389           else
390           begin 
391             match aux_ordering B.compare hd1 hd2 with
392             | XINCOMPARABLE 
393             | XGT -> false
394             | XLT -> List.for_all (fun x -> lpo_lt x t) tl1
395             | XEQ -> 
396                 let rec compare_args l1 l2 =
397                 match l1,l2 with
398                 | [],_ 
399                 | _,[] -> false
400                 | a1::tl1,a2::tl2 -> 
401                     if eq_foterm a1 a2 then compare_args tl1 tl2
402                     else if lpo_lt a1 a2 then List.for_all (fun x -> lpo_lt x t) tl1
403                     else false
404                 in 
405                 compare_args tl1 tl2
406             | _ -> assert false
407            end
408    in
409     Hashtbl.add cache (s,t) res; res
410   ;;
411
412   let lpo s t =
413     let res =
414     if eq_foterm s t then XEQ
415     else if lpo_lt s t then XLT
416     else if lpo_lt t s then XGT
417     else XINCOMPARABLE
418     in
419      Hashtbl.clear cache; res
420   ;;
421     
422
423   let compare_terms = compare_terms lpo;;
424
425   let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;
426   let compare_terms x y =
427     profiler.HExtlib.profile (compare_terms x) y
428   ;;
429
430 end
431