X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=994a141c93f5d8215ac4f7e9930b6528aa1e6cfe;hb=5358a88f120d52959a1cd2dfc134aa872bca61ba;hp=86c77a7c0588a4851034ef8cfddd1b1b7d7bf079;hpb=9883f04161a9972f0641dd85faf224b4f2846f05;p=helm.git diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 86c77a7c0..994a141c9 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -11,12 +11,12 @@ (* $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 Subst = FoSubst - module Order = Orderings.Orderings(B) + module Order = B module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) @@ -81,7 +81,7 @@ module Superposition (B : Terms.Blob) = 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-> + | Terms.Node (hd::l) as t-> let bag,t,id1 = f bag t pos ctx id in if id = id1 then let bag, l, _, id = @@ -92,10 +92,11 @@ module Superposition (B : Terms.Blob) = 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 + (bag, [hd], List.tl l, id) l in bag, Terms.Node l, id else bag,t,id1 + | _ -> assert false in aux bag pos ctx id t ;; @@ -103,7 +104,7 @@ module Superposition (B : Terms.Blob) = let build_clause bag filter rule t subst id id2 pos dir = let proof = Terms.Step(rule,id,id2,dir,pos,subst) in let t = Subst.apply_subst subst t in - if filter t then + if filter subst then let literal = match t with | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> @@ -128,6 +129,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 = @@ -143,11 +145,17 @@ module Superposition (B : Terms.Blob) = try let subst = prof_demod_u.HExtlib.profile - (Unif.unification (varlist@vl) varlist subterm) side + (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 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 @@ -282,7 +290,7 @@ module Superposition (B : Terms.Blob) = 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 + (try ignore(Unif.unification (* vl *) [] l r); true with FoUnif.UnificationFailure _ -> false) | _, Terms.Equation (_,_,_,_), _, _ -> false | _, Terms.Predicate _, _, _ -> assert false @@ -336,7 +344,7 @@ 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 @@ -367,7 +375,7 @@ module Superposition (B : Terms.Blob) = 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) -> @@ -474,7 +482,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_unit_clause maxvar IDX.DT.empty clause in let bag, alist, atable = List.fold_left (fun (bag, alist, atable) c -> @@ -482,7 +490,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_unit_clause maxvar atable c) (bag,[],IDX.DT.empty) alist in bag, Some (clause, (alist,atable)) @@ -495,7 +503,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_unit_clause maxvar atable cl in (* Simplification of new_clause with : * * - actives and cl if new_clause is not cl * @@ -506,7 +514,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_unit_clause maxvar IDX.DT.empty clause in let bag, newa, alist, atable = List.fold_left (fun (bag, newa, alist, atable) c -> @@ -516,7 +524,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_unit_clause maxvar atable c else bag, c1 :: newa, alist, atable) (bag,[],[],IDX.DT.empty) alist @@ -558,7 +566,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_unit_clause maxvar atable clause) in keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable) bag (newa@tl) @@ -620,9 +628,9 @@ module Superposition (B : Terms.Blob) = 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 @@ -649,24 +657,35 @@ module Superposition (B : Terms.Blob) = (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) -> 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) -> - fold_build_new_clause bag maxvar id Terms.Superposition - (function (* Riazanov: p.33 condition (iv) *) - | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq -> - Order.compare_terms l r <> Terms.Eq - | _ -> assert false) - ((all_positions [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) - r (superposition table vl)) @ - (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) -> + 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 + let o = Order.compare_terms l r in + o <> avoid && o <> Terms.Eq + in + let bag, maxvar,r_terms = + fold_build_new_clause bag maxvar id Terms.Superposition + (filtering Terms.Gt) + (all_positions [3] + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + r (superposition table vl)) + 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)) + in + bag, maxvar, r_terms @ l_terms | _ -> assert false ;; @@ -676,7 +695,7 @@ module Superposition (B : Terms.Blob) = (* 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_unit_clause maxvar IDX.DT.empty current in (* let bag, (alist, atable) = let bag, alist = HExtlib.filter_map_acc (simplify ctable) bag alist @@ -698,7 +717,7 @@ module Superposition (B : Terms.Blob) = (* 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_unit_clause maxvar atable current in debug "Indexed"; let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in @@ -711,8 +730,8 @@ module Superposition (B : Terms.Blob) = in debug "Another superposition"; let new_clauses = new_clauses @ additional_new_clauses in - debug (Printf.sprintf "Demodulating %d clauses" - (List.length new_clauses)); + 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