From eca915d2656084f1e58149a476a2d305758b00f9 Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 24 Jun 2009 12:30:56 +0000 Subject: [PATCH] Implemented check for duplicates (in goals) --- .../components/ng_paramodulation/foSubst.ml | 8 ++--- .../components/ng_paramodulation/foSubst.mli | 2 +- .../components/ng_paramodulation/foUnif.ml | 36 ++++++++++++++++--- .../components/ng_paramodulation/foUnif.mli | 8 ++++- .../components/ng_paramodulation/paramod.ml | 20 +++++------ .../ng_paramodulation/superposition.ml | 26 ++++++++++---- .../ng_paramodulation/superposition.mli | 3 +- 7 files changed, 75 insertions(+), 28 deletions(-) diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml index 6154306b5..5cb84e1c9 100644 --- a/helm/software/components/ng_paramodulation/foSubst.ml +++ b/helm/software/components/ng_paramodulation/foSubst.ml @@ -15,16 +15,16 @@ let build_subst n t tail = (n,t) :: tail ;; - let rec lookup_subst var subst = + let rec lookup var subst = match var with | Terms.Var i -> (try - lookup_subst (List.assoc i subst) subst + lookup (List.assoc i subst) subst with Not_found -> var) | _ -> var ;; - let lookup_subst i subst = lookup_subst (Terms.Var i) subst;; + let lookup i subst = lookup (Terms.Var i) subst;; let is_in_subst i subst = List.mem_assoc i subst;; @@ -39,7 +39,7 @@ let rec apply_subst subst = function | (Terms.Leaf _) as t -> t | Terms.Var i -> - (match lookup_subst i subst with + (match lookup i subst with | Terms.Node _ as t -> apply_subst subst t | t -> t) | (Terms.Node l) -> diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli index 441e35581..1ed311433 100644 --- a/helm/software/components/ng_paramodulation/foSubst.mli +++ b/helm/software/components/ng_paramodulation/foSubst.mli @@ -19,7 +19,7 @@ module Subst (B : Terms.Blob) : val build_subst : int -> 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.substitution - val lookup_subst : + val lookup : int -> 'a Terms.substitution -> 'a Terms.foterm val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist val apply_subst : diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml index 6eb014062..83179b404 100644 --- a/helm/software/components/ng_paramodulation/foUnif.ml +++ b/helm/software/components/ng_paramodulation/foUnif.ml @@ -18,19 +18,18 @@ module Founif (B : Terms.Blob) = struct module U = FoUtils.Utils(B) let unification vars locked_vars t1 t2 = - let lookup = Subst.lookup_subst in let rec occurs_check subst what where = match where with | Terms.Var i when i = what -> true | Terms.Var i -> - let t = lookup i subst in + let t = Subst.lookup i subst in if not (U.eq_foterm t where) then occurs_check subst what t else false | Terms.Node l -> List.exists (occurs_check subst what) l | _ -> false in let rec unif subst s t = - let s = match s with Terms.Var i -> lookup i subst | _ -> s - and t = match t with Terms.Var i -> lookup i subst | _ -> t + let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s + and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t in match s, t with @@ -67,5 +66,32 @@ module Founif (B : Terms.Blob) = struct let subst = unif Subst.id_subst t1 t2 in let vars = Subst.filter subst vars in subst, vars - +;; + + let alpha_eq s t = + let rec equiv subst s t = + let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s + and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t + + in + match s, t with + | s, t when U.eq_foterm s t -> subst + | Terms.Var i, Terms.Var j + when (not (List.exists (fun (_,k) -> k=t) subst)) -> + let subst = Subst.build_subst i t subst in + subst + | Terms.Node l1, Terms.Node l2 -> ( + try + List.fold_left2 + (fun subst' s t -> equiv subst' s t) + subst l1 l2 + with Invalid_argument _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + ) + | _, _ -> + raise (UnificationFailure (lazy "Inference.unification.unif")) + in + equiv Subst.id_subst s t +;; + end diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli index fc682c5fc..6d50f70ee 100644 --- a/helm/software/components/ng_paramodulation/foUnif.mli +++ b/helm/software/components/ng_paramodulation/foUnif.mli @@ -16,7 +16,7 @@ exception UnificationFailure of string Lazy.t;; module Founif (B : Terms.Blob) : sig - val unification: + val unification: (* global varlist for both terms t1 and t2 *) Terms.varlist -> (* locked variables: if equal to FV(t2) we match t1 with t2*) @@ -25,4 +25,10 @@ module Founif (B : Terms.Blob) : B.t Terms.foterm -> B.t Terms.substitution * Terms.varlist + + val alpha_eq: + B.t Terms.foterm -> + B.t Terms.foterm -> + B.t Terms.substitution + end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index e747d6693..e9726116e 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -53,14 +53,10 @@ let nparamod rdb metasenv subst context t table = (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives) in - let backward_infer_step bag maxvar actives passives g_actives g_passives g_current = + let backward_infer_step bag maxvar actives passives + g_actives g_passives g_current = (* superposition left, simplifications on goals *) debug "infer_left step..."; - debug ("Selected goal : " ^ Pp.pp_unit_clause g_current); - let bag, g_current = - Sup.simplify_goal maxvar (snd actives) bag g_current - in - debug "Simplified goal"; let bag, maxvar, new_goals = Sup.infer_left bag maxvar g_current actives in @@ -96,8 +92,9 @@ let nparamod rdb metasenv subst context t table = let bag, g_actives = List.fold_left (fun (bag,acc) c -> - let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in - bag, c::acc) + match Sup.simplify_goal maxvar (snd actives) bag acc c with + | None -> bag, acc + | Some (bag,c) -> bag,c::acc) (bag,[]) g_actives in let ctable = IDX.index_unit_clause IDX.DT.empty current in @@ -132,8 +129,11 @@ let nparamod rdb metasenv subst context t table = let rec aux_select passives g_passives = let backward,current,passives,g_passives = select passives g_passives in if backward then - backward_infer_step bag maxvar actives passives - g_actives g_passives current + match Sup.simplify_goal maxvar (snd actives) bag g_actives current with + | None -> aux_select passives g_passives + | Some x -> let bag,g_current = x in + backward_infer_step bag maxvar actives passives + g_actives g_passives g_current else (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *) match Sup.keep_simplified current actives bag maxvar with diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 82fe83037..ffca04b96 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -332,15 +332,28 @@ module Superposition (B : Terms.Blob) = bag (newa@tl) in keep_simplified_aux ~new_cl:true cl (alist,atable) bag [] - ;; - + ;; + + 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] + in + try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true + with FoUnif.UnificationFailure _ -> false +;; + (* this is like simplify but raises Success *) - let simplify_goal maxvar table bag clause = + let simplify_goal maxvar table bag g_actives clause = let bag, clause = demodulate bag clause table in if (is_identity_clause clause) then raise (Success (bag, maxvar, clause)) else match is_subsumed ~unify:true bag maxvar clause table with - | None -> bag, clause + | None -> + if List.exists (are_alpha_eq clause) g_actives then None + else Some (bag, clause) | Some ((bag,maxvar),c) -> debug "Goal subsumed"; raise (Success (bag,maxvar,c)) @@ -470,8 +483,9 @@ module Superposition (B : Terms.Blob) = let bag, new_goals = List.fold_left (fun (bag, acc) g -> - let bag, g = simplify_goal maxvar atable bag g in - bag,g::acc) + match simplify_goal maxvar atable bag [] g with + | None -> assert false + | Some (bag,g) -> bag,g::acc) (bag, []) new_goals in debug "Simplified new goals with active clauses"; diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index a89b13f5b..bcfb0091e 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -49,8 +49,9 @@ module Superposition (B : Terms.Blob) : int -> Index.Index(B).DT.t -> B.t Terms.bag -> + B.t Terms.unit_clause list -> B.t Terms.unit_clause -> - B.t Terms.bag * B.t Terms.unit_clause + (B.t Terms.bag * B.t Terms.unit_clause) option val one_pass_simplification: B.t Terms.unit_clause -> -- 2.39.2