src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
author blanchet
Fri Mar 14 11:15:46 2014 +0100 (2014-03-14 ago)
changeset 56128 c106ac2ff76d
parent 56081 72fad75baf7e
child 56985 82c83978fbd9
permissions -rw-r--r--
undo rewrite rules (e.g. for 'fun_app') in Isar
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
immler@31037
     2
    Author:     Philipp Meyer, TU Muenchen
blanchet@36370
     3
    Author:     Jasmin Blanchette, TU Muenchen
immler@31037
     4
blanchet@40977
     5
Minimization of fact list for Metis using external provers.
immler@31037
     6
*)
immler@31037
     7
blanchet@55202
     8
signature SLEDGEHAMMER_PROVER_MINIMIZE =
boehmes@32525
     9
sig
blanchet@46340
    10
  type stature = ATP_Problem_Generate.stature
blanchet@55287
    11
  type proof_method = Sledgehammer_Proof_Methods.proof_method
blanchet@55287
    12
  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
blanchet@55201
    13
  type mode = Sledgehammer_Prover.mode
blanchet@55201
    14
  type params = Sledgehammer_Prover.params
blanchet@55201
    15
  type prover = Sledgehammer_Prover.prover
blanchet@35867
    16
blanchet@55205
    17
  val is_prover_supported : Proof.context -> string -> bool
blanchet@55205
    18
  val is_prover_installed : Proof.context -> string -> bool
blanchet@55205
    19
  val default_max_facts_of_prover : Proof.context -> string -> int
blanchet@55205
    20
  val get_prover : Proof.context -> mode -> string -> prover
blanchet@55205
    21
blanchet@42646
    22
  val binary_min_facts : int Config.T
blanchet@48250
    23
  val auto_minimize_min_facts : int Config.T
blanchet@48250
    24
  val auto_minimize_max_time : real Config.T
blanchet@54824
    25
  val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
blanchet@55285
    26
    Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option ->
blanchet@54824
    27
    ((string * stature) * thm list) list ->
blanchet@54824
    28
    ((string * stature) * thm list) list option
blanchet@55285
    29
      * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string)
blanchet@55285
    30
         * string)
blanchet@54503
    31
  val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
blanchet@55205
    32
blanchet@54503
    33
  val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
blanchet@54503
    34
    Proof.state -> unit
blanchet@35866
    35
end;
boehmes@32525
    36
blanchet@55202
    37
structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE =
immler@31037
    38
struct
immler@31037
    39
blanchet@43085
    40
open ATP_Util
blanchet@39496
    41
open ATP_Proof
blanchet@46320
    42
open ATP_Problem_Generate
blanchet@55212
    43
open ATP_Proof_Reconstruct
blanchet@51200
    44
open ATP_Systems
blanchet@36142
    45
open Sledgehammer_Util
blanchet@48250
    46
open Sledgehammer_Fact
blanchet@55287
    47
open Sledgehammer_Proof_Methods
blanchet@55202
    48
open Sledgehammer_Isar
blanchet@55201
    49
open Sledgehammer_Prover
blanchet@55205
    50
open Sledgehammer_Prover_ATP
blanchet@55205
    51
open Sledgehammer_Prover_SMT
blanchet@56081
    52
open Sledgehammer_Prover_SMT2
blanchet@55205
    53
blanchet@55452
    54
fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
blanchet@55212
    55
    minimize_command
blanchet@55212
    56
    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
blanchet@55212
    57
  let
blanchet@55285
    58
    val meth =
blanchet@55285
    59
      if name = metisN then Metis_Method (type_enc, lam_trans)
blanchet@56081
    60
      else if name = smtN then SMT2_Method
blanchet@55285
    61
      else raise Fail ("unknown proof_method: " ^ quote name)
blanchet@55212
    62
    val used_facts = facts |> map fst
blanchet@55212
    63
  in
blanchet@55452
    64
    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
blanchet@55452
    65
        state subgoal meth [meth] of
blanchet@55212
    66
      play as (_, Played time) =>
blanchet@55212
    67
      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
blanchet@55212
    68
       preplay = Lazy.value play,
blanchet@55212
    69
       message =
blanchet@55212
    70
         fn play =>
blanchet@55212
    71
            let
blanchet@55285
    72
              val (_, override_params) = extract_proof_method params meth
blanchet@55212
    73
              val one_line_params =
blanchet@55212
    74
                (play, proof_banner mode name, used_facts, minimize_command override_params name,
blanchet@55212
    75
                 subgoal, subgoal_count)
blanchet@55212
    76
              val num_chained = length (#facts (Proof.goal state))
blanchet@55212
    77
            in
blanchet@55212
    78
              one_line_proof_text num_chained one_line_params
blanchet@55212
    79
            end,
blanchet@55212
    80
       message_tail = ""}
blanchet@55212
    81
    | play =>
blanchet@55212
    82
      let
blanchet@55212
    83
        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
blanchet@55212
    84
      in
blanchet@55212
    85
        {outcome = SOME failure, used_facts = [], used_from = [],
blanchet@55212
    86
         run_time = Time.zeroTime, preplay = Lazy.value play,
blanchet@55212
    87
         message = fn _ => string_of_atp_failure failure, message_tail = ""}
blanchet@55212
    88
      end)
blanchet@55212
    89
  end
blanchet@55212
    90
blanchet@55205
    91
fun is_prover_supported ctxt =
blanchet@55205
    92
  let val thy = Proof_Context.theory_of ctxt in
blanchet@56081
    93
    is_proof_method orf is_atp thy orf is_smt_prover ctxt orf is_smt2_prover ctxt
blanchet@55205
    94
  end
blanchet@55205
    95
blanchet@55205
    96
fun is_prover_installed ctxt =
blanchet@56081
    97
  is_proof_method orf is_smt_prover ctxt orf is_smt2_prover ctxt orf
blanchet@56081
    98
  is_atp_installed (Proof_Context.theory_of ctxt)
blanchet@55205
    99
blanchet@55285
   100
val proof_method_default_max_facts = 20
blanchet@55205
   101
blanchet@55205
   102
fun default_max_facts_of_prover ctxt name =
blanchet@55205
   103
  let val thy = Proof_Context.theory_of ctxt in
blanchet@55285
   104
    if is_proof_method name then
blanchet@55285
   105
      proof_method_default_max_facts
blanchet@55205
   106
    else if is_atp thy name then
blanchet@55205
   107
      fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
blanchet@56081
   108
    else if is_smt_prover ctxt name then
blanchet@55205
   109
      SMT_Solver.default_max_relevant ctxt name
blanchet@56081
   110
    else if is_smt2_prover ctxt name then
blanchet@56081
   111
      SMT2_Solver.default_max_relevant ctxt name
blanchet@56081
   112
    else
blanchet@56081
   113
      error ("No such prover: " ^ name ^ ".")
blanchet@55205
   114
  end
blanchet@55205
   115
blanchet@55205
   116
fun get_prover ctxt mode name =
blanchet@55205
   117
  let val thy = Proof_Context.theory_of ctxt in
blanchet@55285
   118
    if is_proof_method name then run_proof_method mode name
blanchet@55205
   119
    else if is_atp thy name then run_atp mode name
blanchet@55205
   120
    else if is_smt_prover ctxt name then run_smt_solver mode name
blanchet@56081
   121
    else if is_smt2_prover ctxt name then run_smt2_solver mode name
blanchet@55205
   122
    else error ("No such prover: " ^ name ^ ".")
blanchet@55205
   123
  end
blanchet@35866
   124
blanchet@36370
   125
(* wrapper for calling external prover *)
wenzelm@31236
   126
blanchet@40061
   127
fun n_facts names =
blanchet@38698
   128
  let val n = length names in
blanchet@40061
   129
    string_of_int n ^ " fact" ^ plural_s n ^
blanchet@38092
   130
    (if n > 0 then
blanchet@48085
   131
       ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
blanchet@38092
   132
     else
blanchet@38092
   133
       "")
blanchet@38092
   134
  end
blanchet@38092
   135
blanchet@41091
   136
fun print silent f = if silent then () else Output.urgent_message (f ())
blanchet@41091
   137
blanchet@54824
   138
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
blanchet@55297
   139
      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
blanchet@55297
   140
      smt_proofs, preplay_timeout, ...} : params)
blanchet@54824
   141
    silent (prover : prover) timeout i n state goal facts =
wenzelm@31236
   142
  let
blanchet@41277
   143
    val _ =
blanchet@41277
   144
      print silent (fn () =>
blanchet@54816
   145
        "Testing " ^ n_facts (map fst facts) ^
blanchet@54816
   146
        (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
blanchet@51005
   147
    val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
blanchet@38100
   148
    val params =
blanchet@53800
   149
      {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
blanchet@53800
   150
       provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
blanchet@53800
   151
       uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
blanchet@53800
   152
       max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
blanchet@53800
   153
       max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
blanchet@55297
   154
       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
blanchet@55297
   155
       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
blanchet@55297
   156
       preplay_timeout = preplay_timeout, expect = ""}
blanchet@40065
   157
    val problem =
blanchet@54141
   158
      {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@54141
   159
       factss = [("", facts)]}
blanchet@45370
   160
    val result as {outcome, used_facts, run_time, ...} =
blanchet@45520
   161
      prover params (K (K (K ""))) problem
blanchet@36223
   162
  in
blanchet@55202
   163
    print silent (fn () =>
blanchet@55202
   164
      (case outcome of
blanchet@55202
   165
        SOME failure => string_of_atp_failure failure
blanchet@55202
   166
      | NONE =>
blanchet@55202
   167
        "Found proof" ^
blanchet@55202
   168
         (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
blanchet@55202
   169
         " (" ^ string_of_time run_time ^ ")."));
blanchet@38092
   170
    result
blanchet@36223
   171
  end
wenzelm@31236
   172
blanchet@40204
   173
(* minimalization of facts *)
wenzelm@31236
   174
blanchet@45372
   175
(* Give the external prover some slack. The ATP gets further slack because the
blanchet@45372
   176
   Sledgehammer preprocessing time is included in the estimate below but isn't
blanchet@45372
   177
   part of the timeout. *)
blanchet@45372
   178
val slack_msecs = 200
blanchet@45372
   179
blanchet@54816
   180
fun new_timeout timeout run_time =
blanchet@54816
   181
  Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
blanchet@54816
   182
  |> Time.fromMilliseconds
blanchet@45372
   183
blanchet@45367
   184
(* The linear algorithm usually outperforms the binary algorithm when over 60%
blanchet@45367
   185
   of the facts are actually needed. The binary algorithm is much more
blanchet@45367
   186
   appropriate for provers that cannot return the list of used facts and hence
blanchet@45367
   187
   returns all facts as used. Since we cannot know in advance how many facts are
blanchet@45367
   188
   actually needed, we heuristically set the threshold to 10 facts. *)
blanchet@42646
   189
val binary_min_facts =
blanchet@55202
   190
  Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20)
blanchet@48250
   191
val auto_minimize_min_facts =
blanchet@48250
   192
  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
blanchet@48250
   193
      (fn generic => Config.get_generic generic binary_min_facts)
blanchet@48250
   194
val auto_minimize_max_time =
blanchet@55202
   195
  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} (K 5.0)
blanchet@40977
   196
blanchet@45368
   197
fun linear_minimize test timeout result xs =
blanchet@45368
   198
  let
blanchet@45368
   199
    fun min _ [] p = p
blanchet@45368
   200
      | min timeout (x :: xs) (seen, result) =
blanchet@54816
   201
        (case test timeout (xs @ seen) of
blanchet@54816
   202
          result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
blanchet@55202
   203
          min (new_timeout timeout run_time) (filter_used_facts true used_facts xs)
blanchet@55202
   204
            (filter_used_facts false used_facts seen, result)
blanchet@54816
   205
        | _ => min timeout xs (x :: seen, result))
blanchet@54816
   206
  in
blanchet@54816
   207
    min timeout xs ([], result)
blanchet@54816
   208
  end
blanchet@38015
   209
blanchet@45368
   210
fun binary_minimize test timeout result xs =
blanchet@40977
   211
  let
blanchet@55202
   212
    fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) =
blanchet@41743
   213
        let
blanchet@45367
   214
          val (l0, r0) = chop (length xs div 2) xs
blanchet@41743
   215
(*
blanchet@55202
   216
          val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
blanchet@55202
   217
          val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs))
blanchet@55202
   218
          val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0))
blanchet@55202
   219
          val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0))
blanchet@41743
   220
*)
blanchet@45367
   221
          val depth = depth + 1
blanchet@45372
   222
          val timeout = new_timeout timeout run_time
blanchet@41743
   223
        in
blanchet@55202
   224
          (case test timeout (sup @ l0) of
blanchet@45372
   225
            result as {outcome = NONE, used_facts, ...} =>
blanchet@48798
   226
            min depth result (filter_used_facts true used_facts sup)
blanchet@48798
   227
                      (filter_used_facts true used_facts l0)
blanchet@45367
   228
          | _ =>
blanchet@55202
   229
            (case test timeout (sup @ r0) of
blanchet@45367
   230
              result as {outcome = NONE, used_facts, ...} =>
blanchet@48798
   231
              min depth result (filter_used_facts true used_facts sup)
blanchet@48798
   232
                        (filter_used_facts true used_facts r0)
blanchet@45367
   233
            | _ =>
blanchet@45367
   234
              let
blanchet@45367
   235
                val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
blanchet@55202
   236
                val (sup, r0) = (sup, r0) |> pairself (filter_used_facts true (map fst sup_r0))
blanchet@45367
   237
                val (sup_l, (r, result)) = min depth result (sup @ l) r0
blanchet@48798
   238
                val sup = sup |> filter_used_facts true (map fst sup_l)
blanchet@55202
   239
              in (sup, (l @ r, result)) end))
blanchet@40977
   240
        end
blanchet@41743
   241
(*
blanchet@41743
   242
        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
blanchet@41743
   243
*)
blanchet@45367
   244
      | min _ result sup xs = (sup, (xs, result))
blanchet@45367
   245
  in
blanchet@55202
   246
    (case snd (min 0 result [] xs) of
blanchet@45372
   247
      ([x], result as {run_time, ...}) =>
blanchet@45372
   248
      (case test (new_timeout timeout run_time) [] of
blanchet@55202
   249
        result as {outcome = NONE, ...} => ([], result)
blanchet@55202
   250
      | _ => ([x], result))
blanchet@55202
   251
    | p => p)
blanchet@45367
   252
  end
blanchet@40977
   253
blanchet@54816
   254
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
blanchet@54816
   255
    preplay0 facts =
wenzelm@31236
   256
  let
blanchet@40941
   257
    val ctxt = Proof.context_of state
blanchet@54815
   258
    val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
blanchet@54130
   259
    fun test timeout = test_facts params silent prover timeout i n state goal
blanchet@48796
   260
    val (chained, non_chained) = List.partition is_fact_chained facts
blanchet@48799
   261
    (* Push chained facts to the back, so that they are less likely to be
blanchet@48799
   262
       kicked out by the linear minimization algorithm. *)
blanchet@48796
   263
    val facts = non_chained @ chained
wenzelm@31236
   264
  in
blanchet@54815
   265
    (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
blanchet@55202
   266
     (case test timeout facts of
blanchet@45371
   267
       result as {outcome = NONE, used_facts, run_time, ...} =>
blanchet@38015
   268
       let
blanchet@48798
   269
         val facts = filter_used_facts true used_facts facts
blanchet@45372
   270
         val min =
blanchet@54815
   271
           if length facts >= Config.get ctxt binary_min_facts then binary_minimize
blanchet@54815
   272
           else linear_minimize
blanchet@45368
   273
         val (min_facts, {preplay, message, message_tail, ...}) =
blanchet@45371
   274
           min test (new_timeout timeout run_time) result facts
blanchet@48321
   275
       in
blanchet@48321
   276
         print silent (fn () => cat_lines
blanchet@48321
   277
             ["Minimized to " ^ n_facts (map fst min_facts)] ^
blanchet@48796
   278
              (case min_facts |> filter is_fact_chained |> length of
blanchet@48321
   279
                 0 => ""
blanchet@48321
   280
               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
blanchet@54503
   281
         (if learn then do_learn (maps snd min_facts) else ());
blanchet@51187
   282
         (SOME min_facts,
blanchet@54815
   283
          (if is_some preplay0 andalso length min_facts = length facts then the preplay0
blanchet@54815
   284
           else preplay,
blanchet@51187
   285
           message, message_tail))
blanchet@48321
   286
       end
blanchet@43052
   287
     | {outcome = SOME TimedOut, preplay, ...} =>
blanchet@54816
   288
       (NONE, (preplay, fn _ =>
blanchet@54816
   289
          "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
blanchet@54816
   290
          \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
blanchet@55202
   291
     | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
blanchet@55285
   292
    handle ERROR msg =>
blanchet@55285
   293
      (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
wenzelm@31236
   294
  end
wenzelm@31236
   295
blanchet@55285
   296
fun adjust_proof_method_params override_params
blanchet@54816
   297
    ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
blanchet@54816
   298
      uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
blanchet@55297
   299
      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
blanchet@55297
   300
      timeout, preplay_timeout, expect} : params) =
blanchet@48250
   301
  let
blanchet@48250
   302
    fun lookup_override name default_value =
blanchet@55202
   303
      (case AList.lookup (op =) override_params name of
blanchet@48250
   304
        SOME [s] => SOME s
blanchet@55202
   305
      | _ => default_value)
blanchet@55285
   306
    (* Only those options that proof_methods are interested in are considered here. *)
blanchet@48250
   307
    val type_enc = lookup_override "type_enc" type_enc
blanchet@48250
   308
    val lam_trans = lookup_override "lam_trans" lam_trans
blanchet@48250
   309
  in
blanchet@53800
   310
    {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
blanchet@53800
   311
     provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
blanchet@53800
   312
     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
blanchet@53800
   313
     max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
blanchet@49918
   314
     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
blanchet@55297
   315
     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
blanchet@55288
   316
     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
blanchet@48250
   317
  end
blanchet@48250
   318
blanchet@55205
   319
fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
blanchet@55205
   320
    ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
blanchet@55205
   321
    (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} :
blanchet@55205
   322
     prover_result) =
blanchet@48250
   323
  if is_some outcome orelse null used_facts then
blanchet@48250
   324
    result
blanchet@48250
   325
  else
blanchet@48250
   326
    let
blanchet@55205
   327
      val thy = Proof_Context.theory_of ctxt
blanchet@48250
   328
      val num_facts = length used_facts
blanchet@55205
   329
blanchet@48250
   330
      val ((perhaps_minimize, (minimize_name, params)), preplay) =
blanchet@48250
   331
        if mode = Normal then
blanchet@48250
   332
          if num_facts >= Config.get ctxt auto_minimize_min_facts then
blanchet@48250
   333
            ((true, (name, params)), preplay)
blanchet@48250
   334
          else
blanchet@48250
   335
            let
blanchet@48250
   336
              fun can_min_fast_enough time =
blanchet@48250
   337
                0.001
blanchet@48250
   338
                * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
blanchet@48250
   339
                <= Config.get ctxt auto_minimize_max_time
blanchet@48250
   340
              fun prover_fast_enough () = can_min_fast_enough run_time
blanchet@48250
   341
            in
blanchet@51190
   342
              (case Lazy.force preplay of
blanchet@55285
   343
                 (meth as Metis_Method _, Played timeout) =>
blanchet@51191
   344
                 if isar_proofs = SOME true then
blanchet@54816
   345
                   (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
blanchet@54816
   346
                      itself. *)
blanchet@55205
   347
                   (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
blanchet@51191
   348
                 else if can_min_fast_enough timeout then
blanchet@55285
   349
                   (true, extract_proof_method params meth
blanchet@51190
   350
                          ||> (fn override_params =>
blanchet@55285
   351
                                  adjust_proof_method_params override_params params))
blanchet@51190
   352
                 else
blanchet@51190
   353
                   (prover_fast_enough (), (name, params))
blanchet@56081
   354
               | (SMT2_Method, Played timeout) =>
blanchet@54816
   355
                 (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
blanchet@54816
   356
                    itself. *)
blanchet@51190
   357
                 (can_min_fast_enough timeout, (name, params))
blanchet@51190
   358
               | _ => (prover_fast_enough (), (name, params)),
blanchet@51190
   359
               preplay)
blanchet@48250
   360
            end
blanchet@48250
   361
        else
blanchet@54127
   362
          ((false, (name, params)), preplay)
blanchet@48250
   363
      val minimize = minimize |> the_default perhaps_minimize
blanchet@48250
   364
      val (used_facts, (preplay, message, _)) =
blanchet@48250
   365
        if minimize then
blanchet@48392
   366
          minimize_facts do_learn minimize_name params
blanchet@54824
   367
            (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
blanchet@54824
   368
            goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from))
blanchet@48250
   369
          |>> Option.map (map fst)
blanchet@48250
   370
        else
blanchet@48250
   371
          (SOME used_facts, (preplay, message, ""))
blanchet@48250
   372
    in
blanchet@55202
   373
      (case used_facts of
blanchet@48250
   374
        SOME used_facts =>
blanchet@55202
   375
        {outcome = NONE, used_facts = used_facts, used_from = used_from, run_time = run_time,
blanchet@55202
   376
         preplay = preplay, message = message, message_tail = message_tail}
blanchet@55202
   377
      | NONE => result)
blanchet@48250
   378
    end
blanchet@48250
   379
blanchet@51187
   380
fun get_minimizing_prover ctxt mode do_learn name params minimize_command
blanchet@51187
   381
                          problem =
blanchet@48250
   382
  get_prover ctxt mode name params minimize_command problem
blanchet@48384
   383
  |> maybe_minimize ctxt mode do_learn name params problem
blanchet@48250
   384
blanchet@48321
   385
fun run_minimize (params as {provers, ...}) do_learn i refs state =
blanchet@38045
   386
  let
blanchet@38045
   387
    val ctxt = Proof.context_of state
blanchet@54130
   388
    val {goal, facts = chained_ths, ...} = Proof.goal state
blanchet@38696
   389
    val reserved = reserved_isar_keyword_table ()
blanchet@48396
   390
    val css = clasimpset_rule_table_of ctxt
blanchet@54130
   391
    val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css)
blanchet@38045
   392
  in
blanchet@55202
   393
    (case subgoal_count state of
wenzelm@40132
   394
      0 => Output.urgent_message "No subgoal!"
blanchet@55202
   395
    | n => (case provers of
blanchet@41265
   396
             [] => error "No prover is set."
blanchet@41265
   397
           | prover :: _ =>
blanchet@41265
   398
             (kill_provers ();
blanchet@54130
   399
              minimize_facts do_learn prover params false i n state goal NONE facts
blanchet@43261
   400
              |> (fn (_, (preplay, message, message_tail)) =>
blanchet@50669
   401
                     message (Lazy.force preplay) ^ message_tail
blanchet@55202
   402
                     |> Output.urgent_message))))
blanchet@38045
   403
  end
blanchet@38045
   404
blanchet@35866
   405
end;