src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
author blanchet
Tue Aug 17 16:47:40 2010 +0200 (2010-08-17)
changeset 38490 57de0f12516f
parent 38488 3abda3c76df9
child 38586 09fe051f2782
permissions -rw-r--r--
tuning
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
     2     Author:     Philipp Meyer, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Minimization of theorem list for Metis using automatic theorem provers.
     6 *)
     7 
     8 signature SLEDGEHAMMER_FACT_MINIMIZE =
     9 sig
    10   type params = Sledgehammer.params
    11 
    12   val minimize_theorems :
    13     params -> int -> int -> Proof.state -> (string * thm list) list
    14     -> (string * thm list) list option * string
    15   val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
    16 end;
    17 
    18 structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
    19 struct
    20 
    21 open Sledgehammer_Util
    22 open Sledgehammer_Fact_Filter
    23 open Sledgehammer_Proof_Reconstruct
    24 open Sledgehammer
    25 
    26 (* wrapper for calling external prover *)
    27 
    28 fun string_for_failure Unprovable = "Unprovable."
    29   | string_for_failure TimedOut = "Timed out."
    30   | string_for_failure _ = "Unknown error."
    31 
    32 fun n_theorems name_thms_pairs =
    33   let val n = length name_thms_pairs in
    34     string_of_int n ^ " theorem" ^ plural_s n ^
    35     (if n > 0 then
    36        ": " ^ space_implode " "
    37                   (name_thms_pairs
    38                    |> map (perhaps (try (unprefix chained_prefix)))
    39                    |> sort_distinct string_ord)
    40      else
    41        "")
    42   end
    43 
    44 fun test_theorems ({debug, verbose, overlord, atps, full_types,
    45                     relevance_threshold, relevance_convergence, theory_relevant,
    46                     defs_relevant, isar_proof, isar_shrink_factor,
    47                     ...} : params)
    48                   (prover : prover) explicit_apply timeout subgoal state
    49                   name_thms_pairs =
    50   let
    51     val _ =
    52       priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
    53     val params =
    54       {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    55        full_types = full_types, explicit_apply = explicit_apply,
    56        relevance_threshold = relevance_threshold,
    57        relevance_convergence = relevance_convergence,
    58        theory_relevant = theory_relevant, defs_relevant = defs_relevant,
    59        isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    60        timeout = timeout, minimize_timeout = timeout}
    61     val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    62     val {context = ctxt, facts, goal} = Proof.goal state
    63     val problem =
    64      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    65       relevance_override = {add = [], del = [], only = false},
    66       axioms = SOME axioms}
    67     val result as {outcome, used_thm_names, ...} =
    68       prover params (K "") problem
    69   in
    70     priority (case outcome of
    71                 NONE =>
    72                 if length used_thm_names = length name_thms_pairs then
    73                   "Found proof."
    74                 else
    75                   "Found proof with " ^ n_theorems used_thm_names ^ "."
    76               | SOME failure => string_for_failure failure);
    77     result
    78   end
    79 
    80 (* minimalization of thms *)
    81 
    82 fun filter_used_facts used =
    83   filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
    84 
    85 fun sublinear_minimize _ [] p = p
    86   | sublinear_minimize test (x :: xs) (seen, result) =
    87     case test (xs @ seen) of
    88       result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
    89       sublinear_minimize test (filter_used_facts used_thm_names xs)
    90                          (filter_used_facts used_thm_names seen, result)
    91     | _ => sublinear_minimize test xs (x :: seen, result)
    92 
    93 (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
    94    preprocessing time is included in the estimate below but isn't part of the
    95    timeout. *)
    96 val fudge_msecs = 250
    97 
    98 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
    99   | minimize_theorems
   100         (params as {debug, verbose, overlord, atps as atp :: _, full_types,
   101                     relevance_threshold, relevance_convergence, theory_relevant,
   102                     defs_relevant, isar_proof, isar_shrink_factor,
   103                     minimize_timeout, ...})
   104         i n state name_thms_pairs =
   105   let
   106     val thy = Proof.theory_of state
   107     val prover = get_prover_fun thy atp
   108     val msecs = Time.toMilliseconds minimize_timeout
   109     val _ =
   110       priority ("Sledgehammer minimize: ATP " ^ quote atp ^
   111                 " with a time limit of " ^ string_of_int msecs ^ " ms.")
   112     val {context = ctxt, goal, ...} = Proof.goal state
   113     val (_, hyp_ts, concl_t) = strip_subgoal goal i
   114     val explicit_apply =
   115       not (forall (Meson.is_fol_term thy)
   116                   (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
   117     fun do_test timeout =
   118       test_theorems params prover explicit_apply timeout i state
   119     val timer = Timer.startRealTimer ()
   120   in
   121     (case do_test minimize_timeout name_thms_pairs of
   122        result as {outcome = NONE, pool, used_thm_names,
   123                   conjecture_shape, ...} =>
   124        let
   125          val time = Timer.checkRealTimer timer
   126          val new_timeout =
   127            Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
   128            |> Time.fromMilliseconds
   129          val (min_thms, {proof, axiom_names, ...}) =
   130            sublinear_minimize (do_test new_timeout)
   131                (filter_used_facts used_thm_names name_thms_pairs) ([], result)
   132          val n = length min_thms
   133          val _ = priority (cat_lines
   134            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
   135             (case filter (String.isPrefix chained_prefix o fst) min_thms of
   136                [] => ""
   137              | chained => " (including " ^ Int.toString (length chained) ^
   138                           " chained)") ^ ".")
   139        in
   140          (SOME min_thms,
   141           proof_text isar_proof
   142               (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   143               (full_types, K "", proof, axiom_names, goal, i) |> fst)
   144        end
   145      | {outcome = SOME TimedOut, ...} =>
   146        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
   147               \option (e.g., \"timeout = " ^
   148               string_of_int (10 + msecs div 1000) ^ " s\").")
   149      | {outcome = SOME UnknownError, ...} =>
   150        (* Failure sometimes mean timeout, unfortunately. *)
   151        (NONE, "Failure: No proof was found with the current time limit. You \
   152               \can increase the time limit using the \"timeout\" \
   153               \option (e.g., \"timeout = " ^
   154               string_of_int (10 + msecs div 1000) ^ " s\").")
   155      | {message, ...} => (NONE, "ATP error: " ^ message))
   156     handle ERROR msg => (NONE, "Error: " ^ msg)
   157   end
   158 
   159 fun run_minimize params i refs state =
   160   let
   161     val ctxt = Proof.context_of state
   162     val chained_ths = #facts (Proof.goal state)
   163     val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
   164   in
   165     case subgoal_count state of
   166       0 => priority "No subgoal!"
   167     | n =>
   168       (kill_atps ();
   169        priority (#2 (minimize_theorems params i n state name_thms_pairs)))
   170   end
   171 
   172 end;