From 23f2fafa1bd91f271c0b5cf982b1cc59dc74cc35 Mon Sep 17 00:00:00 2001 From: denes Date: Thu, 9 Jul 2009 09:11:36 +0000 Subject: [PATCH] Cleaned a bit --- .../components/ng_paramodulation/orderings.ml | 81 ++++--------------- 1 file changed, 16 insertions(+), 65 deletions(-) diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 6880f6d18..28fbe1507 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -18,6 +18,15 @@ module Orderings (B : Terms.Blob) = struct module Pp = Pp.Pp(B) type weight = int * (int * int) list;; + +let rec eq_foterm x y = + x == y || + match x, y with + | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2 + | Terms.Var i, Terms.Var j -> i = j + | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2 + | _ -> false + ;; let string_of_weight (cw, mw) = let s = @@ -224,7 +233,7 @@ let compute_goal_weight (_,l, _, _) = let rec lpo s t = match s,t with - | s, t when s = t -> + | s, t when eq_foterm s t -> XEQ | Terms.Var _, Terms.Var _ -> XINCOMPARABLE @@ -282,76 +291,18 @@ let compute_goal_weight (_,l, _, _) = ;; -let rec lpo_old t1 t2 = - match t1, t2 with - | t1, t2 when t1 = t2 -> XEQ - | t1, (Terms.Var m) -> - if List.mem m (Terms.vars_of_term t1) then XGT else XINCOMPARABLE - | (Terms.Var m), t2 -> - if List.mem m (Terms.vars_of_term t2) then XLT else XINCOMPARABLE - | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> ( - let res = - let f o r t = - if r then true else - match lpo_old t o with - | XGT | XEQ -> true - | _ -> false - in - let res1 = List.fold_left (f t2) false tl1 in - if res1 then XGT - else let res2 = List.fold_left (f t1) false tl2 in - if res2 then XLT - else XINCOMPARABLE - in - if res <> XINCOMPARABLE then - res - else - let f o r t = - if not r then false else - match lpo_old o t with - | XGT -> true - | _ -> false - in - match aux_ordering hd1 hd2 with - | XGT -> - let res = List.fold_left (f t1) true tl2 in - if res then XGT - else XINCOMPARABLE - | XLT -> - let res = List.fold_left (f t2) true tl1 in - if res then XLT - else XINCOMPARABLE - | XEQ -> ( - let lex_res = - try - List.fold_left2 - (fun r t1 t2 -> if r <> XEQ then r else lpo_old t1 t2) - XEQ tl1 tl2 - with Invalid_argument _ -> - XINCOMPARABLE - in - match lex_res with - | XGT -> - if List.fold_left (f t1) true tl2 then XGT - else XINCOMPARABLE - | XLT -> - if List.fold_left (f t2) true tl1 then XLT - else XINCOMPARABLE - | _ -> XINCOMPARABLE - ) - | _ -> XINCOMPARABLE - ) - | t1, t2 -> aux_ordering t1 t2 -;; - let compare_terms x y = match nonrec_kbo x y with -(* match lpo x y with *) | XINCOMPARABLE -> Terms.Incomparable | XGT -> Terms.Gt | XLT -> Terms.Lt | XEQ -> Terms.Eq | _ -> assert false - ;; + ;; + + let profiler = HExtlib.profile ~enable:true "compare_terms";; + let compare_terms x y = + profiler.HExtlib.profile (compare_terms x) y + ;; end -- 2.39.2