From: denes Date: Fri, 31 Jul 2009 12:40:27 +0000 (+0000) Subject: Now iterating superposition X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0842258ce37ce992a0d52c813a9a5cb4c3f2bb52 Now iterating superposition --- diff --git a/helm/software/components/ng_paramodulation/clauses.ml b/helm/software/components/ng_paramodulation/clauses.ml index 5955fcae1..f8724601c 100644 --- a/helm/software/components/ng_paramodulation/clauses.ml +++ b/helm/software/components/ng_paramodulation/clauses.ml @@ -25,8 +25,8 @@ module Clauses (B : Orderings.Blob) = struct let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2 let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2 - let fresh_clause maxvar (id, nlit, plit, varlist, proof) = - let maxvar, varlist, subst = Utils.relocate maxvar varlist FoSubst.id_subst in + let fresh_clause maxvar ?(subst=FoSubst.id_subst) (id, nlit, plit, varlist, proof) = + let maxvar, varlist, subst = Utils.relocate maxvar varlist subst in let apply_subst_on_lit = function | Terms.Equation (l,r,ty,o) -> let l = FoSubst.apply_subst subst l in @@ -99,4 +99,14 @@ module Clauses (B : Orderings.Blob) = struct with Invalid_argument _ -> false ;; + let vars_of_clause (id,nlit,plit,_,pr) = + let vars_of_lit acc lit = + match lit with + | (Terms.Predicate t,_) -> Terms.vars_of_term ~start_acc:acc t + | (Terms.Equation (l,r,ty,o),_) -> + Terms.vars_of_term ~start_acc:(Terms.vars_of_term ~start_acc:acc l) r + in + List.fold_left vars_of_lit [] (nlit@plit) +;; + end diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli index 81738c2a4..b857eb016 100644 --- a/helm/software/components/ng_paramodulation/clauses.mli +++ b/helm/software/components/ng_paramodulation/clauses.mli @@ -22,7 +22,9 @@ module Clauses (B : Orderings.Blob) : val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int - val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int + val fresh_clause : int -> + ?subst: B.t Terms.substitution -> + B.t Terms.clause -> B.t Terms.clause * int val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list -> B.t Terms.foterm -> B.t Terms.clause * int @@ -40,4 +42,10 @@ module Clauses (B : Orderings.Blob) : val are_alpha_eq_cl : B.t Terms.clause -> B.t Terms.clause -> bool + val vars_of_clause : + B.t Terms.clause -> int list + + (*val apply_subst : + B.t Terms.substitution -> B.t Terms.clause -> B.t Terms.clause*) + end diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index daafbd3ac..63507aea6 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -102,7 +102,7 @@ module Superposition (B : Orderings.Blob) = aux bag pos ctx id lit t ;; - let build_clause bag filter rule t subst id id2 pos dir clause_ctx = + let build_clause ~fresh bag maxvar filter rule t subst id id2 pos dir clause_ctx = let proof = Terms.Step(rule,id,id2,dir,pos,subst) in let t = Subst.apply_subst subst t in if filter subst then @@ -114,16 +114,23 @@ module Superposition (B : Orderings.Blob) = | t -> Terms.Predicate t in let nlit,plit = clause_ctx literal in - let bag, uc = - Terms.add_to_bag (0, nlit, plit, Terms.vars_of_term t, proof) bag + let cl = (0, nlit, plit, [], proof) in + let vl = Clauses.vars_of_clause cl in + let cl,maxvar = + if fresh then Clauses.fresh_clause ~subst maxvar (0, nlit, plit, vl, proof) + else cl,maxvar in - Some (bag, uc, literal) + let bag, cl = + Terms.add_to_bag (0, nlit, plit, vl, proof) bag + in + Some (bag, maxvar, cl, literal) else ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) ;; let prof_build_clause = HExtlib.profile ~enable "build_clause";; - let build_clause bag filter rule t subst id id2 pos x = - prof_build_clause.HExtlib.profile (build_clause bag filter rule t subst id id2 pos) x + let build_clause ~fresh bag maxvar filter rule t subst id id2 pos x = + prof_build_clause.HExtlib.profile + (build_clause ~fresh bag maxvar filter rule t subst id id2 pos) x ;; @@ -186,11 +193,11 @@ module Superposition (B : Orderings.Blob) = match demod table vl t with | None -> (bag,t,id,lit) | Some (newside, subst, id2, dir) -> - match build_clause bag (fun _ -> true) + match build_clause ~fresh:false bag 0 (fun _ -> true) Terms.Demodulation (ctx newside) subst id id2 pos dir clause_ctx with | None -> assert false - | Some (bag,(id,_,_,_,_),lit) -> + | Some (bag,_,(id,_,_,_,_),lit) -> (bag,newside,id,lit) ;; @@ -279,24 +286,14 @@ module Superposition (B : Orderings.Blob) = with FoUnif.UnificationFailure _ -> false) | _ -> false - let build_new_clause bag maxvar filter rule t subst id id2 pos dir = - let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term - (Subst.apply_subst subst t)) subst in - match build_clause bag filter rule t subst id id2 pos dir (fun x -> [],[(x,true)]) with - | Some (bag, c, _) -> Some ((bag, maxvar), c) - | None -> None - ;; - let prof_build_new_clause = HExtlib.profile ~enable "build_new_clause";; - let build_new_clause bag maxvar filter rule t subst id id2 pos x = - prof_build_new_clause.HExtlib.profile (build_new_clause bag maxvar filter - rule t subst id id2 pos) x - ;; - - let fold_build_new_clause bag maxvar id rule filter res = + let fold_build_new_clause bag maxvar id rule filter res clause_ctx = let (bag, maxvar), res = HExtlib.filter_map_acc (fun (bag, maxvar) (t,subst,id2,pos,dir) -> - build_new_clause bag maxvar filter rule t subst id id2 pos dir) + match build_clause ~fresh:true bag maxvar filter + rule t subst id id2 pos dir clause_ctx with + | None -> None + | Some (bag,maxvar,res,_) -> Some ((bag,maxvar),res)) (bag, maxvar) res in bag, maxvar, res @@ -342,8 +339,8 @@ module Superposition (B : Orderings.Blob) = | None -> None | Some (id2, dir, subst) -> 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) + build_clause ~fresh:true bag maxvar (fun _ -> true) + Terms.Superposition id_t subst id id2 [2] dir (fun l -> [],[l,true])) | _ -> None (* TODO : implement subsumption for clauses *) ;; let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";; @@ -362,7 +359,7 @@ module Superposition (B : Orderings.Blob) = let subst1 = Unif.unification (* vl *) [] l r in let lit = match nlit,plit with - | [],[Terms.Equation (l,r,ty,o),_] -> + | [Terms.Equation (l,r,ty,o),_],[] -> Terms.Equation (FoSubst.apply_subst subst1 l, FoSubst.apply_subst subst1 r, ty, o) | _ -> assert false @@ -377,11 +374,11 @@ module Superposition (B : Orderings.Blob) = (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) in (match - build_new_clause bag maxvar (fun _ -> true) + build_clause ~fresh:true bag maxvar (fun _ -> true) Terms.Superposition id_t - subst1 id id2 (pos@[2]) dir + subst1 id id2 (pos@[2]) dir (fun l -> [],[l,true]) with - | Some ((bag, maxvar), c) -> + | Some (bag, maxvar, c, _) -> Some(bag,maxvar,c,newsubst) | None -> assert false) | None -> @@ -604,10 +601,10 @@ module Superposition (B : Orderings.Blob) = (* =================== inference ===================== *) (* this is OK for both the sup_left and sup_right inference steps *) - let superposition table varlist subterm pos context = + let superposition table varlist is_pos subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in HExtlib.filter_map - (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) -> + (fun (dir, is_cand_pos, _, (id,nlit,plit,vl,_ (*as uc*))) -> match nlit,plit with | [],[Terms.Equation (l,r,_,o),_] -> (let side, newside = if dir=Terms.Left2Right then l,r else r,l in @@ -634,22 +631,22 @@ module Superposition (B : Orderings.Blob) = ;; (* Superposes selected equation with equalities in table *) - let superposition_with_table bag maxvar (id,nlit,plit,vl,_) table = - match nlit,plit with - | [],[Terms.Equation (l,r,ty,Terms.Lt),_] -> + let superposition_with_table bag maxvar id vl lit is_pos clause_ctx table = + match lit with + | Terms.Equation (l,r,ty,Terms.Lt) -> 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 ]) - r (superposition table vl)) - | [],[Terms.Equation (l,r,ty,Terms.Invertible),_] - | [],[Terms.Equation (l,r,ty,Terms.Gt),_] -> + r (superposition table vl is_pos)) clause_ctx + | 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 ]) - l (superposition table vl)) - | [],[Terms.Equation (l,r,ty,Terms.Incomparable),_] -> + l (superposition table vl is_pos)) clause_ctx + | Terms.Equation (l,r,ty,Terms.Incomparable) -> let filtering avoid subst = (* Riazanov: p.33 condition (iv) *) let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in @@ -661,19 +658,32 @@ module Superposition (B : Orderings.Blob) = (filtering Terms.Gt) (all_positions [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) - r (superposition table vl)) + r (superposition table vl is_pos)) clause_ctx 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 ]) - l (superposition table vl)) + l (superposition table vl is_pos)) clause_ctx in bag, maxvar, r_terms @ l_terms | _ -> assert false ;; + let superpose_literal id vl table is_pos (bag,maxvar,pre,post,acc) (lit,sel) = + let clause_ctx = + if is_pos then fun l -> [],pre@[l,true]@post + else fun l -> pre@[l,true]@post,[] + in + let bag, maxvar, newc = + superposition_with_table bag maxvar id vl lit is_pos clause_ctx table + in + if post = [] then bag,maxvar,pre@[lit,sel],[],newc@acc + else bag,maxvar,pre@[lit,sel],List.tl post,newc@acc + ;; + + (* the current equation is normal w.r.t. demodulation with atable * (and is not the identity) *) let infer_right bag maxvar current (alist,atable) = @@ -691,11 +701,18 @@ module Superposition (B : Orderings.Blob) = (* We superpose active clauses with current *) let bag, maxvar, new_clauses = List.fold_left - (fun (bag, maxvar, acc) active -> - let bag, maxvar, newc = - superposition_with_table bag maxvar active ctable + (fun (bag, maxvar, acc) (id,nlit,plit,vl,_) -> + let bag, maxvar, _, _, acc = + if nlit = [] then bag,maxvar,[],[],acc + else List.fold_left + (superpose_literal id vl ctable false) (bag,maxvar,[],List.tl nlit,acc) nlit in - bag, maxvar, newc @ acc) + let bag, maxvar, _, _, acc = + if plit = [] then bag,maxvar,[],[],acc + else List.fold_left + (superpose_literal id vl ctable true) (bag,maxvar,[],List.tl plit,acc) plit + in + bag, maxvar, acc) (bag, maxvar, []) alist in debug (lazy "First superpositions"); @@ -708,13 +725,19 @@ module Superposition (B : Orderings.Blob) = let fresh_current, maxvar = Clauses.fresh_clause maxvar current in (* We need to put fresh_current into the bag so that all * * variables clauses refer to are known. *) - let bag, fresh_current = Terms.add_to_bag fresh_current bag in + let bag, (id,nlit,plit,vl,_) = Terms.add_to_bag fresh_current bag in (* We superpose current with active clauses *) - let bag, maxvar, additional_new_clauses = - superposition_with_table bag maxvar fresh_current atable + let bag, maxvar, _, _, new_clauses = + if nlit = [] then bag,maxvar,[],[],new_clauses + else List.fold_left + (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,new_clauses) nlit in + let bag, maxvar, _, _, new_clauses = + if plit = [] then bag,maxvar,[],[],new_clauses + else List.fold_left + (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,new_clauses) plit + in debug (lazy "Another superposition"); - let new_clauses = new_clauses @ additional_new_clauses in debug (lazy (Printf.sprintf "Demodulating %d clauses" (List.length new_clauses))); let bag, new_clauses = @@ -733,8 +756,14 @@ module Superposition (B : Orderings.Blob) = (* We superpose the goal with active clauses *) if (match goal with (_,_,_,[],_) -> true | _ -> false) then bag, maxvar, [] else - let bag, maxvar, new_goals = - superposition_with_table bag maxvar goal atable + let (id,nlit,vl) = + match goal with + | (id,nlit,[],vl,_) -> id,nlit,vl + | _ -> assert false + in + let bag, maxvar, _, _, new_goals = + List.fold_left (superpose_literal id vl atable false) + (bag,maxvar,[],List.tl nlit,[]) nlit in debug (lazy "Superposed goal with active clauses"); (* We simplify the new goals with active clauses *)