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 =
| 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 *)
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
* 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
let rec cmp t1 t2 =
match t1, t2 with
| [], [] -> XEQ
- | _, [] -> XGT
- | [], _ -> XLT
+ | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
+ | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
| hd1::tl1, hd2::tl2 ->
let o = aux_ordering ~head_only hd1 hd2 in
if o = XEQ && not head_only then cmp tl1 tl2 else o
let rec lpo s t =
match s,t with
- | s, t when s = t ->
- XEQ
+ | s, t when eq_foterm s t ->
+ 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) ->
- if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl1
- then XGT
- else if List.exists (fun x -> let o=lpo s x in o=XLT || o=XEQ) tl2
- then XLT
- else begin
- match aux_ordering hd1 hd2 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
- | 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 =
- 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 lpo x y with
- | XINCOMPARABLE -> Terms.Incomparable
- | XGT -> Terms.Gt
- | XLT -> Terms.Lt
- | XEQ -> Terms.Eq
- | _ -> assert false
- ;;
+ match nonrec_kbo 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
projects / helm.git / blobdiff