--- 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)
--- 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 =