From: denes <??>
Date: Thu, 9 Jul 2009 12:03:59 +0000 (+0000)
Subject: Fixed check for condition iv p.33 (Riazzanov)
X-Git-Tag: make_still_working~3714
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d807d5e4fa129504669f775f4f832a1a7eb920a0

Fixed check for condition iv p.33 (Riazzanov)
---

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 86c77a7c0..1a5880434 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -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 ->
@@ -655,18 +655,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
     ;;