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 86c77a7c0588a4851034ef8cfddd1b1b7d7bf079..1a588043409a66b5f40b07014885accfe653b4a1 100644 (file)
--- 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
     ;;