From 1001308d4ecc7dffa20f5f0fe479c77f8cad9b8e Mon Sep 17 00:00:00 2001 From: denes Date: Tue, 9 Jun 2009 13:31:02 +0000 Subject: [PATCH] Optimized weigths comparison, removed normalization --- .../components/ng_paramodulation/orderings.ml | 121 ++++++------------ 1 file changed, 41 insertions(+), 80 deletions(-) diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 66188c4d8..7c8a80995 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -44,9 +44,9 @@ module Orderings (B : Terms.Blob) = struct in let compare w1 w2 = match w1, w2 with - | (m1, _), (m2, _) -> m2 - m1 + | (m1, _), (m2, _) -> m1 - m2 in - (w, List.sort compare l) (* from the biggest meta to the smallest (0) *) + (w, List.sort compare l) (* from the smallest meta to the bigest *) ;; let compute_unit_clause_weight = @@ -69,85 +69,48 @@ module Orderings (B : Terms.Blob) = struct weight_of_polynomial (wl+wr) (ml@mr) ;; - (* returns a "normalized" version of the polynomial weight wl (with type - * weight list), i.e. a list sorted ascending by meta number, - * from 0 to maxmeta. wl must be sorted descending by meta number. Example: - * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> - * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) - let normalize_weight maxmeta (cw, wl) = - let rec aux = function - | 0 -> [] - | m -> (m, 0)::(aux (m-1)) - in - let tmpl = aux maxmeta in - let wl = - List.sort - (fun (m, _) (n, _) -> Pervasives.compare m n) - (List.fold_left - (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl) - in - (cw, wl) - ;; - - - let normalize_weights (cw1, wl1) (cw2, wl2) = - let rec aux wl1 wl2 = - match wl1, wl2 with - | [], [] -> [], [] - | (m, w)::tl1, (n, w')::tl2 when m = n -> - let res1, res2 = aux tl1 tl2 in - (m, w)::res1, (n, w')::res2 - | (m, w)::tl1, ((n, w')::_ as wl2) when m < n -> - let res1, res2 = aux tl1 wl2 in - (m, w)::res1, (m, 0)::res2 - | ((m, w)::_ as wl1), (n, w')::tl2 when m > n -> - let res1, res2 = aux wl1 tl2 in - (n, 0)::res1, (n, w')::res2 - | [], (n, w)::tl2 -> - let res1, res2 = aux [] tl2 in - (n, 0)::res1, (n, w)::res2 - | (m, w)::tl1, [] -> - let res1, res2 = aux tl1 [] in - (m, w)::res1, (m, 0)::res2 - | _, _ -> assert false - in - let cmp (m, _) (n, _) = compare m n in - let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in - (cw1, wl1), (cw2, wl2) - ;; - (* Riazanov: 3.1.5 pag 38 *) - (* TODO: optimize early detection of XINCOMPARABLE case *) +(* Compare weights normalized in a new way : + * Variables should be sorted from the lowest index to the highest + * Variables which do not occur in the term should not be present + * in the normalized polynomial + *) let compare_weights (h1, w1) (h2, w2) = - let res, diffs = - try - List.fold_left2 - (fun ((lt, eq, gt), diffs) w1 w2 -> - match w1, w2 with - | (meta1, w1), (meta2, w2) when meta1 = meta2 -> - let diffs = (w1 - w2) + diffs in - let r = compare w1 w2 in - if r < 0 then (lt+1, eq, gt), diffs - else if r = 0 then (lt, eq+1, gt), diffs - else (lt, eq, gt+1), diffs - | _ -> assert false) - ((0, 0, 0), 0) w1 w2 - with Invalid_argument _ -> assert false + let rec aux hdiff (lt, gt) diffs w1 w2 = + match w1, w2 with + | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) -> + if var1 = var2 then + let diffs = (w1 - w2) + diffs in + let r = compare w1 w2 in + let lt = lt or (r < 0) in + let gt = gt or (r > 0) in + if lt && gt then XINCOMPARABLE else + aux hdiff (lt, gt) diffs tl1 tl2 + else if var1 < var2 then + if lt then XINCOMPARABLE else + aux hdiff (false,true) (diffs+w1) tl1 l2 + else + if gt then XINCOMPARABLE else + aux hdiff (true,false) (diffs-w2) l1 tl2 + | [], (_,w2)::tl2 -> + if gt then XINCOMPARABLE else + aux hdiff (true,false) (diffs-w2) [] tl2 + | (_,w1)::tl1, [] -> + if lt then XINCOMPARABLE else + aux hdiff (false,true) (diffs+w1) tl1 [] + | [], [] -> + if lt then + if hdiff <= 0 then XLT + else if (- diffs) >= hdiff then XLE else XINCOMPARABLE + else if gt then + if hdiff >= 0 then XGT + else if diffs >= (- hdiff) then XGE else XINCOMPARABLE + else + if hdiff < 0 then XLT + else if hdiff > 0 then XGT + else XEQ in - let hdiff = h1 - h2 in - match res with - | (0, _, 0) -> - if hdiff < 0 then XLT - else if hdiff > 0 then XGT - else XEQ - | (m, _, 0) -> - if hdiff <= 0 then XLT - else if (- diffs) >= hdiff then XLE else XINCOMPARABLE - | (0, _, m) -> - if hdiff >= 0 then XGT - else if diffs >= (- hdiff) then XGE else XINCOMPARABLE - | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE - | _ -> assert false + aux (h1-h2) (false,false) 0 w1 w2 ;; (* Riazanov: p. 40, relation >>> @@ -181,7 +144,6 @@ module Orderings (B : Terms.Blob) = struct let nonrec_kbo t1 t2 = let w1 = weight_of_term t1 in let w2 = weight_of_term t2 in - let w1, w2 = normalize_weights w1 w2 in match compare_weights w1 w2 with | XLE -> (* this is .> *) if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE @@ -206,7 +168,6 @@ module Orderings (B : Terms.Blob) = struct in let w1 = weight_of_term t1 in let w2 = weight_of_term t2 in - let w1, w2 = normalize_weights w1 w2 in let comparison = compare_weights w1 w2 in match comparison with | XLE -> -- 2.39.2