X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=09d708e731f5327e4a22ad3f8ca95d65ac7e062a;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=6628ac9b9373e10bbcea02ed895c21e18d26222f;hpb=b7b166c432e2118e3270ff4e07467bfbe4ebc57b;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 6628ac9b9..09d708e73 100644
--- a/matitaB/components/ng_paramodulation/superposition.ml
+++ b/matitaB/components/ng_paramodulation/superposition.ml
@@ -138,26 +138,24 @@ module Superposition (B : Orderings.Blob) =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
       let t = Subst.apply_subst subst t in
       if filter subst then
-        let literal = 
+        let tooflex,literal = 
           match t with
           | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq ->
-               let o = Order.compare_terms l r in
-               (* CSC: to avoid equations of the form ? -> T that
-                  can always be applied and that lead to type-checking errors *)
-               (match l,r,o with 
-                   Terms.Var _,_,Terms.Gt
-                 | _,Terms.Var _,Terms.Lt -> assert false
-                 | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
-                    Terms.Equation (l, r, ty, Terms.Lt)
-                 | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
-                    Terms.Equation (l, r, ty, Terms.Gt)
-                 | _ -> Terms.Equation (l, r, ty, o))
-          | t -> Terms.Predicate t
+            let o = Order.compare_terms l r in
+              (match l,r,o with 
+                 Terms.Var _,_,Terms.Gt
+               | _,Terms.Var _,Terms.Lt -> assert false
+               | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
+                    true, Terms.Equation (l, r, ty, o)
+               | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
+                    true, Terms.Equation (l, r, ty, o)
+               | _ -> false, Terms.Equation (l, r, ty, o))
+          | t -> false,Terms.Predicate t
         in
         let bag, uc = 
           Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag
         in
-        Some (bag, uc)
+        if tooflex then None else Some (bag, uc)
       else
         ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
     ;;
@@ -273,7 +271,7 @@ module Superposition (B : Orderings.Blob) =
             match build_clause bag (fun _ -> true)
               Terms.Demodulation (ctx inewside) subst id id2 pos dir
             with
-              | None -> assert false
+              | None -> (bag,[],t,id) (* see tooflex; was assert false *)
               | Some (bag,(id,_,_,_)) ->
                     (bag,subst,newside,id)
     ;;