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