+
+ let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_goal_weight = compute_goal_weight;;
+
+ (* Riazanov: p. 40, relation >_n *)
+ let nonrec_kbo t1 t2 =
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ match compare_weights w1 w2 with
+ | XLE -> (* this is .> *)
+ if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
+ | XGE ->
+ if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
+ | XEQ -> let res = aux_ordering B.compare t1 t2 in
+ if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+ else res
+ | res -> res
+ ;;
+
+ let compare_terms = compare_terms nonrec_kbo;;
+
+ let profiler = HExtlib.profile ~enable:true "compare_terms(nrkbo)";;
+ let compare_terms x y =
+ profiler.HExtlib.profile (compare_terms x) y
+ ;;
+
+end
+
+module KBO (B : Terms.Blob) = struct
+ let name = "kbo"
+ include B
+
+ module Pp = Pp.Pp(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_goal_weight = compute_goal_weight;;
+
+ (* Riazanov: p. 38, relation > *)
+ let rec kbo t1 t2 =
+ let aux = aux_ordering B.compare ~head_only:true in
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> XEQ
+ | _, [] -> XGT
+ | [], _ -> XLT
+ | hd1::tl1, hd2::tl2 ->
+ let o = kbo hd1 hd2 in
+ if o = XEQ then cmp tl1 tl2
+ else o
+ in
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ let comparison = compare_weights w1 w2 in
+ match comparison with
+ | XLE ->
+ let r = aux t1 t2 in
+ if r = XLT then XLT
+ else if r = XEQ then (
+ match t1, t2 with
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
+ if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
+ | _, _ -> assert false
+ ) else XINCOMPARABLE
+ | XGE ->
+ let r = aux t1 t2 in
+ if r = XGT then XGT
+ else if r = XEQ then (
+ match t1, t2 with
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
+ if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
+ | _, _ -> assert false
+ ) else XINCOMPARABLE
+ | XEQ ->
+ let r = aux t1 t2 in
+ if r = XEQ then (
+ match t1, t2 with
+ | Terms.Var i, Terms.Var j when i=j -> XEQ
+ | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
+ | _, _ -> XINCOMPARABLE
+ ) else r
+ | res -> res
+ ;;
+
+ let compare_terms = compare_terms kbo;;
+
+ let profiler = HExtlib.profile ~enable:true "compare_terms(kbo)";;
+ let compare_terms x y =
+ profiler.HExtlib.profile (compare_terms x) y
+ ;;
+
+end
+
+module LPO (B : Terms.Blob) = struct
+ let name = "lpo"
+ include B
+
+ module Pp = Pp.Pp(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_goal_weight = compute_goal_weight;;
+
+ let rec lpo s t =
+ match s,t with
+ | s, t when eq_foterm s t ->
+ XEQ
+ | Terms.Var _, Terms.Var _ ->
+ XINCOMPARABLE
+ | _, Terms.Var i ->
+ 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
+ | 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 B.compare 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 B.compare s t
+
+ ;;
+
+ let compare_terms = compare_terms lpo;;
+
+ let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;
+ let compare_terms x y =
+ profiler.HExtlib.profile (compare_terms x) y
+ ;;
+
+end