src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
author blanchet
Fri May 14 11:23:42 2010 +0200 (2010-05-14)
changeset 36909 7d5587f6d5f7
parent 36607 e5f7235f39c5
child 36924 ff01d3ae9ad4
permissions -rw-r--r--
made Sledgehammer's full-typed proof reconstruction work for the first time;
previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.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_MINIMIZER =
     9 sig
    10   type params = ATP_Manager.params
    11   type prover_result = ATP_Manager.prover_result
    12 
    13   val minimize_theorems :
    14     params -> int -> int -> Proof.state -> (string * thm list) list
    15     -> (string * thm list) list option * string
    16 end;
    17 
    18 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
    19 struct
    20 
    21 open Sledgehammer_Util
    22 open Sledgehammer_Fact_Preprocessor
    23 open Sledgehammer_Proof_Reconstruct
    24 open ATP_Manager
    25 
    26 (* Linear minimization algorithm *)
    27 
    28 fun linear_minimize test s =
    29   let
    30     fun aux [] p = p
    31       | aux (x :: xs) (needed, result) =
    32         case test (xs @ needed) of
    33           SOME result => aux xs (needed, result)
    34         | NONE => aux xs (x :: needed, result)
    35   in aux s end
    36 
    37 
    38 (* wrapper for calling external prover *)
    39 
    40 fun string_for_failure Unprovable = "Unprovable."
    41   | string_for_failure TimedOut = "Timed out."
    42   | string_for_failure OutOfResources = "Failed."
    43   | string_for_failure OldSpass = "Error."
    44   | string_for_failure MalformedOutput = "Error."
    45   | string_for_failure UnknownError = "Failed."
    46 fun string_for_outcome NONE = "Success."
    47   | string_for_outcome (SOME failure) = string_for_failure failure
    48 
    49 fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
    50         timeout subgoal state filtered_clauses name_thms_pairs =
    51   let
    52     val num_theorems = length name_thms_pairs
    53     val _ = priority ("Testing " ^ string_of_int num_theorems ^
    54                       " theorem" ^ plural_s num_theorems ^ "...")
    55     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    56     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    57     val {context = ctxt, facts, goal} = Proof.goal state
    58     val problem =
    59      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    60       relevance_override = {add = [], del = [], only = false},
    61       axiom_clauses = SOME axclauses,
    62       filtered_clauses = SOME (the_default axclauses filtered_clauses)}
    63   in
    64     prover params (K "") timeout problem
    65     |> tap (fn result : prover_result =>
    66          priority (string_for_outcome (#outcome result)))
    67   end
    68 
    69 (* minimalization of thms *)
    70 
    71 fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
    72                                   isar_proof, shrink_factor, ...})
    73                       i n state name_thms_pairs =
    74   let
    75     val thy = Proof.theory_of state
    76     val prover = case atps of
    77                    [atp_name] => get_prover thy atp_name
    78                  | _ => error "Expected a single ATP."
    79     val msecs = Time.toMilliseconds minimize_timeout
    80     val _ =
    81       priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
    82                 " with a time limit of " ^ string_of_int msecs ^ " ms.")
    83     val test_thms_fun =
    84       sledgehammer_test_theorems params prover minimize_timeout i state
    85     fun test_thms filtered thms =
    86       case test_thms_fun filtered thms of
    87         (result as {outcome = NONE, ...}) => SOME result
    88       | _ => NONE
    89 
    90     val {context = ctxt, facts, goal} = Proof.goal state;
    91   in
    92     (* try prove first to check result and get used theorems *)
    93     (case test_thms_fun NONE name_thms_pairs of
    94       result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
    95                  filtered_clauses, ...} =>
    96         let
    97           val used = internal_thm_names |> Vector.foldr (op ::) []
    98                                         |> sort_distinct string_ord
    99           val to_use =
   100             if length used < length name_thms_pairs then
   101               filter (fn (name1, _) => exists (curry (op =) name1) used)
   102                      name_thms_pairs
   103             else name_thms_pairs
   104           val (min_thms, {proof, internal_thm_names, ...}) =
   105             linear_minimize (test_thms (SOME filtered_clauses)) to_use
   106                             ([], result)
   107           val m = length min_thms
   108           val _ = priority (cat_lines
   109             ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
   110         in
   111           (SOME min_thms,
   112            proof_text isar_proof
   113                (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
   114                (K "", proof, internal_thm_names, goal, i) |> fst)
   115         end
   116     | {outcome = SOME TimedOut, ...} =>
   117         (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
   118                \option (e.g., \"timeout = " ^
   119                string_of_int (10 + msecs div 1000) ^ " s\").")
   120     | {outcome = SOME UnknownError, ...} =>
   121         (* Failure sometimes mean timeout, unfortunately. *)
   122         (NONE, "Failure: No proof was found with the current time limit. You \
   123                \can increase the time limit using the \"timeout\" \
   124                \option (e.g., \"timeout = " ^
   125                string_of_int (10 + msecs div 1000) ^ " s\").")
   126     | {message, ...} => (NONE, "ATP error: " ^ message))
   127     handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n [])
   128          | ERROR msg => (NONE, "Error: " ^ msg)
   129   end
   130 
   131 end;