From: denes <??>
Date: Wed, 22 Jul 2009 13:14:51 +0000 (+0000)
Subject: Fixes
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8e4367191fdfd125596658e35d4b99cd3047a5bc

Fixes
---

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 633c32854..beb3aed86 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -86,6 +86,7 @@ module Index(B : Orderings.Blob) = struct
     = Make(FotermIndexable)(ClauseSet)
 
   let index_literal t c is_pos pos = function
+    | Terms.Equation (l,_,_,Terms.Invertible)
     | Terms.Equation (l,_,_,Terms.Gt) -> 
           DT.index t l (Terms.Left2Right,is_pos,pos,c)
     | Terms.Equation (_,r,_,Terms.Lt) ->
diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index f8e1d4231..47f6b4512 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -194,8 +194,52 @@ 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 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
+	  UnificationFailure _ -> false
+
   let compute_clause_weight = compute_clause_weight;;
-  let compute_goal_weight = compute_goal_weight;;
   
   (* Riazanov: p. 40, relation >_n *)
   let nonrec_kbo t1 t2 =