summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

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

5 Minimization of theorem list for Metis using automatic theorem provers.

6 *)

8 signature SLEDGEHAMMER_FACT_MINIMIZER =

9 sig

10 type params = ATP_Manager.params

11 type prover_result = ATP_Manager.prover_result

13 val minimize_theorems :

14 params -> int -> int -> Proof.state -> (string * thm list) list

15 -> (string * thm list) list option * string

16 end;

18 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =

19 struct

21 open Sledgehammer_Util

22 open Sledgehammer_Fact_Preprocessor

23 open Sledgehammer_Proof_Reconstruct

24 open ATP_Manager

26 (* Linear minimization algorithm *)

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

38 (* wrapper for calling external prover *)

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

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

69 (* minimalization of thms *)

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

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

131 end;