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 (* (weight of constants, [(meta, weight_of_meta)]) *)
15 type weight = int * (int * int) list;;
17 let string_of_weight (cw, mw) =
20 (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
22 Printf.sprintf "[%d; %s]" cw s
25 let weight_of_term term =
26 let vars_dict = Hashtbl.create 5 in
27 let rec aux = function
30 let oldw = Hashtbl.find vars_dict i in
31 Hashtbl.replace vars_dict i (oldw+1)
33 Hashtbl.add vars_dict i 1);
36 | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
40 Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
44 | (m1, _), (m2, _) -> m2 - m1
46 (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
49 let compute_clause_weight = assert false (*
53 let w, m = (weight_of_term
54 ~consider_metas:true ~count_metas_occurrences:false right) in
55 w + (factor * (List.length m)) ;
56 | Terms.Le -> assert false
58 let w, m = (weight_of_term
59 ~consider_metas:true ~count_metas_occurrences:false left) in
60 w + (factor * (List.length m)) ;
61 | Terms.Ge -> assert false
63 | Terms.Incomparable ->
64 let w1, m1 = (weight_of_term
65 ~consider_metas:true ~count_metas_occurrences:false right) in
66 let w2, m2 = (weight_of_term
67 ~consider_metas:true ~count_metas_occurrences:false left) in
68 w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
72 (* returns a "normalized" version of the polynomial weight wl (with type
73 * weight list), i.e. a list sorted ascending by meta number,
74 * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
75 * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
76 * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
77 let normalize_weight maxmeta (cw, wl) =
78 let rec aux = function
80 | m -> (m, 0)::(aux (m-1))
82 let tmpl = aux maxmeta in
85 (fun (m, _) (n, _) -> Pervasives.compare m n)
87 (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
93 let normalize_weights (cw1, wl1) (cw2, wl2) =
97 | (m, w)::tl1, (n, w')::tl2 when m = n ->
98 let res1, res2 = aux tl1 tl2 in
99 (m, w)::res1, (n, w')::res2
100 | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
101 let res1, res2 = aux tl1 wl2 in
102 (m, w)::res1, (m, 0)::res2
103 | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
104 let res1, res2 = aux wl1 tl2 in
105 (n, 0)::res1, (n, w')::res2
107 let res1, res2 = aux [] tl2 in
108 (n, 0)::res1, (n, w)::res2
110 let res1, res2 = aux tl1 [] in
111 (m, w)::res1, (m, 0)::res2
112 | _, _ -> assert false
114 let cmp (m, _) (n, _) = compare m n in
115 let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
116 (cw1, wl1), (cw2, wl2)
119 (* Riazanov: 3.1.5 pag 38 *)
120 (* TODO: optimize early detection of Terms.Incomparable case *)
121 let compare_weights (h1, w1) (h2, w2) =
125 (fun ((lt, eq, gt), diffs) w1 w2 ->
127 | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
128 let diffs = (w1 - w2) + diffs in
129 let r = compare w1 w2 in
130 if r < 0 then (lt+1, eq, gt), diffs
131 else if r = 0 then (lt, eq+1, gt), diffs
132 else (lt, eq, gt+1), diffs
135 with Invalid_argument _ -> assert false
137 let hdiff = h1 - h2 in
140 if hdiff < 0 then Terms.Lt
141 else if hdiff > 0 then Terms.Gt
144 if hdiff <= 0 then Terms.Lt
145 else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
147 if hdiff >= 0 then Terms.Gt
148 else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
149 | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
154 let rec aux_ordering t1 t2 =
157 | _, Terms.Var _ -> Terms.Incomparable
159 | Terms.Leaf a1, Terms.Leaf a2 ->
160 let cmp = Pervasives.compare a1 a2 in
161 if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
163 | Terms.Leaf _, Terms.Node _ -> Terms.Lt
164 | Terms.Node _, Terms.Leaf _ -> Terms.Gt
166 | Terms.Node l1, Terms.Node l2 ->
172 | hd1::tl1, hd2::tl2 ->
173 let o = aux_ordering hd1 hd2 in
174 if o = Terms.Eq then cmp tl1 tl2
180 let nonrec_kbo t1 t2 =
181 let w1 = weight_of_term t1 in
182 let w2 = weight_of_term t2 in
183 let w1, w2 = normalize_weights w1 w2 in
184 match compare_weights w1 w2 with
185 | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
186 | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
187 | Terms.Eq -> aux_ordering t1 t2
193 let aux = aux_ordering ~recursion:false in
194 let w1 = weight_of_term t1
195 and w2 = weight_of_term t2 in
201 | hd1::tl1, hd2::tl2 ->
205 if o = Terms.Eq then cmp tl1 tl2
208 let w1, w2 = normalize_weights w1 w2 in
209 let comparison = compare_weights w1 w2 in
210 match comparison with
213 if r = Terms.Lt then Terms.Lt
214 else if r = Terms.Eq then (
216 | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
217 if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
218 | _, _ -> Terms.Incomparable
219 ) else Terms.Incomparable
222 if r = Terms.Gt then Terms.Gt
223 else if r = Terms.Eq then (
225 | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
226 if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
227 | _, _ -> Terms.Incomparable
228 ) else Terms.Incomparable
231 if r = Terms.Eq then (
233 | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
235 | _, _ -> Terms.Incomparable
241 let compare_terms = nonrec_kbo;;