src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57054 fed0329ea8e2
child 57208 5bf2a5c498c2
permissions -rw-r--r--
simplified counterexample handling
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@57054
    54
fun run_proof_method mode name (params as {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@57054
    64
    (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose timeout facts state
blanchet@57054
    65
        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@57054
    69
       message = fn play =>
blanchet@57054
    70
          let
blanchet@57054
    71
            val ctxt = Proof.context_of state
blanchet@57054
    72
            val (_, override_params) = extract_proof_method params meth
blanchet@57054
    73
            val one_line_params =
blanchet@57054
    74
              (play, proof_banner mode name, used_facts, minimize_command override_params name,
blanchet@57054
    75
               subgoal, subgoal_count)
blanchet@57054
    76
            val num_chained = length (#facts (Proof.goal state))
blanchet@57054
    77
          in
blanchet@57054
    78
            one_line_proof_text ctxt num_chained one_line_params
blanchet@57054
    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@57054
   130
    (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
blanchet@38092
   131
  end
blanchet@38092
   132
blanchet@41091
   133
fun print silent f = if silent then () else Output.urgent_message (f ())
blanchet@41091
   134
blanchet@54824
   135
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
blanchet@55297
   136
      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
blanchet@55297
   137
      smt_proofs, preplay_timeout, ...} : params)
blanchet@54824
   138
    silent (prover : prover) timeout i n state goal facts =
wenzelm@31236
   139
  let
blanchet@57054
   140
    val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
blanchet@57054
   141
      (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
blanchet@57054
   142
blanchet@51005
   143
    val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
blanchet@38100
   144
    val params =
blanchet@53800
   145
      {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
blanchet@53800
   146
       provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
blanchet@53800
   147
       uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
blanchet@53800
   148
       max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
blanchet@53800
   149
       max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
blanchet@55297
   150
       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
blanchet@55297
   151
       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
blanchet@55297
   152
       preplay_timeout = preplay_timeout, expect = ""}
blanchet@40065
   153
    val problem =
blanchet@54141
   154
      {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@54141
   155
       factss = [("", facts)]}
blanchet@45370
   156
    val result as {outcome, used_facts, run_time, ...} =
blanchet@45520
   157
      prover params (K (K (K ""))) problem
blanchet@36223
   158
  in
blanchet@55202
   159
    print silent (fn () =>
blanchet@55202
   160
      (case outcome of
blanchet@55202
   161
        SOME failure => string_of_atp_failure failure
blanchet@55202
   162
      | NONE =>
blanchet@55202
   163
        "Found proof" ^
blanchet@55202
   164
         (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
blanchet@55202
   165
         " (" ^ string_of_time run_time ^ ")."));
blanchet@38092
   166
    result
blanchet@36223
   167
  end
wenzelm@31236
   168
blanchet@40204
   169
(* minimalization of facts *)
wenzelm@31236
   170
blanchet@45372
   171
(* Give the external prover some slack. The ATP gets further slack because the
blanchet@45372
   172
   Sledgehammer preprocessing time is included in the estimate below but isn't
blanchet@45372
   173
   part of the timeout. *)
blanchet@45372
   174
val slack_msecs = 200
blanchet@45372
   175
blanchet@54816
   176
fun new_timeout timeout run_time =
blanchet@54816
   177
  Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
blanchet@54816
   178
  |> Time.fromMilliseconds
blanchet@45372
   179
blanchet@45367
   180
(* The linear algorithm usually outperforms the binary algorithm when over 60%
blanchet@45367
   181
   of the facts are actually needed. The binary algorithm is much more
blanchet@45367
   182
   appropriate for provers that cannot return the list of used facts and hence
blanchet@45367
   183
   returns all facts as used. Since we cannot know in advance how many facts are
blanchet@45367
   184
   actually needed, we heuristically set the threshold to 10 facts. *)
blanchet@42646
   185
val binary_min_facts =
blanchet@55202
   186
  Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20)
blanchet@48250
   187
val auto_minimize_min_facts =
blanchet@48250
   188
  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
blanchet@48250
   189
      (fn generic => Config.get_generic generic binary_min_facts)
blanchet@48250
   190
val auto_minimize_max_time =
blanchet@55202
   191
  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} (K 5.0)
blanchet@40977
   192
blanchet@45368
   193
fun linear_minimize test timeout result xs =
blanchet@45368
   194
  let
blanchet@45368
   195
    fun min _ [] p = p
blanchet@45368
   196
      | min timeout (x :: xs) (seen, result) =
blanchet@54816
   197
        (case test timeout (xs @ seen) of
blanchet@54816
   198
          result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
blanchet@55202
   199
          min (new_timeout timeout run_time) (filter_used_facts true used_facts xs)
blanchet@55202
   200
            (filter_used_facts false used_facts seen, result)
blanchet@54816
   201
        | _ => min timeout xs (x :: seen, result))
blanchet@54816
   202
  in
blanchet@54816
   203
    min timeout xs ([], result)
blanchet@54816
   204
  end
blanchet@38015
   205
blanchet@45368
   206
fun binary_minimize test timeout result xs =
blanchet@40977
   207
  let
blanchet@55202
   208
    fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) =
blanchet@41743
   209
        let
blanchet@45367
   210
          val (l0, r0) = chop (length xs div 2) xs
blanchet@41743
   211
(*
blanchet@55202
   212
          val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
blanchet@55202
   213
          val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs))
blanchet@55202
   214
          val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0))
blanchet@55202
   215
          val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0))
blanchet@41743
   216
*)
blanchet@45367
   217
          val depth = depth + 1
blanchet@45372
   218
          val timeout = new_timeout timeout run_time
blanchet@41743
   219
        in
blanchet@55202
   220
          (case test timeout (sup @ l0) of
blanchet@45372
   221
            result as {outcome = NONE, used_facts, ...} =>
blanchet@48798
   222
            min depth result (filter_used_facts true used_facts sup)
blanchet@48798
   223
                      (filter_used_facts true used_facts l0)
blanchet@45367
   224
          | _ =>
blanchet@55202
   225
            (case test timeout (sup @ r0) of
blanchet@45367
   226
              result as {outcome = NONE, used_facts, ...} =>
blanchet@48798
   227
              min depth result (filter_used_facts true used_facts sup)
blanchet@57054
   228
                (filter_used_facts true used_facts r0)
blanchet@45367
   229
            | _ =>
blanchet@45367
   230
              let
blanchet@45367
   231
                val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
blanchet@55202
   232
                val (sup, r0) = (sup, r0) |> pairself (filter_used_facts true (map fst sup_r0))
blanchet@45367
   233
                val (sup_l, (r, result)) = min depth result (sup @ l) r0
blanchet@48798
   234
                val sup = sup |> filter_used_facts true (map fst sup_l)
blanchet@55202
   235
              in (sup, (l @ r, result)) end))
blanchet@40977
   236
        end
blanchet@41743
   237
(*
blanchet@41743
   238
        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
blanchet@41743
   239
*)
blanchet@45367
   240
      | min _ result sup xs = (sup, (xs, result))
blanchet@45367
   241
  in
blanchet@55202
   242
    (case snd (min 0 result [] xs) of
blanchet@45372
   243
      ([x], result as {run_time, ...}) =>
blanchet@45372
   244
      (case test (new_timeout timeout run_time) [] of
blanchet@55202
   245
        result as {outcome = NONE, ...} => ([], result)
blanchet@55202
   246
      | _ => ([x], result))
blanchet@55202
   247
    | p => p)
blanchet@45367
   248
  end
blanchet@40977
   249
blanchet@54816
   250
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
blanchet@54816
   251
    preplay0 facts =
wenzelm@31236
   252
  let
blanchet@40941
   253
    val ctxt = Proof.context_of state
blanchet@54815
   254
    val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
blanchet@54130
   255
    fun test timeout = test_facts params silent prover timeout i n state goal
blanchet@48796
   256
    val (chained, non_chained) = List.partition is_fact_chained facts
blanchet@57054
   257
    (* Push chained facts to the back, so that they are less likely to be kicked out by the linear
blanchet@57054
   258
       minimization algorithm. *)
blanchet@48796
   259
    val facts = non_chained @ chained
wenzelm@31236
   260
  in
blanchet@54815
   261
    (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
blanchet@55202
   262
     (case test timeout facts of
blanchet@45371
   263
       result as {outcome = NONE, used_facts, run_time, ...} =>
blanchet@38015
   264
       let
blanchet@48798
   265
         val facts = filter_used_facts true used_facts facts
blanchet@45372
   266
         val min =
blanchet@54815
   267
           if length facts >= Config.get ctxt binary_min_facts then binary_minimize
blanchet@54815
   268
           else linear_minimize
blanchet@45368
   269
         val (min_facts, {preplay, message, message_tail, ...}) =
blanchet@45371
   270
           min test (new_timeout timeout run_time) result facts
blanchet@48321
   271
       in
blanchet@48321
   272
         print silent (fn () => cat_lines
blanchet@48321
   273
             ["Minimized to " ^ n_facts (map fst min_facts)] ^
blanchet@48796
   274
              (case min_facts |> filter is_fact_chained |> length of
blanchet@48321
   275
                 0 => ""
blanchet@48321
   276
               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
blanchet@54503
   277
         (if learn then do_learn (maps snd min_facts) else ());
blanchet@51187
   278
         (SOME min_facts,
blanchet@54815
   279
          (if is_some preplay0 andalso length min_facts = length facts then the preplay0
blanchet@54815
   280
           else preplay,
blanchet@51187
   281
           message, message_tail))
blanchet@48321
   282
       end
blanchet@43052
   283
     | {outcome = SOME TimedOut, preplay, ...} =>
blanchet@54816
   284
       (NONE, (preplay, fn _ =>
blanchet@54816
   285
          "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
blanchet@54816
   286
          \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
blanchet@55202
   287
     | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
blanchet@55285
   288
    handle ERROR msg =>
blanchet@55285
   289
      (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
wenzelm@31236
   290
  end
wenzelm@31236
   291
blanchet@55285
   292
fun adjust_proof_method_params override_params
blanchet@54816
   293
    ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
blanchet@54816
   294
      uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
blanchet@55297
   295
      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
blanchet@55297
   296
      timeout, preplay_timeout, expect} : params) =
blanchet@48250
   297
  let
blanchet@48250
   298
    fun lookup_override name default_value =
blanchet@55202
   299
      (case AList.lookup (op =) override_params name of
blanchet@48250
   300
        SOME [s] => SOME s
blanchet@55202
   301
      | _ => default_value)
blanchet@55285
   302
    (* Only those options that proof_methods are interested in are considered here. *)
blanchet@48250
   303
    val type_enc = lookup_override "type_enc" type_enc
blanchet@48250
   304
    val lam_trans = lookup_override "lam_trans" lam_trans
blanchet@48250
   305
  in
blanchet@53800
   306
    {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
blanchet@53800
   307
     provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
blanchet@53800
   308
     uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
blanchet@53800
   309
     max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
blanchet@49918
   310
     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
blanchet@55297
   311
     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
blanchet@55288
   312
     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
blanchet@48250
   313
  end
blanchet@48250
   314
blanchet@55205
   315
fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
blanchet@55205
   316
    ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
blanchet@55205
   317
    (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} :
blanchet@55205
   318
     prover_result) =
blanchet@48250
   319
  if is_some outcome orelse null used_facts then
blanchet@48250
   320
    result
blanchet@48250
   321
  else
blanchet@48250
   322
    let
blanchet@55205
   323
      val thy = Proof_Context.theory_of ctxt
blanchet@48250
   324
      val num_facts = length used_facts
blanchet@55205
   325
blanchet@48250
   326
      val ((perhaps_minimize, (minimize_name, params)), preplay) =
blanchet@48250
   327
        if mode = Normal then
blanchet@48250
   328
          if num_facts >= Config.get ctxt auto_minimize_min_facts then
blanchet@48250
   329
            ((true, (name, params)), preplay)
blanchet@48250
   330
          else
blanchet@48250
   331
            let
blanchet@48250
   332
              fun can_min_fast_enough time =
blanchet@48250
   333
                0.001
blanchet@48250
   334
                * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
blanchet@48250
   335
                <= Config.get ctxt auto_minimize_max_time
blanchet@48250
   336
              fun prover_fast_enough () = can_min_fast_enough run_time
blanchet@48250
   337
            in
blanchet@51190
   338
              (case Lazy.force preplay of
blanchet@55285
   339
                 (meth as Metis_Method _, Played timeout) =>
blanchet@51191
   340
                 if isar_proofs = SOME true then
blanchet@54816
   341
                   (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
blanchet@54816
   342
                      itself. *)
blanchet@55205
   343
                   (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
blanchet@51191
   344
                 else if can_min_fast_enough timeout then
blanchet@55285
   345
                   (true, extract_proof_method params meth
blanchet@51190
   346
                          ||> (fn override_params =>
blanchet@55285
   347
                                  adjust_proof_method_params override_params params))
blanchet@51190
   348
                 else
blanchet@51190
   349
                   (prover_fast_enough (), (name, params))
blanchet@56081
   350
               | (SMT2_Method, Played timeout) =>
blanchet@54816
   351
                 (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
blanchet@54816
   352
                    itself. *)
blanchet@51190
   353
                 (can_min_fast_enough timeout, (name, params))
blanchet@51190
   354
               | _ => (prover_fast_enough (), (name, params)),
blanchet@51190
   355
               preplay)
blanchet@48250
   356
            end
blanchet@48250
   357
        else
blanchet@54127
   358
          ((false, (name, params)), preplay)
blanchet@48250
   359
      val minimize = minimize |> the_default perhaps_minimize
blanchet@48250
   360
      val (used_facts, (preplay, message, _)) =
blanchet@48250
   361
        if minimize then
blanchet@48392
   362
          minimize_facts do_learn minimize_name params
blanchet@54824
   363
            (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
blanchet@54824
   364
            goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from))
blanchet@48250
   365
          |>> Option.map (map fst)
blanchet@48250
   366
        else
blanchet@48250
   367
          (SOME used_facts, (preplay, message, ""))
blanchet@48250
   368
    in
blanchet@55202
   369
      (case used_facts of
blanchet@48250
   370
        SOME used_facts =>
blanchet@55202
   371
        {outcome = NONE, used_facts = used_facts, used_from = used_from, run_time = run_time,
blanchet@55202
   372
         preplay = preplay, message = message, message_tail = message_tail}
blanchet@55202
   373
      | NONE => result)
blanchet@48250
   374
    end
blanchet@48250
   375
blanchet@57054
   376
fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem =
blanchet@48250
   377
  get_prover ctxt mode name params minimize_command problem
blanchet@48384
   378
  |> maybe_minimize ctxt mode do_learn name params problem
blanchet@48250
   379
blanchet@48321
   380
fun run_minimize (params as {provers, ...}) do_learn i refs state =
blanchet@38045
   381
  let
blanchet@38045
   382
    val ctxt = Proof.context_of state
blanchet@54130
   383
    val {goal, facts = chained_ths, ...} = Proof.goal state
blanchet@38696
   384
    val reserved = reserved_isar_keyword_table ()
blanchet@48396
   385
    val css = clasimpset_rule_table_of ctxt
blanchet@54130
   386
    val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css)
blanchet@38045
   387
  in
blanchet@55202
   388
    (case subgoal_count state of
wenzelm@40132
   389
      0 => Output.urgent_message "No subgoal!"
blanchet@57054
   390
    | n =>
blanchet@57054
   391
      (case provers of
blanchet@57054
   392
        [] => error "No prover is set."
blanchet@57054
   393
      | prover :: _ =>
blanchet@57054
   394
        (kill_provers ();
blanchet@57054
   395
         minimize_facts do_learn prover params false i n state goal NONE facts
blanchet@57054
   396
         |> (fn (_, (preplay, message, message_tail)) =>
blanchet@57054
   397
                Output.urgent_message (message (Lazy.force preplay) ^ message_tail)))))
blanchet@38045
   398
  end
blanchet@38045
   399
blanchet@35866
   400
end;