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 rec eq_foterm x y =
25 | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
26 | Terms.Var i, Terms.Var j -> i = j
27 | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2
31 let string_of_weight (cw, mw) =
34 (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
36 Printf.sprintf "[%d; %s]" cw s
39 let weight_of_term term =
40 let vars_dict = Hashtbl.create 5 in
41 let rec aux = function
44 let oldw = Hashtbl.find vars_dict i in
45 Hashtbl.replace vars_dict i (oldw+1)
47 Hashtbl.add vars_dict i 1);
50 | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
54 Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
58 | (m1, _), (m2, _) -> m1 - m2
60 (w, List.sort compare l) (* from the smallest meta to the bigest *)
63 let compute_unit_clause_weight (_,l, _, _) =
64 let weight_of_polynomial w m =
66 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
69 | Terms.Predicate t ->
70 let w, m = weight_of_term t in
71 weight_of_polynomial w m
72 | Terms.Equation (_,x,_,Terms.Lt)
73 | Terms.Equation (x,_,_,Terms.Gt) ->
74 let w, m = weight_of_term x in
75 weight_of_polynomial w m
76 | Terms.Equation (l,r,_,Terms.Eq)
77 | Terms.Equation (l,r,_,Terms.Incomparable) ->
78 let wl, ml = weight_of_term l in
79 let wr, mr = weight_of_term r in
80 weight_of_polynomial (wl+wr) (ml@mr)
83 let compute_goal_weight (_,l, _, _) =
84 let weight_of_polynomial w m =
86 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
89 | Terms.Predicate t ->
90 let w, m = weight_of_term t in
91 weight_of_polynomial w m
92 | Terms.Equation (l,r,_,_) ->
93 let wl, ml = weight_of_term l in
94 let wr, mr = weight_of_term r in
95 let wl = weight_of_polynomial wl ml in
96 let wr = weight_of_polynomial wr mr in
100 (* Riazanov: 3.1.5 pag 38 *)
101 (* Compare weights normalized in a new way :
102 * Variables should be sorted from the lowest index to the highest
103 * Variables which do not occur in the term should not be present
104 * in the normalized polynomial
106 let compare_weights (h1, w1) (h2, w2) =
107 let rec aux hdiff (lt, gt) diffs w1 w2 =
109 | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
111 let diffs = (w1 - w2) + diffs in
112 let r = compare w1 w2 in
113 let lt = lt or (r < 0) in
114 let gt = gt or (r > 0) in
115 if lt && gt then XINCOMPARABLE else
116 aux hdiff (lt, gt) diffs tl1 tl2
117 else if var1 < var2 then
118 if lt then XINCOMPARABLE else
119 aux hdiff (false,true) (diffs+w1) tl1 l2
121 if gt then XINCOMPARABLE else
122 aux hdiff (true,false) (diffs-w2) l1 tl2
124 if gt then XINCOMPARABLE else
125 aux hdiff (true,false) (diffs-w2) [] tl2
127 if lt then XINCOMPARABLE else
128 aux hdiff (false,true) (diffs+w1) tl1 []
131 if hdiff <= 0 then XLT
132 else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
134 if hdiff >= 0 then XGT
135 else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
137 if hdiff < 0 then XLT
138 else if hdiff > 0 then XGT
141 aux (h1-h2) (false,false) 0 w1 w2
144 (* Riazanov: p. 40, relation >>>
145 * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
146 let rec aux_ordering ?(head_only=false) t1 t2 =
148 (* We want to discard any identity equality. *
149 * If we give back XEQ, no inference rule *
150 * will be applied on this equality *)
151 | Terms.Var i, Terms.Var j when i = j ->
155 | _, Terms.Var _ -> XINCOMPARABLE
157 | Terms.Leaf a1, Terms.Leaf a2 ->
158 let cmp = B.compare a1 a2 in
159 if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
160 | Terms.Leaf _, Terms.Node _ -> XLT
161 | Terms.Node _, Terms.Leaf _ -> XGT
163 | Terms.Node l1, Terms.Node l2 ->
169 | hd1::tl1, hd2::tl2 ->
170 let o = aux_ordering ~head_only hd1 hd2 in
171 if o = XEQ && not head_only then cmp tl1 tl2 else o
176 (* Riazanov: p. 40, relation >_n *)
177 let nonrec_kbo t1 t2 =
178 let w1 = weight_of_term t1 in
179 let w2 = weight_of_term t2 in
180 match compare_weights w1 w2 with
181 | XLE -> (* this is .> *)
182 if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
184 if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
185 | XEQ -> aux_ordering t1 t2
189 (* Riazanov: p. 38, relation > *)
191 let aux = aux_ordering ~head_only:true in
197 | hd1::tl1, hd2::tl2 ->
198 let o = kbo hd1 hd2 in
199 if o = XEQ then cmp tl1 tl2
202 let w1 = weight_of_term t1 in
203 let w2 = weight_of_term t2 in
204 let comparison = compare_weights w1 w2 in
205 match comparison with
209 else if r = XEQ then (
211 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
212 if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
213 | _, _ -> assert false
218 else if r = XEQ then (
220 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
221 if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
222 | _, _ -> assert false
228 | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
229 | _, _ -> XINCOMPARABLE
236 | s, t when eq_foterm s t ->
238 | Terms.Var _, Terms.Var _ ->
241 if (List.mem i (Terms.vars_of_term s)) then XGT
244 if (List.mem i (Terms.vars_of_term t)) then XLT
246 | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
247 let rec ge_subterm t ol = function
252 | XGT | XEQ -> (true,res::ol)
253 | o -> ge_subterm t (o::ol) tl
255 let (res, l_ol) = ge_subterm t [] tl1 in
257 else let (res, r_ol) = ge_subterm s [] tl2 in
260 let rec check_subterms t = function
263 if o = XLT then check_subterms t (ol,tl)
266 if lpo x t = XLT then check_subterms t ([],tl)
269 match aux_ordering hd1 hd2 with
270 | XGT -> if check_subterms s (r_ol,tl2) then XGT
272 | XLT -> if check_subterms t (l_ol,tl1) then XLT
275 let lex = List.fold_left2
276 (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
281 if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
284 if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
287 | XINCOMPARABLE -> XINCOMPARABLE
290 | _,_ -> aux_ordering s t
294 let compare_terms x y =
295 match nonrec_kbo x y with
296 | XINCOMPARABLE -> Terms.Incomparable
303 let profiler = HExtlib.profile ~enable:true "compare_terms";;
304 let compare_terms x y =
305 profiler.HExtlib.profile (compare_terms x) y