1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
1.3 @@ -15,6 +15,7 @@
1.4 type prover_result = Sledgehammer_Provers.prover_result
1.5
1.6 val trace : bool Config.T
1.7 + val MaShN : string
1.8 val meshN : string
1.9 val iterN : string
1.10 val mashN : string
1.11 @@ -51,12 +52,15 @@
1.12 val mash_suggest_facts :
1.13 Proof.context -> params -> string -> int -> term list -> term -> fact list
1.14 -> fact list
1.15 - val mash_learn_thy : Proof.context -> params -> theory -> Time.time -> unit
1.16 + val mash_learn_thy :
1.17 + Proof.context -> params -> theory -> Time.time -> fact list -> string
1.18 val mash_learn_proof :
1.19 Proof.context -> params -> term -> thm list -> fact list -> unit
1.20 val relevant_facts :
1.21 Proof.context -> params -> string -> int -> fact_override -> term list
1.22 -> term -> fact list -> fact list
1.23 + val kill_learners : unit -> unit
1.24 + val running_learners : unit -> unit
1.25 end;
1.26
1.27 structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
1.28 @@ -74,6 +78,8 @@
1.29 Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
1.30 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
1.31
1.32 +val MaShN = "MaSh"
1.33 +
1.34 val meshN = "mesh"
1.35 val iterN = "iter"
1.36 val mashN = "mash"
1.37 @@ -481,8 +487,6 @@
1.38 let
1.39 val thy = Proof_Context.theory_of ctxt
1.40 val fact_graph = #fact_graph (mash_get ())
1.41 -val _ = warning (PolyML.makestring (length (fact_graph |> Graph.keys), length (fact_graph |> Graph.maximals),
1.42 -length (fact_graph |> Graph.minimals))) (*###*)
1.43 val parents = parents_wrt_facts facts fact_graph
1.44 val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
1.45 val suggs =
1.46 @@ -509,34 +513,23 @@
1.47 in ((name, parents, feats, deps) :: upds, graph) end
1.48
1.49 val pass1_learn_timeout_factor = 0.5
1.50 -val pass2_learn_timeout_factor = 10.0
1.51
1.52 (* The timeout is understood in a very slack fashion. *)
1.53 -fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy
1.54 - timeout =
1.55 +fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
1.56 + facts =
1.57 let
1.58 val timer = Timer.startRealTimer ()
1.59 val prover = hd provers
1.60 fun timed_out frac =
1.61 Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
1.62 - val css_table = clasimpset_rule_table_of ctxt
1.63 - val facts = all_facts_of thy css_table
1.64 val {fact_graph, ...} = mash_get ()
1.65 fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)
1.66 val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)
1.67 in
1.68 if null new_facts then
1.69 - ()
1.70 + ""
1.71 else
1.72 let
1.73 - val n = length new_facts
1.74 - val _ =
1.75 - if verbose then
1.76 - "MaShing " ^ string_of_int n ^ " fact" ^ plural_s n ^
1.77 - " (advisory timeout: " ^ string_from_time timeout ^ ")..."
1.78 - |> Output.urgent_message
1.79 - else
1.80 - ()
1.81 val ths = facts |> map snd
1.82 val all_names =
1.83 ths |> filter_out (is_likely_tautology ctxt prover orf is_too_meta)
1.84 @@ -566,22 +559,15 @@
1.85 fact_graph = fact_graph})
1.86 end
1.87 in
1.88 - TimeLimit.timeLimit (time_mult pass2_learn_timeout_factor timeout)
1.89 - mash_map trans
1.90 - handle TimeLimit.TimeOut =>
1.91 - (if verbose then
1.92 - "MaSh timed out trying to learn " ^ string_of_int n ^
1.93 - " fact" ^ plural_s n ^ " in " ^
1.94 - string_from_time (Timer.checkRealTimer timer) ^ "."
1.95 - |> Output.urgent_message
1.96 - else
1.97 - ());
1.98 - (if verbose then
1.99 - "MaSh learned " ^ string_of_int n ^ " fact" ^ plural_s n ^ " in " ^
1.100 - string_from_time (Timer.checkRealTimer timer) ^ "."
1.101 - |> Output.urgent_message
1.102 - else
1.103 - ())
1.104 + mash_map trans;
1.105 + if verbose then
1.106 + "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
1.107 + (if verbose then
1.108 + " in " ^ string_from_time (Timer.checkRealTimer timer)
1.109 + else
1.110 + "") ^ "."
1.111 + else
1.112 + ""
1.113 end
1.114 end
1.115
1.116 @@ -623,19 +609,23 @@
1.117 let
1.118 val thy = Proof_Context.theory_of ctxt
1.119 fun maybe_learn can_suggest =
1.120 - if Time.toSeconds timeout >= min_secs_for_learning then
1.121 - if Multithreading.enabled () then
1.122 - let
1.123 - val factor =
1.124 - if can_suggest then short_learn_timeout_factor
1.125 - else long_learn_timeout_factor
1.126 - in
1.127 - Future.fork (fn () => mash_learn_thy ctxt params thy
1.128 - (time_mult factor timeout)); ()
1.129 - end
1.130 - else
1.131 - mash_learn_thy ctxt params thy
1.132 - (time_mult short_learn_timeout_factor timeout)
1.133 + if Async_Manager.has_running_threads MaShN orelse null facts then
1.134 + ()
1.135 + else if Time.toSeconds timeout >= min_secs_for_learning then
1.136 + let
1.137 + val factor =
1.138 + if can_suggest then short_learn_timeout_factor
1.139 + else long_learn_timeout_factor
1.140 + val soft_timeout = time_mult factor timeout
1.141 + val hard_timeout = time_mult 2.0 soft_timeout
1.142 + val birth_time = Time.now ()
1.143 + val death_time = Time.+ (birth_time, hard_timeout)
1.144 + val desc = ("machine learner for Sledgehammer", "")
1.145 + in
1.146 + Async_Manager.launch MaShN birth_time death_time desc
1.147 + (fn () =>
1.148 + (true, mash_learn_thy ctxt params thy soft_timeout facts))
1.149 + end
1.150 else
1.151 ()
1.152 val fact_filter =
1.153 @@ -667,4 +657,7 @@
1.154 |> not (null add_ths) ? prepend_facts add_ths
1.155 end
1.156
1.157 +fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
1.158 +fun running_learners () = Async_Manager.running_threads MaShN "learner"
1.159 +
1.160 end;