src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
author blanchet
Mon Apr 26 21:20:43 2010 +0200 (2010-04-26)
changeset 36402 1b20805974c7
parent 36393 be73a2b2443b
child 36481 af99c98121d6
permissions -rw-r--r--
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure
blanchet@36375
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
immler@31037
     2
    Author:     Philipp Meyer, TU Muenchen
blanchet@36370
     3
    Author:     Jasmin Blanchette, TU Muenchen
immler@31037
     4
blanchet@35867
     5
Minimization of theorem list for Metis using automatic theorem provers.
immler@31037
     6
*)
immler@31037
     7
blanchet@36375
     8
signature SLEDGEHAMMER_FACT_MINIMIZER =
boehmes@32525
     9
sig
blanchet@35969
    10
  type params = ATP_Manager.params
blanchet@35867
    11
  type prover_result = ATP_Manager.prover_result
blanchet@35867
    12
blanchet@35866
    13
  val minimize_theorems :
blanchet@36378
    14
    params -> int -> Proof.state -> (string * thm list) list
blanchet@35866
    15
    -> (string * thm list) list option * string
blanchet@35866
    16
end;
boehmes@32525
    17
blanchet@36375
    18
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
immler@31037
    19
struct
immler@31037
    20
blanchet@36142
    21
open Sledgehammer_Util
blanchet@35866
    22
open Sledgehammer_Fact_Preprocessor
blanchet@36063
    23
open Sledgehammer_Proof_Reconstruct
blanchet@35867
    24
open ATP_Manager
blanchet@35866
    25
blanchet@35866
    26
(* Linear minimization algorithm *)
nipkow@33492
    27
blanchet@36223
    28
fun linear_minimize test s =
blanchet@35866
    29
  let
blanchet@36223
    30
    fun aux [] p = p
blanchet@36223
    31
      | aux (x :: xs) (needed, result) =
blanchet@36223
    32
        case test (xs @ needed) of
blanchet@36223
    33
          SOME result => aux xs (needed, result)
blanchet@36223
    34
        | NONE => aux xs (x :: needed, result)
blanchet@36223
    35
  in aux s end
wenzelm@31236
    36
immler@31037
    37
blanchet@36370
    38
(* wrapper for calling external prover *)
wenzelm@31236
    39
blanchet@36370
    40
fun string_for_failure Unprovable = "Unprovable."
blanchet@36370
    41
  | string_for_failure TimedOut = "Timed out."
blanchet@36370
    42
  | string_for_failure OutOfResources = "Failed."
blanchet@36370
    43
  | string_for_failure OldSpass = "Error."
blanchet@36370
    44
  | string_for_failure MalformedOutput = "Error."
blanchet@36370
    45
  | string_for_failure UnknownError = "Failed."
blanchet@36370
    46
fun string_for_outcome NONE = "Success."
blanchet@36370
    47
  | string_for_outcome (SOME failure) = string_for_failure failure
wenzelm@31236
    48
blanchet@35969
    49
fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
blanchet@36223
    50
        timeout subgoal state filtered_clauses name_thms_pairs =
wenzelm@31236
    51
  let
blanchet@36142
    52
    val num_theorems = length name_thms_pairs
blanchet@36142
    53
    val _ = priority ("Testing " ^ string_of_int num_theorems ^
blanchet@36142
    54
                      " theorem" ^ plural_s num_theorems ^ "...")
boehmes@32525
    55
    val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
blanchet@35866
    56
    val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
blanchet@36263
    57
    val {context = ctxt, facts, goal} = Proof.goal state
wenzelm@32941
    58
    val problem =
blanchet@36063
    59
     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
blanchet@35969
    60
      relevance_override = {add = [], del = [], only = false},
blanchet@36232
    61
      axiom_clauses = SOME axclauses,
blanchet@36232
    62
      filtered_clauses = SOME (the_default axclauses filtered_clauses)}
blanchet@36223
    63
  in
blanchet@36370
    64
    prover params (K "") timeout problem
blanchet@36370
    65
    |> tap (priority o string_for_outcome o #outcome)
blanchet@36223
    66
  end
wenzelm@31236
    67
wenzelm@31236
    68
(* minimalization of thms *)
wenzelm@31236
    69
blanchet@36378
    70
fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
blanchet@36402
    71
                                  shrink_factor, sorts, ...})
blanchet@36378
    72
                      i state name_thms_pairs =
wenzelm@31236
    73
  let
blanchet@36378
    74
    val thy = Proof.theory_of state
blanchet@36378
    75
    val prover = case atps of
blanchet@36378
    76
                   [atp_name] => get_prover thy atp_name
blanchet@36378
    77
                 | _ => error "Expected a single ATP."
blanchet@35969
    78
    val msecs = Time.toMilliseconds minimize_timeout
blanchet@36224
    79
    val n = length name_thms_pairs
wenzelm@31236
    80
    val _ =
blanchet@36378
    81
      priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
blanchet@36224
    82
                " with a time limit of " ^ string_of_int msecs ^ " ms.")
blanchet@35969
    83
    val test_thms_fun =
blanchet@36063
    84
      sledgehammer_test_theorems params prover minimize_timeout i state
immler@31752
    85
    fun test_thms filtered thms =
blanchet@36223
    86
      case test_thms_fun filtered thms of
blanchet@36370
    87
        (result as {outcome = NONE, ...}) => SOME result
blanchet@36223
    88
      | _ => NONE
blanchet@36223
    89
blanchet@36223
    90
    val {context = ctxt, facts, goal} = Proof.goal state;
blanchet@36223
    91
    val n = Logic.count_prems (prop_of goal)
wenzelm@31236
    92
  in
wenzelm@31236
    93
    (* try prove first to check result and get used theorems *)
immler@31409
    94
    (case test_thms_fun NONE name_thms_pairs of
blanchet@36402
    95
      result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
blanchet@36402
    96
                 filtered_clauses, ...} =>
wenzelm@31236
    97
        let
blanchet@36223
    98
          val used = internal_thm_names |> Vector.foldr (op ::) []
blanchet@36223
    99
                                        |> sort_distinct string_ord
wenzelm@31236
   100
          val to_use =
blanchet@36223
   101
            if length used < length name_thms_pairs then
blanchet@36393
   102
              filter (fn (name1, _) => exists (curry (op =) name1) used)
blanchet@36223
   103
                     name_thms_pairs
wenzelm@33305
   104
            else name_thms_pairs
blanchet@36231
   105
          val (min_thms, {proof, internal_thm_names, ...}) =
blanchet@36223
   106
            linear_minimize (test_thms (SOME filtered_clauses)) to_use
blanchet@36223
   107
                            ([], result)
blanchet@36224
   108
          val n = length min_thms
wenzelm@32947
   109
          val _ = priority (cat_lines
blanchet@36224
   110
            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
blanchet@36223
   111
        in
blanchet@36223
   112
          (SOME min_thms,
blanchet@36402
   113
           proof_text isar_proof
blanchet@36402
   114
                      (pool, debug, shrink_factor, sorts, ctxt,
blanchet@36402
   115
                       conjecture_shape)
blanchet@36287
   116
                      (K "", proof, internal_thm_names, goal, i) |> fst)
blanchet@36223
   117
        end
blanchet@36370
   118
    | {outcome = SOME TimedOut, ...} =>
blanchet@36142
   119
        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
blanchet@36142
   120
               \option (e.g., \"timeout = " ^
blanchet@36142
   121
               string_of_int (10 + msecs div 1000) ^ " s\").")
blanchet@36370
   122
    | {outcome = SOME UnknownError, ...} =>
blanchet@36142
   123
        (* Failure sometimes mean timeout, unfortunately. *)
blanchet@36142
   124
        (NONE, "Failure: No proof was found with the current time limit. You \
blanchet@36142
   125
               \can increase the time limit using the \"timeout\" \
blanchet@36142
   126
               \option (e.g., \"timeout = " ^
blanchet@36370
   127
               string_of_int (10 + msecs div 1000) ^ " s\").")
blanchet@36370
   128
    | {message, ...} => (NONE, "ATP error: " ^ message))
blanchet@36382
   129
    handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n [])
blanchet@36382
   130
         | ERROR msg => (NONE, "Error: " ^ msg)
wenzelm@31236
   131
  end
wenzelm@31236
   132
blanchet@35866
   133
end;