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
18 type weight = int * (int * int) list;;
20 let string_of_weight (cw, mw) =
23 (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
25 Printf.sprintf "[%d; %s]" cw s
28 let weight_of_term term =
29 let vars_dict = Hashtbl.create 5 in
30 let rec aux = function
33 let oldw = Hashtbl.find vars_dict i in
34 Hashtbl.replace vars_dict i (oldw+1)
36 Hashtbl.add vars_dict i 1);
39 | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
43 Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
47 | (m1, _), (m2, _) -> m2 - m1
49 (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
52 let compute_unit_clause_weight =
53 let weight_of_polynomial w m =
55 w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
58 | Terms.Predicate t ->
59 let w, m = weight_of_term t in
60 weight_of_polynomial w m
61 | Terms.Equation (_,x,_,Terms.Lt)
62 | Terms.Equation (x,_,_,Terms.Gt) ->
63 let w, m = weight_of_term x in
64 weight_of_polynomial w m
65 | Terms.Equation (l,r,_,Terms.Eq)
66 | Terms.Equation (l,r,_,Terms.Incomparable) ->
67 let wl, ml = weight_of_term l in
68 let wr, mr = weight_of_term r in
69 weight_of_polynomial (wl+wr) (ml@mr)
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 XINCOMPARABLE 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 XLT
141 else if hdiff > 0 then XGT
144 if hdiff <= 0 then XLT
145 else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
147 if hdiff >= 0 then XGT
148 else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
149 | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE
153 (* Riazanov: p. 40, relation >>>
154 * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
155 let rec aux_ordering ?(head_only=false) t1 t2 =
159 | _, Terms.Var _ -> XINCOMPARABLE
161 | Terms.Leaf a1, Terms.Leaf a2 ->
162 let cmp = B.compare a1 a2 in
163 if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
164 | Terms.Leaf _, Terms.Node _ -> XLT
165 | Terms.Node _, Terms.Leaf _ -> XGT
167 | Terms.Node l1, Terms.Node l2 ->
173 | hd1::tl1, hd2::tl2 ->
174 let o = aux_ordering ~head_only hd1 hd2 in
175 if o = XEQ && not head_only then cmp tl1 tl2 else o
180 (* Riazanov: p. 40, relation >_n *)
181 let nonrec_kbo t1 t2 =
182 let w1 = weight_of_term t1 in
183 let w2 = weight_of_term t2 in
184 let w1, w2 = normalize_weights w1 w2 in
185 match compare_weights w1 w2 with
186 | XLE -> (* this is .> *)
187 if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
189 if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
190 | XEQ -> aux_ordering t1 t2
194 (* Riazanov: p. 38, relation > *)
196 let aux = aux_ordering ~head_only:true in
202 | hd1::tl1, hd2::tl2 ->
203 let o = kbo hd1 hd2 in
204 if o = XEQ then cmp tl1 tl2
207 let w1 = weight_of_term t1 in
208 let w2 = weight_of_term t2 in
209 let w1, w2 = normalize_weights w1 w2 in
210 let comparison = compare_weights w1 w2 in
211 match comparison with
215 else if r = XEQ then (
217 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
218 if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
219 | _, _ -> assert false
224 else if r = XEQ then (
226 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
227 if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
228 | _, _ -> assert false
234 | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
235 | _, _ -> XINCOMPARABLE
240 let compare_terms x y =
241 match nonrec_kbo x y with
242 | XINCOMPARABLE -> Terms.Incomparable