src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
author blanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42740 31334a7b109d
parent 42724 4d6bcf846759
child 43004 20e9caff1f86
permissions -rw-r--r--
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
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@38988
    10
  type locality = Sledgehammer_Filter.locality
blanchet@41087
    11
  type params = Sledgehammer_Provers.params
blanchet@35867
    12
blanchet@42646
    13
  val binary_min_facts : int Config.T
blanchet@41255
    14
  val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
blanchet@40061
    15
  val minimize_facts :
blanchet@41742
    16
    string -> params -> bool option -> bool -> int -> int -> Proof.state
blanchet@41091
    17
    -> ((string * locality) * thm list) list
blanchet@38752
    18
    -> ((string * locality) * thm list) list option * string
blanchet@38996
    19
  val run_minimize :
blanchet@38996
    20
    params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
blanchet@35866
    21
end;
boehmes@32525
    22
blanchet@38988
    23
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
immler@31037
    24
struct
immler@31037
    25
blanchet@39496
    26
open ATP_Proof
blanchet@36142
    27
open Sledgehammer_Util
blanchet@38988
    28
open Sledgehammer_Filter
blanchet@41087
    29
open Sledgehammer_Provers
blanchet@35866
    30
blanchet@36370
    31
(* wrapper for calling external prover *)
wenzelm@31236
    32
blanchet@40061
    33
fun n_facts names =
blanchet@38698
    34
  let val n = length names in
blanchet@40061
    35
    string_of_int n ^ " fact" ^ plural_s n ^
blanchet@38092
    36
    (if n > 0 then
blanchet@38698
    37
       ": " ^ (names |> map fst
blanchet@38698
    38
                     |> sort_distinct string_ord |> space_implode " ")
blanchet@38092
    39
     else
blanchet@38092
    40
       "")
blanchet@38092
    41
  end
blanchet@38092
    42
blanchet@41091
    43
fun print silent f = if silent then () else Output.urgent_message (f ())
blanchet@41091
    44
blanchet@42724
    45
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
blanchet@42740
    46
                 max_new_mono_instances, type_sys, isar_proof,
blanchet@42740
    47
                 isar_shrink_factor, ...} : params)
blanchet@41742
    48
        explicit_apply_opt silent (prover : prover) timeout i n state facts =
wenzelm@31236
    49
  let
blanchet@41742
    50
    val thy = Proof.theory_of state
blanchet@41277
    51
    val _ =
blanchet@41277
    52
      print silent (fn () =>
blanchet@41277
    53
          "Testing " ^ n_facts (map fst facts) ^
blanchet@41277
    54
          (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
blanchet@41277
    55
          else "") ^ "...")
blanchet@41742
    56
    val {goal, ...} = Proof.goal state
blanchet@41742
    57
    val explicit_apply =
blanchet@41742
    58
      case explicit_apply_opt of
blanchet@41742
    59
        SOME explicit_apply => explicit_apply
blanchet@41742
    60
      | NONE =>
blanchet@41742
    61
        let val (_, hyp_ts, concl_t) = strip_subgoal goal i in
blanchet@41742
    62
          not (forall (Meson.is_fol_term thy)
blanchet@41742
    63
                      (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
blanchet@41742
    64
        end
blanchet@38100
    65
    val params =
blanchet@42060
    66
      {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
blanchet@41138
    67
       provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
blanchet@41138
    68
       relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
blanchet@42740
    69
       max_mono_iters = max_mono_iters,
blanchet@42740
    70
       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
blanchet@42740
    71
       isar_shrink_factor = isar_shrink_factor, slicing = false,
blanchet@42740
    72
       timeout = timeout, expect = ""}
blanchet@40204
    73
    val facts =
blanchet@41090
    74
      facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
blanchet@40065
    75
    val problem =
blanchet@40065
    76
      {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@41741
    77
       facts = facts, smt_filter = NONE}
blanchet@40204
    78
    val result as {outcome, used_facts, ...} = prover params (K "") problem
blanchet@36223
    79
  in
blanchet@41277
    80
    print silent (fn () =>
blanchet@41277
    81
        case outcome of
blanchet@41745
    82
          SOME failure => string_for_failure failure
blanchet@41745
    83
        | NONE => if length used_facts = length facts then "Found proof."
blanchet@41745
    84
                  else "Found proof with " ^ n_facts used_facts ^ ".");
blanchet@38092
    85
    result
blanchet@36223
    86
  end
wenzelm@31236
    87
blanchet@40204
    88
(* minimalization of facts *)
wenzelm@31236
    89
blanchet@40977
    90
(* The sublinear algorithm works well in almost all situations, except when the
blanchet@40977
    91
   external prover cannot return the list of used facts and hence returns all
blanchet@41267
    92
   facts as used. In that case, the binary algorithm is much more appropriate.
blanchet@41267
    93
   We can usually detect the situation by looking at the number of used facts
blanchet@41267
    94
   reported by the prover. *)
blanchet@42646
    95
val binary_min_facts =
blanchet@42646
    96
  Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
blanchet@42646
    97
                          (K 20)
blanchet@40977
    98
blanchet@40204
    99
fun filter_used_facts used = filter (member (op =) used o fst)
blanchet@38015
   100
blanchet@38015
   101
fun sublinear_minimize _ [] p = p
blanchet@38015
   102
  | sublinear_minimize test (x :: xs) (seen, result) =
blanchet@38015
   103
    case test (xs @ seen) of
blanchet@40204
   104
      result as {outcome = NONE, used_facts, ...} : prover_result =>
blanchet@40204
   105
      sublinear_minimize test (filter_used_facts used_facts xs)
blanchet@40204
   106
                         (filter_used_facts used_facts seen, result)
blanchet@38015
   107
    | _ => sublinear_minimize test xs (x :: seen, result)
blanchet@38015
   108
blanchet@40977
   109
fun binary_minimize test xs =
blanchet@40977
   110
  let
blanchet@40977
   111
    fun p xs = #outcome (test xs : prover_result) = NONE
blanchet@40977
   112
    fun split [] p = p
blanchet@40977
   113
      | split [h] (l, r) = (h :: l, r)
blanchet@40977
   114
      | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
blanchet@41743
   115
    fun min _ _ [] = raise Empty
blanchet@41743
   116
      | min _ _ [s0] = [s0]
blanchet@41743
   117
      | min depth sup xs =
blanchet@41743
   118
        let
blanchet@41743
   119
(*
blanchet@41743
   120
          val _ = warning (replicate_string depth " " ^ "{" ^ ("  " ^
blanchet@41743
   121
                           n_facts (map fst sup) ^ " and " ^
blanchet@41743
   122
                           n_facts (map fst xs)))
blanchet@41743
   123
*)
blanchet@41743
   124
          val (l0, r0) = split xs ([], [])
blanchet@41743
   125
        in
blanchet@40977
   126
          if p (sup @ l0) then
blanchet@41743
   127
            min (depth + 1) sup l0
blanchet@40977
   128
          else if p (sup @ r0) then
blanchet@41743
   129
            min (depth + 1) sup r0
blanchet@40977
   130
          else
blanchet@40977
   131
            let
blanchet@41743
   132
              val l = min (depth + 1) (sup @ r0) l0
blanchet@41743
   133
              val r = min (depth + 1) (sup @ l) r0
blanchet@40977
   134
            in l @ r end
blanchet@40977
   135
        end
blanchet@41743
   136
(*
blanchet@41743
   137
        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
blanchet@41743
   138
*)
blanchet@40977
   139
    val xs =
blanchet@41743
   140
      case min 0 [] xs of
blanchet@40977
   141
        [x] => if p [] then [] else [x]
blanchet@40977
   142
      | xs => xs
blanchet@40977
   143
  in (xs, test xs) end
blanchet@40977
   144
blanchet@40977
   145
(* Give the external prover some slack. The ATP gets further slack because the
blanchet@40977
   146
   Sledgehammer preprocessing time is included in the estimate below but isn't
blanchet@40977
   147
   part of the timeout. *)
blanchet@41277
   148
val slack_msecs = 200
blanchet@38092
   149
blanchet@41742
   150
fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
blanchet@41742
   151
                   silent i n state facts =
wenzelm@31236
   152
  let
blanchet@40941
   153
    val ctxt = Proof.context_of state
blanchet@42444
   154
    val prover = get_prover ctxt false prover_name
blanchet@38590
   155
    val msecs = Time.toMilliseconds timeout
blanchet@41091
   156
    val _ = print silent (fn () => "Sledgehammer minimize: " ^
blanchet@40977
   157
                                   quote prover_name ^ ".")
blanchet@38100
   158
    fun do_test timeout =
blanchet@41742
   159
      test_facts params explicit_apply_opt silent prover timeout i n state
blanchet@38092
   160
    val timer = Timer.startRealTimer ()
wenzelm@31236
   161
  in
blanchet@40204
   162
    (case do_test timeout facts of
blanchet@40204
   163
       result as {outcome = NONE, used_facts, ...} =>
blanchet@38015
   164
       let
blanchet@38092
   165
         val time = Timer.checkRealTimer timer
blanchet@38092
   166
         val new_timeout =
blanchet@41277
   167
           Int.min (msecs, Time.toMilliseconds time + slack_msecs)
blanchet@38092
   168
           |> Time.fromMilliseconds
blanchet@40977
   169
         val facts = filter_used_facts used_facts facts
blanchet@40061
   170
         val (min_thms, {message, ...}) =
blanchet@42646
   171
           if length facts >= Config.get ctxt binary_min_facts then
blanchet@40977
   172
             binary_minimize (do_test new_timeout) facts
blanchet@40977
   173
           else
blanchet@40977
   174
             sublinear_minimize (do_test new_timeout) facts ([], result)
blanchet@38094
   175
         val n = length min_thms
blanchet@41091
   176
         val _ = print silent (fn () => cat_lines
blanchet@40061
   177
           ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
blanchet@38752
   178
            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
blanchet@38698
   179
               0 => ""
wenzelm@41491
   180
             | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
blanchet@40061
   181
       in (SOME min_thms, message) end
blanchet@38015
   182
     | {outcome = SOME TimedOut, ...} =>
blanchet@38015
   183
       (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
blanchet@38015
   184
              \option (e.g., \"timeout = " ^
blanchet@40341
   185
              string_of_int (10 + msecs div 1000) ^ "\").")
blanchet@40977
   186
     | {message, ...} => (NONE, "Prover error: " ^ message))
blanchet@37994
   187
    handle ERROR msg => (NONE, "Error: " ^ msg)
wenzelm@31236
   188
  end
wenzelm@31236
   189
blanchet@41265
   190
fun run_minimize (params as {provers, ...}) i refs state =
blanchet@38045
   191
  let
blanchet@38045
   192
    val ctxt = Proof.context_of state
blanchet@38696
   193
    val reserved = reserved_isar_keyword_table ()
blanchet@38045
   194
    val chained_ths = #facts (Proof.goal state)
blanchet@40204
   195
    val facts =
blanchet@41091
   196
      refs
blanchet@41091
   197
      |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
blanchet@38045
   198
  in
blanchet@38045
   199
    case subgoal_count state of
wenzelm@40132
   200
      0 => Output.urgent_message "No subgoal!"
blanchet@41265
   201
    | n => case provers of
blanchet@41265
   202
             [] => error "No prover is set."
blanchet@41265
   203
           | prover :: _ =>
blanchet@41265
   204
             (kill_provers ();
blanchet@41742
   205
              minimize_facts prover params NONE false i n state facts
blanchet@41265
   206
              |> #2 |> Output.urgent_message)
blanchet@38045
   207
  end
blanchet@38045
   208
blanchet@35866
   209
end;