author  blanchet 
Sat, 18 Dec 2010 13:48:24 +0100  
changeset 41268  56b7e277fd7d 
parent 41266  b6b77c963f11 
child 41274  6a9306c427b9 
permissions  rwrr 
32564  1 
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML 
2 
Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich 

32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

3 
*) 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

4 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

5 
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

6 
struct 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

7 

32521  8 
val proverK = "prover" 
32541  9 
val prover_timeoutK = "prover_timeout" 
32521  10 
val keepK = "keep" 
11 
val full_typesK = "full_types" 

41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

12 
val type_sysK = "type_sys" 
32525  13 
val minimizeK = "minimize" 
14 
val minimize_timeoutK = "minimize_timeout" 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

15 
val metis_ftK = "metis_ft" 
32521  16 

17 
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " 

32525  18 
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

19 
fun reconstructor_tag reconstructor id = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

20 
"#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " 
32521  21 

32525  22 
val separator = "" 
23 

32521  24 

32549  25 
datatype sh_data = ShData of { 
26 
calls: int, 

27 
success: int, 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

28 
nontriv_calls: int, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

29 
nontriv_success: int, 
32585  30 
lemmas: int, 
32818  31 
max_lems: int, 
32549  32 
time_isa: int, 
40062  33 
time_prover: int, 
34 
time_prover_fail: int} 

32549  35 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

36 
datatype re_data = ReData of { 
32549  37 
calls: int, 
38 
success: int, 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

39 
nontriv_calls: int, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

40 
nontriv_success: int, 
32676  41 
proofs: int, 
32549  42 
time: int, 
32550  43 
timeout: int, 
32990  44 
lemmas: int * int * int, 
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

45 
posns: (Position.T * bool) list 
32550  46 
} 
32549  47 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

48 
datatype min_data = MinData of { 
32609  49 
succs: int, 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

50 
ab_ratios: int 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

51 
} 
32521  52 

32818  53 
fun make_sh_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

54 
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, 
40062  55 
time_prover,time_prover_fail) = 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

56 
ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

57 
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, 
40062  58 
time_isa=time_isa, time_prover=time_prover, 
59 
time_prover_fail=time_prover_fail} 

32521  60 

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

61 
fun make_min_data (succs, ab_ratios) = 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

62 
MinData{succs=succs, ab_ratios=ab_ratios} 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

63 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

64 
fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

65 
timeout,lemmas,posns) = 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

66 
ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

67 
nontriv_success=nontriv_success, proofs=proofs, time=time, 
32990  68 
timeout=timeout, lemmas=lemmas, posns=posns} 
32549  69 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

70 
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) 
35871
c93bda4fdf15
remove the iteration counter from Sledgehammer's minimizer
blanchet
parents:
35867
diff
changeset

71 
val empty_min_data = make_min_data (0, 0) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

72 
val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

73 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

74 
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

75 
lemmas, max_lems, time_isa, 
40062  76 
time_prover, time_prover_fail}) = (calls, success, nontriv_calls, 
77 
nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

78 

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

79 
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

80 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

81 
fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

82 
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

83 
nontriv_success, proofs, time, timeout, lemmas, posns) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

84 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

85 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

86 
datatype reconstructor_mode = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

87 
Unminimized  Minimized  UnminimizedFT  MinimizedFT 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

88 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

89 
datatype data = Data of { 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

90 
sh: sh_data, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

91 
min: min_data, 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

92 
re_u: re_data, (* reconstructor with unminimized set of lemmas *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

93 
re_m: re_data, (* reconstructor with minimized set of lemmas *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

94 
re_uft: re_data, (* reconstructor with unminimized set of lemmas and fullytyped *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

95 
re_mft: re_data, (* reconstructor with minimized set of lemmas and fullytyped *) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

96 
mini: bool (* with minimization *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

97 
} 
32521  98 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

99 
fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

100 
Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft, 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

101 
mini=mini} 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

102 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

103 
val empty_data = make_data (empty_sh_data, empty_min_data, 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

104 
empty_re_data, empty_re_data, empty_re_data, empty_re_data, false) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

105 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

106 
fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

107 
let val sh' = make_sh_data (f (tuple_of_sh_data sh)) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

108 
in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

109 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

110 
fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

111 
let val min' = make_min_data (f (tuple_of_min_data min)) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

112 
in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end 
32521  113 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

114 
fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

115 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

116 
fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

117 
 map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

118 
 map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

119 
 map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft) 
32521  120 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

121 
val f' = make_re_data o f o tuple_of_re_data 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

122 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

123 
val (re_u', re_m', re_uft', re_mft') = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

124 
map_me f' m (re_u, re_m, re_uft, re_mft) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

125 
in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

126 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

127 
fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

128 
make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) 
32990  129 

130 
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); 

32521  131 

32818  132 
val inc_sh_calls = map_sh_data 
40062  133 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
134 
=> (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) 

32549  135 

32818  136 
val inc_sh_success = map_sh_data 
40062  137 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
138 
=> (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

139 

ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

140 
val inc_sh_nontriv_calls = map_sh_data 
40062  141 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
142 
=> (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

143 

ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

144 
val inc_sh_nontriv_success = map_sh_data 
40062  145 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
146 
=> (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) 

32585  147 

32818  148 
fun inc_sh_lemmas n = map_sh_data 
40062  149 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
150 
=> (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) 

32521  151 

32818  152 
fun inc_sh_max_lems n = map_sh_data 
40062  153 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
154 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) 

32549  155 

32818  156 
fun inc_sh_time_isa t = map_sh_data 
40062  157 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
158 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) 

32818  159 

40062  160 
fun inc_sh_time_prover t = map_sh_data 
161 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 

162 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) 

32521  163 

40062  164 
fun inc_sh_time_prover_fail t = map_sh_data 
165 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 

166 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

167 

32818  168 
val inc_min_succs = map_min_data 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

169 
(fn (succs,ab_ratios) => (succs+1, ab_ratios)) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

170 

32818  171 
fun inc_min_ab_ratios r = map_min_data 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

172 
(fn (succs, ab_ratios) => (succs, ab_ratios+r)) 
32549  173 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

174 
val inc_reconstructor_calls = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

175 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

176 
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) 
32533  177 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

178 
val inc_reconstructor_success = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

179 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

180 
=> (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

181 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

182 
val inc_reconstructor_nontriv_calls = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

183 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

184 
=> (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

185 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

186 
val inc_reconstructor_nontriv_success = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

187 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

188 
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) 
32676  189 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

190 
val inc_reconstructor_proofs = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

191 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

192 
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

193 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

194 
fun inc_reconstructor_time m t = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

195 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

196 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m 
32536  197 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

198 
val inc_reconstructor_timeout = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

199 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

200 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) 
32549  201 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

202 
fun inc_reconstructor_lemmas m n = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

203 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

204 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

205 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

206 
fun inc_reconstructor_posns m pos = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

207 
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

208 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m 
32521  209 

210 
local 

211 

212 
val str = string_of_int 

213 
val str3 = Real.fmt (StringCvt.FIX (SOME 3)) 

214 
fun percentage a b = string_of_int (a * 100 div b) 

215 
fun time t = Real.fromInt t / 1000.0 

216 
fun avg_time t n = 

217 
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 

218 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

219 
fun log_sh_data log 
40062  220 
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = 
32818  221 
(log ("Total number of sledgehammer calls: " ^ str calls); 
222 
log ("Number of successful sledgehammer calls: " ^ str success); 

223 
log ("Number of sledgehammer lemmas: " ^ str lemmas); 

224 
log ("Max number of sledgehammer lemmas: " ^ str max_lems); 

225 
log ("Success rate: " ^ percentage success calls ^ "%"); 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

226 
log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

227 
log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); 
32818  228 
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); 
40062  229 
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); 
230 
log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); 

32536  231 
log ("Average time for sledgehammer calls (Isabelle): " ^ 
32818  232 
str3 (avg_time time_isa calls)); 
32533  233 
log ("Average time for successful sledgehammer calls (ATP): " ^ 
40062  234 
str3 (avg_time time_prover success)); 
32536  235 
log ("Average time for failed sledgehammer calls (ATP): " ^ 
40062  236 
str3 (avg_time time_prover_fail (calls  success))) 
32533  237 
) 
32521  238 

32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

239 

39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

240 
fun str_of_pos (pos, triv) = 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

241 
let val str0 = string_of_int o the_default 0 
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

242 
in 
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

243 
str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^ 
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

244 
(if triv then "[T]" else "") 
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

245 
end 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

246 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

247 
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

248 
re_nontriv_success, re_proofs, re_time, re_timeout, 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

249 
(lemmas, lems_sos, lems_max), re_posns) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

250 
(log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

251 
log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

252 
" (proof: " ^ str re_proofs ^ ")"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

253 
log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

254 
log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

255 
log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

256 
log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

257 
" (proof: " ^ str re_proofs ^ ")"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

258 
log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

259 
log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

260 
log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

261 
log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

262 
log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

263 
str3 (avg_time re_time re_success)); 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

264 
if tag="" 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

265 
then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

266 
else () 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

267 
) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

268 

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

269 
fun log_min_data log (succs, ab_ratios) = 
32609  270 
(log ("Number of successful minimizations: " ^ string_of_int succs); 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

271 
log ("After/before ratios: " ^ string_of_int ab_ratios) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

272 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

273 

32521  274 
in 
275 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

276 
fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

277 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

278 
val ShData {calls=sh_calls, ...} = sh 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

279 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

280 
fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

281 
fun log_re tag m = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

282 
log_re_data log tag sh_calls (tuple_of_re_data m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

283 
fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () => 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

284 
(log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2))) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

285 
in 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

286 
if sh_calls > 0 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

287 
then 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

288 
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

289 
log_sh_data log (tuple_of_sh_data sh); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

290 
log ""; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

291 
if not mini 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

292 
then log_reconstructor ("", re_u) ("fullytyped ", re_uft) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

293 
else 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

294 
app_if re_u (fn () => 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

295 
(log_reconstructor ("unminimized ", re_u) ("unminimized fullytyped ", re_uft); 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

296 
log ""; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

297 
app_if re_m (fn () => 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

298 
(log_min_data log (tuple_of_min_data min); log ""; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

299 
log_reconstructor ("", re_m) ("fullytyped ", re_mft)))))) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

300 
else () 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

301 
end 
32521  302 

303 
end 

304 

305 

306 
(* Warning: we implicitly assume singlethreaded execution here! *) 

32740  307 
val data = Unsynchronized.ref ([] : (int * data) list) 
32521  308 

32740  309 
fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

310 
fun done id ({log, ...}: Mirabelle.done_args) = 
32521  311 
AList.lookup (op =) (!data) id 
312 
> Option.map (log_data id log) 

313 
> K () 

314 

32740  315 
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) 
32521  316 

317 

40069  318 
fun get_prover ctxt args = 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

319 
let 
40062  320 
fun default_prover_name () = 
40069  321 
hd (#provers (Sledgehammer_Isar.default_params ctxt [])) 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

322 
handle Empty => error "No ATP available." 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

323 
fun get_prover name = 
41264  324 
(name, Sledgehammer_Run.get_minimizing_prover ctxt false name) 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

325 
in 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

326 
(case AList.lookup (op =) args proverK of 
40062  327 
SOME name => get_prover name 
328 
 NONE => get_prover (default_prover_name ())) 

33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

329 
end 
32525  330 

38988  331 
type locality = Sledgehammer_Filter.locality 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

332 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

333 
(* hack *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

334 
fun reconstructor_from_msg msg = 
41154  335 
if String.isSubstring "metisFT" msg then "metisFT" 
336 
else if String.isSubstring "metis" msg then "metis" 

337 
else "smt" 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

338 

32521  339 
local 
340 

32536  341 
datatype sh_result = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

342 
SH_OK of int * int * (string * locality) list  
32536  343 
SH_FAIL of int * int  
344 
SH_ERROR 

345 

41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

346 
fun run_sh prover_name prover type_sys hard_timeout timeout dir st = 
32521  347 
let 
38998  348 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st 
349 
val i = 1 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

350 
fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir 
39321  351 
 change_dir NONE = I 
352 
val st' = 

353 
st > Proof.map_context 

354 
(change_dir dir 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

355 
#> Config.put Sledgehammer_Provers.measure_run_time true) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

356 
val params as {type_sys, relevance_thresholds, max_relevant, ...} = 
40069  357 
Sledgehammer_Isar.default_params ctxt 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

358 
[("verbose", "true"), 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

359 
("type_sys", type_sys), 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

360 
("timeout", Int.toString timeout)] 
40062  361 
val default_max_relevant = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

362 
Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40301
diff
changeset

363 
val is_built_in_const = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

364 
Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40694
diff
changeset

365 
val relevance_fudge = 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

366 
Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

367 
val relevance_override = {add = [], del = [], only = false} 
38998  368 
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

369 
val no_dangerous_types = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

370 
Sledgehammer_ATP_Translate.types_dangerous_types type_sys 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40200
diff
changeset

371 
val facts = 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

372 
Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41091
diff
changeset

373 
relevance_thresholds 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40301
diff
changeset

374 
(the_default default_max_relevant max_relevant) is_built_in_const 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

375 
relevance_fudge relevance_override chained_ths hyp_ts concl_t 
39004
f1b465f889b5
translate the axioms to FOF once and for all ATPs
blanchet
parents:
39003
diff
changeset

376 
val problem = 
39321  377 
{state = st', goal = goal, subgoal = i, 
40065  378 
subgoal_count = Sledgehammer_Util.subgoal_count st, 
41243  379 
facts = facts > map Sledgehammer_Provers.Untranslated_Fact, 
380 
smt_head = NONE} 

32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

381 
val time_limit = 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

382 
(case hard_timeout of 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

383 
NONE => I 
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

384 
 SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) 
40374
443b426e05ea
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
blanchet
parents:
40372
diff
changeset

385 
val ({outcome, message, used_facts, run_time_in_msecs, ...} 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset

386 
: Sledgehammer_Provers.prover_result, 
35971  387 
time_isa) = time_limit (Mirabelle.cpu_time 
38103  388 
(prover params (K ""))) problem 
40374
443b426e05ea
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
blanchet
parents:
40372
diff
changeset

389 
val time_prover = run_time_in_msecs > the_default ~1 
32521  390 
in 
36405  391 
case outcome of 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40200
diff
changeset

392 
NONE => (message, SH_OK (time_isa, time_prover, used_facts)) 
40062  393 
 SOME _ => (message, SH_FAIL (time_isa, time_prover)) 
32521  394 
end 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37631
diff
changeset

395 
handle ERROR msg => ("error: " ^ msg, SH_ERROR) 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

396 
 TimeLimit.TimeOut => ("timeout", SH_ERROR) 
32521  397 

32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

398 
fun thms_of_name ctxt name = 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

399 
let 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset

400 
val lex = Keyword.get_lexicons 
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

401 
val get = maps (ProofContext.get_fact ctxt o fst) 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

402 
in 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

403 
Source.of_string name 
40526  404 
> Symbol.source 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36954
diff
changeset

405 
> Token.source {do_recover=SOME false} lex Position.start 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36954
diff
changeset

406 
> Token.source_proper 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36954
diff
changeset

407 
> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE 
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

408 
> Source.exhaust 
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

409 
end 
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset

410 

32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

411 
in 
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

412 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

413 
fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

414 
let 
39340  415 
val triv_str = if trivial then "[T] " else "" 
32536  416 
val _ = change_data id inc_sh_calls 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

417 
val _ = if trivial then () else change_data id inc_sh_nontriv_calls 
40069  418 
val (prover_name, prover) = get_prover (Proof.context_of st) args 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

419 
val type_sys = AList.lookup (op =) args type_sysK > the_default "smart" 
32525  420 
val dir = AList.lookup (op =) args keepK 
32541  421 
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) 
41268  422 
(* always use a hard timeout, but give some slack so that the automatic 
423 
minimizer has a chance to do its magic *) 

424 
val hard_timeout = SOME (2 * timeout) 

41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

425 
val (msg, result) = 
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

426 
run_sh prover_name prover type_sys hard_timeout timeout dir st 
32525  427 
in 
32536  428 
case result of 
40062  429 
SH_OK (time_isa, time_prover, names) => 
38700  430 
let 
39377  431 
fun get_thms (_, Sledgehammer_Filter.Chained) = NONE 
38826  432 
 get_thms (name, loc) = 
433 
SOME ((name, loc), thms_of_name (Proof.context_of st) name) 

32525  434 
in 
32818  435 
change_data id inc_sh_success; 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

436 
if trivial then () else change_data id inc_sh_nontriv_success; 
32818  437 
change_data id (inc_sh_lemmas (length names)); 
438 
change_data id (inc_sh_max_lems (length names)); 

439 
change_data id (inc_sh_time_isa time_isa); 

40062  440 
change_data id (inc_sh_time_prover time_prover); 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

441 
reconstructor := reconstructor_from_msg msg; 
38826  442 
named_thms := SOME (map_filter get_thms names); 
39340  443 
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ 
40062  444 
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) 
32525  445 
end 
40062  446 
 SH_FAIL (time_isa, time_prover) => 
32536  447 
let 
448 
val _ = change_data id (inc_sh_time_isa time_isa) 

40062  449 
val _ = change_data id (inc_sh_time_prover_fail time_prover) 
39340  450 
in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end 
32536  451 
 SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) 
32525  452 
end 
453 

454 
end 

455 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

456 
fun run_minimize args reconstructor named_thms id 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

457 
({pre=st, log, ...}: Mirabelle.run_args) = 
32525  458 
let 
40069  459 
val ctxt = Proof.context_of st 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

460 
val n0 = length (these (!named_thms)) 
40069  461 
val (prover_name, _) = get_prover ctxt args 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

462 
val type_sys = AList.lookup (op =) args type_sysK > the_default "smart" 
32525  463 
val timeout = 
464 
AList.lookup (op =) args minimize_timeoutK 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40554
diff
changeset

465 
> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) 
32525  466 
> the_default 5 
40069  467 
val params = Sledgehammer_Isar.default_params ctxt 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

468 
[("provers", prover_name), 
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

469 
("verbose", "true"), 
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

470 
("type_sys", type_sys), 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

471 
("timeout", Int.toString timeout)] 
37587  472 
val minimize = 
41266  473 
Sledgehammer_Minimize.minimize_facts prover_name params true 1 
40065  474 
(Sledgehammer_Util.subgoal_count st) 
32525  475 
val _ = log separator 
476 
in 

35971  477 
case minimize st (these (!named_thms)) of 
35871
c93bda4fdf15
remove the iteration counter from Sledgehammer's minimizer
blanchet
parents:
35867
diff
changeset

478 
(SOME named_thms', msg) => 
32609  479 
(change_data id inc_min_succs; 
480 
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

481 
if length named_thms' = n0 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

482 
then log (minimize_tag id ^ "already minimal") 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

483 
else (reconstructor := reconstructor_from_msg msg; 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

484 
named_thms := SOME named_thms'; 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

485 
log (minimize_tag id ^ "succeeded:\n" ^ msg)) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

486 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

487 
 (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg) 
32525  488 
end 
489 

490 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

491 
fun run_reconstructor trivial full m name reconstructor named_thms id 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

492 
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = 
32525  493 
let 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

494 
fun do_reconstructor thms ctxt = 
41154  495 
(if !reconstructor = "smt" then 
496 
SMT_Solver.smt_tac 

497 
else if full orelse !reconstructor = "metisFT" then 

498 
Metis_Tactics.metisFT_tac 

499 
else 

500 
Metis_Tactics.metis_tac) ctxt thms 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

501 
fun apply_reconstructor thms = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

502 
Mirabelle.can_apply timeout (do_reconstructor thms) st 
32521  503 

504 
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

505 
 with_time (true, t) = (change_data id (inc_reconstructor_success m); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

506 
if trivial then () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

507 
else change_data id (inc_reconstructor_nontriv_success m); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

508 
change_data id (inc_reconstructor_lemmas m (length named_thms)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

509 
change_data id (inc_reconstructor_time m t); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

510 
change_data id (inc_reconstructor_posns m (pos, trivial)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

511 
if name = "proof" then change_data id (inc_reconstructor_proofs m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

512 
else (); 
32521  513 
"succeeded (" ^ string_of_int t ^ ")") 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

514 
fun timed_reconstructor thms = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

515 
(with_time (Mirabelle.cpu_time apply_reconstructor thms), true) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

516 
handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); 
34052  517 
("timeout", false)) 
518 
 ERROR msg => ("error: " ^ msg, false) 

32521  519 

32525  520 
val _ = log separator 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

521 
val _ = change_data id (inc_reconstructor_calls m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

522 
val _ = if trivial then () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

523 
else change_data id (inc_reconstructor_nontriv_calls m) 
32521  524 
in 
32525  525 
maps snd named_thms 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

526 
> timed_reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

527 
>> log o prefix (reconstructor_tag reconstructor id) 
34052  528 
> snd 
32521  529 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

530 

40301  531 
val try_inner_timeout = seconds 5.0 
532 
val try_outer_timeout = seconds 30.0 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

533 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

534 
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

535 
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

536 
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

537 
then () else 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

538 
let 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

539 
val reconstructor = Unsynchronized.ref "" 
38700  540 
val named_thms = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

541 
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

542 
val minimize = AList.defined (op =) args minimizeK 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

543 
val metis_ft = AList.defined (op =) args metis_ftK 
40694
77435a7853d1
reverted c059d550afec  the triviality check had apparently nothing to do with spontaneous Interrupt exceptions
blanchet
parents:
40670
diff
changeset

544 
val trivial = 
40670
c059d550afec
disable triviality checking  it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day
blanchet
parents:
40667
diff
changeset

545 
TimeLimit.timeLimit try_outer_timeout 
39363  546 
(Try.invoke_try (SOME try_inner_timeout)) pre 
547 
handle TimeLimit.TimeOut => false 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

548 
fun apply_reconstructor m1 m2 = 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

549 
if metis_ft 
34052  550 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

551 
if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

552 
(run_reconstructor trivial false m1 name reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

553 
(these (!named_thms))) id st) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

554 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

555 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

556 
(run_reconstructor trivial true m2 name reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

557 
(these (!named_thms))) id st; ()) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

558 
else () 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

559 
else 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

560 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

561 
(run_reconstructor trivial false m1 name reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

562 
(these (!named_thms))) id st; ()) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

563 
in 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

564 
change_data id (set_mini minimize); 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

565 
Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

566 
named_thms) id st; 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

567 
if is_some (!named_thms) 
32612  568 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

569 
(apply_reconstructor Unminimized UnminimizedFT; 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

570 
if minimize andalso not (null (these (!named_thms))) 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

571 
then 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

572 
(Mirabelle.catch minimize_tag 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

573 
(run_minimize args reconstructor named_thms) id st; 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

574 
apply_reconstructor Minimized MinimizedFT) 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

575 
else ()) 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

576 
else () 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

577 
end 
32818  578 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

579 

32511  580 
fun invoke args = 
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32511
diff
changeset

581 
let 
36373
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36294
diff
changeset

582 
val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK 
32521  583 
in Mirabelle.register (init, sledgehammer_action args, done) end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

584 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

585 
end 