X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=c5db7a4e2ae8bc927c082bd1ceacfeee21afaba2;hb=d5e373656748835ecfe33041bbb87b786446b75f;hp=63507aea6b4aeda4c0eb16f00e52fadf09b2452a;hpb=0842258ce37ce992a0d52c813a9a5cb4c3f2bb52;p=helm.git diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 63507aea6..c5db7a4e2 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -24,7 +24,7 @@ module Superposition (B : Orderings.Blob) = exception Success of B.t Terms.bag * int * B.t Terms.clause let debug s = prerr_endline (Lazy.force s);; - (* let debug _ = ();; *) + let debug _ = ();; let enable = true;; let rec list_first f = function @@ -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 @@ -118,11 +146,12 @@ module Superposition (B : Orderings.Blob) = 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 + else (0,nlit,plit,vl,proof),maxvar in let bag, cl = - Terms.add_to_bag (0, nlit, plit, vl, proof) bag + Terms.add_to_bag cl bag in + debug (lazy (Pp.pp_clause cl)); Some (bag, maxvar, cl, literal) else ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) @@ -189,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) @@ -221,14 +350,14 @@ 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 | Some ((bag, id, lit),jump) -> demod_lit ~jump_to_right:jump bag id lit clause_ctx in - (*let cmp_bag,cmp_cl = match nlit,plit with + (*match nlit,plit with |[],[lit,_] -> let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> nlit, [l,true]) in @@ -239,8 +368,7 @@ module Superposition (B : Orderings.Blob) = in let cl,_,_ = Terms.get_from_bag id bag in bag,cl - |_ -> assert false - in*) + |_ -> assert false*) let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id else List.fold_left (fun (pre,post,bag,id) (lit,sel) -> @@ -287,6 +415,7 @@ module Superposition (B : Orderings.Blob) = | _ -> false let fold_build_new_clause bag maxvar id rule filter res clause_ctx = + debug (lazy (string_of_int (List.length res))); let (bag, maxvar), res = HExtlib.filter_map_acc (fun (bag, maxvar) (t,subst,id2,pos,dir) -> @@ -334,6 +463,7 @@ module Superposition (B : Orderings.Blob) = let is_subsumed ~unify bag maxvar (id, nlit, plit, vl, _) table = match nlit,plit with + | [Terms.Equation (l,r,ty,_) ,_],[] | [],[Terms.Equation (l,r,ty,_) ,_]-> (match rewrite_eq ~unify l r ty vl table with | None -> None @@ -352,7 +482,7 @@ module Superposition (B : Orderings.Blob) = let rec deep_eq ~unify l r ty pos contextl contextr table acc = match acc with | None -> None - | Some(bag,maxvar,(id,nlit,plit,vl,p),subst) -> + | Some(bag,maxvar,(id,nlit,plit,vl,p as cl),subst) -> let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in try @@ -362,9 +492,9 @@ module Superposition (B : Orderings.Blob) = | [Terms.Equation (l,r,ty,o),_],[] -> Terms.Equation (FoSubst.apply_subst subst1 l, FoSubst.apply_subst subst1 r, ty, o) - | _ -> assert false + | _ -> debug (lazy (Pp.pp_clause cl));assert false in - Some(bag,maxvar,(id,[],[lit,true],vl,p),Subst.concat subst1 subst) + Some(bag,maxvar,(id,[lit,true],[],vl,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> match rewrite_eq ~unify l r ty vl table with | Some (id2, dir, subst1) -> @@ -376,7 +506,7 @@ module Superposition (B : Orderings.Blob) = (match build_clause ~fresh:true bag maxvar (fun _ -> true) Terms.Superposition id_t - subst1 id id2 (pos@[2]) dir (fun l -> [],[l,true]) + subst1 id id2 (pos@[2]) dir (fun l -> [l,true],[]) with | Some (bag, maxvar, c, _) -> Some(bag,maxvar,c,newsubst) @@ -566,7 +696,6 @@ module Superposition (B : Orderings.Blob) = if no_demod then bag, clause else demodulate bag clause table in if List.exists (Clauses.are_alpha_eq_cl clause) g_actives then None else - (debug (lazy (Pp.pp_clause clause)); if (is_goal_trivial clause) then raise (Success (bag, maxvar, clause)) else @@ -583,7 +712,7 @@ module Superposition (B : Orderings.Blob) = | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> prerr_endline "Goal subsumed"; - raise (Success (bag,maxvar,cl))) + raise (Success (bag,maxvar,cl)) (* else match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) @@ -608,6 +737,8 @@ module Superposition (B : Orderings.Blob) = match nlit,plit with | [],[Terms.Equation (l,r,_,o),_] -> (let side, newside = if dir=Terms.Left2Right then l,r else r,l in + debug (lazy (Pp.pp_foterm subterm)); + debug (lazy (Pp.pp_foterm side)); try let subst = Unif.unification (* (varlist@vl)*) [] subterm side @@ -620,9 +751,7 @@ module Superposition (B : Orderings.Blob) = if o <> Terms.Lt && o <> Terms.Eq then Some (context newside, subst, id, pos, dir) else - ((*prerr_endline ("Filtering: " ^ - Pp.pp_foterm side ^ " =(< || =)" ^ - Pp.pp_foterm newside);*)None) + (debug (lazy "Filtering out..."); None) else Some (context newside, subst, id, pos, dir) with FoUnif.UnificationFailure _ -> None) @@ -727,17 +856,18 @@ module Superposition (B : Orderings.Blob) = * variables clauses refer to are known. *) let bag, (id,nlit,plit,vl,_) = Terms.add_to_bag fresh_current bag in (* We superpose current with active clauses *) - let bag, maxvar, _, _, new_clauses = - if nlit = [] then bag,maxvar,[],[],new_clauses + let bag, maxvar, _, _, additional_new_clauses = + if nlit = [] then bag,maxvar,[],[],[] else List.fold_left - (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,new_clauses) nlit + (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,[]) nlit in - let bag, maxvar, _, _, new_clauses = - if plit = [] then bag,maxvar,[],[],new_clauses + let bag, maxvar, _, _, additional_new_clauses = + if plit = [] then bag,maxvar,[],[],[] else List.fold_left - (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,new_clauses) plit + (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,additional_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 = @@ -765,7 +895,7 @@ module Superposition (B : Orderings.Blob) = List.fold_left (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,[]) nlit in - debug (lazy "Superposed goal with active clauses"); + debug (lazy (string_of_int (List.length new_goals) ^ " new goals")); (* We simplify the new goals with active clauses *) let bag, new_goals = List.fold_left