--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Nov 06 22:18:54 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Nov 06 22:18:54 2011 +0100
@@ -426,12 +426,21 @@
fun filter_used_facts used = filter (member (op =) used o fst)
-fun play_one_line_proof debug timeout ths state i reconstructors =
+fun play_one_line_proof debug verbose timeout ths state i reconstructors =
let
fun play [] [] = Failed_to_Play (hd reconstructors)
| play timed_outs [] = Trust_Playable (List.last timed_outs, SOME timeout)
| play timed_out (reconstructor :: reconstructors) =
- let val timer = Timer.startRealTimer () in
+ let
+ val _ =
+ if verbose then
+ "Trying \"" ^ name_of_reconstructor reconstructor ^ "\" for " ^
+ string_from_time timeout ^ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val timer = Timer.startRealTimer ()
+ in
case timed_reconstructor reconstructor debug timeout ths state i of
SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
| _ => play timed_out reconstructors
@@ -767,8 +776,8 @@
Output.urgent_message "Preplaying proof..."
else
());
- play_one_line_proof debug preplay_timeout used_ths state subgoal
- metis_reconstructors
+ play_one_line_proof debug verbose preplay_timeout used_ths state
+ subgoal metis_reconstructors
end,
fn preplay =>
let
@@ -953,8 +962,8 @@
if name = SMT_Solver.solver_name_of ctxt then ""
else "smt_solver = " ^ maybe_quote name
in
- case play_one_line_proof debug preplay_timeout used_ths state
- subgoal metis_reconstructors of
+ case play_one_line_proof debug verbose preplay_timeout used_ths
+ state subgoal metis_reconstructors of
p as Played _ => p
| _ => Trust_Playable (SMT (smt_settings ()), NONE)
end,
@@ -976,7 +985,8 @@
preplay = preplay, message = message, message_tail = message_tail}
end
-fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
+fun run_metis mode name ({debug, verbose, timeout, ...} : params)
+ minimize_command
({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
val reconstructor =
@@ -986,7 +996,7 @@
val (used_facts, used_ths) =
facts |> map untranslated_fact |> ListPair.unzip
in
- case play_one_line_proof debug timeout used_ths state subgoal
+ case play_one_line_proof debug verbose timeout used_ths state subgoal
[reconstructor] of
play as Played (_, time) =>
{outcome = NONE, used_facts = used_facts, run_time = time,