From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 14 Nov 2011 07:58:46 +0000 (+0000)
Subject: Too flexible terms are pruned.
X-Git-Tag: make_still_working~2120
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d6578d33463c053073c6dab75728ca318717e1de

Too flexible terms are pruned.
---

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml
index 5906bc06d..67eca9fce 100644
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -94,14 +94,24 @@ let empty_state = P.empty_state
 
 let size_of_state = P.size_of_state
 
+let tooflex (_,l,_,_) =
+  match l with
+    | Terms.Equation (l,r,_,o) ->
+      (match l,r,o with
+       | Terms.Var _, _, (Terms.Incomparable | Terms.Invertible) -> true
+       | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> true
+       | _ -> false)
+    | _ -> false
+;;  
+
 let forward_infer_step status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
   let saturate (t,ty) = 
     NCicBlob.saturate status metasenv subst context t ty in
   let bag,clause = P.mk_passive bag (saturate (t,ty)) in
     if Terms.is_eq_clause clause then
-      ((*prerr_endline "is eq";*)
-      P.forward_infer_step (P.replace_bag s bag) clause 0)
+      if tooflex clause then (debug (lazy "pruning tooflex"); s)
+      else P.forward_infer_step (P.replace_bag s bag) clause 0
     else ((*print (lazy "not eq");*) s)
 ;;
 
diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 6628ac9b9..12df50ebc 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)
     ;;