From b7b166c432e2118e3270ff4e07467bfbe4ebc57b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 28 Oct 2011 10:59:33 +0000 Subject: [PATCH] New management of resulting subst in deep_eq: used to be malformed. --- .../components/ng_paramodulation/nCicProof.ml | 19 +----- .../ng_paramodulation/superposition.ml | 68 +++++++++++++------ 2 files changed, 48 insertions(+), 39 deletions(-) diff --git a/matitaB/components/ng_paramodulation/nCicProof.ml b/matitaB/components/ng_paramodulation/nCicProof.ml index 50c25315f..5f8ed1733 100644 --- a/matitaB/components/ng_paramodulation/nCicProof.ml +++ b/matitaB/components/ng_paramodulation/nCicProof.ml @@ -231,24 +231,7 @@ let debug c _ = c;; let lit = Subst.apply_subst subst lit in extract status 0 [] lit in (* composition of all subst acting on goal *) - let res_subst = - let rec rsaux ongoal acc = - function - | [] -> acc (* is the final subst for refl *) - | id::tl when ongoal -> - let lit,vl,proof = get_literal id in - (match proof with - | Terms.Exact _ -> rsaux ongoal acc tl - | Terms.Step (_, _, _, _, _, s) -> - rsaux ongoal (s@acc) tl) - | id::tl -> - (* subst is the the substitution for refl *) - rsaux (id=mp) subst tl - in - let r = rsaux false [] steps in - (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r); - prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *) - r + let res_subst = subst in let rec aux ongoal seen = function | [] -> NCic.Rel 1 diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml index 1152571ce..6628ac9b9 100644 --- a/matitaB/components/ng_paramodulation/superposition.ml +++ b/matitaB/components/ng_paramodulation/superposition.ml @@ -27,8 +27,7 @@ module Superposition (B : Orderings.Blob) = * B.t Terms.substitution let print s = prerr_endline (Lazy.force s);; - let debug _ = ();; - (* let debug = print;; *) + let debug _ = ();; let enable = true;; let rec list_first f = function @@ -110,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 @@ -143,7 +142,16 @@ module Superposition (B : Orderings.Blob) = 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) + (* 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 in let bag, uc = @@ -366,12 +374,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 @@ -390,8 +403,12 @@ module Superposition (B : Orderings.Blob) = | [] -> 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) @@ -401,9 +418,9 @@ 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) -> + | 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 @@ -415,38 +432,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]) 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) @@ -637,7 +662,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 @@ -660,12 +685,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)) *) ;; -- 2.39.2