src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
author blanchet
Wed Dec 12 21:48:29 2012 +0100 (2012-12-12 ago)
changeset 50510 7e4f2f8d9b50
parent 50020 6b9611abcd4c
child 50557 31313171deb5
permissions -rw-r--r--
export a pair of ML functions
blanchet@38988
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_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@38988
     8
signature SLEDGEHAMMER_MINIMIZE =
boehmes@32525
     9
sig
blanchet@46340
    10
  type stature = ATP_Problem_Generate.stature
blanchet@49914
    11
  type play = Sledgehammer_Reconstruct.play
blanchet@48250
    12
  type mode = Sledgehammer_Provers.mode
blanchet@41087
    13
  type params = Sledgehammer_Provers.params
blanchet@48250
    14
  type prover = Sledgehammer_Provers.prover
blanchet@35867
    15
blanchet@42646
    16
  val binary_min_facts : int Config.T
blanchet@48250
    17
  val auto_minimize_min_facts : int Config.T
blanchet@48250
    18
  val auto_minimize_max_time : real Config.T
blanchet@40061
    19
  val minimize_facts :
blanchet@48399
    20
    (string -> thm list -> unit) -> string -> params -> bool -> int -> int
blanchet@48399
    21
    -> Proof.state -> ((string * stature) * thm list) list
blanchet@46340
    22
    -> ((string * stature) * thm list) list option
blanchet@43261
    23
       * ((unit -> play) * (play -> string) * string)
blanchet@48321
    24
  val get_minimizing_prover :
blanchet@48399
    25
    Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
blanchet@38996
    26
  val run_minimize :
blanchet@48399
    27
    params -> (string -> thm list -> unit) -> int
blanchet@48399
    28
    -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
blanchet@35866
    29
end;
boehmes@32525
    30
blanchet@38988
    31
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
immler@31037
    32
struct
immler@31037
    33
blanchet@43085
    34
open ATP_Util
blanchet@39496
    35
open ATP_Proof
blanchet@46320
    36
open ATP_Problem_Generate
blanchet@36142
    37
open Sledgehammer_Util
blanchet@48250
    38
open Sledgehammer_Fact
blanchet@49914
    39
open Sledgehammer_Reconstruct
blanchet@41087
    40
open Sledgehammer_Provers
blanchet@35866
    41
blanchet@36370
    42
(* wrapper for calling external prover *)
wenzelm@31236
    43
blanchet@40061
    44
fun n_facts names =
blanchet@38698
    45
  let val n = length names in
blanchet@40061
    46
    string_of_int n ^ " fact" ^ plural_s n ^
blanchet@38092
    47
    (if n > 0 then
blanchet@48085
    48
       ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
blanchet@38092
    49
     else
blanchet@38092
    50
       "")
blanchet@38092
    51
  end
blanchet@38092
    52
blanchet@41091
    53
fun print silent f = if silent then () else Output.urgent_message (f ())
blanchet@41091
    54
blanchet@42724
    55
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
blanchet@46301
    56
                 max_new_mono_instances, type_enc, strict, lam_trans,
blanchet@50020
    57
                 uncurried_aliases, isar_proofs, isar_shrink,
blanchet@46409
    58
                 preplay_timeout, ...} : params)
blanchet@43064
    59
               silent (prover : prover) timeout i n state facts =
wenzelm@31236
    60
  let
blanchet@41277
    61
    val _ =
blanchet@41277
    62
      print silent (fn () =>
blanchet@41277
    63
          "Testing " ^ n_facts (map fst facts) ^
blanchet@41277
    64
          (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
blanchet@43085
    65
           else "") ^ "...")
blanchet@41742
    66
    val {goal, ...} = Proof.goal state
blanchet@44463
    67
    val facts =
blanchet@44463
    68
      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
blanchet@38100
    69
    val params =
blanchet@42060
    70
      {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
blanchet@46301
    71
       provers = provers, type_enc = type_enc, strict = strict,
blanchet@46409
    72
       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
blanchet@48321
    73
       learn = false, fact_filter = NONE, max_facts = SOME (length facts),
blanchet@48314
    74
       fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
blanchet@49918
    75
       max_new_mono_instances = max_new_mono_instances,
blanchet@50020
    76
       isar_proofs = isar_proofs, isar_shrink = isar_shrink,
blanchet@49918
    77
       slice = false, minimize = SOME false, timeout = timeout,
blanchet@45707
    78
       preplay_timeout = preplay_timeout, expect = ""}
blanchet@40065
    79
    val problem =
blanchet@40065
    80
      {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@47531
    81
       facts = facts}
blanchet@45370
    82
    val result as {outcome, used_facts, run_time, ...} =
blanchet@45520
    83
      prover params (K (K (K ""))) problem
blanchet@36223
    84
  in
blanchet@43259
    85
    print silent
blanchet@43259
    86
          (fn () =>
blanchet@43259
    87
              case outcome of
blanchet@43259
    88
                SOME failure => string_for_failure failure
blanchet@43259
    89
              | NONE =>
blanchet@43259
    90
                "Found proof" ^
blanchet@43259
    91
                 (if length used_facts = length facts then ""
blanchet@45370
    92
                  else " with " ^ n_facts used_facts) ^
blanchet@45370
    93
                 " (" ^ string_from_time run_time ^ ").");
blanchet@38092
    94
    result
blanchet@36223
    95
  end
wenzelm@31236
    96
blanchet@40204
    97
(* minimalization of facts *)
wenzelm@31236
    98
blanchet@45372
    99
(* Give the external prover some slack. The ATP gets further slack because the
blanchet@45372
   100
   Sledgehammer preprocessing time is included in the estimate below but isn't
blanchet@45372
   101
   part of the timeout. *)
blanchet@45372
   102
val slack_msecs = 200
blanchet@45372
   103
blanchet@45372
   104
fun new_timeout timeout run_time =
blanchet@45372
   105
  Int.min (Time.toMilliseconds timeout,
blanchet@45372
   106
           Time.toMilliseconds run_time + slack_msecs)
blanchet@45372
   107
  |> Time.fromMilliseconds
blanchet@45372
   108
blanchet@45367
   109
(* The linear algorithm usually outperforms the binary algorithm when over 60%
blanchet@45367
   110
   of the facts are actually needed. The binary algorithm is much more
blanchet@45367
   111
   appropriate for provers that cannot return the list of used facts and hence
blanchet@45367
   112
   returns all facts as used. Since we cannot know in advance how many facts are
blanchet@45367
   113
   actually needed, we heuristically set the threshold to 10 facts. *)
blanchet@42646
   114
val binary_min_facts =
blanchet@42646
   115
  Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
blanchet@45368
   116
                          (K 20)
blanchet@48250
   117
val auto_minimize_min_facts =
blanchet@48250
   118
  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
blanchet@48250
   119
      (fn generic => Config.get_generic generic binary_min_facts)
blanchet@48250
   120
val auto_minimize_max_time =
blanchet@48250
   121
  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
blanchet@48250
   122
                           (K 5.0)
blanchet@40977
   123
blanchet@45368
   124
fun linear_minimize test timeout result xs =
blanchet@45368
   125
  let
blanchet@45368
   126
    fun min _ [] p = p
blanchet@45368
   127
      | min timeout (x :: xs) (seen, result) =
blanchet@45368
   128
        case test timeout (xs @ seen) of
blanchet@45372
   129
          result as {outcome = NONE, used_facts, run_time, ...}
blanchet@45372
   130
          : prover_result =>
blanchet@48798
   131
          min (new_timeout timeout run_time)
blanchet@48798
   132
              (filter_used_facts true used_facts xs)
blanchet@48798
   133
              (filter_used_facts false used_facts seen, result)
blanchet@45368
   134
        | _ => min timeout xs (x :: seen, result)
blanchet@48799
   135
  in min timeout xs ([], result) end
blanchet@38015
   136
blanchet@45368
   137
fun binary_minimize test timeout result xs =
blanchet@40977
   138
  let
blanchet@45372
   139
    fun min depth (result as {run_time, ...} : prover_result) sup
blanchet@45372
   140
            (xs as _ :: _ :: _) =
blanchet@41743
   141
        let
blanchet@45367
   142
          val (l0, r0) = chop (length xs div 2) xs
blanchet@41743
   143
(*
blanchet@45366
   144
          val _ = warning (replicate_string depth " " ^ "{ " ^
blanchet@45366
   145
                           "sup: " ^ n_facts (map fst sup))
blanchet@45366
   146
          val _ = warning (replicate_string depth " " ^ "  " ^
blanchet@45366
   147
                           "xs: " ^ n_facts (map fst xs))
blanchet@45366
   148
          val _ = warning (replicate_string depth " " ^ "  " ^
blanchet@45366
   149
                           "l0: " ^ n_facts (map fst l0))
blanchet@45366
   150
          val _ = warning (replicate_string depth " " ^ "  " ^
blanchet@45366
   151
                           "r0: " ^ n_facts (map fst r0))
blanchet@41743
   152
*)
blanchet@45367
   153
          val depth = depth + 1
blanchet@45372
   154
          val timeout = new_timeout timeout run_time
blanchet@41743
   155
        in
blanchet@45368
   156
          case test timeout (sup @ l0) of
blanchet@45372
   157
            result as {outcome = NONE, used_facts, ...} =>
blanchet@48798
   158
            min depth result (filter_used_facts true used_facts sup)
blanchet@48798
   159
                      (filter_used_facts true used_facts l0)
blanchet@45367
   160
          | _ =>
blanchet@45368
   161
            case test timeout (sup @ r0) of
blanchet@45367
   162
              result as {outcome = NONE, used_facts, ...} =>
blanchet@48798
   163
              min depth result (filter_used_facts true used_facts sup)
blanchet@48798
   164
                        (filter_used_facts true used_facts r0)
blanchet@45367
   165
            | _ =>
blanchet@45367
   166
              let
blanchet@45367
   167
                val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
blanchet@45367
   168
                val (sup, r0) =
blanchet@48798
   169
                  (sup, r0)
blanchet@48798
   170
                  |> pairself (filter_used_facts true (map fst sup_r0))
blanchet@45367
   171
                val (sup_l, (r, result)) = min depth result (sup @ l) r0
blanchet@48798
   172
                val sup = sup |> filter_used_facts true (map fst sup_l)
blanchet@45367
   173
              in (sup, (l @ r, result)) end
blanchet@40977
   174
        end
blanchet@41743
   175
(*
blanchet@41743
   176
        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
blanchet@41743
   177
*)
blanchet@45367
   178
      | min _ result sup xs = (sup, (xs, result))
blanchet@45367
   179
  in
blanchet@45367
   180
    case snd (min 0 result [] xs) of
blanchet@45372
   181
      ([x], result as {run_time, ...}) =>
blanchet@45372
   182
      (case test (new_timeout timeout run_time) [] of
blanchet@45367
   183
         result as {outcome = NONE, ...} => ([], result)
blanchet@45367
   184
       | _ => ([x], result))
blanchet@45367
   185
    | p => p
blanchet@45367
   186
  end
blanchet@40977
   187
blanchet@48321
   188
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
blanchet@48321
   189
                   i n state facts =
wenzelm@31236
   190
  let
blanchet@40941
   191
    val ctxt = Proof.context_of state
blanchet@45574
   192
    val prover =
blanchet@45574
   193
      get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
blanchet@45368
   194
    fun test timeout = test_facts params silent prover timeout i n state
blanchet@48796
   195
    val (chained, non_chained) = List.partition is_fact_chained facts
blanchet@48799
   196
    (* Push chained facts to the back, so that they are less likely to be
blanchet@48799
   197
       kicked out by the linear minimization algorithm. *)
blanchet@48796
   198
    val facts = non_chained @ chained
wenzelm@31236
   199
  in
blanchet@48796
   200
    (print silent (fn () => "Sledgehammer minimizer: " ^
blanchet@48796
   201
                            quote prover_name ^ ".");
blanchet@48796
   202
     case test timeout facts of
blanchet@45371
   203
       result as {outcome = NONE, used_facts, run_time, ...} =>
blanchet@38015
   204
       let
blanchet@48798
   205
         val facts = filter_used_facts true used_facts facts
blanchet@45372
   206
         val min =
blanchet@42646
   207
           if length facts >= Config.get ctxt binary_min_facts then
blanchet@45368
   208
             binary_minimize
blanchet@40977
   209
           else
blanchet@45368
   210
             linear_minimize
blanchet@45368
   211
         val (min_facts, {preplay, message, message_tail, ...}) =
blanchet@45371
   212
           min test (new_timeout timeout run_time) result facts
blanchet@48321
   213
       in
blanchet@48321
   214
         print silent (fn () => cat_lines
blanchet@48321
   215
             ["Minimized to " ^ n_facts (map fst min_facts)] ^
blanchet@48796
   216
              (case min_facts |> filter is_fact_chained |> length of
blanchet@48321
   217
                 0 => ""
blanchet@48321
   218
               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
blanchet@48399
   219
         (if learn then do_learn prover_name (maps snd min_facts) else ());
blanchet@48321
   220
         (SOME min_facts, (preplay, message, message_tail))
blanchet@48321
   221
       end
blanchet@43052
   222
     | {outcome = SOME TimedOut, preplay, ...} =>
blanchet@43052
   223
       (NONE,
blanchet@43052
   224
        (preplay,
blanchet@43052
   225
         fn _ => "Timeout: You can increase the time limit using the \
blanchet@43052
   226
                 \\"timeout\" option (e.g., \"timeout = " ^
blanchet@45371
   227
                 string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
blanchet@45371
   228
                 "\").",
blanchet@43261
   229
         ""))
blanchet@43052
   230
     | {preplay, message, ...} =>
blanchet@43261
   231
       (NONE, (preplay, prefix "Prover error: " o message, "")))
blanchet@43166
   232
    handle ERROR msg =>
blanchet@45519
   233
           (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
wenzelm@31236
   234
  end
wenzelm@31236
   235
blanchet@48250
   236
fun adjust_reconstructor_params override_params
blanchet@48250
   237
        ({debug, verbose, overlord, blocking, provers, type_enc, strict,
blanchet@48321
   238
         lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
blanchet@49918
   239
         fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
blanchet@50020
   240
         isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
blanchet@48321
   241
         : params) =
blanchet@48250
   242
  let
blanchet@48250
   243
    fun lookup_override name default_value =
blanchet@48250
   244
      case AList.lookup (op =) override_params name of
blanchet@48250
   245
        SOME [s] => SOME s
blanchet@48250
   246
      | _ => default_value
blanchet@48250
   247
    (* Only those options that reconstructors are interested in are considered
blanchet@48250
   248
       here. *)
blanchet@48250
   249
    val type_enc = lookup_override "type_enc" type_enc
blanchet@48250
   250
    val lam_trans = lookup_override "lam_trans" lam_trans
blanchet@48250
   251
  in
blanchet@48250
   252
    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
blanchet@48250
   253
     provers = provers, type_enc = type_enc, strict = strict,
blanchet@48250
   254
     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
blanchet@48321
   255
     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
blanchet@48314
   256
     fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
blanchet@49918
   257
     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
blanchet@50020
   258
     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
blanchet@49918
   259
     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
blanchet@48250
   260
  end
blanchet@48250
   261
blanchet@48384
   262
fun maybe_minimize ctxt mode do_learn name
blanchet@49918
   263
        (params as {verbose, isar_proofs, minimize, ...})
blanchet@48384
   264
        ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
blanchet@48384
   265
        (result as {outcome, used_facts, run_time, preplay, message,
blanchet@48384
   266
                    message_tail} : prover_result) =
blanchet@48250
   267
  if is_some outcome orelse null used_facts then
blanchet@48250
   268
    result
blanchet@48250
   269
  else
blanchet@48250
   270
    let
blanchet@48250
   271
      val num_facts = length used_facts
blanchet@48250
   272
      val ((perhaps_minimize, (minimize_name, params)), preplay) =
blanchet@48250
   273
        if mode = Normal then
blanchet@48250
   274
          if num_facts >= Config.get ctxt auto_minimize_min_facts then
blanchet@48250
   275
            ((true, (name, params)), preplay)
blanchet@48250
   276
          else
blanchet@48250
   277
            let
blanchet@48250
   278
              fun can_min_fast_enough time =
blanchet@48250
   279
                0.001
blanchet@48250
   280
                * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
blanchet@48250
   281
                <= Config.get ctxt auto_minimize_max_time
blanchet@48250
   282
              fun prover_fast_enough () = can_min_fast_enough run_time
blanchet@48250
   283
            in
blanchet@49918
   284
              if isar_proofs then
blanchet@48250
   285
                ((prover_fast_enough (), (name, params)), preplay)
blanchet@48250
   286
              else
blanchet@48250
   287
                let val preplay = preplay () in
blanchet@48250
   288
                  (case preplay of
blanchet@48250
   289
                     Played (reconstr, timeout) =>
blanchet@48250
   290
                     if can_min_fast_enough timeout then
blanchet@48250
   291
                       (true, extract_reconstructor params reconstr
blanchet@48250
   292
                              ||> (fn override_params =>
blanchet@48250
   293
                                      adjust_reconstructor_params
blanchet@48250
   294
                                          override_params params))
blanchet@48250
   295
                     else
blanchet@48250
   296
                       (prover_fast_enough (), (name, params))
blanchet@48250
   297
                   | _ => (prover_fast_enough (), (name, params)),
blanchet@48250
   298
                   K preplay)
blanchet@48250
   299
                end
blanchet@48250
   300
            end
blanchet@48250
   301
        else
blanchet@48250
   302
          ((false, (name, params)), preplay)
blanchet@48250
   303
      val minimize = minimize |> the_default perhaps_minimize
blanchet@48250
   304
      val (used_facts, (preplay, message, _)) =
blanchet@48250
   305
        if minimize then
blanchet@48392
   306
          minimize_facts do_learn minimize_name params
blanchet@48392
   307
                         (mode <> Normal orelse not verbose) subgoal
blanchet@48250
   308
                         subgoal_count state
blanchet@48798
   309
                         (filter_used_facts true used_facts
blanchet@48250
   310
                              (map (apsnd single o untranslated_fact) facts))
blanchet@48250
   311
          |>> Option.map (map fst)
blanchet@48250
   312
        else
blanchet@48250
   313
          (SOME used_facts, (preplay, message, ""))
blanchet@48250
   314
    in
blanchet@48250
   315
      case used_facts of
blanchet@48250
   316
        SOME used_facts =>
blanchet@48394
   317
        {outcome = NONE, used_facts = used_facts, run_time = run_time,
blanchet@48394
   318
         preplay = preplay, message = message, message_tail = message_tail}
blanchet@48250
   319
      | NONE => result
blanchet@48250
   320
    end
blanchet@48250
   321
blanchet@48321
   322
fun get_minimizing_prover ctxt mode do_learn name params minimize_command
blanchet@48321
   323
                          problem =
blanchet@48250
   324
  get_prover ctxt mode name params minimize_command problem
blanchet@48384
   325
  |> maybe_minimize ctxt mode do_learn name params problem
blanchet@48250
   326
blanchet@48321
   327
fun run_minimize (params as {provers, ...}) do_learn i refs state =
blanchet@38045
   328
  let
blanchet@38045
   329
    val ctxt = Proof.context_of state
blanchet@38696
   330
    val reserved = reserved_isar_keyword_table ()
blanchet@48292
   331
    val chained_ths = #facts (Proof.goal state)
blanchet@48396
   332
    val css = clasimpset_rule_table_of ctxt
blanchet@40204
   333
    val facts =
blanchet@46388
   334
      refs |> maps (map (apsnd single)
blanchet@48396
   335
                    o fact_from_ref ctxt reserved chained_ths css)
blanchet@38045
   336
  in
blanchet@38045
   337
    case subgoal_count state of
wenzelm@40132
   338
      0 => Output.urgent_message "No subgoal!"
blanchet@41265
   339
    | n => case provers of
blanchet@41265
   340
             [] => error "No prover is set."
blanchet@41265
   341
           | prover :: _ =>
blanchet@41265
   342
             (kill_provers ();
blanchet@48321
   343
              minimize_facts do_learn prover params false i n state facts
blanchet@43261
   344
              |> (fn (_, (preplay, message, message_tail)) =>
blanchet@43261
   345
                     message (preplay ()) ^ message_tail
blanchet@43261
   346
                     |> Output.urgent_message))
blanchet@38045
   347
  end
blanchet@38045
   348
blanchet@35866
   349
end;