# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 568b3193e53efb9125d26adca3c45bb2c62b011c # Parent ef800e91d072cdd940c59edafefff903af8e7fc1 don't include hidden facts in relevance filter + tweak MaSh learning diff -r ef800e91d072 -r 568b3193e53e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 18 08:44:04 2012 +0200 @@ -204,14 +204,13 @@ andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN | _ => false) (prop_of th) -fun is_theorem_bad_for_atps ho_atp exporter thm = +fun is_theorem_bad_for_atps ho_atp thm = is_metastrange_theorem thm orelse - (not exporter andalso - let val t = prop_of thm in - is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse - is_that_fact thm - end) + let val t = prop_of thm in + is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse + is_that_fact thm + end fun hackish_string_for_term ctxt t = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) @@ -346,7 +345,7 @@ fun maybe_filter_no_atps ctxt = not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table = +fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -363,9 +362,10 @@ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) fun add_facts global foldx facts = foldx (fn (name0, ths) => - if not exporter andalso name0 <> "" andalso + if name0 <> "" andalso forall (not o member Thm.eq_thm_prop add_ths) ths andalso (Facts.is_concealed facts name0 orelse + not (can (Proof_Context.get_thms ctxt) name0) orelse (not (Config.get ctxt ignore_no_atp) andalso is_package_def name0) orelse exists (fn s => String.isSuffix s name0) @@ -385,24 +385,22 @@ #> fold (fn th => fn (j, (multis, unis)) => (j + 1, if not (member Thm.eq_thm_prop add_ths th) andalso - is_theorem_bad_for_atps ho_atp exporter th then + is_theorem_bad_for_atps ho_atp th then (multis, unis) else let val new = (((fn () => - if name0 = "" then - th |> backquote_thm - else - [Facts.extern ctxt facts name0, - Name_Space.extern ctxt full_space name0, - name0] - |> find_first check_thms - |> (fn SOME name => - make_name reserved multi j name - | NONE => "")), - stature_of_thm global assms chained_ths - css_table name0 th), th) + if name0 = "" then + th |> backquote_thm + else + [Facts.extern ctxt facts name0, + Name_Space.extern ctxt full_space name0] + |> find_first check_thms + |> the_default name0 + |> make_name reserved multi j), + stature_of_thm global assms chained_ths + css_table name0 th), th) in if multi then (new :: multis, unis) else (multis, new :: unis) @@ -419,7 +417,7 @@ fun all_facts_of thy css_table = let val ctxt = Proof_Context.init_global thy in - all_facts ctxt false Symtab.empty true [] [] css_table + all_facts ctxt false Symtab.empty [] [] css_table |> rev (* try to restore the original order of facts, for MaSh *) end @@ -438,7 +436,7 @@ o fact_from_ref ctxt reserved chained_ths css_table) add else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in - all_facts ctxt ho_atp reserved false add chained_ths css_table + all_facts ctxt ho_atp reserved add chained_ths css_table |> filter_out (member Thm.eq_thm_prop del o snd) |> maybe_filter_no_atps ctxt end) diff -r ef800e91d072 -r 568b3193e53e src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -564,7 +564,7 @@ let val thy = Proof_Context.theory_of ctxt val prover = hd provers - val name = ATP_Util.timestamp () ^ serial_string () (* fresh enough *) + val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *) val feats = features_of ctxt prover thy General [t] val deps = used_ths |> map Thm.get_name_hint in @@ -583,8 +583,7 @@ (* The threshold should be large enough so that MaSh doesn't kick in for Auto Sledgehammer and Try. *) val min_secs_for_learning = 15 -val short_learn_timeout_factor = 0.2 -val long_learn_timeout_factor = 4.0 +val learn_timeout_factor = 2.0 fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = @@ -597,16 +596,13 @@ else let val thy = Proof_Context.theory_of ctxt - fun maybe_learn can_suggest = + fun maybe_learn () = if not learn orelse Async_Manager.has_running_threads MaShN then () else if Time.toSeconds timeout >= min_secs_for_learning then let - val factor = - if can_suggest then short_learn_timeout_factor - else long_learn_timeout_factor - val soft_timeout = time_mult factor timeout - val hard_timeout = time_mult 2.0 soft_timeout + val soft_timeout = time_mult learn_timeout_factor timeout + val hard_timeout = time_mult 4.0 soft_timeout val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) val desc = ("machine learner for Sledgehammer", "") @@ -619,12 +615,10 @@ () val fact_filter = case fact_filter of - SOME ff => - (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt) - else (); ff) + SOME ff => (() |> ff <> iterN ? maybe_learn; ff) | NONE => - if mash_can_suggest_facts ctxt then (maybe_learn true; meshN) - else if mash_could_suggest_facts () then (maybe_learn false; iterN) + if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) + else if mash_could_suggest_facts () then (maybe_learn (); iterN) else iterN val add_ths = Attrib.eval_thms ctxt add fun prepend_facts ths accepts =