Removed unused parameter of unification procedure (vars)

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 86c77a7c0588a4851034ef8cfddd1b1b7d7bf079..0a7c5cfcc1c82fdb0be718e4ddde26bca391d876 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -11,12 +11,12 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-module Superposition (B : Terms.Blob) = 
+module Superposition (B : Orderings.Blob) = 
   struct
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
     module Subst = FoSubst 
-    module Order = Orderings.Orderings(B)
+    module Order = B
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
     
@@ -103,7 +103,7 @@ module Superposition (B : Terms.Blob) =
     let build_clause bag filter rule t subst id id2 pos dir =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
       let t = Subst.apply_subst subst t in
-      if filter t then
+      if filter subst then
         let literal = 
           match t with
           | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
@@ -128,6 +128,7 @@ module Superposition (B : Terms.Blob) =
     let prof_demod_u = HExtlib.profile ~enable "demod.unify";;
     let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";;
     let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";;
+    let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";;
 
     let demod table varlist subterm =
       let cands = 
@@ -143,10 +144,16 @@ module Superposition (B : Terms.Blob) =
                try 
                  let subst =
                    prof_demod_u.HExtlib.profile 
-                     (Unif.unification (varlist@vl) varlist subterm) side 
+                     (Unif.unification (* (varlist@vl) *) varlist subterm) side 
                  in 
-                 let side = Subst.apply_subst subst side in
-                 let newside = Subst.apply_subst subst newside in
+                 let side = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) side 
+                 in
+                 let newside = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) newside 
+                 in
                  if o = Terms.Incomparable then
                    let o = 
                      prof_demod_o.HExtlib.profile 
@@ -282,7 +289,7 @@ module Superposition (B : Terms.Blob) =
     let is_identity_clause ~unify = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
       | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
-          (try ignore(Unif.unification vl [] l r); true
+          (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Equation (_,_,_,_), _, _ -> false
       | _, Terms.Predicate _, _, _ -> assert false          
@@ -336,7 +343,7 @@ module Superposition (B : Terms.Blob) =
         | [] -> None
         | (id2,dir,c,vl1)::tl ->
             try
-              let subst = Unif.unification (vl@vl1) locked_vars c t in
+              let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
               Some (id2, dir, subst)
             with FoUnif.UnificationFailure _ -> aux tl
       in
@@ -367,7 +374,7 @@ module Superposition (B : Terms.Blob) =
           let l = Subst.apply_subst subst l in 
           let r = Subst.apply_subst subst r in 
             try 
-              let subst1 = Unif.unification vl [] l r in
+              let subst1 = Unif.unification (* vl *) [] l r in
               let lit = 
                 match lit with Terms.Predicate _ -> assert false
                   | Terms.Equation (l,r,ty,o) -> 
@@ -620,7 +627,7 @@ module Superposition (B : Terms.Blob) =
                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
                try 
                  let subst = 
-                   Unif.unification (varlist@vl) [] subterm side 
+                   Unif.unification (* (varlist@vl)*)  [] subterm side 
                  in 
                  if o = Terms.Incomparable then
                    let side = Subst.apply_subst subst side in
@@ -655,18 +662,28 @@ module Superposition (B : Terms.Blob) =
             (all_positions [2] 
               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
               l (superposition table vl))
-      | Terms.Equation (l,r,ty,Terms.Incomparable) -> 
-          fold_build_new_clause bag maxvar id Terms.Superposition
-            (function (* Riazanov: p.33 condition (iv) *)
-              | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq -> 
-                  Order.compare_terms l r <> Terms.Eq
-              | _ -> assert false)
-            ((all_positions [3] 
-               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
-               r (superposition table vl)) @         
-             (all_positions [2] 
-               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
-               l (superposition table vl)))
+      | Terms.Equation (l,r,ty,Terms.Incomparable) ->
+         let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
+           let l = Subst.apply_subst subst l in
+           let r = Subst.apply_subst subst r in
+           let o = Order.compare_terms l r in
+           o <> avoid && o <> Terms.Eq
+         in
+          let bag, maxvar,r_terms =
+           fold_build_new_clause bag maxvar id Terms.Superposition
+              (filtering Terms.Gt)
+              (all_positions [3] 
+                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+                r (superposition table vl))
+         in
+         let bag, maxvar, l_terms =
+           fold_build_new_clause bag maxvar id Terms.Superposition
+              (filtering Terms.Lt)
+              (all_positions [2] 
+                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+                r (superposition table vl))
+         in
+           bag, maxvar, r_terms @ l_terms
       | _ -> assert false
     ;;