;;
let are_invertible l r =
- let varlist = Terms.vars_of_term l in
+ 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
UnificationFailure _ -> false
+;;
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
| 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