author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37628  78334f400ae6 
child 37926  e6ff246c0cdb 
permissions  rwrr 
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36370
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

2 
Author: Philipp Meyer, TU Muenchen 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

4 

35867  5 
Minimization of theorem list for Metis using automatic theorem provers. 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

6 
*) 
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

7 

36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36370
diff
changeset

8 
signature SLEDGEHAMMER_FACT_MINIMIZER = 
32525  9 
sig 
35969  10 
type params = ATP_Manager.params 
35867  11 
type prover_result = ATP_Manager.prover_result 
12 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

13 
val minimize_theorems : 
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset

14 
params > int > int > Proof.state > (string * thm list) list 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

15 
> (string * thm list) list option * string 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

16 
end; 
32525  17 

36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36370
diff
changeset

18 
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

19 
struct 
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

20 

37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37506
diff
changeset

21 
open Clausifier 
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

22 
open Metis_Clauses 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

23 
open Sledgehammer_Util 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset

24 
open Sledgehammer_Proof_Reconstruct 
35867  25 
open ATP_Manager 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

26 

513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

27 
(* Linear minimization algorithm *) 
33492
4168294a9f96
Command atp_minimize uses the naive linear algorithm now
nipkow
parents:
33316
diff
changeset

28 

36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

29 
fun linear_minimize test s = 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

30 
let 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

31 
fun aux [] p = p 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

32 
 aux (x :: xs) (needed, result) = 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

33 
case test (xs @ needed) of 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

34 
SOME result => aux xs (needed, result) 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

35 
 NONE => aux xs (x :: needed, result) 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

36 
in aux s end 
31236  37 

31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

38 

36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

39 
(* wrapper for calling external prover *) 
31236  40 

36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

41 
fun string_for_failure Unprovable = "Unprovable." 
37418  42 
 string_for_failure IncompleteUnprovable = "Failed." 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

43 
 string_for_failure TimedOut = "Timed out." 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

44 
 string_for_failure OutOfResources = "Failed." 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

45 
 string_for_failure OldSpass = "Error." 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

46 
 string_for_failure MalformedOutput = "Error." 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

47 
 string_for_failure UnknownError = "Failed." 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

48 
fun string_for_outcome NONE = "Success." 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

49 
 string_for_outcome (SOME failure) = string_for_failure failure 
31236  50 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

51 
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

52 
filtered_clauses name_thms_pairs = 
31236  53 
let 
37628  54 
val thy = Proof.theory_of state 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

55 
val num_theorems = length name_thms_pairs 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

56 
val _ = priority ("Testing " ^ string_of_int num_theorems ^ 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

57 
" theorem" ^ plural_s num_theorems ^ "...") 
32525  58 
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs 
37628  59 
val axclauses = cnf_rules_pairs thy true name_thm_pairs 
36263
56bf63d70120
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
blanchet
parents:
36232
diff
changeset

60 
val {context = ctxt, facts, goal} = Proof.goal state 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32937
diff
changeset

61 
val problem = 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset

62 
{subgoal = subgoal, goal = (ctxt, (facts, goal)), 
35969  63 
relevance_override = {add = [], del = [], only = false}, 
36232
4d425766a47f
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
blanchet
parents:
36231
diff
changeset

64 
axiom_clauses = SOME axclauses, 
4d425766a47f
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
blanchet
parents:
36231
diff
changeset

65 
filtered_clauses = SOME (the_default axclauses filtered_clauses)} 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

66 
in 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

67 
prover params (K "") timeout problem 
36607
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36488
diff
changeset

68 
> tap (fn result : prover_result => 
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36488
diff
changeset

69 
priority (string_for_outcome (#outcome result))) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

70 
end 
31236  71 

72 
(* minimalization of thms *) 

73 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

74 
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, 
36924  75 
isar_proof, isar_shrink_factor, ...}) 
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset

76 
i n state name_thms_pairs = 
31236  77 
let 
36378  78 
val thy = Proof.theory_of state 
79 
val prover = case atps of 

80 
[atp_name] => get_prover thy atp_name 

81 
 _ => error "Expected a single ATP." 

35969  82 
val msecs = Time.toMilliseconds minimize_timeout 
31236  83 
val _ = 
36378  84 
priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ 
36224  85 
" with a time limit of " ^ string_of_int msecs ^ " ms.") 
35969  86 
val test_thms_fun = 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset

87 
sledgehammer_test_theorems params prover minimize_timeout i state 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset

88 
fun test_thms filtered thms = 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

89 
case test_thms_fun filtered thms of 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

90 
(result as {outcome = NONE, ...}) => SOME result 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

91 
 _ => NONE 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

92 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

93 
val {context = ctxt, goal, ...} = Proof.goal state; 
31236  94 
in 
95 
(* try prove first to check result and get used theorems *) 

31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31236
diff
changeset

96 
(case test_thms_fun NONE name_thms_pairs of 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset

97 
result as {outcome = NONE, pool, internal_thm_names, conjecture_shape, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset

98 
filtered_clauses, ...} => 
31236  99 
let 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

100 
val used = internal_thm_names > Vector.foldr (op ::) [] 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

101 
> sort_distinct string_ord 
31236  102 
val to_use = 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

103 
if length used < length name_thms_pairs then 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36382
diff
changeset

104 
filter (fn (name1, _) => exists (curry (op =) name1) used) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

105 
name_thms_pairs 
33305  106 
else name_thms_pairs 
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36224
diff
changeset

107 
val (min_thms, {proof, internal_thm_names, ...}) = 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

108 
linear_minimize (test_thms (SOME filtered_clauses)) to_use 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

109 
([], result) 
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset

110 
val m = length min_thms 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

111 
val _ = priority (cat_lines 
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset

112 
["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

113 
in 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

114 
(SOME min_thms, 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset

115 
proof_text isar_proof 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37418
diff
changeset

116 
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37418
diff
changeset

117 
(full_types, K "", proof, internal_thm_names, goal, i) > fst) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

118 
end 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

119 
 {outcome = SOME TimedOut, ...} => 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

120 
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

121 
\option (e.g., \"timeout = " ^ 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

122 
string_of_int (10 + msecs div 1000) ^ " s\").") 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

123 
 {outcome = SOME UnknownError, ...} => 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

124 
(* Failure sometimes mean timeout, unfortunately. *) 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

125 
(NONE, "Failure: No proof was found with the current time limit. You \ 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

126 
\can increase the time limit using the \"timeout\" \ 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

127 
\option (e.g., \"timeout = " ^ 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

128 
string_of_int (10 + msecs div 1000) ^ " s\").") 
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

129 
 {message, ...} => (NONE, "ATP error: " ^ message)) 
37506
32a1ee39c49b
missing "Unsynchronized" + make exception take a unit
blanchet
parents:
37498
diff
changeset

130 
handle TRIVIAL () => (SOME [], metis_line full_types i n []) 
36382  131 
 ERROR msg => (NONE, "Error: " ^ msg) 
31236  132 
end 
133 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

134 
end; 