X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=63507aea6b4aeda4c0eb16f00e52fadf09b2452a;hb=0842258ce37ce992a0d52c813a9a5cb4c3f2bb52;hp=1a588043409a66b5f40b07014885accfe653b4a1;hpb=d807d5e4fa129504669f775f4f832a1a7eb920a0;p=helm.git diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 1a5880434..63507aea6 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -11,19 +11,20 @@ (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *) -module Superposition (B : Terms.Blob) = +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 = Orderings.Orderings(B) + 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.unit_clause + exception Success of B.t Terms.bag * int * B.t Terms.clause - let debug s = prerr_endline s;; - let debug _ = ();; + let debug s = prerr_endline (Lazy.force s);; + (* let debug _ = ();; *) let enable = true;; let rec list_first f = function @@ -77,30 +78,31 @@ module Superposition (B : Terms.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 - | Terms.Node l as t-> - let bag,t,id1 = f bag t pos ctx id in + 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,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, [], 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 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 @@ -111,16 +113,24 @@ module Superposition (B : Terms.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 cl,maxvar + in + let bag, cl = + Terms.add_to_bag (0, nlit, plit, vl, proof) bag in - Some (bag, uc) + 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 ;; @@ -128,6 +138,7 @@ module Superposition (B : Terms.Blob) = let prof_demod_u = HExtlib.profile ~enable "demod.unify";; let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";; let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";; + let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";; let demod table varlist subterm = let cands = @@ -135,144 +146,125 @@ module Superposition (B : Terms.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, (id,lit,vl,_)) -> - 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 = Subst.apply_subst subst side in - let newside = Subst.apply_subst subst newside in - if o = Terms.Incomparable 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_unit_clause uc );*)None) - else - Some (newside, subst, id, dir) - with FoUnif.UnificationFailure _ -> None) - (IDX.ClauseSet.elements cands) + (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 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 demodulate_once_old ~jump_to_right bag (id, literal, vl, pr) table = - match literal 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) - ;; - - 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 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 + |[],[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 + 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 - 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_unit_clause c1); - prerr_endline (Pp.pp_unit_clause c2); - prerr_endline "Bag :"; - prerr_endline (Pp.pp_bag bag1); - assert false - end*) + 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 @@ -280,38 +272,34 @@ module Superposition (B : Terms.Blob) = (* move away *) let is_identity_clause ~unify = function - | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true - | _, Terms.Equation (l,r,_,_), vl, proof when unify -> - (try ignore(Unif.unification vl [] l r); true + | _, [], [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 = 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 @@ -320,7 +308,8 @@ module Superposition (B : Terms.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 @@ -336,23 +325,23 @@ module Superposition (B : Terms.Blob) = | [] -> None | (id2,dir,c,vl1)::tl -> try - let subst = Unif.unification (vl@vl1) locked_vars c t in + let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in Some (id2, dir, subst) with FoUnif.UnificationFailure _ -> aux tl in 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,_) ,_]-> + (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 = @@ -363,18 +352,19 @@ module Superposition (B : Terms.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),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 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) + | _ -> 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) -> @@ -384,11 +374,11 @@ module Superposition (B : Terms.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 -> @@ -419,9 +409,9 @@ module Superposition (B : Terms.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) @@ -431,10 +421,10 @@ module Superposition (B : Terms.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 = @@ -456,7 +446,7 @@ module Superposition (B : Terms.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 @@ -474,7 +464,7 @@ module Superposition (B : Terms.Blob) = match simplify atable maxvar bag new_clause with | bag,None -> bag,None (* new_clause has been discarded *) | bag,(Some clause) -> - let ctable = IDX.index_unit_clause IDX.DT.empty clause in + let ctable = IDX.index_clause IDX.DT.empty clause in let bag, alist, atable = List.fold_left (fun (bag, alist, atable) c -> @@ -482,7 +472,7 @@ module Superposition (B : Terms.Blob) = |bag,None -> (bag,alist,atable) (* an active clause as been discarded *) |bag,Some c1 -> - bag, c :: alist, IDX.index_unit_clause atable c) + bag, c :: alist, IDX.index_clause atable c) (bag,[],IDX.DT.empty) alist in bag, Some (clause, (alist,atable)) @@ -495,7 +485,7 @@ module Superposition (B : Terms.Blob) = let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause = let atable1 = if new_cl then atable else - IDX.index_unit_clause atable cl + IDX.index_clause atable cl in (* Simplification of new_clause with : * * - actives and cl if new_clause is not cl * @@ -506,7 +496,7 @@ module Superposition (B : Terms.Blob) = | bag,Some clause -> (* Simplification of each active clause with clause * * which is the simplified form of new_clause *) - let ctable = IDX.index_unit_clause IDX.DT.empty clause in + let ctable = IDX.index_clause IDX.DT.empty clause in let bag, newa, alist, atable = List.fold_left (fun (bag, newa, alist, atable) c -> @@ -516,7 +506,7 @@ module Superposition (B : Terms.Blob) = |bag,Some c1 -> if (c1 == c) then bag, newa, c :: alist, - IDX.index_unit_clause atable c + IDX.index_clause atable c else bag, c1 :: newa, alist, atable) (bag,[],[],IDX.DT.empty) alist @@ -558,7 +548,7 @@ module Superposition (B : Terms.Blob) = | bag,(None, Some _) -> bag,None | bag,(Some cl1, Some (clause, (alist,atable), newa)) -> let alist,atable = - (clause::alist, IDX.index_unit_clause atable clause) + (clause::alist, IDX.index_clause atable clause) in keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable) bag (newa@tl) @@ -575,16 +565,17 @@ module Superposition (B : Terms.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 + (debug (lazy (Pp.pp_clause clause)); + 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) @@ -592,7 +583,7 @@ module Superposition (B : Terms.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) @@ -610,19 +601,18 @@ module Superposition (B : Terms.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 try let subst = - Unif.unification (varlist@vl) [] subterm side + Unif.unification (* (varlist@vl)*) [] subterm side in - if o = Terms.Incomparable then + if o = Terms.Incomparable || o = Terms.Invertible then let side = Subst.apply_subst subst side in let newside = Subst.apply_subst subst newside in let o = Order.compare_terms side newside in @@ -636,25 +626,26 @@ module Superposition (B : Terms.Blob) = 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 @@ -667,66 +658,92 @@ module Superposition (B : Terms.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; l; x ]) - r (superposition table vl)) + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) + 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) = (* We demodulate actives clause with current until all * * active clauses are reduced w.r.t each other *) (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *) - let ctable = IDX.index_unit_clause IDX.DT.empty current in + let ctable = IDX.index_clause IDX.DT.empty current in (* let bag, (alist, atable) = let bag, alist = HExtlib.filter_map_acc (simplify ctable) bag alist in - bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist) + 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_unit_clause atable current + current :: alist, IDX.index_clause atable current in - debug "Indexed"; - let fresh_current, maxvar = Utils.fresh_unit_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, _, _, 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 - 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, _, _, 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"); + 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 ;; @@ -737,12 +754,18 @@ module Superposition (B : Terms.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 "Superposed goal with active clauses"); (* We simplify the new goals with active clauses *) let bag, new_goals = List.fold_left @@ -752,7 +775,7 @@ module Superposition (B : Terms.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 ;;