src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
changeset 36375 2482446a604c
parent 36370 a4f601daa175
child 36378 f32c567dbcaa
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Apr 23 17:38:25 2010 +0200
     1.3 @@ -0,0 +1,128 @@
     1.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
     1.5 +    Author:     Philipp Meyer, TU Muenchen
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7 +
     1.8 +Minimization of theorem list for Metis using automatic theorem provers.
     1.9 +*)
    1.10 +
    1.11 +signature SLEDGEHAMMER_FACT_MINIMIZER =
    1.12 +sig
    1.13 +  type params = ATP_Manager.params
    1.14 +  type prover = ATP_Manager.prover
    1.15 +  type prover_result = ATP_Manager.prover_result
    1.16 +
    1.17 +  val minimize_theorems :
    1.18 +    params -> prover -> string -> int -> Proof.state -> (string * thm list) list
    1.19 +    -> (string * thm list) list option * string
    1.20 +end;
    1.21 +
    1.22 +structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
    1.23 +struct
    1.24 +
    1.25 +open Sledgehammer_Util
    1.26 +open Sledgehammer_Fact_Preprocessor
    1.27 +open Sledgehammer_Proof_Reconstruct
    1.28 +open ATP_Manager
    1.29 +
    1.30 +(* Linear minimization algorithm *)
    1.31 +
    1.32 +fun linear_minimize test s =
    1.33 +  let
    1.34 +    fun aux [] p = p
    1.35 +      | aux (x :: xs) (needed, result) =
    1.36 +        case test (xs @ needed) of
    1.37 +          SOME result => aux xs (needed, result)
    1.38 +        | NONE => aux xs (x :: needed, result)
    1.39 +  in aux s end
    1.40 +
    1.41 +
    1.42 +(* wrapper for calling external prover *)
    1.43 +
    1.44 +fun string_for_failure Unprovable = "Unprovable."
    1.45 +  | string_for_failure TimedOut = "Timed out."
    1.46 +  | string_for_failure OutOfResources = "Failed."
    1.47 +  | string_for_failure OldSpass = "Error."
    1.48 +  | string_for_failure MalformedOutput = "Error."
    1.49 +  | string_for_failure UnknownError = "Failed."
    1.50 +fun string_for_outcome NONE = "Success."
    1.51 +  | string_for_outcome (SOME failure) = string_for_failure failure
    1.52 +
    1.53 +fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
    1.54 +        timeout subgoal state filtered_clauses name_thms_pairs =
    1.55 +  let
    1.56 +    val num_theorems = length name_thms_pairs
    1.57 +    val _ = priority ("Testing " ^ string_of_int num_theorems ^
    1.58 +                      " theorem" ^ plural_s num_theorems ^ "...")
    1.59 +    val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    1.60 +    val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    1.61 +    val {context = ctxt, facts, goal} = Proof.goal state
    1.62 +    val problem =
    1.63 +     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    1.64 +      relevance_override = {add = [], del = [], only = false},
    1.65 +      axiom_clauses = SOME axclauses,
    1.66 +      filtered_clauses = SOME (the_default axclauses filtered_clauses)}
    1.67 +  in
    1.68 +    prover params (K "") timeout problem
    1.69 +    |> tap (priority o string_for_outcome o #outcome)
    1.70 +  end
    1.71 +
    1.72 +(* minimalization of thms *)
    1.73 +
    1.74 +fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
    1.75 +                                  sorts, ...})
    1.76 +                      prover atp_name i state name_thms_pairs =
    1.77 +  let
    1.78 +    val msecs = Time.toMilliseconds minimize_timeout
    1.79 +    val n = length name_thms_pairs
    1.80 +    val _ =
    1.81 +      priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^
    1.82 +                " with a time limit of " ^ string_of_int msecs ^ " ms.")
    1.83 +    val test_thms_fun =
    1.84 +      sledgehammer_test_theorems params prover minimize_timeout i state
    1.85 +    fun test_thms filtered thms =
    1.86 +      case test_thms_fun filtered thms of
    1.87 +        (result as {outcome = NONE, ...}) => SOME result
    1.88 +      | _ => NONE
    1.89 +
    1.90 +    val {context = ctxt, facts, goal} = Proof.goal state;
    1.91 +    val n = Logic.count_prems (prop_of goal)
    1.92 +  in
    1.93 +    (* try prove first to check result and get used theorems *)
    1.94 +    (case test_thms_fun NONE name_thms_pairs of
    1.95 +      result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
    1.96 +        let
    1.97 +          val used = internal_thm_names |> Vector.foldr (op ::) []
    1.98 +                                        |> sort_distinct string_ord
    1.99 +          val to_use =
   1.100 +            if length used < length name_thms_pairs then
   1.101 +              filter (fn (name1, _) => List.exists (curry (op =) name1) used)
   1.102 +                     name_thms_pairs
   1.103 +            else name_thms_pairs
   1.104 +          val (min_thms, {proof, internal_thm_names, ...}) =
   1.105 +            linear_minimize (test_thms (SOME filtered_clauses)) to_use
   1.106 +                            ([], result)
   1.107 +          val n = length min_thms
   1.108 +          val _ = priority (cat_lines
   1.109 +            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
   1.110 +        in
   1.111 +          (SOME min_thms,
   1.112 +           proof_text isar_proof debug modulus sorts ctxt
   1.113 +                      (K "", proof, internal_thm_names, goal, i) |> fst)
   1.114 +        end
   1.115 +    | {outcome = SOME TimedOut, ...} =>
   1.116 +        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
   1.117 +               \option (e.g., \"timeout = " ^
   1.118 +               string_of_int (10 + msecs div 1000) ^ " s\").")
   1.119 +    | {outcome = SOME UnknownError, ...} =>
   1.120 +        (* Failure sometimes mean timeout, unfortunately. *)
   1.121 +        (NONE, "Failure: No proof was found with the current time limit. You \
   1.122 +               \can increase the time limit using the \"timeout\" \
   1.123 +               \option (e.g., \"timeout = " ^
   1.124 +               string_of_int (10 + msecs div 1000) ^ " s\").")
   1.125 +    | {message, ...} => (NONE, "ATP error: " ^ message))
   1.126 +    handle Sledgehammer_HOL_Clause.TRIVIAL =>
   1.127 +        (SOME [], metis_line i n [])
   1.128 +      | ERROR msg => (NONE, "Error: " ^ msg)
   1.129 +  end
   1.130 +
   1.131 +end;