From: denes Date: Fri, 25 Sep 2009 22:14:33 +0000 (+0000) Subject: Ported innermost strategy for demodulation from trunk X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d5e373656748835ecfe33041bbb87b786446b75f Ported innermost strategy for demodulation from trunk --- diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 35e10ad42..8ffa24a0f 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,9 +1,10 @@ pp.cmi: terms.cmi foSubst.cmi: terms.cmi +foUtils.cmi: terms.cmi +foUnif.cmi: terms.cmi orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi orderings.cmi +clauses.cmi: terms.cmi orderings.cmi index.cmi: terms.cmi orderings.cmi -foUnif.cmi: terms.cmi orderings.cmi superposition.cmi: terms.cmi orderings.cmi index.cmi stats.cmi: terms.cmi orderings.cmi paramod.cmi: terms.cmi orderings.cmi @@ -16,24 +17,30 @@ pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi -orderings.cmo: terms.cmi pp.cmi orderings.cmi -orderings.cmx: terms.cmx pp.cmx orderings.cmi -foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi -foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi -index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi -foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi +foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx foSubst.cmx foUtils.cmi +foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +orderings.cmo: terms.cmi pp.cmi foUtils.cmi foUnif.cmi foSubst.cmi \ + orderings.cmi +orderings.cmx: terms.cmx pp.cmx foUtils.cmx foUnif.cmx foSubst.cmx \ + orderings.cmi +clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \ + clauses.cmi +clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \ + clauses.cmi +index.cmo: terms.cmi orderings.cmi foUtils.cmi clauses.cmi index.cmi +index.cmx: terms.cmx orderings.cmx foUtils.cmx clauses.cmx index.cmi superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi + foUnif.cmi foSubst.cmi clauses.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo: terms.cmi stats.cmi -stats.cmx: terms.cmx stats.cmi + foUnif.cmx foSubst.cmx clauses.cmx superposition.cmi +stats.cmo: terms.cmi pp.cmi stats.cmi +stats.cmx: terms.cmx pp.cmx stats.cmi paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi + foUtils.cmi foUnif.cmi clauses.cmi paramod.cmi paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi + foUtils.cmx foUnif.cmx clauses.cmx paramod.cmi nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index ff34709e9..2b52ce34a 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -94,7 +94,3 @@ let nparamod rdb metasenv subst context (g_t,g_ty) table = proofterm, metasenv, subst) solutions ;; - - - - diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index fd7be3b7e..c5db7a4e2 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -101,7 +101,35 @@ module Superposition (B : Orderings.Blob) = in aux bag pos ctx id lit t ;; - + + let visit bag pos ctx id lit t f = + let rec aux bag pos ctx id subst lit = function + | Terms.Leaf _ as t -> + let bag,subst,t,id,lit = f bag t pos ctx id lit + in assert (subst=[]); bag,t,id,lit + | Terms.Var i as t -> + let t= Subst.apply_subst subst t in + bag,t,id,lit + | Terms.Node (hd::l) -> + let bag, l, _, id,lit = + List.fold_left + (fun (bag,pre,post,id,lit) t -> + let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in + let newpos = (List.length pre)::pos in + let bag,newt,id,lit = aux bag newpos newctx id subst lit t in + if post = [] then bag, pre@[newt], [], id, lit + else bag, pre @ [newt], List.tl post, id, lit) + (bag, [hd], List.map (Subst.apply_subst subst) (List.tl l), id, lit) l + in + let bag,subst,t,id1,lit = f bag (Terms.Node l) pos ctx id lit + in + if id1 = id then (assert (subst=[]); bag,t,id,lit) + else aux bag pos ctx id1 subst lit t + | _ -> assert false + in + aux bag pos ctx id [] lit t + ;; + 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 @@ -190,6 +218,106 @@ module Superposition (B : Orderings.Blob) = prof_demod.HExtlib.profile (demod table varlist) x ;; + let mydemod table varlist subterm = + let cands = + prof_demod_r.HExtlib.profile + (IDX.DT.retrieve_generalizations table) subterm + in + list_first + (fun (dir, is_pos, pos, (id,nlit,plit,vl,_)) -> + match (nlit,plit) with + | [],[(lit,_)] -> + (match lit with + | Terms.Predicate _ -> assert false + | Terms.Equation (l,r,_,o) -> + let side, newside = if dir=Terms.Left2Right then l,r else r,l in + try + let subst = + prof_demod_u.HExtlib.profile + (Unif.unification (* (varlist@vl) *) varlist subterm) side + in + let iside = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) side + in + let inewside = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) newside + in + if o = Terms.Incomparable || o = Terms.Invertible then + let o = + prof_demod_o.HExtlib.profile + (Order.compare_terms inewside) iside in + (* Riazanov, pp. 45 (ii) *) + if o = Terms.Lt then + Some (newside, subst, id, dir) + else + ((*prerr_endline ("Filtering: " ^ + Pp.pp_foterm side ^ " =(< || =)" ^ + Pp.pp_foterm newside ^ " coming from " ^ + Pp.pp_unit_clause uc );*)None) + else + Some (newside, subst, id, dir) + with FoUnif.UnificationFailure _ -> None) + | _ -> assert false) + (IDX.ClauseSet.elements cands) + ;; + + let ctx_demod table vl clause_ctx bag t pos ctx id lit = + match mydemod table vl t with + | None -> (bag,[],t,id,lit) + | Some (newside, subst, id2, dir) -> + let inewside = Subst.apply_subst subst newside in + match build_clause ~fresh:false bag 0 (fun _ -> true) + Terms.Demodulation (ctx inewside) subst id id2 pos dir clause_ctx + with + | None -> assert false + | Some (bag,_,(id,_,_,_,_),lit) -> + (bag,subst,newside,id,lit) + ;; + + let rec demodulate bag (id,nlit,plit,vl,proof) table = + let rec demod_lit ~jump_to_right bag id lit clause_ctx = + (match lit with + | Terms.Predicate t -> assert false + | Terms.Equation (l,r,ty,_) -> assert false + (*let bag,l,id1,lit = + visit bag [2] + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id lit l + (ctx_demod table vl clause_ctx) + in + let bag,_,id2,lit = + visit bag [3] + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 lit r + (ctx_demod table vl clause_ctx) + in + let cl,_,_ = Terms.get_from_bag id2 bag in + bag,id2,cl *) ) + in + let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id + else List.fold_left + (fun (pre,post,bag,id) (lit,sel) -> + let bag, id, lit = + demod_lit ~jump_to_right:false bag id lit (fun l -> pre@[l,sel]@post,plit) + in + if post=[] then pre@[(lit,sel)],[],bag,id + else pre@[(lit,sel)],List.tl post,bag,id) + ([],List.tl nlit, bag, id) nlit + in + let _,_,bag,id = if plit = [] then plit,[],bag,id + else List.fold_left + (fun (pre,post,bag,id) (lit,sel) -> + let bag, id, lit = + demod_lit ~jump_to_right:false bag id lit (fun l -> nlit,pre@[l,sel]@post) + in + if post=[] then pre@[(lit,sel)],[],bag,id + else pre@[(lit,sel)],List.tl post,bag,id) + ([],List.tl plit, bag, id) plit + in + let cl,_,_ = Terms.get_from_bag id bag in + bag,cl + ;; + let parallel_demod table vl clause_ctx bag t pos ctx id lit = match demod table vl t with | None -> (bag,t,id,lit) @@ -222,7 +350,7 @@ module Superposition (B : Orderings.Blob) = Some ((bag,id2,lit),jump_to_right) ;; - let rec demodulate bag (id,nlit,plit,vl,proof) table = + let rec demodulate_old bag (id,nlit,plit,vl,proof) table = let rec demod_lit ~jump_to_right bag id lit clause_ctx = match demodulate_once ~jump_to_right bag id lit vl table clause_ctx with | None -> bag, id, lit diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index ad780c82c..c6877901b 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -75,5 +75,4 @@ module Superposition (B : Orderings.Blob) : B.t Terms.clause -> bool - end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index c15c85af2..76eda3717 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -85,7 +85,7 @@ type 'a bag = int (* max ID *) module type Blob = sig (* Blob is the type for opaque leaves: - * - checking equlity should be efficient + * - checking equality should be efficient * - atoms have to be equipped with a total order relation *) type t