# HG changeset patch # User blanchet # Date 1406760355 -7200 # Node ID a297879fe5b8d74cafd26fc0eed8d0ec97014eb8 # Parent 9ea51eddf81c5ca26b506db013967850b1a42b33 cascading timeout in parallel evaluation, to rapidly find optimum diff -r 9ea51eddf81c -r a297879fe5b8 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Jul 30 23:52:56 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Jul 31 00:45:55 2014 +0200 @@ -174,7 +174,7 @@ in (case preplay_isar_step ctxt timeout hopeless step'' of meths_outcomes as (_, Played time'') :: _ => - (* l' successfully eliminated *) + (* "l'" successfully eliminated *) (decrement_step_count (); set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; map (replace_successor l' [l]) lfs'; @@ -215,13 +215,12 @@ val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l) val timeouts = map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0 - val meths_outcomess = - map3 (preplay_isar_step ctxt) timeouts hopelesses succs' + val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs' in (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of NONE => steps | SOME times => - (* candidate successfully eliminated *) + (* "l" successfully eliminated *) (decrement_step_count (); map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times succs' meths_outcomess; diff -r 9ea51eddf81c -r a297879fe5b8 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Wed Jul 30 23:52:56 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Jul 31 00:45:55 2014 +0200 @@ -41,6 +41,26 @@ val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) +fun par_list_map_filter_with_timeout get_time timeout0 f xs = + let + val next_timeout = Unsynchronized.ref timeout0 + + fun apply_f x = + let val timeout = !next_timeout in + if timeout = Time.zeroTime then + NONE + else + let val y = f timeout x in + (case get_time y of + SOME time => next_timeout := time + | _ => ()); + SOME y + end + end + in + map_filter I (Par_List.map apply_f xs) + end + fun enrich_context_with_local_facts proof ctxt = let val thy = Proof_Context.theory_of ctxt @@ -140,16 +160,16 @@ fun preplay_isar_step_for_method ctxt timeout meth = try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed -fun preplay_isar_step ctxt timeout hopeless step = +fun preplay_isar_step ctxt timeout0 hopeless step = let - fun try_method meth = - (case preplay_isar_step_for_method ctxt timeout meth step of - outcome as Played _ => SOME (meth, outcome) - | _ => NONE) + fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt timeout meth step) + fun get_time (_, Played time) = SOME time + | get_time _ = NONE val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless in - the_list (Par_List.get_some try_method meths) + par_list_map_filter_with_timeout get_time timeout0 preplay meths + |> sort (play_outcome_ord o pairself snd) end type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table @@ -181,7 +201,7 @@ if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime fun get_best_method_outcome force = - tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *) + tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *) #> map (apsnd force) #> sort (play_outcome_ord o pairself snd) #> hd