X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=f7062b3abebbe2b4d95956ec6f024fd4b46dcb07;hb=refs%2Fheads%2Fmatita-lablgtk3;hp=4c6e0a977d7c7600e4a2449e9cb2bd2c11d0eb34;hpb=5642a453e8b4bbe228d126aa0c44d31e101969ec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 4c6e0a977..f7062b3ab 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -40,7 +40,8 @@ let rec eq_foterm f 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
+    | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 -> 
+        List.for_all2 (eq_foterm f) l1 l2
     | _ -> false
 ;;
   
@@ -249,12 +250,14 @@ let relocate maxvar varlist subst =
   ;;
 
   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;;
@@ -401,6 +404,7 @@ module LPO (B : Terms.Blob) = struct
                   | 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
@@ -413,6 +417,8 @@ module LPO (B : Terms.Blob) = struct
                         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