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.
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_______________________________________________________________ *)
14 type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
16 module Orderings (B : Terms.Blob) = struct
20 type weight = int * (int * int) list;;
22 let string_of_weight (cw, mw) =
25 (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
27 Printf.sprintf "[%d; %s]" cw s
30 let weight_of_term term =
31 let vars_dict = Hashtbl.create 5 in
32 let rec aux = function
35 let oldw = Hashtbl.find vars_dict i in
36 Hashtbl.replace vars_dict i (oldw+1)
38 Hashtbl.add vars_dict i 1);
41 | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
45 Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
49 | (m1, _), (m2, _) -> m1 - m2
51 (w, List.sort compare l) (* from the smallest meta to the bigest *)
54 let compute_unit_clause_weight (_,l, _, _) =
55 let weight_of_polynomial w m =
57 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
60 | Terms.Predicate t ->
61 let w, m = weight_of_term t in
62 weight_of_polynomial w m
63 | Terms.Equation (_,x,_,Terms.Lt)
64 | Terms.Equation (x,_,_,Terms.Gt) ->
65 let w, m = weight_of_term x in
66 weight_of_polynomial w m
67 | Terms.Equation (l,r,_,Terms.Eq)
68 | Terms.Equation (l,r,_,Terms.Incomparable) ->
69 let wl, ml = weight_of_term l in
70 let wr, mr = weight_of_term r in
71 weight_of_polynomial (wl+wr) (ml@mr)
74 let compute_goal_weight (_,l, _, _) =
75 let weight_of_polynomial w m =
77 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
80 | Terms.Predicate t ->
81 let w, m = weight_of_term t in
82 weight_of_polynomial w m
83 | Terms.Equation (l,r,_,_) ->
84 let wl, ml = weight_of_term l in
85 let wr, mr = weight_of_term r in
86 let wl = weight_of_polynomial wl ml in
87 let wr = weight_of_polynomial wr mr in
91 (* Riazanov: 3.1.5 pag 38 *)
92 (* Compare weights normalized in a new way :
93 * Variables should be sorted from the lowest index to the highest
94 * Variables which do not occur in the term should not be present
95 * in the normalized polynomial
97 let compare_weights (h1, w1) (h2, w2) =
98 let rec aux hdiff (lt, gt) diffs w1 w2 =
100 | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
102 let diffs = (w1 - w2) + diffs in
103 let r = compare w1 w2 in
104 let lt = lt or (r < 0) in
105 let gt = gt or (r > 0) in
106 if lt && gt then XINCOMPARABLE else
107 aux hdiff (lt, gt) diffs tl1 tl2
108 else if var1 < var2 then
109 if lt then XINCOMPARABLE else
110 aux hdiff (false,true) (diffs+w1) tl1 l2
112 if gt then XINCOMPARABLE else
113 aux hdiff (true,false) (diffs-w2) l1 tl2
115 if gt then XINCOMPARABLE else
116 aux hdiff (true,false) (diffs-w2) [] tl2
118 if lt then XINCOMPARABLE else
119 aux hdiff (false,true) (diffs+w1) tl1 []
122 if hdiff <= 0 then XLT
123 else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
125 if hdiff >= 0 then XGT
126 else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
128 if hdiff < 0 then XLT
129 else if hdiff > 0 then XGT
132 aux (h1-h2) (false,false) 0 w1 w2
135 (* Riazanov: p. 40, relation >>>
136 * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
137 let rec aux_ordering ?(head_only=false) t1 t2 =
139 (* We want to discard any identity equality. *
140 * If we give back XEQ, no inference rule *
141 * will be applied on this equality *)
142 | Terms.Var i, Terms.Var j when i = j ->
146 | _, Terms.Var _ -> XINCOMPARABLE
148 | Terms.Leaf a1, Terms.Leaf a2 ->
149 let cmp = B.compare a1 a2 in
150 if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
151 | Terms.Leaf _, Terms.Node _ -> XLT
152 | Terms.Node _, Terms.Leaf _ -> XGT
154 | Terms.Node l1, Terms.Node l2 ->
160 | hd1::tl1, hd2::tl2 ->
161 let o = aux_ordering ~head_only hd1 hd2 in
162 if o = XEQ && not head_only then cmp tl1 tl2 else o
167 (* Riazanov: p. 40, relation >_n *)
168 let nonrec_kbo t1 t2 =
169 let w1 = weight_of_term t1 in
170 let w2 = weight_of_term t2 in
171 match compare_weights w1 w2 with
172 | XLE -> (* this is .> *)
173 if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
175 if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
176 | XEQ -> aux_ordering t1 t2
180 (* Riazanov: p. 38, relation > *)
182 let aux = aux_ordering ~head_only:true in
188 | hd1::tl1, hd2::tl2 ->
189 let o = kbo hd1 hd2 in
190 if o = XEQ then cmp tl1 tl2
193 let w1 = weight_of_term t1 in
194 let w2 = weight_of_term t2 in
195 let comparison = compare_weights w1 w2 in
196 match comparison with
200 else if r = XEQ then (
202 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
203 if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
204 | _, _ -> assert false
209 else if r = XEQ then (
211 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
212 if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
213 | _, _ -> assert false
219 | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
220 | _, _ -> XINCOMPARABLE
229 | Terms.Var _, Terms.Var _ ->
232 if (List.mem i (Terms.vars_of_term s)) then XGT
235 if (List.mem i (Terms.vars_of_term t)) then XLT
237 | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
238 let rec ge_subterm t ol = function
243 | XGT | XEQ -> (true,res::ol)
244 | o -> ge_subterm t (o::ol) tl
246 let (res, l_ol) = ge_subterm t [] tl1 in
248 else let (res, r_ol) = ge_subterm s [] tl2 in
251 let rec check_subterms t = function
254 if o = XLT then check_subterms t (ol,tl)
257 if lpo x t = XLT then check_subterms t ([],tl)
260 match aux_ordering hd1 hd2 with
261 | XGT -> if check_subterms s (r_ol,tl2) then XGT
263 | XLT -> if check_subterms t (l_ol,tl1) then XLT
266 let lex = List.fold_left2
267 (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
272 if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
275 if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
278 | XINCOMPARABLE -> XINCOMPARABLE
281 | _,_ -> aux_ordering s t
285 let rec lpo_old t1 t2 =
287 | t1, t2 when t1 = t2 -> XEQ
288 | t1, (Terms.Var m) ->
289 if List.mem m (Terms.vars_of_term t1) then XGT else XINCOMPARABLE
290 | (Terms.Var m), t2 ->
291 if List.mem m (Terms.vars_of_term t2) then XLT else XINCOMPARABLE
292 | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> (
296 match lpo_old t o with
300 let res1 = List.fold_left (f t2) false tl1 in
302 else let res2 = List.fold_left (f t1) false tl2 in
306 if res <> XINCOMPARABLE then
310 if not r then false else
311 match lpo_old o t with
315 match aux_ordering hd1 hd2 with
317 let res = List.fold_left (f t1) true tl2 in
321 let res = List.fold_left (f t2) true tl1 in
328 (fun r t1 t2 -> if r <> XEQ then r else lpo_old t1 t2)
330 with Invalid_argument _ ->
335 if List.fold_left (f t1) true tl2 then XGT
338 if List.fold_left (f t2) true tl1 then XLT
344 | t1, t2 -> aux_ordering t1 t2
347 let compare_terms x y =
348 match nonrec_kbo x y with
349 (* match lpo x y with *)
350 | XINCOMPARABLE -> Terms.Incomparable