# HG changeset patch # User blanchet # Date 1292714005 -3600 # Node ID 1369c27c6966b2230df3fc1a4e6822fa96ec349d # Parent 285aea0c153cec154ab5e939c12b45644a1aa930 reduce the minimizer slack and add verbose information diff -r 285aea0c153c -r 1369c27c6966 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 18 23:31:22 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sun Dec 19 00:13:25 2010 +0100 @@ -30,10 +30,10 @@ (* wrapper for calling external prover *) -fun string_for_failure ATP_Proof.Unprovable = "Unprovable." - | string_for_failure ATP_Proof.TimedOut = "Timed out." - | string_for_failure ATP_Proof.Interrupted = "Interrupted." - | string_for_failure _ = "Error." +fun short_string_for_failure ATP_Proof.Unprovable = "Unprovable." + | short_string_for_failure ATP_Proof.TimedOut = "Timed out." + | short_string_for_failure ATP_Proof.Interrupted = "Interrupted." + | short_string_for_failure _ = "Error." fun n_facts names = let val n = length names in @@ -47,11 +47,15 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) -fun test_facts ({debug, overlord, provers, type_sys, isar_proof, +fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof, isar_shrink_factor, ...} : params) silent (prover : prover) explicit_apply timeout i n state facts = let - val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...") + val _ = + print silent (fn () => + "Testing " ^ n_facts (map fst facts) ^ + (if verbose then " (timeout: " ^ string_from_time timeout ^ ")" + else "") ^ "...") val params = {debug = debug, verbose = false, overlord = overlord, blocking = true, provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, @@ -66,12 +70,12 @@ facts = facts, smt_head = NONE} val result as {outcome, used_facts, ...} = prover params (K "") problem in - print silent - (fn () => case outcome of - SOME failure => string_for_failure failure - | NONE => - if length used_facts = length facts then "Found proof." - else "Found proof with " ^ n_facts used_facts ^ "."); + print silent (fn () => + case outcome of + SOME failure => short_string_for_failure failure + | NONE => + if length used_facts = length facts then "Found proof." + else "Found proof with " ^ n_facts used_facts ^ "."); result end @@ -123,7 +127,7 @@ (* Give the external prover some slack. The ATP gets further slack because the Sledgehammer preprocessing time is included in the estimate below but isn't part of the timeout. *) -val fudge_msecs = 1000 +val slack_msecs = 200 fun minimize_facts prover_name (params as {timeout, ...}) silent i n state facts = @@ -148,7 +152,7 @@ let val time = Timer.checkRealTimer timer val new_timeout = - Int.min (msecs, Time.toMilliseconds time + fudge_msecs) + Int.min (msecs, Time.toMilliseconds time + slack_msecs) |> Time.fromMilliseconds val facts = filter_used_facts used_facts facts val (min_thms, {message, ...}) =