--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:46:26 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Nov 06 13:57:17 2011 +0100
@@ -70,7 +70,7 @@
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
- val result as {outcome, used_facts, run_time_in_msecs, ...} =
+ val result as {outcome, used_facts, run_time, ...} =
prover params (K (K "")) problem
in
print silent
@@ -80,9 +80,8 @@
| NONE =>
"Found proof" ^
(if length used_facts = length facts then ""
- else " with " ^ n_facts used_facts) ^ " (" ^
- string_from_time (Time.fromMilliseconds run_time_in_msecs) ^
- ").");
+ else " with " ^ n_facts used_facts) ^
+ " (" ^ string_from_time run_time ^ ").");
result
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Nov 06 13:46:26 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Nov 06 13:57:17 2011 +0100
@@ -52,7 +52,7 @@
type prover_result =
{outcome: failure option,
used_facts: (string * locality) list,
- run_time_in_msecs: int,
+ run_time: Time.time,
preplay: unit -> play,
message: play -> string,
message_tail: string}
@@ -323,7 +323,7 @@
type prover_result =
{outcome: failure option,
used_facts: (string * locality) list,
- run_time_in_msecs: int,
+ run_time: Time.time,
preplay: unit -> play,
message: play -> string,
message_tail: string}
@@ -797,7 +797,7 @@
| SOME failure =>
([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
+ {outcome = outcome, used_facts = used_facts, run_time = Time.fromMilliseconds msecs, (*###*)
preplay = preplay, message = message, message_tail = message_tail}
end
@@ -928,8 +928,7 @@
end
else
{outcome = if is_none outcome then NONE else the outcome0,
- used_facts = used_facts,
- run_time_in_msecs = Time.toMilliseconds time_so_far}
+ used_facts = used_facts, run_time = time_so_far}
end
in do_slice timeout 1 NONE Time.zeroTime end
@@ -942,7 +941,7 @@
val num_facts = length facts
val facts = facts ~~ (0 upto num_facts - 1)
|> map (smt_weighted_fact ctxt num_facts)
- val {outcome, used_facts, run_time_in_msecs} =
+ val {outcome, used_facts, run_time} =
smt_filter_loop ctxt name params state subgoal smt_filter facts
val (used_facts, used_ths) = used_facts |> ListPair.unzip
val outcome = outcome |> Option.map failure_from_smt_failure
@@ -968,16 +967,14 @@
subgoal, subgoal_count)
in one_line_proof_text one_line_params end,
if verbose then
- "\nSMT solver real CPU time: " ^
- string_from_time (Time.fromMilliseconds run_time_in_msecs) ^ "."
+ "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
else
"")
| SOME failure =>
(K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
in
- {outcome = outcome, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, preplay = preplay,
- message = message, message_tail = message_tail}
+ {outcome = outcome, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
end
fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
@@ -993,8 +990,7 @@
case play_one_line_proof debug timeout used_ths state subgoal
[reconstructor] of
play as Played (_, time) =>
- {outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = Time.toMilliseconds time,
+ {outcome = NONE, used_facts = used_facts, run_time = time,
preplay = K play,
message = fn play =>
let
@@ -1007,7 +1003,7 @@
let
val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
in
- {outcome = SOME failure, used_facts = [], run_time_in_msecs = ~1,
+ {outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
preplay = K play, message = fn _ => string_for_failure failure,
message_tail = ""}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 06 13:46:26 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 06 13:57:17 2011 +0100
@@ -75,8 +75,8 @@
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
- (result as {outcome, used_facts, run_time_in_msecs, preplay,
- message, message_tail} : prover_result) =
+ (result as {outcome, used_facts, run_time, preplay, message,
+ message_tail} : prover_result) =
if is_some outcome orelse null used_facts then
result
else
@@ -88,10 +88,11 @@
((true, name), preplay)
else
let
- fun can_min_fast_enough msecs =
- 0.001 * Real.fromInt ((num_facts + 2) * msecs)
+ fun can_min_fast_enough time =
+ 0.001
+ * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
<= Config.get ctxt auto_minimize_max_time
- val prover_fast_enough = can_min_fast_enough run_time_in_msecs
+ val prover_fast_enough = can_min_fast_enough run_time
in
if isar_proof then
((prover_fast_enough, name), preplay)
@@ -99,7 +100,7 @@
let val preplay = preplay () in
(case preplay of
Played (reconstructor, timeout) =>
- if can_min_fast_enough (Time.toMilliseconds timeout) then
+ if can_min_fast_enough timeout then
(true, prover_name_for_reconstructor reconstructor
|> the_default name)
else
@@ -133,9 +134,8 @@
|> Output.urgent_message
else
();
- {outcome = NONE, used_facts = used_facts,
- run_time_in_msecs = run_time_in_msecs, preplay = preplay,
- message = message, message_tail = message_tail})
+ {outcome = NONE, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail})
| NONE => result
end