From 6f35dd77922431b667f7eb4669ab3fbb6092c343 Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 24 Jun 2009 16:00:35 +0000 Subject: [PATCH] Extended is_identity test First step towards age selection --- .../components/ng_paramodulation/foUtils.ml | 6 +- .../components/ng_paramodulation/foUtils.mli | 5 +- .../components/ng_paramodulation/nCicBlob.ml | 3 +- .../components/ng_paramodulation/paramod.ml | 101 ++++++++++++------ .../ng_paramodulation/superposition.ml | 6 +- 5 files changed, 81 insertions(+), 40 deletions(-) diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index f56cccd89..26b7f6fa4 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -140,9 +140,13 @@ module Utils (B : Terms.Blob) = struct (Order.compute_unit_clause_weight cl, cl) ;; - let compare_passive_clauses (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) = + let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) = if w1 = w2 then id1 - id2 else w1 - w2 ;; + let compare_passive_clauses_age (_,(id1,_,_,_)) (_,(id2,_,_,_)) = + id1 - id2 + ;; + end diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index d0fb30367..5cbe461a0 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -46,7 +46,10 @@ module Utils (B : Terms.Blob) : val empty_bag : B.t Terms.bag - val compare_passive_clauses : + val compare_passive_clauses_weight : + B.t Terms.passive_clause -> B.t Terms.passive_clause -> int + + val compare_passive_clauses_age : B.t Terms.passive_clause -> B.t Terms.passive_clause -> int end diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 208d6d533..e611266d9 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -198,9 +198,8 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct let lit,vl,proof = get_literal id in if not ongoal && id = mp then ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*) - assert (vl = []); NCic.LetIn ("clause_" ^ string_of_int id, - extract amount vl lit, + extract amount [] lit, (NCic.Appl [eq_refl;NCic.Implicit `Type;NCic.Implicit `Term]), aux true ((id,([],lit))::seen) (id::tl))) else diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index e9726116e..1c91ee54e 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,7 +1,5 @@ -(* LOOPING : COL057-1.ma *) - let debug s = - () (* prerr_endline s *) + prerr_endline s ;; let nparamod rdb metasenv subst context t table = @@ -21,36 +19,76 @@ let nparamod rdb metasenv subst context t table = let module Sup = Superposition.Superposition(B) in let module Utils = FoUtils.Utils(B) in - let module OrderedPassives = + let module WeightOrderedPassives = + struct + type t = B.t Terms.passive_clause + + let compare = Utils.compare_passive_clauses_weight + end + in + let module AgeOrderedPassives = struct type t = B.t Terms.passive_clause - let compare = Utils.compare_passive_clauses + let compare = Utils.compare_passive_clauses_age end in - let module PassiveSet = Set.Make(OrderedPassives) + let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in + let module AgePassiveSet = Set.Make(AgeOrderedPassives) in + let add_passive_clause (passives_w,passives_a) cl = + let cl = Utils.mk_passive_clause cl in + WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a in - let add_passive_clause passives cl = - PassiveSet.add (Utils.mk_passive_clause cl) passives + let remove_passive_clause (passives_w,passives_a) cl = + let passives_w = WeightPassiveSet.remove cl passives_w in + let passives_a = AgePassiveSet.remove cl passives_a in + passives_w,passives_a + in + let add_passive_clauses (passives_w,passives_a) new_clauses = + let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause + (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses + in + (WeightPassiveSet.union new_clauses_w passives_w, + AgePassiveSet.union new_clauses_a passives_a) + in + let is_passive_set_empty (passives_w,passives_a) = + if (WeightPassiveSet.is_empty passives_w) then begin + assert (AgePassiveSet.is_empty passives_a); true + end else begin + assert (not (AgePassiveSet.is_empty passives_a)); false + end + in + let passive_set_cardinal (passives_w,_) = + WeightPassiveSet.cardinal passives_w + in + let passive_singleton cl = + (WeightPassiveSet.singleton cl,AgePassiveSet.singleton cl) + in + let passive_empty_set = + (WeightPassiveSet.empty,AgePassiveSet.empty) + in + let pick_min_passive use_age (passives_w,passives_a) = + if use_age then AgePassiveSet.min_elt passives_a + else WeightPassiveSet.min_elt passives_w in let timeout = Unix.gettimeofday () +. amount_of_time in - (* TODO : fairness condition *) + (* TODO : global age over facts and goals (without comparing weights) *) let select passives g_passives = - if PassiveSet.is_empty passives then begin - assert (not (PassiveSet.is_empty g_passives)); - let g_cl = PassiveSet.min_elt g_passives in - (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives) + if is_passive_set_empty passives then begin + assert (not (is_passive_set_empty g_passives)); + let g_cl = pick_min_passive false g_passives in + (true,snd g_cl,passives,remove_passive_clause g_passives g_cl) end - else let cl = PassiveSet.min_elt passives in - if PassiveSet.is_empty g_passives then - (false,snd cl,PassiveSet.remove cl passives,g_passives) + else let cl = pick_min_passive false passives in + if is_passive_set_empty g_passives then + (false,snd cl,remove_passive_clause passives cl,g_passives) else - let g_cl = PassiveSet.min_elt g_passives in + let g_cl = pick_min_passive false g_passives in if (fst cl <= fst g_cl) then - (false,snd cl,PassiveSet.remove cl passives,g_passives) + (false,snd cl,remove_passive_clause passives cl,g_passives) else - (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives) + (true,snd g_cl,passives,remove_passive_clause g_passives g_cl) in let backward_infer_step bag maxvar actives passives @@ -61,11 +99,8 @@ let nparamod rdb metasenv subst context t table = Sup.infer_left bag maxvar g_current actives in debug "Performed infer_left step"; - let new_goals = List.fold_left add_passive_clause - PassiveSet.empty new_goals - in - bag, maxvar, actives, passives, g_current::g_actives, - (PassiveSet.union new_goals g_passives) + bag, maxvar, actives, passives, g_current::g_actives, + (add_passive_clauses g_passives new_goals) in let forward_infer_step bag maxvar actives passives g_actives @@ -106,13 +141,9 @@ let nparamod rdb metasenv subst context t table = bag,m,ng@acc) (bag,maxvar,[]) g_actives in - let new_clauses = List.fold_left add_passive_clause - PassiveSet.empty new_clauses in - let new_goals = List.fold_left add_passive_clause - PassiveSet.empty new_goals in bag, maxvar, actives, - PassiveSet.union new_clauses passives, g_actives, - PassiveSet.union new_goals g_passives + add_passive_clauses passives new_clauses, g_actives, + add_passive_clauses g_passives new_goals in let rec given_clause bag maxvar actives passives g_actives g_passives = @@ -152,12 +183,12 @@ let nparamod rdb metasenv subst context t table = (List.length g_actives)); debug (Printf.sprintf "Number of passive goals : %d" - (PassiveSet.cardinal g_passives)); + (passive_set_cardinal g_passives)); debug (Printf.sprintf "Number of actives : %d" (List.length (fst actives))); debug (Printf.sprintf "Number of passives : %d" - (PassiveSet.cardinal passives)); + (passive_set_cardinal passives)); given_clause bag maxvar actives passives g_actives g_passives in @@ -169,13 +200,15 @@ let nparamod rdb metasenv subst context t table = in let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in let g_actives = [] in - let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in + let g_passives = + passive_singleton (Utils.mk_passive_clause goal) + in let passives, bag, maxvar = List.fold_left (fun (cl, bag, maxvar) t -> let bag, maxvar, c = mk_clause bag maxvar t in (add_passive_clause cl c), bag, maxvar) - (PassiveSet.empty, bag, maxvar) table + (passive_empty_set, bag, maxvar) table in let actives = [], IDX.DT.empty in try given_clause bag maxvar actives passives g_actives g_passives diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index ffca04b96..891c8dcac 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -180,8 +180,10 @@ module Superposition (B : Terms.Blob) = (* move away *) let is_identity_clause = function | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true - | _, Terms.Predicate _, _, _ -> assert false - | _ -> false + | _, Terms.Equation (l,r,_,_), vl, proof -> + (try ignore(Unif.unification vl [] l r); true + with FoUnif.UnificationFailure _ -> false) + | _, Terms.Predicate _, _, _ -> assert false ;; let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir = -- 2.39.5