# HG changeset patch # User blanchet # Date 1320584237 -3600 # Node ID bab52dafa63a520b0df036d6981bf2dc68169182 # Parent fbf2e1bdbf16620f8dea15419728dc416915ec1c use "Time.time" rather than milliseconds internally diff -r fbf2e1bdbf16 -r bab52dafa63a src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 diff -r fbf2e1bdbf16 -r bab52dafa63a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r fbf2e1bdbf16 -r bab52dafa63a src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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