From d6578d33463c053073c6dab75728ca318717e1de Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 14 Nov 2011 07:58:46 +0000 Subject: [PATCH] Too flexible terms are pruned. --- .../ng_paramodulation/nCicParamod.ml | 14 ++++++++-- .../ng_paramodulation/superposition.ml | 26 +++++++++---------- 2 files changed, 24 insertions(+), 16 deletions(-) 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) ;; -- 2.39.2