# HG changeset patch
# User desharna
# Date 1632926903 -7200
# Node ID 3604db245a639605840a184d4962affd5e221286
# Parent  1bd6eba713725c3cc161bca415b4cd63137d799d
tuned atp_prover sliding

diff -r 1bd6eba71372 -r 3604db245a63 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Sep 29 16:47:53 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Sep 29 16:48:23 2021 +0200
@@ -210,6 +210,9 @@
             |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths)
           end
 
+        val real_ms = Real.fromInt o Time.toMilliseconds
+        val slices_timeout = real_ms timeout
+
         fun run_slice time_left (cache_key, cache_value) (slice, (time_frac,
             (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
                best_uncurried_aliases),
@@ -220,15 +223,12 @@
             val num_facts =
               Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
               |> Integer.min (length facts)
-            val generate_info = (case format of DFG _ => true | _ => false)
             val strictness = if strict then Strict else Non_Strict
             val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
-            val sound = is_type_enc_sound type_enc
-            val real_ms = Real.fromInt o Time.toMilliseconds
             val slice_timeout =
               (real_ms time_left
                |> (if slice < num_actual_slices - 1 then
-                     curry Real.min (time_frac * real_ms timeout)
+                     curry Real.min (time_frac * slices_timeout)
                    else
                      I))
               * 0.001
@@ -243,20 +243,25 @@
                 |> writeln
               else
                 ()
-            val readable_names = not (Config.get ctxt atp_full_names)
-            val lam_trans = lam_trans |> the_default best_lam_trans
-            val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
             val value as (atp_problem, _, _, _) =
               if cache_key = SOME key then
                 cache_value
               else
-                facts
-                |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
-                |> take num_facts
-                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
-                |> map (apsnd Thm.prop_of)
-                |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
-                  lam_trans uncurried_aliases readable_names true hyp_ts concl_t
+                let
+                  val sound = is_type_enc_sound type_enc
+                  val generate_info = (case format of DFG _ => true | _ => false)
+                  val readable_names = not (Config.get ctxt atp_full_names)
+                  val lam_trans = lam_trans |> the_default best_lam_trans
+                  val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
+                in
+                  facts
+                  |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
+                  |> take num_facts
+                  |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
+                  |> map (apsnd Thm.prop_of)
+                  |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
+                    lam_trans uncurried_aliases readable_names true hyp_ts concl_t
+                end
 
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem