X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=c5db7a4e2ae8bc927c082bd1ceacfeee21afaba2;hb=d5e373656748835ecfe33041bbb87b786446b75f;hp=93468738b59242492a79bd15514f6b9a1c43d368;hpb=39a2078b0e835d39895a5b6c0862d668ece544f3;p=helm.git diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 93468738b..c5db7a4e2 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -14,15 +14,16 @@ module Superposition (B : Orderings.Blob) = struct module IDX = Index.Index(B) - module Unif = FoUnif.Founif(B) + module Unif = FoUnif.FoUnif(B) module Subst = FoSubst module Order = B module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) + module Clauses = Clauses.Clauses(B) exception Success of B.t Terms.bag * int * B.t Terms.clause - let debug s = prerr_endline s;; + let debug s = prerr_endline (Lazy.force s);; let debug _ = ();; let enable = true;; @@ -77,31 +78,59 @@ module Superposition (B : Orderings.Blob) = aux pos ctx t ;; - let parallel_positions bag pos ctx id t f = - let rec aux bag pos ctx id = function - | Terms.Leaf _ as t -> f bag t pos ctx id - | Terms.Var _ as t -> bag,t,id + let parallel_positions bag pos ctx id lit t f = + let rec aux bag pos ctx id lit = function + | Terms.Leaf _ as t -> f bag t pos ctx id lit + | Terms.Var _ as t -> bag,t,id,lit | Terms.Node (hd::l) as t-> - let bag,t,id1 = f bag t pos ctx id in + let bag,t,id1,lit = f bag t pos ctx id lit in if id = id1 then - let bag, l, _, id = + let bag, l, _, id, lit = List.fold_left - (fun (bag,pre,post,id) t -> + (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 = aux bag newpos newctx id t in - if post = [] then bag, pre@[newt], [], id - else bag, pre @ [newt], List.tl post, id) - (bag, [hd], List.tl l, id) l + let bag,newt,id,lit = aux bag newpos newctx id lit t in + if post = [] then bag, pre@[newt], [], id,lit + else bag, pre @ [newt], List.tl post, id, lit) + (bag, [hd], List.tl l, id,lit) l in - bag, Terms.Node l, id - else bag,t,id1 + bag, Terms.Node l, id, lit + else bag,t,id1,lit | _ -> assert false in - aux bag pos ctx id t + 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 bag filter rule t subst id id2 pos dir = + + 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 @@ -112,16 +141,25 @@ module Superposition (B : Orderings.Blob) = Terms.Equation (l, r, ty, o) | t -> Terms.Predicate t in - let bag, uc = - Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag + let nlit,plit = clause_ctx literal in + 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 (0,nlit,plit,vl,proof),maxvar in - Some (bag, uc) + let bag, cl = + 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) ;; 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 ;; @@ -138,7 +176,58 @@ module Superposition (B : Orderings.Blob) = in list_first (fun (dir, is_pos, pos, (id,nlit,plit,vl,_)) -> - match lit with + 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 side = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) side + in + let newside = + 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 newside) side 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_clause uc );*)None) + else + Some (newside, subst, id, dir) + with FoUnif.UnificationFailure _ -> None) + | _ -> None) + (IDX.ClauseSet.elements cands) + ;; + let prof_demod = HExtlib.profile ~enable "demod";; + let demod table varlist x = + 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 @@ -147,18 +236,18 @@ module Superposition (B : Orderings.Blob) = prof_demod_u.HExtlib.profile (Unif.unification (* (varlist@vl) *) varlist subterm) side in - let side = + let iside = prof_demod_s.HExtlib.profile (Subst.apply_subst subst) side in - let newside = + 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 newside) side in + (Order.compare_terms inewside) iside in (* Riazanov, pp. 45 (ii) *) if o = Terms.Lt then Some (newside, subst, id, dir) @@ -166,121 +255,144 @@ module Superposition (B : Orderings.Blob) = ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm side ^ " =(< || =)" ^ Pp.pp_foterm newside ^ " coming from " ^ - Pp.pp_clause uc );*)None) + Pp.pp_unit_clause uc );*)None) else Some (newside, subst, id, dir) with FoUnif.UnificationFailure _ -> None) + | _ -> assert false) (IDX.ClauseSet.elements cands) ;; - let prof_demod = HExtlib.profile ~enable "demod";; - let demod table varlist x = - prof_demod.HExtlib.profile (demod table varlist) x - ;; - let demodulate_once_old ~jump_to_right bag (id, literal, vl, pr) table = - match literal with + 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,_) -> - let left_position = if jump_to_right then None else - first_position [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l - (demod table vl) - in - match left_position with - | Some (newt, subst, id2, dir, pos) -> - begin - match build_clause bag (fun _ -> true) Terms.Demodulation - newt subst id id2 pos dir - with - | None -> assert false - | Some x -> Some (x,false) - end - | None -> - match first_position - [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r - (demod table vl) - with - | None -> None - | Some (newt, subst, id2, dir, pos) -> - match build_clause bag (fun _ -> true) - Terms.Demodulation newt subst id id2 pos dir - with - | None -> assert false - | Some x -> Some (x,true) + | 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 bag t pos ctx id = + let parallel_demod table vl clause_ctx bag t pos ctx id lit = match demod table vl t with - | None -> (bag,t,id) + | None -> (bag,t,id,lit) | Some (newside, subst, id2, dir) -> - match build_clause bag (fun _ -> true) - Terms.Demodulation (ctx newside) subst id id2 pos dir + 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,_,_,_)) -> - (bag,newside,id) + | Some (bag,_,(id,_,_,_,_),lit) -> + (bag,newside,id,lit) ;; - let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table = + let demodulate_once ~jump_to_right bag id literal vl table clause_ctx = match literal with | Terms.Predicate t -> assert false - | Terms.Equation (l,r,ty,_) -> - let bag,l,id1 = if jump_to_right then (bag,l,id) else + | Terms.Equation (l,r,ty,_) as lit -> + let bag,l,id1,lit = if jump_to_right then (bag,l,id,lit) else parallel_positions bag [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l - (parallel_demod table vl) + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id lit l + (parallel_demod table vl clause_ctx) in let jump_to_right = id1 = id in - let bag,r,id2 = + let bag,r,id2,lit = parallel_positions bag [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r - (parallel_demod table vl) + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 lit r + (parallel_demod table vl clause_ctx) in if id = id2 then None else - let cl,_,_ = Terms.get_from_bag id2 bag in - Some ((bag,cl),jump_to_right) - ;; - - let rec demodulate ~jump_to_right bag clause table = - match demodulate_once ~jump_to_right bag clause table with - | None -> bag, clause - | Some ((bag, clause),r) -> demodulate ~jump_to_right:r - bag clause table - ;; - - let rec demodulate_old ~jump_to_right bag clause table = - match demodulate_once_old ~jump_to_right bag clause table with - | None -> bag, clause - | Some ((bag, clause),r) -> demodulate_old ~jump_to_right:r - bag clause table + Some ((bag,id2,lit),jump_to_right) ;; - let are_alpha_eq cl1 cl2 = - let get_term (_,lit,_,_) = - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,_) -> - Terms.Node [Terms.Leaf B.eqP; ty; l ; r] + 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 - try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true - with FoUnif.UnificationFailure _ -> false - ;; - - let demodulate bag clause table = -(* let (bag1,c1), (_,c2) =*) - demodulate ~jump_to_right:false bag clause table -(* demodulate_old ~jump_to_right:false bag clause table *) -(* in - if are_alpha_eq c1 c2 then bag1,c1 - else begin - prerr_endline (Pp.pp_clause c1); - prerr_endline (Pp.pp_clause c2); - prerr_endline "Bag :"; - prerr_endline (Pp.pp_bag bag1); - assert false - end*) + (*match nlit,plit with + |[],[lit,_] -> + let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> nlit, [l,true]) + in + let cl,_,_ = Terms.get_from_bag id bag in + bag,cl + |[lit,_],[] -> + let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> [l,true],[]) + in + let cl,_,_ = Terms.get_from_bag id bag in + bag,cl + |_ -> assert false*) + 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 prof_demodulate = HExtlib.profile ~enable "demodulate";; let demodulate bag clause x = prof_demodulate.HExtlib.profile (demodulate bag clause) x @@ -288,38 +400,35 @@ module Superposition (B : Orderings.Blob) = (* move away *) let is_identity_clause ~unify = function - | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true - | _, Terms.Equation (l,r,_,_), vl, proof when unify -> + | _, [], [Terms.Equation (_,_,_,Terms.Eq),_], _, _ -> true + | _, [], [Terms.Equation (l,r,_,_),_], vl, _ when unify -> (try ignore(Unif.unification (* vl *) [] l r); true with FoUnif.UnificationFailure _ -> false) - | _, Terms.Equation (_,_,_,_), _, _ -> false - | _, Terms.Predicate _, _, _ -> assert 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 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 is_goal_trivial = function + | _, [Terms.Equation (_,_,_,Terms.Eq),_], [], _, _ -> true + | _, [Terms.Equation (l,r,_,_),_], [], vl, _ -> + (try ignore(Unif.unification (* vl *) [] l r); true + with FoUnif.UnificationFailure _ -> false) + | _ -> false - let fold_build_new_clause bag maxvar id rule filter res = + 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) -> - 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 ;; - + (* Tries to rewrite an equality to identity, using unit equalities in table *) let rewrite_eq ~unify l r ty vl table = let retrieve = if unify then IDX.DT.retrieve_unifiables else IDX.DT.retrieve_generalizations in @@ -328,7 +437,8 @@ module Superposition (B : Orderings.Blob) = 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 + | (d,_,_, (id,[],[Terms.Equation (l,r,ty,_),_],vl,_))-> id, d, l, r, vl + | (d,_,_, (id,[Terms.Equation (l,r,ty,_),_],[],vl,_))-> id, d, l, r, vl |_ -> assert false in let reverse = (dir = Terms.Left2Right) = b in @@ -351,16 +461,17 @@ module Superposition (B : Orderings.Blob) = aux (cands1 @ cands2) ;; - let is_subsumed ~unify bag maxvar (id, lit, vl, _) table = - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,_) -> - match rewrite_eq ~unify l r ty vl table with + 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 | 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";; let is_subsumed ~unify bag maxvar c x = @@ -371,18 +482,19 @@ 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,lit,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 let subst1 = Unif.unification (* vl *) [] l r in let lit = - match lit with Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,o) -> + match nlit,plit with + | [Terms.Equation (l,r,ty,o),_],[] -> Terms.Equation (FoSubst.apply_subst subst1 l, FoSubst.apply_subst subst1 r, ty, o) + | _ -> debug (lazy (Pp.pp_clause cl));assert false in - Some(bag,maxvar,(id,lit,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) -> @@ -392,11 +504,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 -> @@ -427,9 +539,9 @@ module Superposition (B : Orderings.Blob) = let rec orphan_murder bag acc i = match Terms.get_from_bag i bag with - | (_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc) - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc) - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ -> + | (_,_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc) + | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc) + | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ -> if (List.mem i acc) then (false,acc) else match orphan_murder bag acc i1 with | (true,acc) -> (true,acc) @@ -439,10 +551,10 @@ module Superposition (B : Orderings.Blob) = ;; let orphan_murder bag actives cl = - let (id,_,_,_) = cl in - let actives = List.map (fun (i,_,_,_) -> i) actives in + let (id,_,_,_,_) = cl in + let actives = List.map (fun (i,_,_,_,_) -> i) actives in let (res,_) = orphan_murder bag actives id in - if res then debug "Orphan murdered"; res + if res then debug (lazy "Orphan murdered"); res ;; let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";; let orphan_murder bag actives x = @@ -464,7 +576,7 @@ module Superposition (B : Orderings.Blob) = let simplify table maxvar bag clause = match simplify table maxvar bag clause with | bag, None -> - let (id,_,_,_) = clause in + let (id,_,_,_,_) = clause in let (_,_,iter) = Terms.get_from_bag id bag in Terms.replace_in_bag (clause,true,iter) bag, None | bag, Some clause -> bag, Some clause @@ -583,16 +695,16 @@ module Superposition (B : Orderings.Blob) = let bag, clause = if no_demod then bag, clause else demodulate bag clause table in - if List.exists (are_alpha_eq clause) g_actives then None else - if (is_identity_clause ~unify:true clause) + if List.exists (Clauses.are_alpha_eq_cl clause) g_actives then None else + if (is_goal_trivial clause) then raise (Success (bag, maxvar, clause)) else - let (id,lit,vl,_) = clause in + let (id,nlit,plit,vl,_) = clause in if vl = [] then Some (bag,clause) else let l,r,ty = - match lit with - | Terms.Equation(l,r,ty,_) -> l,r,ty + match nlit,plit with + | [Terms.Equation(l,r,ty,_),_],[] -> l,r,ty | _ -> assert false in match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) @@ -618,14 +730,15 @@ 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,lit,vl,_ (*as uc*))) -> - 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 + (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 + debug (lazy (Pp.pp_foterm subterm)); + debug (lazy (Pp.pp_foterm side)); try let subst = Unif.unification (* (varlist@vl)*) [] subterm side @@ -638,32 +751,30 @@ 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) + | _ -> assert false) (IDX.ClauseSet.elements cands) ;; (* Superposes selected equation with equalities in table *) - let superposition_with_table bag maxvar (id,selected,vl,_) table = - match selected with - | Terms.Predicate _ -> assert false + 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)) + 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)) + 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 @@ -676,19 +787,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) = @@ -702,40 +826,54 @@ module Superposition (B : Orderings.Blob) = in bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist) in*) - debug "Simplified active clauses with fact"; + debug (lazy "Simplified active clauses with fact"); (* 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 "First superpositions"; + debug (lazy "First superpositions"); (* We add current to active clauses so that it can be * * superposed with itself *) let alist, atable = current :: alist, IDX.index_clause atable current in - debug "Indexed"; - let fresh_current, maxvar = Utils.fresh_clause maxvar current in + debug (lazy "Indexed"); + 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, _, _, additional_new_clauses = + if nlit = [] then bag,maxvar,[],[],[] + else List.fold_left + (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,[]) nlit in - debug "Another superposition"; - let new_clauses = new_clauses @ additional_new_clauses in - debug (Printf.sprintf "Demodulating %d clauses" - (List.length 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,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 = HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses in - debug "Demodulated new clauses"; + debug (lazy "Demodulated new clauses"); bag, maxvar, (alist, atable), new_clauses ;; @@ -746,12 +884,18 @@ module Superposition (B : Orderings.Blob) = let infer_left bag maxvar goal (_alist, atable) = (* We superpose the goal with active clauses *) - if (match goal with (_,_,[],_) -> true | _ -> false) then bag, maxvar, [] + 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 "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 @@ -761,7 +905,7 @@ module Superposition (B : Orderings.Blob) = | Some (bag,g) -> bag,g::acc) (bag, []) new_goals in - debug "Simplified new goals with active clauses"; + debug (lazy "Simplified new goals with active clauses"); bag, maxvar, List.rev new_goals ;;