X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=09d708e731f5327e4a22ad3f8ca95d65ac7e062a;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=42cf063b64f08b3e352693d7a30bebff78025e95;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml index 42cf063b6..09d708e73 100644 --- a/matitaB/components/ng_paramodulation/superposition.ml +++ b/matitaB/components/ng_paramodulation/superposition.ml @@ -109,8 +109,8 @@ module Superposition (B : Orderings.Blob) = let visit bag pos ctx id t f = let rec aux bag pos ctx id subst = function | Terms.Leaf _ as t -> - let bag,subst,t,id = f bag t pos ctx id - in assert (subst=[]); bag,t,id + let bag,subst,t,id = f bag t pos ctx id in + assert (subst=[]); bag,t,id | Terms.Var i as t -> let t= Subst.apply_subst subst t in bag,t,id @@ -138,17 +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 - Terms.Equation (l, r, ty, o) - | t -> Terms.Predicate t + | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq -> + 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) ;; @@ -264,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) ;; @@ -281,12 +288,12 @@ module Superposition (B : Orderings.Blob) = | Terms.Equation (l,r,ty,_) -> let bag,l,id1 = visit bag [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) id l (ctx_demod table vl) in let bag,_,id2 = visit bag [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) id1 r (ctx_demod table vl) in let cl,_,_ = Terms.get_from_bag id2 bag in @@ -310,7 +317,7 @@ module Superposition (B : Orderings.Blob) = match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,_) -> - Terms.Node [Terms.Leaf B.eqP; ty; l ; r] + Terms.Node [Terms.Leaf (B.eqP()); ty; l ; r] in try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true with FoUnif.UnificationFailure _ -> false @@ -365,12 +372,17 @@ module Superposition (B : Orderings.Blob) = bag, maxvar, res ;; - let rewrite_eq ~unify l r ty vl table = + (* rewrite_eq check if in table there an equation matching l=r; + used in subsumption and deep_eq. In deep_eq, we need to match + several times times w.r.t. the same table, hence we should refresh + the retrieved clauses, to avoid clashes of variables *) + + let rewrite_eq ~refresh ~unify maxvar l r ty vl table = let retrieve = if unify then IDX.DT.retrieve_unifiables else IDX.DT.retrieve_generalizations in let lcands = retrieve table l in let rcands = retrieve table r in - let f b c = + let f b c = let id, dir, l, r, vl = match c with | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl @@ -379,18 +391,22 @@ module Superposition (B : Orderings.Blob) = let reverse = (dir = Terms.Left2Right) = b in let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right else r,l, Terms.Right2Left in - (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl) + (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl) in let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in - let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in + let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in let locked_vars = if unify then [] else vl in let rec aux = function | [] -> None | (id2,dir,c,vl1)::tl -> try + let c,maxvar = if refresh then + let maxvar,_,r = Utils.relocate maxvar vl1 [] in + Subst.apply_subst r c,maxvar + else c,maxvar in let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in - Some (id2, dir, subst) + Some (id2, dir, subst, maxvar) with FoUnif.UnificationFailure _ -> aux tl in aux (cands1 @ cands2) @@ -400,10 +416,10 @@ module Superposition (B : Orderings.Blob) = match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,_) -> - match rewrite_eq ~unify l r ty vl table with + match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with | None -> None - | Some (id2, dir, subst) -> - let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in + | Some (id2, dir, subst, maxvar) -> + let id_t = Terms.Node [ Terms.Leaf (B.eqP()); ty; r; r ] in build_new_clause bag maxvar (fun _ -> true) Terms.Superposition id_t subst id id2 [2] dir ;; @@ -414,38 +430,46 @@ module Superposition (B : Orderings.Blob) = (* id refers to a clause proving contextl l = contextr r *) let rec deep_eq ~unify l r ty pos contextl contextr table acc = + (* let _ = prerr_endline ("pos = " ^ String.concat "," + (List.map string_of_int pos)) in *) match acc with | None -> None | Some(bag,maxvar,(id,lit,vl,p),subst) -> (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *) + (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *) + (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *) let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in + (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *) + (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *) try let subst1 = Unif.unification (* vl *) [] l r in let lit = match lit with Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,o) -> - Terms.Equation (FoSubst.apply_subst subst1 l, - FoSubst.apply_subst subst1 r, ty, o) + let l = Subst.apply_subst subst1 l in + let r = Subst.apply_subst subst1 r in + Terms.Equation (l, r, ty, o) in Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> - match rewrite_eq ~unify l r ty vl table with - | Some (id2, dir, subst1) -> + match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with + | Some (id2, dir, subst1, maxvar) -> (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1); - prerr_endline ("old subst = "^Pp.pp_substitution subst);*) + prerr_endline ("old subst = "^Pp.pp_substitution subst); *) let newsubst = Subst.concat subst1 subst in let id_t = FoSubst.apply_subst newsubst - (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) + (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r]) in - (match + (match build_new_clause_reloc bag maxvar (fun _ -> true) Terms.Superposition id_t - subst1 id id2 (pos@[2]) dir - with + subst1 id id2 (pos@[2]) dir + with | Some ((bag, maxvar), c), r -> - (* prerr_endline ("r = "^Pp.pp_substitution r); *) + (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *) + (* prerr_endline ("r = "^Pp.pp_substitution r); *) let newsubst = Subst.flat (Subst.concat r subst) in Some(bag,maxvar,c,newsubst) @@ -636,7 +660,7 @@ module Superposition (B : Orderings.Blob) = let bag, clause = if no_demod then bag, clause else demodulate bag clause table in - let _ = debug (lazy ("demodulated goal : " + let _ = debug(lazy ("demodulated goal : " ^ Pp.pp_unit_clause clause)) in if List.exists (are_alpha_eq clause) g_actives then None @@ -659,12 +683,13 @@ module Superposition (B : Orderings.Blob) = | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> debug (lazy "Goal subsumed"); + debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst)); raise (Success (bag,maxvar,cl,subst)) (* match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) | Some ((bag,maxvar),c) -> - prerr_endline "Goal subsumed"; + debug (lazy "Goal subsumed"); raise (Success (bag,maxvar,c)) *) ;; @@ -714,14 +739,14 @@ module Superposition (B : Orderings.Blob) = fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) r (superposition table vl)) | Terms.Equation (l,r,ty,Terms.Invertible) | Terms.Equation (l,r,ty,Terms.Gt) -> fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) l (superposition table vl)) | Terms.Equation (l,r,ty,Terms.Incomparable) -> let filtering avoid subst = (* Riazanov: p.33 condition (iv) *) @@ -734,14 +759,14 @@ module Superposition (B : Orderings.Blob) = fold_build_new_clause bag maxvar id Terms.Superposition (filtering Terms.Gt) (all_positions [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) r (superposition table vl)) in let bag, maxvar, l_terms = fold_build_new_clause bag maxvar id Terms.Superposition (filtering Terms.Lt) (all_positions [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) l (superposition table vl)) in bag, maxvar, r_terms @ l_terms