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 | XINVERTIBLE
20 (* This order relation should be:
21 * - stable for instantiation
22 * - total on ground terms
26 t Terms.foterm -> t Terms.foterm -> Terms.comparison
28 val compute_unit_clause_weight : 't Terms.unit_clause -> int
30 val compute_goal_weight : 't Terms.unit_clause -> int
36 type weight = int * (int * int) list;;
38 let rec eq_foterm f x y =
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 -> List.for_all2 (eq_foterm f) l1 l2
47 let string_of_weight (cw, mw) =
50 (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
52 Printf.sprintf "[%d; %s]" cw s
55 let weight_of_term term =
56 let vars_dict = Hashtbl.create 5 in
57 let rec aux = function
60 let oldw = Hashtbl.find vars_dict i in
61 Hashtbl.replace vars_dict i (oldw+1)
63 Hashtbl.add vars_dict i 1);
66 | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
70 Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
74 | (m1, _), (m2, _) -> m1 - m2
76 (w, List.sort compare l) (* from the smallest meta to the bigest *)
79 let compute_unit_clause_weight (_,l, _, _) =
80 let weight_of_polynomial w m =
82 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
85 | Terms.Predicate t ->
86 let w, m = weight_of_term t in
87 weight_of_polynomial w m
88 | Terms.Equation (_,x,_,Terms.Lt)
89 | Terms.Equation (x,_,_,Terms.Gt) ->
90 let w, m = weight_of_term x in
91 weight_of_polynomial w m
92 | Terms.Equation (l,r,_,Terms.Eq)
93 | Terms.Equation (l,r,_,Terms.Incomparable)
94 | Terms.Equation (l,r,_,Terms.Invertible) ->
95 let wl, ml = weight_of_term l in
96 let wr, mr = weight_of_term r in
97 weight_of_polynomial (wl+wr) (ml@mr)
101 let compute_goal_weight (_,l, _, _) =
102 let weight_of_polynomial w m =
104 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
107 | Terms.Predicate t ->
108 let w, m = weight_of_term t in
109 weight_of_polynomial w m
110 | Terms.Equation (l,r,_,_) ->
111 let wl, ml = weight_of_term l in
112 let wr, mr = weight_of_term r in
113 let wl = weight_of_polynomial wl ml in
114 let wr = weight_of_polynomial wr mr in
118 let compute_goal_weight = compute_unit_clause_weight;;
120 (* Riazanov: 3.1.5 pag 38 *)
121 (* Compare weights normalized in a new way :
122 * Variables should be sorted from the lowest index to the highest
123 * Variables which do not occur in the term should not be present
124 * in the normalized polynomial
126 let compare_weights (h1, w1) (h2, w2) =
127 let rec aux hdiff (lt, gt) diffs w1 w2 =
129 | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
131 let diffs = (w1 - w2) + diffs in
132 let r = Pervasives.compare w1 w2 in
133 let lt = lt or (r < 0) in
134 let gt = gt or (r > 0) in
135 if lt && gt then XINCOMPARABLE else
136 aux hdiff (lt, gt) diffs tl1 tl2
137 else if var1 < var2 then
138 if lt then XINCOMPARABLE else
139 aux hdiff (false,true) (diffs+w1) tl1 l2
141 if gt then XINCOMPARABLE else
142 aux hdiff (true,false) (diffs-w2) l1 tl2
144 if gt then XINCOMPARABLE else
145 aux hdiff (true,false) (diffs-w2) [] tl2
147 if lt then XINCOMPARABLE else
148 aux hdiff (false,true) (diffs+w1) tl1 []
151 if hdiff <= 0 then XLT
152 else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
154 if hdiff >= 0 then XGT
155 else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
157 if hdiff < 0 then XLT
158 else if hdiff > 0 then XGT
161 aux (h1-h2) (false,false) 0 w1 w2
164 (* Riazanov: p. 40, relation >>>
165 * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
166 let rec aux_ordering b_compare ?(head_only=false) t1 t2 =
168 (* We want to discard any identity equality. *
169 * If we give back XEQ, no inference rule *
170 * will be applied on this equality *)
171 | Terms.Var i, Terms.Var j when i = j ->
175 | _, Terms.Var _ -> XINCOMPARABLE
177 | Terms.Leaf a1, Terms.Leaf a2 ->
178 let cmp = b_compare a1 a2 in
179 if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
180 | Terms.Leaf _, Terms.Node _ -> XLT
181 | Terms.Node _, Terms.Leaf _ -> XGT
183 | Terms.Node l1, Terms.Node l2 ->
187 | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
188 | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
189 | hd1::tl1, hd2::tl2 ->
190 let o = aux_ordering b_compare ~head_only hd1 hd2 in
191 if o = XEQ && not head_only then cmp tl1 tl2 else o
196 let compare_terms o x y =
198 | XINCOMPARABLE -> Terms.Incomparable
202 | XINVERTIBLE -> Terms.Invertible
206 module NRKBO (B : Terms.Blob) = struct
212 let eq_foterm = eq_foterm B.eq;;
214 exception UnificationFailure of string Lazy.t;;
217 (* DUPLICATE CODE FOR TESTS (see FoUnif) *)
219 let rec equiv subst s t =
220 let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
221 and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
225 | s, t when eq_foterm s t -> subst
226 | Terms.Var i, Terms.Var j
227 when (not (List.exists (fun (_,k) -> k=t) subst)) ->
228 let subst = FoSubst.build_subst i t subst in
230 | Terms.Node l1, Terms.Node l2 -> (
233 (fun subst' s t -> equiv subst' s t)
235 with Invalid_argument _ ->
236 raise (UnificationFailure (lazy "Inference.unification.unif"))
239 raise (UnificationFailure (lazy "Inference.unification.unif"))
241 equiv FoSubst.id_subst s t
244 let relocate maxvar varlist subst =
246 (fun i (maxvar, varlist, s) ->
247 maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
248 varlist (maxvar+1, [], subst)
251 let are_invertible l r =
252 let varlist = (Terms.vars_of_term l)@(Terms.vars_of_term r) in
253 let maxvar = List.fold_left max 0 varlist in
254 let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
255 let newl = FoSubst.apply_subst subst l in
256 let newr = FoSubst.apply_subst subst r in
257 try (let subst = alpha_eq l newr in eq_foterm newl (FoSubst.apply_subst subst r)) with
258 UnificationFailure _ -> false
261 let compute_unit_clause_weight = compute_unit_clause_weight;;
262 let compute_goal_weight = compute_goal_weight;;
264 (* Riazanov: p. 40, relation >_n *)
265 let nonrec_kbo t1 t2 =
266 let w1 = weight_of_term t1 in
267 let w2 = weight_of_term t2 in
268 match compare_weights w1 w2 with
269 | XLE -> (* this is .> *)
270 if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
272 if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
273 | XEQ -> let res = aux_ordering B.compare t1 t2 in
274 if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
279 let compare_terms = compare_terms nonrec_kbo;;
281 let profiler = HExtlib.profile ~enable:true "compare_terms(nrkbo)";;
282 let compare_terms x y =
283 profiler.HExtlib.profile (compare_terms x) y
288 module KBO (B : Terms.Blob) = struct
294 let eq_foterm = eq_foterm B.eq;;
296 let compute_unit_clause_weight = compute_unit_clause_weight;;
297 let compute_goal_weight = compute_goal_weight;;
299 (* Riazanov: p. 38, relation > *)
301 let aux = aux_ordering B.compare ~head_only:true in
307 | hd1::tl1, hd2::tl2 ->
308 let o = kbo hd1 hd2 in
309 if o = XEQ then cmp tl1 tl2
312 let w1 = weight_of_term t1 in
313 let w2 = weight_of_term t2 in
314 let comparison = compare_weights w1 w2 in
315 match comparison with
319 else if r = XEQ then (
321 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
322 if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
323 | _, _ -> assert false
328 else if r = XEQ then (
330 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
331 if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
332 | _, _ -> assert false
338 | Terms.Var i, Terms.Var j when i=j -> XEQ
339 | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
340 | _, _ -> XINCOMPARABLE
345 let compare_terms = compare_terms kbo;;
347 let profiler = HExtlib.profile ~enable:true "compare_terms(kbo)";;
348 let compare_terms x y =
349 profiler.HExtlib.profile (compare_terms x) y
354 module LPO (B : Terms.Blob) = struct
360 let eq_foterm = eq_foterm B.eq;;
362 let compute_unit_clause_weight = compute_unit_clause_weight;;
363 let compute_goal_weight = compute_goal_weight;;
367 | s, t when eq_foterm s t ->
369 | Terms.Var _, Terms.Var _ ->
372 if (List.mem i (Terms.vars_of_term s)) then XGT
375 if (List.mem i (Terms.vars_of_term t)) then XLT
377 | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
378 let rec ge_subterm t ol = function
383 | XGT | XEQ -> (true,res::ol)
384 | o -> ge_subterm t (o::ol) tl
386 let (res, l_ol) = ge_subterm t [] tl1 in
388 else let (res, r_ol) = ge_subterm s [] tl2 in
391 let rec check_subterms t = function
394 if o = XLT then check_subterms t (ol,tl)
397 if lpo x t = XLT then check_subterms t ([],tl)
400 match aux_ordering B.compare hd1 hd2 with
401 | XGT -> if check_subterms s (r_ol,tl2) then XGT
403 | XLT -> if check_subterms t (l_ol,tl1) then XLT
406 let lex = List.fold_left2
407 (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
412 if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
415 if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
418 | XINCOMPARABLE -> XINCOMPARABLE
421 | _,_ -> aux_ordering B.compare s t
425 let compare_terms = compare_terms lpo;;
427 let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;
428 let compare_terms x y =
429 profiler.HExtlib.profile (compare_terms x) y