From: denes Date: Thu, 30 Jul 2009 21:30:08 +0000 (+0000) Subject: Ported demodulation on clauses X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b714e87e96f14f332a5157567a4c62a4b28fa8eb;p=helm.git Ported demodulation on clauses --- diff --git a/helm/software/components/ng_paramodulation/clauses.ml b/helm/software/components/ng_paramodulation/clauses.ml index 895d3865e..5955fcae1 100644 --- a/helm/software/components/ng_paramodulation/clauses.ml +++ b/helm/software/components/ng_paramodulation/clauses.ml @@ -20,6 +20,7 @@ module type Blob = module Clauses (B : Orderings.Blob) = struct module Order = B;; module Utils = FoUtils.Utils(B) + module Unif = FoUnif.FoUnif(B) let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2 let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2 @@ -81,4 +82,21 @@ module Clauses (B : Orderings.Blob) = struct id1 - id2 ;; + let are_alpha_eq_cl cl1 cl2 = + let (_,nlit1,plit1,_,_) = cl1 in + let (_,nlit2,plit2,_,_) = cl2 in + let alpha_eq (lit1,_) (lit2,_) = + 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] + in + try ignore(Unif.alpha_eq (get_term lit1) (get_term lit2)) ; true + with FoUnif.UnificationFailure _ -> false + in + try (List.for_all2 alpha_eq nlit1 nlit2 && List.for_all2 alpha_eq plit1 plit2) + with Invalid_argument _ -> false + ;; + end diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli index 885e97607..81738c2a4 100644 --- a/helm/software/components/ng_paramodulation/clauses.mli +++ b/helm/software/components/ng_paramodulation/clauses.mli @@ -37,4 +37,7 @@ module Clauses (B : Orderings.Blob) : val compare_passive_clauses_age : int * B.t Terms.clause -> int * B.t Terms.clause -> int + val are_alpha_eq_cl : + B.t Terms.clause -> B.t Terms.clause -> bool + end diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 89b390b07..5eb3c43a5 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -186,12 +186,13 @@ let compare_terms o x y = | _ -> assert false ;; -let are_invertible relocate alpha_eq l r = - let varlist = Terms.vars_of_term l in +let are_invertible relocate alpha_eq eq_foterm l r = + let varlist = (Terms.vars_of_term l)@(Terms.vars_of_term r) in let maxvar = List.fold_left max 0 varlist in let _,_,subst = relocate maxvar varlist FoSubst.id_subst in - let l = FoSubst.apply_subst subst l in - try (ignore(alpha_eq l r);true) with + let newl = FoSubst.apply_subst subst l in + let newr = FoSubst.apply_subst subst r in + try (let subst = alpha_eq l newr in eq_foterm newl (FoSubst.apply_subst subst r)) with FoUnif.UnificationFailure _ -> false;; module NRKBO (B : Terms.Blob) = struct @@ -204,7 +205,7 @@ module NRKBO (B : Terms.Blob) = struct let eq_foterm = eq_foterm B.eq;; - let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;; + let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;; let compute_clause_weight = compute_clause_weight;; @@ -242,7 +243,7 @@ module KBO (B : Terms.Blob) = struct let eq_foterm = eq_foterm B.eq;; - let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;; + let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;; let compute_clause_weight = compute_clause_weight;; let compute_goal_weight = compute_goal_weight;; @@ -312,7 +313,7 @@ module LPO (B : Terms.Blob) = struct let eq_foterm = eq_foterm B.eq;; - let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;; + let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;; let compute_clause_weight = compute_clause_weight;; let compute_goal_weight = compute_goal_weight;; diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 1f64314c9..4a6886205 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -12,7 +12,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let debug s = prerr_endline (Lazy.force s) ;; -let debug _ = ();; +(* let debug _ = ();; *) let monster = 100;; @@ -64,15 +64,15 @@ module Paramod (B : Orderings.Blob) = struct module WeightPassiveSet = Set.Make(WeightOrderedPassives) module AgePassiveSet = Set.Make(AgeOrderedPassives) - let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl = - let cl = if no_weight then (0,cl) - else Clauses.mk_passive_clause cl in + let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl = + let (w,cl) = Clauses.mk_passive_clause cl in + let cl = (w+bonus_weight,cl) in WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a ;; - let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g = - let g = if no_weight then (0,g) - else Clauses.mk_passive_goal g in + let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g = + let (w,g) = Clauses.mk_passive_goal g in + let g = (w+bonus_weight,g) in WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a ;; @@ -82,20 +82,20 @@ module Paramod (B : Orderings.Blob) = struct passives_w,passives_a ;; - let add_passive_clauses ?(no_weight=false) + let add_passive_clauses ?(bonus_weight=0) (passives_w,passives_a) new_clauses = let new_clauses_w,new_clauses_a = - List.fold_left (add_passive_clause ~no_weight) + List.fold_left (add_passive_clause ~bonus_weight) (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses in (WeightPassiveSet.union new_clauses_w passives_w, AgePassiveSet.union new_clauses_a passives_a) ;; - let add_passive_goals ?(no_weight=false) + let add_passive_goals ?(bonus_weight=0) (passives_w,passives_a) new_clauses = let new_clauses_w,new_clauses_a = - List.fold_left (add_passive_goal ~no_weight) + List.fold_left (add_passive_goal ~bonus_weight) (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses in (WeightPassiveSet.union new_clauses_w passives_w, @@ -342,14 +342,14 @@ module Paramod (B : Orderings.Blob) = struct let bag,c = Terms.add_to_bag c bag in (bag,maxvar,c::l) in - let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in + let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in let goal = match goals with | [g] -> g | _ -> assert false in let passives = - add_passive_clauses ~no_weight:true passive_empty_set hypotheses + add_passive_clauses ~bonus_weight:(-1000) passive_empty_set hypotheses in let g_passives = - add_passive_goal ~no_weight:true passive_empty_set goal + add_passive_goal ~bonus_weight:(-1000) passive_empty_set goal in let g_actives = [] in let actives = [], IDX.DT.empty in diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index d93fade27..5008489df 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -88,18 +88,22 @@ let string_of_comparison = function | Terms.Invertible -> "=<->=" let pp_literal ~formatter:f l = - match fst l with - | Terms.Predicate t -> + match l with + | Terms.Predicate t,sel -> Format.fprintf f "@[{"; + if sel then Format.fprintf f "*"; pp_foterm f t; + if sel then Format.fprintf f "*"; Format.fprintf f "}@;" - | Terms.Equation (lhs, rhs, ty, comp) -> + | Terms.Equation (lhs, rhs, ty, comp),sel -> Format.fprintf f "@[{"; + if sel then Format.fprintf f "*"; pp_foterm f ty; Format.fprintf f "}:@;@["; pp_foterm f lhs; Format.fprintf f "@;%s@;" (string_of_comparison comp); pp_foterm f rhs; + if sel then Format.fprintf f "*"; Format.fprintf f "@]@;" ;; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 413ab93b6..daafbd3ac 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 @@ -78,31 +78,31 @@ 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 build_clause bag filter rule t subst id id2 pos dir = + let build_clause bag 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 @@ -113,10 +113,11 @@ module Superposition (B : Orderings.Blob) = Terms.Equation (l, r, ty, o) | t -> Terms.Predicate t in + let nlit,plit = clause_ctx literal in let bag, uc = - Terms.add_to_bag (0, [], [literal,true], Terms.vars_of_term t, proof) bag + Terms.add_to_bag (0, nlit, plit, Terms.vars_of_term t, proof) bag in - Some (bag, uc) + Some (bag, uc, literal) else ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) ;; @@ -181,75 +182,82 @@ module Superposition (B : Orderings.Blob) = prof_demod.HExtlib.profile (demod table varlist) x ;; - 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 + 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, nlit, plit, vl, pr) table = - match nlit,plit with - |[literal,_], [] - |[],[literal,_] -> - (match literal with + 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)) - | _ -> assert false; + Some ((bag,id2,lit),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 are_alpha_eq cl1 cl2 = - 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 + 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 - 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*) + (*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 + 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 @@ -274,8 +282,8 @@ module Superposition (B : Orderings.Blob) = 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) + match build_clause bag filter rule t subst id id2 pos dir (fun x -> [],[(x,true)]) with + | Some (bag, c, _) -> Some ((bag, maxvar), c) | None -> None ;; let prof_build_new_clause = HExtlib.profile ~enable "build_new_clause";; @@ -304,6 +312,7 @@ module Superposition (B : Orderings.Blob) = 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 @@ -335,7 +344,7 @@ module Superposition (B : Orderings.Blob) = 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) - | _ -> assert false + | _ -> None (* TODO : implement subsumption for clauses *) ;; let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";; let is_subsumed ~unify bag maxvar c x = @@ -559,7 +568,8 @@ 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 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 @@ -568,7 +578,7 @@ module Superposition (B : Orderings.Blob) = else let l,r,ty = match nlit,plit with - | [],[Terms.Equation(l,r,ty,_),_] -> l,r,ty + | [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) @@ -576,7 +586,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) @@ -596,7 +606,6 @@ module Superposition (B : Orderings.Blob) = (* this is OK for both the sup_left and sup_right inference steps *) let superposition table varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in - debug (lazy (string_of_int (IDX.ClauseSet.cardinal cands) ^ " candidates found")); HExtlib.filter_map (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) -> match nlit,plit with