author  blanchet 
Sun, 05 Feb 2012 12:27:10 +0100  
changeset 46426  fd15abc50fc1 
parent 46415  26153cbe97bf 
child 46435  e9c90516bc0d 
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" 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

11 
val type_encK = "type_enc" 
46386  12 
val strictK = "strict" 
45706  13 
val sliceK = "slice" 
45514  14 
val lam_transK = "lam_trans" 
46415  15 
val uncurried_aliasesK = "uncurried_aliases" 
42725
64dea91bbe0e
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents:
42642
diff
changeset

16 
val e_weight_methodK = "e_weight_method" 
44099  17 
val force_sosK = "force_sos" 
41752  18 
val max_relevantK = "max_relevant" 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

19 
val max_callsK = "max_calls" 
32525  20 
val minimizeK = "minimize" 
21 
val minimize_timeoutK = "minimize_timeout" 

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

22 
val metis_ftK = "metis_ft" 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

23 
val reconstructorK = "reconstructor" 
32521  24 

44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

25 
val preplay_timeout = "4" 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

26 

32521  27 
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " 
32525  28 
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

29 
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

30 
"#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " 
32521  31 

32525  32 
val separator = "" 
33 

32521  34 

32549  35 
datatype sh_data = ShData of { 
36 
calls: int, 

37 
success: int, 

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

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

39 
nontriv_success: int, 
32585  40 
lemmas: int, 
32818  41 
max_lems: int, 
32549  42 
time_isa: int, 
40062  43 
time_prover: int, 
44 
time_prover_fail: int} 

32549  45 

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

46 
datatype re_data = ReData of { 
32549  47 
calls: int, 
48 
success: int, 

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

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

50 
nontriv_success: int, 
32676  51 
proofs: int, 
32549  52 
time: int, 
32550  53 
timeout: int, 
32990  54 
lemmas: int * int * int, 
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

55 
posns: (Position.T * bool) list 
32550  56 
} 
32549  57 

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

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

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

61 
} 
32521  62 

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

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

66 
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

67 
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, 
40062  68 
time_isa=time_isa, time_prover=time_prover, 
69 
time_prover_fail=time_prover_fail} 

32521  70 

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

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

72 
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

73 

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

74 
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

75 
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

76 
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

77 
nontriv_success=nontriv_success, proofs=proofs, time=time, 
32990  78 
timeout=timeout, lemmas=lemmas, posns=posns} 
32549  79 

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

80 
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

81 
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

82 
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

83 

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

84 
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

85 
lemmas, max_lems, time_isa, 
40062  86 
time_prover, time_prover_fail}) = (calls, success, nontriv_calls, 
87 
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

88 

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

89 
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

90 

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

91 
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

92 
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

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

94 

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

95 

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

96 
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

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

98 

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

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

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

101 
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

102 
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

103 
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

104 
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

105 
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

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

107 
} 
32521  108 

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

109 
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

110 
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

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

112 

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

113 
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

114 
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

115 

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

116 
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

117 
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

118 
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

119 

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

120 
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

121 
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

122 
in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end 
32521  123 

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

124 
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

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

126 
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

127 
 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

128 
 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

129 
 map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft) 
32521  130 

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

131 
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

132 

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

133 
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

134 
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

135 
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

136 

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

137 
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

138 
make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) 
32990  139 

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

32521  141 

32818  142 
val inc_sh_calls = map_sh_data 
40062  143 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
144 
=> (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) 

32549  145 

32818  146 
val inc_sh_success = map_sh_data 
40062  147 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
148 
=> (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

149 

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

150 
val inc_sh_nontriv_calls = map_sh_data 
40062  151 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
152 
=> (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

153 

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

154 
val inc_sh_nontriv_success = map_sh_data 
40062  155 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
156 
=> (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) 

32585  157 

32818  158 
fun inc_sh_lemmas n = map_sh_data 
40062  159 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
160 
=> (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) 

32521  161 

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

32549  165 

32818  166 
fun inc_sh_time_isa t = map_sh_data 
40062  167 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
168 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) 

32818  169 

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

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

32521  173 

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

176 
=> (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

177 

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

179 
(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

180 

32818  181 
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

182 
(fn (succs, ab_ratios) => (succs, ab_ratios+r)) 
32549  183 

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

184 
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

185 
(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

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

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

188 
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

189 
(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

190 
=> (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

191 

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

192 
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

193 
(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

194 
=> (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

195 

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

196 
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

197 
(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

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

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

200 
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

201 
(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

202 
=> (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

203 

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

204 
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

205 
(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

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

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

208 
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

209 
(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

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

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

212 
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

213 
(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

214 
=> (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

215 

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

216 
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

217 
(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

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

44090  220 
val str0 = string_of_int o the_default 0 
221 

32521  222 
local 
223 

224 
val str = string_of_int 

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

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

227 
fun time t = Real.fromInt t / 1000.0 

228 
fun avg_time t n = 

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

230 

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

231 
fun log_sh_data log 
40062  232 
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = 
32818  233 
(log ("Total number of sledgehammer calls: " ^ str calls); 
234 
log ("Number of successful sledgehammer calls: " ^ str success); 

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

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

237 
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

238 
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

239 
log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); 
32818  240 
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); 
40062  241 
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); 
242 
log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); 

32536  243 
log ("Average time for sledgehammer calls (Isabelle): " ^ 
32818  244 
str3 (avg_time time_isa calls)); 
32533  245 
log ("Average time for successful sledgehammer calls (ATP): " ^ 
40062  246 
str3 (avg_time time_prover success)); 
32536  247 
log ("Average time for failed sledgehammer calls (ATP): " ^ 
40062  248 
str3 (avg_time time_prover_fail (calls  success))) 
32533  249 
) 
32521  250 

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

251 
fun str_of_pos (pos, triv) = 
44090  252 
str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^ 
253 
(if triv then "[T]" else "") 

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

254 

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

255 
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

256 
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

257 
(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

258 
(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

259 
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

260 
" (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

261 
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

262 
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

263 
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

264 
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

265 
" (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

266 
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

267 
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

268 
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

269 
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

270 
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

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

272 
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

273 
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

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

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

276 

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

277 
fun log_min_data log (succs, ab_ratios) = 
32609  278 
(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

279 
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

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

281 

32521  282 
in 
283 

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

284 
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

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

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

287 

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

288 
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

289 
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

290 
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

291 
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

292 
(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

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

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

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

296 
(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

297 
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

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

299 
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

300 
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

301 
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

302 
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

303 
(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

304 
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

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

306 
(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

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

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

309 
end 
32521  310 

311 
end 

312 

313 

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

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

32740  317 
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

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

321 
> K () 

322 

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

325 

42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

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

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

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

331 
fun get_prover name = 
43021  332 
(name, Sledgehammer_Run.get_minimizing_prover ctxt 
333 
Sledgehammer_Provers.Normal name) 

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

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

335 
(case AList.lookup (op =) args proverK of 
40062  336 
SOME name => get_prover name 
337 
 NONE => get_prover (default_prover_name ())) 

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

338 
end 
32525  339 

46340  340 
type stature = ATP_Problem_Generate.stature 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

341 

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

342 
(* hack *) 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

343 
fun reconstructor_from_msg args msg = 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

344 
(case AList.lookup (op =) args reconstructorK of 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

345 
SOME name => name 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

346 
 NONE => 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

347 
if String.isSubstring "metis (" msg then 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

348 
msg > Substring.full 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

349 
> Substring.position "metis (" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

350 
> snd > Substring.position ")" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

351 
> fst > Substring.string 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

352 
> suffix ")" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

353 
else if String.isSubstring "metis" msg then 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

354 
"metis" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

355 
else 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

356 
"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

357 

32521  358 
local 
359 

32536  360 
datatype sh_result = 
46340  361 
SH_OK of int * int * (string * stature) list  
32536  362 
SH_FAIL of int * int  
363 
SH_ERROR 

364 

46386  365 
fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans 
46415  366 
uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos 
367 
st = 

32521  368 
let 
38998  369 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st 
370 
val i = 1 

44090  371 
fun set_file_name (SOME dir) = 
41337
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

372 
Config.put Sledgehammer_Provers.dest_dir dir 
44090  373 
#> Config.put Sledgehammer_Provers.problem_prefix 
44424  374 
("prob_" ^ str0 (Position.line_of pos) ^ "__") 
41337
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

375 
#> Config.put SMT_Config.debug_files 
43088  376 
(dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_" 
41338  377 
^ serial_string ()) 
44090  378 
 set_file_name NONE = I 
39321  379 
val st' = 
380 
st > Proof.map_context 

44090  381 
(set_file_name dir 
42725
64dea91bbe0e
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents:
42642
diff
changeset

382 
#> (Option.map (Config.put ATP_Systems.e_weight_method) 
64dea91bbe0e
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents:
42642
diff
changeset

383 
e_weight_method > the_default I) 
44099  384 
#> (Option.map (Config.put ATP_Systems.force_sos) 
44636
9a8de0397f65
always measure time for ATPs  auto minimization relies on it
blanchet
parents:
44634
diff
changeset

385 
force_sos > the_default I)) 
45706  386 
val params as {relevance_thresholds, max_relevant, slice, ...} = 
40069  387 
Sledgehammer_Isar.default_params ctxt 
40554
ff446d5e9a62
turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents:
40526
diff
changeset

388 
[("verbose", "true"), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

389 
("type_enc", type_enc), 
46386  390 
("strict", strict), 
45514  391 
("lam_trans", lam_trans > the_default "smart"), 
46415  392 
("uncurried_aliases", uncurried_aliases > the_default "smart"), 
41752  393 
("max_relevant", max_relevant), 
45706  394 
("slice", slice), 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

395 
("timeout", string_of_int timeout), 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

396 
("preplay_timeout", preplay_timeout)] 
40062  397 
val default_max_relevant = 
45706  398 
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

399 
prover_name 
42952
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset

400 
val is_appropriate_prop = 
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset

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

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

403 
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

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

405 
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

406 
val relevance_override = {add = [], del = [], only = false} 
43088  407 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

408 
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

409 
(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

410 
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

411 
 SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) 
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

412 
fun failed failure = 
45371  413 
({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime, 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

414 
preplay = 
46320  415 
K (ATP_Proof_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis), 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

416 
message = K "", message_tail = ""}, ~1) 
45371  417 
val ({outcome, used_facts, run_time, preplay, message, message_tail} 
418 
: Sledgehammer_Provers.prover_result, 

41275  419 
time_isa) = time_limit (Mirabelle.cpu_time (fn () => 
420 
let 

42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

421 
val _ = if is_appropriate_prop concl_t then () 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

422 
else raise Fail "inappropriate" 
44625  423 
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name 
41275  424 
val facts = 
44625  425 
Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override 
426 
chained_ths hyp_ts concl_t 

43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43261
diff
changeset

427 
> filter (is_appropriate_prop o prop_of o snd) 
44625  428 
> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds 
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43261
diff
changeset

429 
(the_default default_max_relevant max_relevant) 
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43261
diff
changeset

430 
is_built_in_const relevance_fudge relevance_override 
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43261
diff
changeset

431 
chained_ths hyp_ts concl_t 
41275  432 
val problem = 
433 
{state = st', goal = goal, subgoal = i, 

434 
subgoal_count = Sledgehammer_Util.subgoal_count st, 

435 
facts = facts > map Sledgehammer_Provers.Untranslated_Fact, 

41741  436 
smt_filter = NONE} 
45520  437 
in prover params (K (K (K ""))) problem end)) () 
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

438 
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

439 
 Fail "inappropriate" => failed ATP_Proof.Inappropriate 
45371  440 
val time_prover = run_time > Time.toMilliseconds 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

441 
val msg = message (preplay ()) ^ message_tail 
32521  442 
in 
36405  443 
case outcome of 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

444 
NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

445 
 SOME _ => (msg, SH_FAIL (time_isa, time_prover)) 
32521  446 
end 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37631
diff
changeset

447 
handle ERROR msg => ("error: " ^ msg, SH_ERROR) 
32521  448 

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

449 
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

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

451 
val lex = Keyword.get_lexicons 
42361  452 
val get = maps (Proof_Context.get_fact ctxt o fst) 
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset

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

454 
Source.of_string name 
40526  455 
> 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

456 
> 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

457 
> 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

458 
> 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

459 
> 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

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

461 

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

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

463 

44090  464 
fun run_sledgehammer trivial args reconstructor named_thms id 
465 
({pre=st, log, pos, ...}: Mirabelle.run_args) = 

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

466 
let 
39340  467 
val triv_str = if trivial then "[T] " else "" 
32536  468 
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

469 
val _ = if trivial then () else change_data id inc_sh_nontriv_calls 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

470 
val (prover_name, prover) = get_prover (Proof.context_of st) args 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

471 
val type_enc = AList.lookup (op =) args type_encK > the_default "smart" 
46386  472 
val strict = AList.lookup (op =) args strictK > the_default "false" 
41752  473 
val max_relevant = AList.lookup (op =) args max_relevantK > the_default "smart" 
45706  474 
val slice = AList.lookup (op =) args sliceK > the_default "true" 
45514  475 
val lam_trans = AList.lookup (op =) args lam_transK 
46415  476 
val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK 
42725
64dea91bbe0e
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents:
42642
diff
changeset

477 
val e_weight_method = AList.lookup (op =) args e_weight_methodK 
44099  478 
val force_sos = AList.lookup (op =) args force_sosK 
42725
64dea91bbe0e
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents:
42642
diff
changeset

479 
> Option.map (curry (op <>) "false") 
32525  480 
val dir = AList.lookup (op =) args keepK 
32541  481 
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) 
41268  482 
(* always use a hard timeout, but give some slack so that the automatic 
483 
minimizer has a chance to do its magic *) 

484 
val hard_timeout = SOME (2 * timeout) 

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

485 
val (msg, result) = 
46386  486 
run_sh prover_name prover type_enc strict max_relevant slice lam_trans 
46415  487 
uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos 
488 
st 

32525  489 
in 
32536  490 
case result of 
40062  491 
SH_OK (time_isa, time_prover, names) => 
38700  492 
let 
46340  493 
fun get_thms (name, stature) = 
494 
SOME ((name, stature), thms_of_name (Proof.context_of st) name) 

32525  495 
in 
32818  496 
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

497 
if trivial then () else change_data id inc_sh_nontriv_success; 
32818  498 
change_data id (inc_sh_lemmas (length names)); 
499 
change_data id (inc_sh_max_lems (length names)); 

500 
change_data id (inc_sh_time_isa time_isa); 

40062  501 
change_data id (inc_sh_time_prover time_prover); 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

502 
reconstructor := reconstructor_from_msg args msg; 
38826  503 
named_thms := SOME (map_filter get_thms names); 
39340  504 
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ 
40062  505 
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) 
32525  506 
end 
40062  507 
 SH_FAIL (time_isa, time_prover) => 
32536  508 
let 
509 
val _ = change_data id (inc_sh_time_isa time_isa) 

40062  510 
val _ = change_data id (inc_sh_time_prover_fail time_prover) 
39340  511 
in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end 
32536  512 
 SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) 
32525  513 
end 
514 

515 
end 

516 

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

517 
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

518 
({pre=st, log, ...}: Mirabelle.run_args) = 
32525  519 
let 
40069  520 
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

521 
val n0 = length (these (!named_thms)) 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

522 
val (prover_name, _) = get_prover ctxt args 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

523 
val type_enc = AList.lookup (op =) args type_encK > the_default "smart" 
46386  524 
val strict = AList.lookup (op =) args strictK > the_default "false" 
32525  525 
val timeout = 
526 
AList.lookup (op =) args minimize_timeoutK 

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

527 
> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) 
32525  528 
> the_default 5 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43052
diff
changeset

529 
val params = Sledgehammer_Isar.default_params ctxt 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

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

531 
("verbose", "true"), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

532 
("type_enc", type_enc), 
46386  533 
("strict", strict), 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

534 
("timeout", string_of_int timeout), 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

535 
("preplay_timeout", preplay_timeout)] 
37587  536 
val minimize = 
41742
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset

537 
Sledgehammer_Minimize.minimize_facts prover_name params 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43052
diff
changeset

538 
true 1 (Sledgehammer_Util.subgoal_count st) 
32525  539 
val _ = log separator 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

540 
val (used_facts, (preplay, message, message_tail)) = 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

541 
minimize st (these (!named_thms)) 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

542 
val msg = message (preplay ()) ^ message_tail 
32525  543 
in 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

544 
case used_facts of 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

545 
SOME named_thms' => 
32609  546 
(change_data id inc_min_succs; 
547 
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

548 
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

549 
then log (minimize_tag id ^ "already minimal") 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

550 
else (reconstructor := reconstructor_from_msg args msg; 
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 
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

552 
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

553 
) 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

554 
 NONE => log (minimize_tag id ^ "failed: " ^ msg) 
32525  555 
end 
556 

44542  557 
fun override_params prover type_enc timeout = 
558 
[("provers", prover), 

44449
b622a98b79fb
don't select facts when using sledgehammer_tac for reconstruction
blanchet
parents:
44448
diff
changeset

559 
("max_relevant", "0"), 
44542  560 
("type_enc", type_enc), 
46386  561 
("strict", "true"), 
45706  562 
("slice", "false"), 
44461  563 
("timeout", timeout > Time.toSeconds > string_of_int)] 
44430  564 

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 
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

566 
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = 
32525  567 
let 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

568 
fun do_reconstructor named_thms ctxt = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

569 
let 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

570 
val ref_of_str = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

571 
suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

572 
#> fst 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

573 
val thms = named_thms > maps snd 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

574 
val facts = named_thms > map (ref_of_str o fst o fst) 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

575 
val relevance_override = {add = facts, del = [], only = true} 
44566
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset

576 
fun my_timeout time_slice = 
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset

577 
timeout > Time.toReal > curry Real.* time_slice > Time.fromReal 
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset

578 
fun sledge_tac time_slice prover type_enc = 
44542  579 
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt 
44566
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset

580 
(override_params prover type_enc (my_timeout time_slice)) 
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset

581 
relevance_override 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

582 
in 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

583 
if !reconstructor = "sledgehammer_tac" then 
44768  584 
sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple" 
585 
ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??" 

586 
ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??" 

587 
ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags" 

46365  588 
ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN 
46320  589 
ctxt thms 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

590 
else if !reconstructor = "smt" then 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

591 
SMT_Solver.smt_tac ctxt thms 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

592 
else if full then 
46320  593 
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] 
594 
ATP_Proof_Reconstruct.metis_default_lam_trans ctxt thms 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

595 
else if String.isPrefix "metis (" (!reconstructor) then 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

596 
let 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

597 
val (type_encs, lam_trans) = 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

598 
!reconstructor 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

599 
> Outer_Syntax.scan Position.start 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

600 
> filter Token.is_proper > tl 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

601 
> Metis_Tactic.parse_metis_options > fst 
46320  602 
>> the_default [ATP_Proof_Reconstruct.partial_typesN] 
603 
> the_default ATP_Proof_Reconstruct.metis_default_lam_trans 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

604 
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

605 
else if !reconstructor = "metis" then 
46320  606 
Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.metis_default_lam_trans ctxt 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

607 
thms 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

608 
else 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

609 
K all_tac 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

610 
end 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

611 
fun apply_reconstructor named_thms = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

612 
Mirabelle.can_apply timeout (do_reconstructor named_thms) st 
32521  613 

614 
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

615 
 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

616 
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

617 
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

618 
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

619 
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

620 
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

621 
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

622 
else (); 
32521  623 
"succeeded (" ^ string_of_int t ^ ")") 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

624 
fun timed_reconstructor named_thms = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

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

626 
handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); 
34052  627 
("timeout", false)) 
628 
 ERROR msg => ("error: " ^ msg, false) 

32521  629 

32525  630 
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

631 
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

632 
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

633 
else change_data id (inc_reconstructor_nontriv_calls m) 
32521  634 
in 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

635 
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

636 
> 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

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

640 

41276
285aea0c153c
two layers of timeouts seem to be less reliable than a single layer
blanchet
parents:
41275
diff
changeset

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

642 

44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

643 
(* crude hack *) 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

644 
val num_sledgehammer_calls = Unsynchronized.ref 0 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

645 

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

646 
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

647 
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

648 
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

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

650 
let 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

651 
val max_calls = 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

652 
AList.lookup (op =) args max_callsK > the_default "10000000" 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

653 
> Int.fromString > the 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

654 
val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1; 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

655 
in 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

656 
if !num_sledgehammer_calls > max_calls then () 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

657 
else 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

658 
let 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

659 
val reconstructor = Unsynchronized.ref "" 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

660 
val named_thms = 
46340  661 
Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

662 
val minimize = AList.defined (op =) args minimizeK 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

663 
val metis_ft = AList.defined (op =) args metis_ftK 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

664 
val trivial = 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

665 
Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

666 
handle TimeLimit.TimeOut => false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

667 
fun apply_reconstructor m1 m2 = 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

668 
if metis_ft 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

669 
then 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

670 
if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

671 
(run_reconstructor trivial false m1 name reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

672 
(these (!named_thms))) id st) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

673 
then 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

674 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

675 
(run_reconstructor trivial true m2 name reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

676 
(these (!named_thms))) id st; ()) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

677 
else () 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

678 
else 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

679 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

680 
(run_reconstructor trivial false m1 name reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

681 
(these (!named_thms))) id st; ()) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

682 
in 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

683 
change_data id (set_mini minimize); 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

684 
Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

685 
named_thms) id st; 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

686 
if is_some (!named_thms) 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

687 
then 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

688 
(apply_reconstructor Unminimized UnminimizedFT; 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

689 
if minimize andalso not (null (these (!named_thms))) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

690 
then 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

691 
(Mirabelle.catch minimize_tag 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

692 
(run_minimize args reconstructor named_thms) id st; 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

693 
apply_reconstructor Minimized MinimizedFT) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

694 
else ()) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

695 
else () 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

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

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

699 

32511  700 
fun invoke args = 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43351
diff
changeset

701 
Mirabelle.register (init, sledgehammer_action args, done) 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

702 

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

703 
end 