(* $Id$ *)
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
module type Blob =
sig
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
+ | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 ->
+ List.for_all2 (eq_foterm f) l1 l2
| _ -> false
;;
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.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)
;;
+(* UNUSED for now *)
let compute_goal_weight (_,l, _, _) =
let weight_of_polynomial w m =
let factor = 2 in
let wr = weight_of_polynomial wr mr in
- (abs (wl-wr))
;;
+
+let compute_goal_weight = compute_unit_clause_weight;;
(* Riazanov: 3.1.5 pag 38 *)
(* Compare weights normalized in a new way :
| XGT -> Terms.Gt
| XLT -> Terms.Lt
| XEQ -> Terms.Eq
+ | XINVERTIBLE -> Terms.Invertible
| _ -> assert false
;;
let eq_foterm = eq_foterm B.eq;;
+exception UnificationFailure of string Lazy.t;;
+
+
+(* DUPLICATE CODE FOR TESTS (see FoUnif) *)
+ let alpha_eq s t =
+ let rec equiv subst s t =
+ let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
+ and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
+
+ in
+ match s, t with
+ | s, t when eq_foterm s t -> subst
+ | Terms.Var i, Terms.Var j
+ when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+ let subst = FoSubst.build_subst i t subst in
+ subst
+ | Terms.Node l1, Terms.Node l2 -> (
+ try
+ List.fold_left2
+ (fun subst' s t -> equiv subst' s t)
+ subst l1 l2
+ with Invalid_argument _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ )
+ | _, _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ in
+ equiv FoSubst.id_subst s t
+;;
+
+let relocate maxvar varlist subst =
+ List.fold_right
+ (fun i (maxvar, varlist, s) ->
+ maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
+ varlist (maxvar+1, [], subst)
+ ;;
+
+ let are_invertible l r =
+ let varlist = (Terms.vars_of_term l)@(Terms.vars_of_term r) in
+ let maxvar = List.fold_left max 0 varlist in
+ let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+ let newl = FoSubst.apply_subst subst l in
+ let newr = FoSubst.apply_subst subst r in
+ try (let subst = alpha_eq l newr in eq_foterm newl (FoSubst.apply_subst subst r)) with
+ UnificationFailure _ -> false
+;;
+
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
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 -> aux_ordering B.compare t1 t2
+ | XEQ -> let res = aux_ordering B.compare t1 t2 in
+ if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+ else res
| res -> res
;;
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
| XLT -> if check_subterms t (l_ol,tl1) then XLT
else XINCOMPARABLE
| XEQ ->
+ (try
let lex = List.fold_left2
(fun acc si ti -> if acc = XEQ then lpo si ti else acc)
XEQ tl1 tl2
if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
else XINCOMPARABLE
| o -> o)
+ with Invalid_argument _ -> (* assert false *)
+ XINCOMPARABLE)
| XINCOMPARABLE -> XINCOMPARABLE
| _ -> assert false
end