(* $Id$ *)
-(* (weight of constants, [(meta, weight_of_meta)]) *)
-type weight = int * (int * int) list;;
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
+
+module type Blob =
+ sig
+ include Terms.Blob
+
+ (* This order relation should be:
+ * - stable for instantiation
+ * - total on ground terms
+ *
+ *)
+ val compare_terms :
+ t Terms.foterm -> t Terms.foterm -> Terms.comparison
+
+ val compute_clause_weight : 't Terms.clause -> int
+ val name : string
+
+ end
+
+type weight = int * (int * int) list;;
+
+let rec eq_foterm f x y =
+ x == y ||
+ match x, y with
+ | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
+ | Terms.Var i, Terms.Var j -> i = j
+ | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
+ | _ -> false
+;;
+
let string_of_weight (cw, mw) =
let s =
String.concat ", "
in
Printf.sprintf "[%d; %s]" cw s
;;
-
+
let weight_of_term term =
- let vars_dict = Hashtbl.create 5 in
- let rec aux = function
- | Terms.Var i ->
- (try
- let oldw = Hashtbl.find vars_dict i in
- Hashtbl.replace vars_dict i (oldw+1)
- with Not_found ->
- Hashtbl.add vars_dict i 1);
- 0
- | Terms.Leaf _ -> 1
- | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
- in
- let w = aux term in
- let l =
- Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
- in
- let compare w1 w2 =
- match w1, w2 with
- | (m1, _), (m2, _) -> m2 - m1
- in
- (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
+ let vars_dict = Hashtbl.create 5 in
+ let rec aux = function
+ | Terms.Var i ->
+ (try
+ let oldw = Hashtbl.find vars_dict i in
+ Hashtbl.replace vars_dict i (oldw+1)
+ with Not_found ->
+ Hashtbl.add vars_dict i 1);
+ 0
+ | Terms.Leaf _ -> 1
+ | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
+ in
+ let w = aux term in
+ let l =
+ Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
+ in
+ let compare w1 w2 =
+ match w1, w2 with
+ | (m1, _), (m2, _) -> m1 - m2
+ in
+ (w, List.sort compare l) (* from the smallest meta to the bigest *)
;;
-
-let compute_clause_weight = assert false (*
- let factor = 2 in
- match o with
- | Lt ->
- let w, m = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false right) in
- w + (factor * (List.length m)) ;
- | Le -> assert false
- | Gt ->
- let w, m = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false left) in
- w + (factor * (List.length m)) ;
- | Ge -> assert false
- | Eq
- | Incomparable ->
- let w1, m1 = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false right) in
- let w2, m2 = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false left) in
- w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
-*)
-;;
-
-(* 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 compute_literal_weight l =
+ let weight_of_polynomial w m =
+ let factor = 2 in
+ w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
+ in
+ match l with
+ | Terms.Predicate t ->
+ let w, m = weight_of_term t in
+ weight_of_polynomial w m
+ | Terms.Equation (_,x,_,Terms.Lt)
+ | Terms.Equation (x,_,_,Terms.Gt) ->
+ let w, m = weight_of_term x in
+ weight_of_polynomial w m
+ | Terms.Equation (l,r,_,Terms.Eq)
+ | Terms.Equation (l,r,_,Terms.Incomparable)
+ | Terms.Equation (l,r,_,Terms.Invertible) ->
+ let wl, ml = weight_of_term l in
+ let wr, mr = weight_of_term r in
+ weight_of_polynomial (wl+wr) (ml@mr)
;;
+let compute_clause_weight (_,nl,pl,_,_) =
+ List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
-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)
-;;
-
+let compute_goal_weight = compute_clause_weight;;
+
(* Riazanov: 3.1.5 pag 38 *)
-let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)=
- 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
+(* 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 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 = Pervasives.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 Lt
- else if hdiff > 0 then Gt
- else Eq
- | (m, _, 0) ->
- if hdiff <= 0 then Lt
- else if (- diffs) >= hdiff then Le else Incomparable
- | (0, _, m) ->
- if hdiff >= 0 then Gt
- else if diffs >= (- hdiff) then Ge else Incomparable
- | (m, _, n) when m > 0 && n > 0 ->
- Incomparable
- | _ -> assert false
+ aux (h1-h2) (false,false) 0 w1 w2
;;
-
-let rec aux_ordering ?(recursion=true) t1 t2 =
- let module C = Cic in
- let compare_uris u1 u2 =
- let res =
- compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
- if res < 0 then Lt
- else if res = 0 then Eq
- else Gt
- in
+(* Riazanov: p. 40, relation >>>
+ * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
+let rec aux_ordering b_compare ?(head_only=false) t1 t2 =
match t1, t2 with
- | C.Meta _, _
- | _, C.Meta _ -> Incomparable
-
- | t1, t2 when t1 = t2 -> Eq
-
- | C.Rel n, C.Rel m -> if n > m then Lt else Gt
- | C.Rel _, _ -> Lt
- | _, C.Rel _ -> Gt
-
- | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
- | C.Const _, _ -> Lt
- | _, C.Const _ -> Gt
-
- | C.MutInd (u1, tno1, _), C.MutInd (u2, tno2, _) ->
- let res = compare_uris u1 u2 in
- if res <> Eq then res
- else
- let res = compare tno1 tno2 in
- if res = 0 then Eq else if res < 0 then Lt else Gt
- | C.MutInd _, _ -> Lt
- | _, C.MutInd _ -> Gt
-
- | C.MutConstruct (u1, tno1, cno1, _), C.MutConstruct (u2, tno2, cno2, _) ->
- let res = compare_uris u1 u2 in
- if res <> Eq then res
- else
- let res = compare (tno1,cno1) (tno2,cno2) in
- if res = 0 then Eq else if res < 0 then Lt else Gt
- | C.MutConstruct _, _ -> Lt
- | _, C.MutConstruct _ -> Gt
-
- | C.Appl l1, C.Appl l2 when recursion ->
+ (* We want to discard any identity equality. *
+ * If we give back XEQ, no inference rule *
+ * will be applied on this equality *)
+ | Terms.Var i, Terms.Var j when i = j ->
+ XEQ
+ (* 1. *)
+ | Terms.Var _, _
+ | _, Terms.Var _ -> XINCOMPARABLE
+ (* 2.a *)
+ | Terms.Leaf a1, Terms.Leaf a2 ->
+ let cmp = b_compare a1 a2 in
+ if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+ | Terms.Leaf _, Terms.Node _ -> XLT
+ | Terms.Node _, Terms.Leaf _ -> XGT
+ (* 2.b *)
+ | Terms.Node l1, Terms.Node l2 ->
let rec cmp t1 t2 =
match t1, t2 with
- | [], [] -> Eq
- | _, [] -> Gt
- | [], _ -> Lt
+ | [], [] -> XEQ
+ | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
+ | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
| hd1::tl1, hd2::tl2 ->
- let o = aux_ordering hd1 hd2 in
- if o = Eq then cmp tl1 tl2
- else o
+ let o = aux_ordering b_compare ~head_only hd1 hd2 in
+ if o = XEQ && not head_only then cmp tl1 tl2 else o
in
cmp l1 l2
- | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
- aux_ordering h1 h2
-
- | t1, t2 ->
- debug_print
- (lazy
- (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
- (CicPp.ppterm t1) (CicPp.ppterm t2)));
- Incomparable
;;
-
-let nonrec_kbo t1 t2 =
- let w1 = weight_of_term t1 in
- let w2 = weight_of_term t2 in
- match compare_weights ~normalize:true w1 w2 with
- | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
- | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
- | Eq -> aux_ordering t1 t2
- | res -> res
+
+let compare_terms o x y =
+ match o x y with
+ | XINCOMPARABLE -> Terms.Incomparable
+ | XGT -> Terms.Gt
+ | XLT -> Terms.Lt
+ | XEQ -> Terms.Eq
+ | XINVERTIBLE -> Terms.Invertible
+ | _ -> assert false
;;
-let rec kbo t1 t2 =
- let aux = aux_ordering ~recursion:false in
- let w1 = weight_of_term t1
- and w2 = weight_of_term t2 in
- let rec cmp t1 t2 =
- match t1, t2 with
- | [], [] -> Eq
- | _, [] -> Gt
- | [], _ -> Lt
- | hd1::tl1, hd2::tl2 ->
- let o =
- kbo hd1 hd2
- in
- if o = Eq then cmp tl1 tl2
- else o
- in
- let comparison = compare_weights ~normalize:true w1 w2 in
- match comparison with
- | Le ->
- let r = aux t1 t2 in
- if r = Lt then Lt
- else if r = Eq then (
- match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Lt then Lt else Incomparable
- | _, _ -> Incomparable
- ) else Incomparable
- | Ge ->
- let r = aux t1 t2 in
- if r = Gt then Gt
- else if r = Eq then (
- match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Gt then Gt else Incomparable
- | _, _ -> Incomparable
- ) else Incomparable
- | Eq ->
- let r = aux t1 t2 in
- if r = Eq then (
- match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- cmp tl1 tl2
- | _, _ -> Incomparable
- ) else r
- | res -> res
-;;
-
-let compare_terms = nonrec_kbo;;
+let are_invertible relocate alpha_eq l r =
+ let varlist = Terms.vars_of_term l in
+ let maxvar = List.fold_left max 0 varlist in
+ let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+ let l = FoSubst.apply_subst subst l in
+ try (ignore(alpha_eq l r);true) with
+ FoUnif.UnificationFailure _ -> false;;
+
+module NRKBO (B : Terms.Blob) = struct
+ let name = "nrkbo"
+ include B
+
+ module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
+ let compute_clause_weight = compute_clause_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)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
+ let compute_clause_weight = compute_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)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
+ let compute_clause_weight = compute_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
projects / helm.git / blobdiff