Too flexible terms are pruned.

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

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml
index 5906bc06d3989b27c629a8ef4bbf8a952ec85313..67eca9fce3ed0eab1a7e6eddb3b25b1c88fdee2a 100644 (file)
--- 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)
 ;;