| _ -> assert false
;;
-let are_invertible relocate alpha_eq l r =
- let varlist = Terms.vars_of_term l in
+let are_invertible relocate alpha_eq eq_foterm 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 l = FoSubst.apply_subst subst l in
- try (ignore(alpha_eq l r);true) with
+ 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
FoUnif.UnificationFailure _ -> false;;
module NRKBO (B : Terms.Blob) = struct
let eq_foterm = eq_foterm B.eq;;
- let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
let compute_clause_weight = compute_clause_weight;;
let eq_foterm = eq_foterm B.eq;;
- let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
let eq_foterm = eq_foterm B.eq;;
- let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;