# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID e78476a99c705ca7d394bccae195750bf93f1028
# Parent  fccd756ed4bbe008938890724e20d1e6365c6a31
better time slack, to account for ultra-quick proof methods

diff -r fccd756ed4bb -r e78476a99c70 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -94,10 +94,13 @@
   | try_merge _ _ = NONE
 
 val compress_degree = 2
-val merge_timeout_slack = 1.25
+val merge_timeout_slack_time = seconds 0.005
+val merge_timeout_slack_factor = 1.5
 
-(* Precondition: The proof must be labeled canonically
-   (cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *)
+fun slackify_merge_timeout time =
+  time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
+
+(* Precondition: The proof must be labeled canonically. *)
 fun compress_isar_proof ctxt compress_isar preplay_data proof =
   if compress_isar <= 1.0 then
     proof
@@ -166,7 +169,7 @@
               val step'' = Prove (qs, fix, l, t, subs'', by)
 
               (* check if the modified step can be preplayed fast enough *)
-              val timeout = time_mult merge_timeout_slack (Time.+ (time, time'))
+              val timeout = slackify_merge_timeout (Time.+ (time, time'))
               val Played time'' = preplay_isar_step ctxt timeout (hd meths)(*FIXME*) step''
             in
               decrement_step_count (); (* l' successfully eliminated! *)
@@ -230,7 +233,7 @@
               val times0 = map ((fn Played time => time) o
                 forced_preplay_outcome_of_isar_step (!preplay_data)) labels
               val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
-              val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
+              val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
 
               (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
               val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'