Too flexible terms are pruned.

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

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 6628ac9b9373e10bbcea02ed895c21e18d26222f..12df50ebc19fecbf607bea82a091c13db331b1a1 100644 (file)
--- 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)
     ;;