X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=f7062b3abebbe2b4d95956ec6f024fd4b46dcb07;hb=HEAD;hp=4ca5a62d3ad2945667606a5c8716022a0a3e9267;hpb=50ed5ab75a38693c7b7558ca9487998e81bb7f89;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 4ca5a62d3..f7062b3ab 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -11,7 +11,7 @@
 
 (* $Id$ *)
 
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
 
 module type Blob =
   sig 
@@ -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
 ;;
   
@@ -90,7 +91,8 @@ let compute_unit_clause_weight (_,l, _, _) =
         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)
@@ -198,6 +200,7 @@ let compare_terms o x y =
       | XGT -> Terms.Gt
       | XLT -> Terms.Lt
       | XEQ -> Terms.Eq
+      | XINVERTIBLE -> Terms.Invertible
       | _ -> assert false
 ;;
 
@@ -209,6 +212,53 @@ module NRKBO (B : Terms.Blob) = struct
 
   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;;
   
@@ -221,7 +271,9 @@ module NRKBO (B : Terms.Blob) = struct
         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
   ;;
 
@@ -352,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
@@ -364,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