--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200
@@ -415,7 +415,7 @@
subgoal_count = Sledgehammer_Util.subgoal_count st,
facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
smt_filter = NONE}
- in prover params (K "") problem end)) ()
+ in prover params (K (K "")) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time_in_msecs |> the_default ~1
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 17:00:38 2011 +0200
@@ -40,6 +40,7 @@
Proof.context -> type_system -> int list list -> int
-> (string * locality) list vector -> 'a proof -> string list option
val uses_typed_helpers : int list -> 'a proof -> bool
+ val reconstructor_name : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val isar_proof_text :
Proof.context -> isar_params -> one_line_params -> string
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 17:00:38 2011 +0200
@@ -309,16 +309,20 @@
(* Sledgehammer the given subgoal *)
+val default_minimize_prover = Metis_Tactics.metisN
+
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
fun string_for_raw_param (key, values) =
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
fun minimize_command override_params i prover_name fact_names =
- sledgehammerN ^ " " ^ minN ^ " [" ^ prover_name ^
+ sledgehammerN ^ " " ^ minN ^
+ (if prover_name = default_minimize_prover then ""
+ else enclose "[" "]" prover_name) ^
(override_params |> filter is_raw_param_relevant_for_minimize
|> implode o map (prefix ", " o string_for_raw_param)) ^
- "] (" ^ space_implode " " fact_names ^ ")" ^
+ " (" ^ space_implode " " fact_names ^ ")" ^
(if i = 1 then "" else " " ^ string_of_int i)
fun hammer_away override_params subcommand opt_i relevance_override state =
@@ -335,7 +339,9 @@
|> K ()
end
else if subcommand = minN then
- run_minimize (get_params Minimize ctxt override_params)
+ run_minimize (get_params Minimize ctxt
+ (("provers", [default_minimize_prover]) ::
+ override_params))
(the_default 1 opt_i) (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200
@@ -76,7 +76,7 @@
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
val result as {outcome, used_facts, run_time_in_msecs, ...} =
- prover params (K "") problem
+ prover params (K (K "")) problem
in
print silent (fn () =>
case outcome of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200
@@ -58,7 +58,8 @@
run_time_in_msecs: int option,
message: string}
- type prover = params -> minimize_command -> prover_problem -> prover_result
+ type prover =
+ params -> (string -> minimize_command) -> prover_problem -> prover_result
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -318,7 +319,8 @@
used_facts: (string * locality) list,
run_time_in_msecs: int option}
-type prover = params -> minimize_command -> prover_problem -> prover_result
+type prover =
+ params -> (string -> minimize_command) -> prover_problem -> prover_result
(* configuration attributes *)
@@ -516,14 +518,26 @@
| _ => type_sys)
| format => (format, type_sys))
-fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
+fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys
- | determine_format_and_type_sys best_type_systems formats
- (Smart_Type_Sys full_types) =
+ | choose_format_and_type_sys best_type_systems formats
+ (Smart_Type_Sys full_types) =
map type_sys_from_string best_type_systems @ fallback_best_type_systems
|> find_first (if full_types then is_type_sys_virtually_sound else K true)
|> the |> adjust_dumb_type_sys formats
+val metis_minimize_max_time = seconds 2.0
+
+fun choose_minimize_command minimize_command name preplay =
+ (case preplay of
+ Played (reconstructor, time) =>
+ if Time.<= (time, metis_minimize_max_time) then
+ reconstructor_name reconstructor
+ else
+ name
+ | _ => name)
+ |> minimize_command
+
fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
Config.put SMT_Config.verbose debug
#> Config.put SMT_Config.monomorph_full false
@@ -605,8 +619,7 @@
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val (format, type_sys) =
- determine_format_and_type_sys best_type_systems formats
- type_sys
+ choose_format_and_type_sys best_type_systems formats type_sys
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> not fairly_sound
@@ -783,7 +796,8 @@
goal)
val one_line_params =
(preplay, proof_banner mode blocking name, used_facts,
- minimize_command, subgoal, subgoal_count)
+ choose_minimize_command minimize_command name preplay,
+ subgoal, subgoal_count)
in
(proof_text ctxt isar_proof isar_params one_line_params ^
(if verbose then
@@ -970,7 +984,8 @@
| _ => Trust_Playable (SMT (smt_settings ()), NONE)
val one_line_params =
(preplay, proof_banner mode blocking name, used_facts,
- minimize_command, subgoal, subgoal_count)
+ choose_minimize_command minimize_command name preplay,
+ subgoal, subgoal_count)
in
one_line_proof_text one_line_params ^
(if verbose then
@@ -1002,7 +1017,7 @@
let
val one_line_params =
(play, proof_banner mode blocking name, used_facts,
- minimize_command, subgoal, subgoal_count)
+ minimize_command name, subgoal, subgoal_count)
in
{outcome = NONE, used_facts = used_facts,
run_time_in_msecs = SOME (Time.toMilliseconds time),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200
@@ -128,7 +128,7 @@
smt_filter = smt_filter}
fun really_go () =
problem
- |> get_minimizing_prover ctxt mode name params (minimize_command name)
+ |> get_minimizing_prover ctxt mode name params minimize_command
|> (fn {outcome, message, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
--- a/src/HOL/ex/sledgehammer_tactics.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Mon May 30 17:00:38 2011 +0200
@@ -43,7 +43,7 @@
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
smt_filter = NONE}
in
- (case prover params (K "") problem of
+ (case prover params (K (K "")) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
| _ => NONE)
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)