From ea8676df3c47428157d0d544ec63c320ffa204be Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jul 2009 08:25:41 +0000 Subject: [PATCH] activate kbo, not lpo --- .../components/ng_paramodulation/orderings.ml | 177 +++++++++--------- 1 file changed, 89 insertions(+), 88 deletions(-) diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 2e1d3c4f6..6880f6d18 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -83,9 +83,9 @@ let compute_goal_weight (_,l, _, _) = | Terms.Equation (l,r,_,_) -> let wl, ml = weight_of_term l in let wr, mr = weight_of_term r in - let wl = weight_of_polynomial wl ml in - let wr = weight_of_polynomial wr mr in - - (abs (wl-wr)) + let wl = weight_of_polynomial wl ml in + let wr = weight_of_polynomial wr mr in + - (abs (wl-wr)) ;; (* Riazanov: 3.1.5 pag 38 *) @@ -97,36 +97,36 @@ let compute_goal_weight (_,l, _, _) = let compare_weights (h1, w1) (h2, w2) = 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 + | ((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 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 + if hdiff < 0 then XLT + else if hdiff > 0 then XGT else XEQ in aux (h1-h2) (false,false) 0 w1 w2 @@ -140,7 +140,7 @@ let compute_goal_weight (_,l, _, _) = * If we give back XEQ, no inference rule * * will be applied on this equality *) | Terms.Var i, Terms.Var j when i = j -> - XEQ + XEQ (* 1. *) | Terms.Var _, _ | _, Terms.Var _ -> XINCOMPARABLE @@ -225,61 +225,61 @@ let compute_goal_weight (_,l, _, _) = let rec lpo s t = match s,t with | s, t when s = t -> - XEQ + XEQ | Terms.Var _, Terms.Var _ -> - XINCOMPARABLE + XINCOMPARABLE | _, Terms.Var i -> - if (List.mem i (Terms.vars_of_term s)) then XGT - else XINCOMPARABLE + if (List.mem i (Terms.vars_of_term s)) then XGT + else XINCOMPARABLE | Terms.Var i,_ -> - if (List.mem i (Terms.vars_of_term t)) then XLT - else XINCOMPARABLE + if (List.mem i (Terms.vars_of_term t)) then XLT + else XINCOMPARABLE | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> - let rec ge_subterm t ol = function - | [] -> (false, ol) - | x::tl -> - let res = lpo x t in - match res with - | XGT | XEQ -> (true,res::ol) - | o -> ge_subterm t (o::ol) tl - in - let (res, l_ol) = ge_subterm t [] tl1 in - if res then XGT - else let (res, r_ol) = ge_subterm s [] tl2 in - if res then XLT - else begin - let rec check_subterms t = function - | _,[] -> true - | o::ol,_::tl -> - if o = XLT then check_subterms t (ol,tl) - else false - | [], x::tl -> - if lpo x t = XLT then check_subterms t ([],tl) - else false - in - match aux_ordering hd1 hd2 with - | XGT -> if check_subterms s (r_ol,tl2) then XGT - else XINCOMPARABLE - | XLT -> if check_subterms t (l_ol,tl1) then XLT - else XINCOMPARABLE - | XEQ -> - let lex = List.fold_left2 - (fun acc si ti -> if acc = XEQ then lpo si ti else acc) - XEQ tl1 tl2 - in - (match lex with - | XGT -> - if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT - else XINCOMPARABLE - | XLT -> - if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT - else XINCOMPARABLE - | o -> o) - | XINCOMPARABLE -> XINCOMPARABLE - | _ -> assert false - end + let rec ge_subterm t ol = function + | [] -> (false, ol) + | x::tl -> + let res = lpo x t in + match res with + | XGT | XEQ -> (true,res::ol) + | o -> ge_subterm t (o::ol) tl + in + let (res, l_ol) = ge_subterm t [] tl1 in + if res then XGT + else let (res, r_ol) = ge_subterm s [] tl2 in + if res then XLT + else begin + let rec check_subterms t = function + | _,[] -> true + | o::ol,_::tl -> + if o = XLT then check_subterms t (ol,tl) + else false + | [], x::tl -> + if lpo x t = XLT then check_subterms t ([],tl) + else false + in + match aux_ordering hd1 hd2 with + | XGT -> if check_subterms s (r_ol,tl2) then XGT + else XINCOMPARABLE + | XLT -> if check_subterms t (l_ol,tl1) then XLT + else XINCOMPARABLE + | XEQ -> + let lex = List.fold_left2 + (fun acc si ti -> if acc = XEQ then lpo si ti else acc) + XEQ tl1 tl2 + in + (match lex with + | XGT -> + if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT + else XINCOMPARABLE + | XLT -> + if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT + else XINCOMPARABLE + | o -> o) + | XINCOMPARABLE -> XINCOMPARABLE + | _ -> assert false + end | _,_ -> aux_ordering s t - + ;; let rec lpo_old t1 t2 = @@ -345,12 +345,13 @@ let rec lpo_old t1 t2 = ;; let compare_terms x y = - match lpo x y with - | XINCOMPARABLE -> Terms.Incomparable - | XGT -> Terms.Gt - | XLT -> Terms.Lt - | XEQ -> Terms.Eq - | _ -> assert false + 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 ;; end -- 2.39.2