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 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