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, _) -> m1 - m2
49 (w, List.sort compare l) (* from the smallest meta to the bigest *)
52 let compute_unit_clause_weight (_,l, _, _) =
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 (* Riazanov: 3.1.5 pag 38 *)
73 (* Compare weights normalized in a new way :
74 * Variables should be sorted from the lowest index to the highest
75 * Variables which do not occur in the term should not be present
76 * in the normalized polynomial
78 let compare_weights (h1, w1) (h2, w2) =
79 let rec aux hdiff (lt, gt) diffs w1 w2 =
81 | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
83 let diffs = (w1 - w2) + diffs in
84 let r = compare w1 w2 in
85 let lt = lt or (r < 0) in
86 let gt = gt or (r > 0) in
87 if lt && gt then XINCOMPARABLE else
88 aux hdiff (lt, gt) diffs tl1 tl2
89 else if var1 < var2 then
90 if lt then XINCOMPARABLE else
91 aux hdiff (false,true) (diffs+w1) tl1 l2
93 if gt then XINCOMPARABLE else
94 aux hdiff (true,false) (diffs-w2) l1 tl2
96 if gt then XINCOMPARABLE else
97 aux hdiff (true,false) (diffs-w2) [] tl2
99 if lt then XINCOMPARABLE else
100 aux hdiff (false,true) (diffs+w1) tl1 []
103 if hdiff <= 0 then XLT
104 else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
106 if hdiff >= 0 then XGT
107 else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
109 if hdiff < 0 then XLT
110 else if hdiff > 0 then XGT
113 aux (h1-h2) (false,false) 0 w1 w2
116 (* Riazanov: p. 40, relation >>>
117 * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
118 let rec aux_ordering ?(head_only=false) t1 t2 =
120 (* We want to discard any identity equality. *
121 * If we give back XEQ, no inference rule *
122 * will be applied on this equality *)
123 | Terms.Var i, Terms.Var j when i = j ->
127 | _, Terms.Var _ -> XINCOMPARABLE
129 | Terms.Leaf a1, Terms.Leaf a2 ->
130 let cmp = B.compare a1 a2 in
131 if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
132 | Terms.Leaf _, Terms.Node _ -> XLT
133 | Terms.Node _, Terms.Leaf _ -> XGT
135 | Terms.Node l1, Terms.Node l2 ->
141 | hd1::tl1, hd2::tl2 ->
142 let o = aux_ordering ~head_only hd1 hd2 in
143 if o = XEQ && not head_only then cmp tl1 tl2 else o
148 (* Riazanov: p. 40, relation >_n *)
149 let nonrec_kbo t1 t2 =
150 let w1 = weight_of_term t1 in
151 let w2 = weight_of_term t2 in
152 match compare_weights w1 w2 with
153 | XLE -> (* this is .> *)
154 if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
156 if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
157 | XEQ -> aux_ordering t1 t2
161 (* Riazanov: p. 38, relation > *)
163 let aux = aux_ordering ~head_only:true in
169 | hd1::tl1, hd2::tl2 ->
170 let o = kbo hd1 hd2 in
171 if o = XEQ then cmp tl1 tl2
174 let w1 = weight_of_term t1 in
175 let w2 = weight_of_term t2 in
176 let comparison = compare_weights w1 w2 in
177 match comparison with
181 else if r = XEQ then (
183 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
184 if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
185 | _, _ -> assert false
190 else if r = XEQ then (
192 | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
193 if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
194 | _, _ -> assert false
200 | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
201 | _, _ -> XINCOMPARABLE
206 let compare_terms x y =
207 match nonrec_kbo x y with
208 | XINCOMPARABLE -> Terms.Incomparable