X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=0dbac61c3be98ac41ab5f212727a5f8a3be946e2;hb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;hp=93468738b59242492a79bd15514f6b9a1c43d368;hpb=b519aa529779c0a4625eb43fa9557862d8cc6617;p=helm.git diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 93468738b..0dbac61c3 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -113,7 +113,7 @@ module Superposition (B : Orderings.Blob) = | t -> Terms.Predicate t in let bag, uc = - Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag + Terms.add_to_bag (0, [], [literal,true], Terms.vars_of_term t, proof) bag in Some (bag, uc) else @@ -138,77 +138,48 @@ module Superposition (B : Orderings.Blob) = in list_first (fun (dir, is_pos, pos, (id,nlit,plit,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 = - 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) - (IDX.ClauseSet.elements cands) + 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 = match demod table vl t with | None -> (bag,t,id) @@ -217,12 +188,14 @@ module Superposition (B : Orderings.Blob) = Terms.Demodulation (ctx newside) subst id id2 pos dir with | None -> assert false - | Some (bag,(id,_,_,_)) -> + | Some (bag,(id,_,_,_,_)) -> (bag,newside,id) ;; - let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table = - match literal with + let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table = + match nlit,plit with + |[],[literal,_] -> + (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 @@ -239,7 +212,8 @@ module Superposition (B : Orderings.Blob) = if id = id2 then None else let cl,_,_ = Terms.get_from_bag id2 bag in - Some ((bag,cl),jump_to_right) + Some ((bag,cl),jump_to_right)) + | _ -> assert false; ;; let rec demodulate ~jump_to_right bag clause table = @@ -249,19 +223,12 @@ module Superposition (B : Orderings.Blob) = 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 - ;; - let are_alpha_eq cl1 cl2 = - let get_term (_,lit,_,_) = - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,_) -> + let get_term (_,nlit,plit,_,_) = + match nlit,plit with + | [], [Terms.Equation (l,r,ty,_),_] -> Terms.Node [Terms.Leaf B.eqP; ty; l ; r] + | _ -> assert false in try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true with FoUnif.UnificationFailure _ -> false @@ -288,12 +255,12 @@ 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, proof when unify -> (try ignore(Unif.unification (* vl *) [] l r); true with FoUnif.UnificationFailure _ -> false) - | _, Terms.Equation (_,_,_,_), _, _ -> false - | _, Terms.Predicate _, _, _ -> assert false + | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false + | _ -> assert false ;; let build_new_clause bag maxvar filter rule t subst id id2 pos dir = @@ -319,7 +286,7 @@ module Superposition (B : Orderings.Blob) = 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 +295,7 @@ 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 |_ -> assert false in let reverse = (dir = Terms.Left2Right) = b in @@ -351,16 +318,16 @@ 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,_) ,_]-> + (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 + Terms.Superposition id_t subst id id2 [2] dir) + | _ -> assert false ;; let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";; let is_subsumed ~unify bag maxvar c x = @@ -371,18 +338,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),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) + | _ -> 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) -> @@ -427,9 +395,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,8 +407,8 @@ 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 ;; @@ -464,7 +432,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 @@ -587,12 +555,12 @@ module Superposition (B : Orderings.Blob) = if (is_identity_clause ~unify:true 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) @@ -621,11 +589,10 @@ module Superposition (B : Orderings.Blob) = let superposition table varlist 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, _, _, (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 @@ -644,27 +611,27 @@ module Superposition (B : Orderings.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 - | Terms.Equation (l,r,ty,Terms.Lt) -> + let superposition_with_table bag maxvar (id,nlit,plit,vl,_) table = + match nlit,plit 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)) - | Terms.Equation (l,r,ty,Terms.Invertible) - | Terms.Equation (l,r,ty,Terms.Gt) -> + | [],[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) -> + | [],[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 @@ -730,8 +697,8 @@ module Superposition (B : Orderings.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 @@ -746,7 +713,7 @@ 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