author  blanchet 
Wed, 11 Sep 2013 09:51:30 +0200  
changeset 53517  1165e8960f59 
parent 53500  53b9326196fe 
child 53551  7b779c075de9 
permissions  rwrr 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_provers.ML 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
32996
d2e48879e65a
removed disjunctive group cancellation  provers run independently;
wenzelm
parents:
32995
diff
changeset

3 
Author: Makarius 
35969  4 
Author: Jasmin Blanchette, TU Muenchen 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

5 

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

6 
Generic prover abstraction for Sledgehammer. 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

7 
*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

8 

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

9 
signature SLEDGEHAMMER_PROVERS = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

10 
sig 
40181  11 
type failure = ATP_Proof.failure 
46340  12 
type stature = ATP_Problem_Generate.stature 
46320  13 
type type_enc = ATP_Problem_Generate.type_enc 
51005
ce4290c33d73
eliminated needless speed optimization  and simplified code quite a bit
blanchet
parents:
50927
diff
changeset

14 
type fact = Sledgehammer_Fact.fact 
52555  15 
type reconstructor = Sledgehammer_Reconstructor.reconstructor 
16 
type play = Sledgehammer_Reconstructor.play 

17 
type minimize_command = Sledgehammer_Reconstructor.minimize_command 

39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

18 

53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset

19 
datatype mode = Auto_Try  Try  Normal  MaSh  Auto_Minimize  Minimize 
43021  20 

35969  21 
type params = 
48321  22 
{debug : bool, 
23 
verbose : bool, 

24 
overlord : bool, 

25 
blocking : bool, 

26 
provers : string list, 

27 
type_enc : string option, 

28 
strict : bool, 

29 
lam_trans : string option, 

30 
uncurried_aliases : bool option, 

31 
learn : bool, 

32 
fact_filter : string option, 

33 
max_facts : int option, 

34 
fact_thresholds : real * real, 

35 
max_mono_iters : int option, 

36 
max_new_mono_instances : int option, 

51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51186
diff
changeset

37 
isar_proofs : bool option, 
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51024
diff
changeset

38 
isar_compress : real, 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset

39 
isar_compress_degree : int, 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset

40 
merge_timeout_slack : real, 
52632
23393c31c7fe
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents:
52556
diff
changeset

41 
isar_try0 : bool, 
23393c31c7fe
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents:
52556
diff
changeset

42 
isar_minimize : bool, 
48321  43 
slice : bool, 
44 
minimize : bool option, 

50557  45 
timeout : Time.time option, 
46 
preplay_timeout : Time.time option, 

51879  47 
preplay_trace : bool, 
48321  48 
expect : string} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

49 

48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

50 
type relevance_fudge = 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

51 
{local_const_multiplier : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

52 
worse_irrel_freq : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

53 
higher_order_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

54 
abs_rel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

55 
abs_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

56 
skolem_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

57 
theory_const_rel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

58 
theory_const_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

59 
chained_const_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

60 
intro_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

61 
elim_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

62 
simp_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

63 
local_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

64 
assum_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

65 
chained_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

66 
max_imperfect : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

67 
max_imperfect_exp : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

68 
threshold_divisor : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

69 
ridiculous_threshold : real} 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

70 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

71 
type prover_problem = 
48321  72 
{state : Proof.state, 
73 
goal : thm, 

74 
subgoal : int, 

75 
subgoal_count : int, 

51010  76 
factss : (string * fact list) list} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

77 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

78 
type prover_result = 
48321  79 
{outcome : failure option, 
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset

80 
used_facts : (string * stature) list, 
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset

81 
used_from : fact list, 
48321  82 
run_time : Time.time, 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

83 
preplay : play Lazy.lazy, 
48321  84 
message : play > string, 
85 
message_tail : string} 

39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

86 

43051  87 
type prover = 
45520  88 
params > ((string * string list) list > string > minimize_command) 
89 
> prover_problem > prover_result 

35867  90 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

91 
val dest_dir : string Config.T 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

92 
val problem_prefix : string Config.T 
48143  93 
val completish : bool Config.T 
44592
54906b0337ab
flip logic of boolean option so it's off by default
blanchet
parents:
44586
diff
changeset

94 
val atp_full_names : bool Config.T 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

95 
val smt_triggers : bool Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

96 
val smt_weights : bool Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

97 
val smt_weight_min_facts : int Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

98 
val smt_min_weight : int Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

99 
val smt_max_weight : int Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

100 
val smt_max_weight_index : int Config.T 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

101 
val smt_weight_curve : (int > int) Unsynchronized.ref 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

102 
val smt_max_slices : int Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

103 
val smt_slice_fact_frac : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

104 
val smt_slice_time_frac : real Config.T 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

105 
val smt_slice_min_secs : int Config.T 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

106 
val SledgehammerN : string 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

107 
val plain_metis : reconstructor 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

108 
val select_smt_solver : string > Proof.context > Proof.context 
45520  109 
val extract_reconstructor : 
45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

110 
params > reconstructor > string * (string * string list) list 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

111 
val is_reconstructor : string > bool 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

112 
val is_atp : theory > string > bool 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

113 
val is_smt_prover : Proof.context > string > bool 
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

114 
val is_ho_atp: Proof.context > string > bool 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

115 
val is_unit_equational_atp : Proof.context > string > bool 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

116 
val is_prover_supported : Proof.context > string > bool 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

117 
val is_prover_installed : Proof.context > string > bool 
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

118 
val remotify_prover_if_supported_and_not_already_remote : 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

119 
Proof.context > string > string option 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

120 
val remotify_prover_if_not_installed : 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

121 
Proof.context > string > string option 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

122 
val default_max_facts_of_prover : Proof.context > bool > string > int 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

123 
val is_unit_equality : term > bool 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

124 
val is_appropriate_prop_of_prover : Proof.context > string > term > bool 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

125 
val is_built_in_const_of_prover : 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

126 
Proof.context > string > string * typ > term list > bool * term list 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

127 
val atp_relevance_fudge : relevance_fudge 
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

128 
val smt_relevance_fudge : relevance_fudge 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

129 
val relevance_fudge_of_prover : Proof.context > string > relevance_fudge 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

130 
val weight_smt_fact : 
46340  131 
Proof.context > int > ((string * stature) * thm) * int 
132 
> (string * stature) * (int option * thm) 

41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

133 
val supported_provers : Proof.context > unit 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

134 
val kill_provers : unit > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

135 
val running_provers : unit > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

136 
val messages : int option > unit 
48798  137 
val is_fact_chained : (('a * stature) * 'b) > bool 
138 
val filter_used_facts : 

139 
bool > (''a * stature) list > ((''a * stature) * 'b) list > 

140 
((''a * stature) * 'b) list 

51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

141 
val isar_proof_reconstructor : Proof.context > string > string 
43021  142 
val get_prover : Proof.context > mode > string > prover 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

143 
end; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

144 

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

145 
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

146 
struct 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

147 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43063
diff
changeset

148 
open ATP_Util 
38028  149 
open ATP_Problem 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset

150 
open ATP_Proof 
38028  151 
open ATP_Systems 
46320  152 
open ATP_Problem_Generate 
153 
open ATP_Proof_Reconstruct 

45521  154 
open Metis_Tactic 
38023  155 
open Sledgehammer_Util 
51005
ce4290c33d73
eliminated needless speed optimization  and simplified code quite a bit
blanchet
parents:
50927
diff
changeset

156 
open Sledgehammer_Fact 
52555  157 
open Sledgehammer_Reconstructor 
158 
open Sledgehammer_Print 

49881
d9d73ebf9274
added proof minimization code from Steffen Smolka
blanchet
parents:
48802
diff
changeset

159 
open Sledgehammer_Reconstruct 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

160 

37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

161 

9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

162 
(** The Sledgehammer **) 
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

163 

53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset

164 
datatype mode = Auto_Try  Try  Normal  MaSh  Auto_Minimize  Minimize 
43021  165 

45376  166 
(* Identifier that distinguishes Sledgehammer from other tools that could use 
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

167 
"Async_Manager". *) 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

168 
val SledgehammerN = "Sledgehammer" 
37585  169 

45520  170 
val reconstructor_names = [metisN, smtN] 
46365  171 
val plain_metis = Metis (hd partial_type_encs, combsN) 
45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

172 
val is_reconstructor = member (op =) reconstructor_names 
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43226
diff
changeset

173 

43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

174 
val is_atp = member (op =) o supported_atps 
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

175 

43233
2749c357f865
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents:
43232
diff
changeset

176 
val select_smt_solver = Context.proof_map o SMT_Config.select_solver 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

177 

45376  178 
fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt) 
40062  179 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

180 
fun is_atp_of_format is_format ctxt name = 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

181 
let val thy = Proof_Context.theory_of ctxt in 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

182 
case try (get_atp thy) name of 
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47531
diff
changeset

183 
SOME config => 
48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48656
diff
changeset

184 
exists (fn (_, ((_, format, _, _, _), _)) => is_format format) 
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47531
diff
changeset

185 
(#best_slices (config ()) ctxt) 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

186 
 NONE => false 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

187 
end 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

188 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

189 
val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ) 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

190 
val is_ho_atp = is_atp_of_format is_format_higher_order 
44597  191 

45376  192 
fun is_prover_supported ctxt = 
42361  193 
let val thy = Proof_Context.theory_of ctxt in 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

194 
is_reconstructor orf is_atp thy orf is_smt_prover ctxt 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

195 
end 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

196 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41336
diff
changeset

197 
fun is_prover_installed ctxt = 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

198 
is_reconstructor orf is_smt_prover ctxt orf 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

199 
is_atp_installed (Proof_Context.theory_of ctxt) 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

200 

51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

201 
fun remotify_prover_if_supported_and_not_already_remote ctxt name = 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

202 
if String.isPrefix remote_prefix name then 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

203 
SOME name 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

204 
else 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

205 
let val remote_name = remote_prefix ^ name in 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

206 
if is_prover_supported ctxt remote_name then SOME remote_name else NONE 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

207 
end 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

208 

260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

209 
fun remotify_prover_if_not_installed ctxt name = 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

210 
if is_prover_supported ctxt name andalso is_prover_installed ctxt name then 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

211 
SOME name 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

212 
else 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

213 
remotify_prover_if_supported_and_not_already_remote ctxt name 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

214 

45706  215 
fun get_slices slice slices = 
216 
(0 upto length slices  1) ~~ slices > not slice ? (List.last #> single) 

42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

217 

48293  218 
val reconstructor_default_max_facts = 20 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

219 

51186
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

220 
fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

221 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

222 
fun default_max_facts_of_prover ctxt slice name = 
42361  223 
let val thy = Proof_Context.theory_of ctxt in 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

224 
if is_reconstructor name then 
48293  225 
reconstructor_default_max_facts 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

226 
else if is_atp thy name then 
51186
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

227 
fold (Integer.max o slice_max_facts) 
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47531
diff
changeset

228 
(get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

229 
else (* is_smt_prover ctxt name *) 
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

230 
SMT_Solver.default_max_relevant ctxt name 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

231 
end 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

232 

42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

233 
fun is_if (@{const_name If}, _) = true 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

234 
 is_if _ = false 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

235 

9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

236 
(* Beware of "if and only if" (which is translated as such) and "If" (which is 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

237 
translated to conditional equations). *) 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

238 
fun is_good_unit_equality T t u = 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

239 
T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u]) 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

240 

42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

241 
fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

242 
 is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) = 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

243 
is_unit_equality t 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

244 
 is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) = 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

245 
is_unit_equality t 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

246 
 is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) = 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

247 
is_good_unit_equality T t u 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

248 
 is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) = 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42952
diff
changeset

249 
is_good_unit_equality T t u 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

250 
 is_unit_equality _ = false 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

251 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

252 
fun is_appropriate_prop_of_prover ctxt name = 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

253 
if is_unit_equational_atp ctxt name then is_unit_equality else K true 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

254 

53517  255 
val atp_irrelevant_const_tab = 
256 
Symtab.make (map (rpair ()) atp_irrelevant_consts) 

257 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

258 
fun is_built_in_const_of_prover ctxt name = 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

259 
if is_smt_prover ctxt name then 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

260 
let val ctxt = ctxt > select_smt_solver name in 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

261 
fn x => fn ts => 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

262 
if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

263 
(true, []) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

264 
else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

265 
(true, ts) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

266 
else 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

267 
(false, ts) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41335
diff
changeset

268 
end 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41241
diff
changeset

269 
else 
53517  270 
fn (s, _) => fn ts => (Symtab.defined atp_irrelevant_const_tab s, ts) 
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

271 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

272 
(* FUDGE *) 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

273 
val atp_relevance_fudge = 
42738  274 
{local_const_multiplier = 1.5, 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

275 
worse_irrel_freq = 100.0, 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

276 
higher_order_irrel_weight = 1.05, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

277 
abs_rel_weight = 0.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

278 
abs_irrel_weight = 2.0, 
47934
08d7aff8c7e6
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
blanchet
parents:
47912
diff
changeset

279 
skolem_irrel_weight = 0.05, 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

280 
theory_const_rel_weight = 0.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

281 
theory_const_irrel_weight = 0.25, 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42730
diff
changeset

282 
chained_const_irrel_weight = 0.25, 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

283 
intro_bonus = 0.15, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

284 
elim_bonus = 0.15, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

285 
simp_bonus = 0.15, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

286 
local_bonus = 0.55, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

287 
assum_bonus = 1.05, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

288 
chained_bonus = 1.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

289 
max_imperfect = 11.5, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

290 
max_imperfect_exp = 1.0, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

291 
threshold_divisor = 2.0, 
41093  292 
ridiculous_threshold = 0.01} 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

293 

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

294 
(* FUDGE (FIXME) *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

295 
val smt_relevance_fudge = 
42738  296 
{local_const_multiplier = #local_const_multiplier atp_relevance_fudge, 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

297 
worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge, 
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

298 
higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge, 
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

299 
abs_rel_weight = #abs_rel_weight atp_relevance_fudge, 
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

300 
abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge, 
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

301 
skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge, 
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

302 
theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge, 
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

303 
theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge, 
42735
1d375de437e9
finetuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents:
42730
diff
changeset

304 
chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge, 
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

305 
intro_bonus = #intro_bonus atp_relevance_fudge, 
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

306 
elim_bonus = #elim_bonus atp_relevance_fudge, 
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

307 
simp_bonus = #simp_bonus atp_relevance_fudge, 
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

308 
local_bonus = #local_bonus atp_relevance_fudge, 
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

309 
assum_bonus = #assum_bonus atp_relevance_fudge, 
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

310 
chained_bonus = #chained_bonus atp_relevance_fudge, 
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

311 
max_imperfect = #max_imperfect atp_relevance_fudge, 
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

312 
max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge, 
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

313 
threshold_divisor = #threshold_divisor atp_relevance_fudge, 
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

314 
ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

315 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

316 
fun relevance_fudge_of_prover ctxt name = 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

317 
if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
40069
diff
changeset

318 

41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

319 
fun supported_provers ctxt = 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

320 
let 
42361  321 
val thy = Proof_Context.theory_of ctxt 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

322 
val (remote_provers, local_provers) = 
45520  323 
reconstructor_names @ 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

324 
sort_strings (supported_atps thy) @ 
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

325 
sort_strings (SMT_Solver.available_solvers_of ctxt) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

326 
> List.partition (String.isPrefix remote_prefix) 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

327 
in 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

328 
Output.urgent_message ("Supported provers: " ^ 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

329 
commas (local_provers @ remote_provers) ^ ".") 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

330 
end 
35969  331 

48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

332 
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

333 
fun running_provers () = Async_Manager.running_threads SledgehammerN "prover" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

334 
val messages = Async_Manager.thread_messages SledgehammerN "prover" 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

335 

48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

336 

40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

337 
(** problems, results, ATPs, etc. **) 
35969  338 

339 
type params = 

48321  340 
{debug : bool, 
341 
verbose : bool, 

342 
overlord : bool, 

343 
blocking : bool, 

344 
provers : string list, 

345 
type_enc : string option, 

346 
strict : bool, 

347 
lam_trans : string option, 

348 
uncurried_aliases : bool option, 

349 
learn : bool, 

350 
fact_filter : string option, 

351 
max_facts : int option, 

352 
fact_thresholds : real * real, 

353 
max_mono_iters : int option, 

354 
max_new_mono_instances : int option, 

51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51186
diff
changeset

355 
isar_proofs : bool option, 
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51024
diff
changeset

356 
isar_compress : real, 
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset

357 
isar_compress_degree : int, 
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52555
diff
changeset

358 
merge_timeout_slack : real, 
52632
23393c31c7fe
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents:
52556
diff
changeset

359 
isar_try0 : bool, 
23393c31c7fe
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents:
52556
diff
changeset

360 
isar_minimize : bool, 
48321  361 
slice : bool, 
362 
minimize : bool option, 

50557  363 
timeout : Time.time option, 
364 
preplay_timeout : Time.time option, 

51879  365 
preplay_trace : bool, 
48321  366 
expect : string} 
35867  367 

48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

368 
type relevance_fudge = 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

369 
{local_const_multiplier : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

370 
worse_irrel_freq : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

371 
higher_order_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

372 
abs_rel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

373 
abs_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

374 
skolem_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

375 
theory_const_rel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

376 
theory_const_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

377 
chained_const_irrel_weight : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

378 
intro_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

379 
elim_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

380 
simp_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

381 
local_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

382 
assum_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

383 
chained_bonus : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

384 
max_imperfect : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

385 
max_imperfect_exp : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

386 
threshold_divisor : real, 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

387 
ridiculous_threshold : real} 
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

388 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

389 
type prover_problem = 
48321  390 
{state : Proof.state, 
391 
goal : thm, 

392 
subgoal : int, 

393 
subgoal_count : int, 

51010  394 
factss : (string * fact list) list} 
35867  395 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

396 
type prover_result = 
48321  397 
{outcome : failure option, 
398 
used_facts : (string * stature) list, 

51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset

399 
used_from : fact list, 
48321  400 
run_time : Time.time, 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

401 
preplay : play Lazy.lazy, 
48321  402 
message : play > string, 
403 
message_tail : string} 

35867  404 

43051  405 
type prover = 
45520  406 
params > ((string * string list) list > string > minimize_command) 
407 
> prover_problem > prover_result 

35867  408 

38023  409 
(* configuration attributes *) 
410 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

411 
(* Empty string means create files in Isabelle's temporary files directory. *) 
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42593
diff
changeset

412 
val dest_dir = 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42593
diff
changeset

413 
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "") 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42593
diff
changeset

414 
val problem_prefix = 
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42593
diff
changeset

415 
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") 
48143  416 
val completish = 
417 
Attrib.setup_config_bool @{binding sledgehammer_completish} (K false) 

28484  418 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

419 
(* In addition to being easier to read, readable names are often much shorter, 
44394
20bd9f90accc
added option to control soundness of encodings more precisely, for evaluation purposes
blanchet
parents:
44393
diff
changeset

420 
especially if types are mangled in names. This makes a difference for some 
20bd9f90accc
added option to control soundness of encodings more precisely, for evaluation purposes
blanchet
parents:
44393
diff
changeset

421 
provers (e.g., E). For these reason, short names are enabled by default. *) 
44592
54906b0337ab
flip logic of boolean option so it's off by default
blanchet
parents:
44586
diff
changeset

422 
val atp_full_names = 
54906b0337ab
flip logic of boolean option so it's off by default
blanchet
parents:
44586
diff
changeset

423 
Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43085
diff
changeset

424 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

425 
val smt_triggers = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

426 
Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

427 
val smt_weights = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

428 
Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

429 
val smt_weight_min_facts = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

430 
Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20) 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

431 

0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

432 
(* FUDGE *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

433 
val smt_min_weight = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

434 
Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

435 
val smt_max_weight = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

436 
Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

437 
val smt_max_weight_index = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

438 
Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200) 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

439 
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

440 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

441 
fun smt_fact_weight ctxt j num_facts = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

442 
if Config.get ctxt smt_weights andalso 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

443 
num_facts >= Config.get ctxt smt_weight_min_facts then 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

444 
let 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

445 
val min = Config.get ctxt smt_min_weight 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

446 
val max = Config.get ctxt smt_max_weight 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

447 
val max_index = Config.get ctxt smt_max_weight_index 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

448 
val curve = !smt_weight_curve 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

449 
in 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

450 
SOME (max  (max  min + 1) * curve (Int.max (0, max_index  j  1)) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

451 
div curve max_index) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

452 
end 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

453 
else 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

454 
NONE 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

455 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

456 
fun weight_smt_fact ctxt num_facts ((info, th), j) = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

457 
let val thy = Proof_Context.theory_of ctxt in 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

458 
(info, (smt_fact_weight ctxt j num_facts, th > Thm.transfer thy)) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

459 
end 
38023  460 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

461 
fun overlord_file_location_of_prover prover = 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

462 
(getenv "ISABELLE_HOME_USER", "prob_" ^ prover) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

463 

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

464 
fun proof_banner mode name = 
43033  465 
case mode of 
466 
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" 

467 
 Try => "Sledgehammer (" ^ quote name ^ ") found a proof" 

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

468 
 _ => "Try this" 
43033  469 

45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

470 
fun bunch_of_reconstructors needs_full_types lam_trans = 
48800  471 
if needs_full_types then 
48802  472 
[Metis (full_type_enc, lam_trans false), 
473 
Metis (really_full_type_enc, lam_trans false), 

474 
Metis (full_type_enc, lam_trans true), 

475 
Metis (really_full_type_enc, lam_trans true), 

476 
SMT] 

477 
else 

48800  478 
[Metis (partial_type_enc, lam_trans false), 
479 
Metis (full_type_enc, lam_trans false), 

480 
Metis (no_typesN, lam_trans true), 

481 
Metis (really_full_type_enc, lam_trans true), 

482 
SMT] 

45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

483 

57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

484 
fun extract_reconstructor ({type_enc, lam_trans, ...} : params) 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

485 
(Metis (type_enc', lam_trans')) = 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

486 
let 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

487 
val override_params = 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

488 
(if is_none type_enc andalso type_enc' = hd partial_type_encs then 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

489 
[] 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

490 
else 
45566
da05ce2de5a8
better threading of type encodings between Sledgehammer and "metis"
blanchet
parents:
45561
diff
changeset

491 
[("type_enc", [hd (unalias_type_enc type_enc')])]) @ 
45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

492 
(if is_none lam_trans andalso lam_trans' = metis_default_lam_trans then 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

493 
[] 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

494 
else 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

495 
[("lam_trans", [lam_trans'])]) 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

496 
in (metisN, override_params) end 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

497 
 extract_reconstructor _ SMT = (smtN, []) 
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

498 

43033  499 
(* based on "Mirabelle.can_apply" and generalized *) 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

500 
fun timed_apply timeout tac state i = 
43033  501 
let 
502 
val {context = ctxt, facts, goal} = Proof.goal state 

503 
val full_tac = Method.insert_tac facts i THEN tac ctxt i 

50557  504 
in time_limit timeout (try (Seq.pull o full_tac)) goal end 
43033  505 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

506 
fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = 
45521  507 
metis_tac [type_enc] lam_trans 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

508 
 tac_of_reconstructor SMT = SMT_Solver.smt_tac 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

509 

45520  510 
fun timed_reconstructor reconstr debug timeout ths = 
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44649
diff
changeset

511 
(Config.put Metis_Tactic.verbose debug 
45557  512 
#> Config.put SMT_Config.verbose debug 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

513 
#> (fn ctxt => tac_of_reconstructor reconstr ctxt ths)) 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

514 
> timed_apply timeout 
43033  515 

48798  516 
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained 
517 

518 
fun filter_used_facts keep_chained used = 

519 
filter ((member (op =) used o fst) orf 

520 
(if keep_chained then is_fact_chained else K false)) 

43033  521 

45781
fc2c368b5f54
use same order of facts for preplay as for actual reconstruction  Metis sometimes exhibits very different timings depending on the order of the facts
blanchet
parents:
45707
diff
changeset

522 
fun play_one_line_proof mode debug verbose timeout pairs state i preferred 
45520  523 
reconstrs = 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

524 
let 
45520  525 
fun get_preferred reconstrs = 
526 
if member (op =) reconstrs preferred then preferred 

527 
else List.last reconstrs 

43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

528 
in 
50557  529 
if timeout = SOME Time.zeroTime then 
45520  530 
Trust_Playable (get_preferred reconstrs, NONE) 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

531 
else 
50557  532 
let 
533 
val _ = 

534 
if mode = Minimize then Output.urgent_message "Preplaying proof..." 

535 
else () 

536 
val ths = pairs > sort_wrt (fst o fst) > map snd 

537 
fun play [] [] = Failed_to_Play (get_preferred reconstrs) 

538 
 play timed_outs [] = 

539 
Trust_Playable (get_preferred timed_outs, timeout) 

540 
 play timed_out (reconstr :: reconstrs) = 

541 
let 

542 
val _ = 

543 
if verbose then 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

544 
"Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^ 
50557  545 
(case timeout of 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

546 
SOME timeout => " for " ^ string_of_time timeout 
50557  547 
 NONE => "") ^ "..." 
548 
> Output.urgent_message 

549 
else 

550 
() 

551 
val timer = Timer.startRealTimer () 

552 
in 

553 
case timed_reconstructor reconstr debug timeout ths state i of 

554 
SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer) 

555 
 _ => play timed_out reconstrs 

556 
end 

557 
handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs 

558 
in play [] reconstrs end 

43033  559 
end 
560 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset

561 

41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

562 
(* generic TPTPbased ATPs *) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

563 

42730
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

564 
(* Too general means, positive equality literal with a variable X as one 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

565 
operand, when X does not occur properly in the other operand. This rules out 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

566 
clearly inconsistent facts such as X = a  X = b, though it by no means 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

567 
guarantees soundness. *) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

568 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

569 
fun get_facts_of_filter _ [(_, facts)] = facts 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

570 
 get_facts_of_filter fact_filter factss = 
51013  571 
case AList.lookup (op =) factss fact_filter of 
572 
SOME facts => facts 

573 
 NONE => snd (hd factss) 

574 

42730
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

575 
(* Unwanted equalities are those between a (bound or schematic) variable that 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

576 
does not properly occur in the second operand. *) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

577 
val is_exhaustive_finite = 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

578 
let 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

579 
fun is_bad_equal (Var z) t = 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

580 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

581 
 is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

582 
 is_bad_equal _ _ = false 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

583 
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

584 
fun do_formula pos t = 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

585 
case (pos, t) of 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

586 
(_, @{const Trueprop} $ t1) => do_formula pos t1 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

587 
 (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

588 
do_formula pos t' 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

589 
 (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

590 
do_formula pos t' 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

591 
 (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

592 
do_formula pos t' 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

593 
 (_, @{const "==>"} $ t1 $ t2) => 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

594 
do_formula (not pos) t1 andalso 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

595 
(t2 = @{prop False} orelse do_formula pos t2) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

596 
 (_, @{const HOL.implies} $ t1 $ t2) => 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

597 
do_formula (not pos) t1 andalso 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

598 
(t2 = @{const False} orelse do_formula pos t2) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

599 
 (_, @{const Not} $ t1) => do_formula (not pos) t1 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

600 
 (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

601 
 (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

602 
 (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

603 
 (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

604 
 _ => false 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

605 
in do_formula true end 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

606 

d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

607 
fun has_bound_or_var_of_type pred = 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

608 
exists_subterm (fn Var (_, T as Type _) => pred T 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

609 
 Abs (_, T as Type _, _) => pred T 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

610 
 _ => false) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

611 

d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

612 
(* Facts are forbidden to contain variables of these types. The typical reason 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

613 
is that they lead to unsoundness. Note that "unit" satisfies numerous 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

614 
equations like "?x = ()". The resulting clauses will have no type constraint, 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

615 
yielding false proofs. Even "bool" leads to many unsound proofs, though only 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

616 
for higherorder problems. *) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

617 

d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

618 
(* Facts containing variables of type "unit" or "bool" or of the form 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

619 
"ALL x. x = A  x = B  x = C" are likely to lead to unsound proofs if types 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

620 
are omitted. *) 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

621 
fun is_dangerous_prop ctxt = 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

622 
transform_elim_prop 
44393  623 
#> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf 
42730
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

624 
is_exhaustive_finite) 
d6db5a815477
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents:
42729
diff
changeset

625 

39492  626 
(* Important messages are important but not so important that users want to see 
627 
them each time. *) 

44649  628 
val atp_important_message_keep_quotient = 25 
39492  629 

44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44397
diff
changeset

630 
fun choose_type_enc soundness best_type_enc format = 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44394
diff
changeset

631 
the_default best_type_enc 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

632 
#> type_enc_of_string soundness 
44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44397
diff
changeset

633 
#> adjust_type_enc format 
42548
ea2a28b1938f
make sure the minimizer monomorphizes when it should
blanchet
parents:
42544
diff
changeset

634 

51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

635 
fun isar_proof_reconstructor ctxt name = 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

636 
let val thy = Proof_Context.theory_of ctxt in 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

637 
if is_atp thy name then name 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

638 
else remotify_prover_if_not_installed ctxt eN > the_default name 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

639 
end 
43051  640 

51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

641 
(* See the analogous logic in the function "maybe_minimize" in 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

642 
"sledgehammer_minimize.ML". *) 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

643 
fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

644 
name preplay = 
45520  645 
let 
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

646 
val maybe_isar_name = 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

647 
name > isar_proofs = SOME true ? isar_proof_reconstructor ctxt 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

648 
val (min_name, override_params) = 
45520  649 
case preplay of 
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

650 
Played (reconstr, _) => 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

651 
if isar_proofs = SOME true then (maybe_isar_name, []) 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

652 
else extract_reconstructor params reconstr 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

653 
 _ => (maybe_isar_name, []) 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

654 
in minimize_command override_params min_name end 
43051  655 

53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset

656 
val max_fact_instances = 10 (* FUDGE *) 
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset

657 

52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

658 
fun repair_monomorph_context max_iters best_max_iters max_new_instances 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

659 
best_max_new_instances = 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

660 
Config.put Monomorph.max_rounds (max_iters > the_default best_max_iters) 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

661 
#> Config.put Monomorph.max_new_instances 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

662 
(max_new_instances > the_default best_max_new_instances) 
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset

663 
#> Config.put Monomorph.max_thm_instances max_fact_instances 
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

664 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

665 
fun suffix_of_mode Auto_Try = "_try" 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

666 
 suffix_of_mode Try = "_try" 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

667 
 suffix_of_mode Normal = "" 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

668 
 suffix_of_mode MaSh = "" 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

669 
 suffix_of_mode Auto_Minimize = "_min" 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

670 
 suffix_of_mode Minimize = "_min" 
44509
369e8c28a61a
added a component in generated file names reflecting whether the minimizer is used  needed for evaluation to keep these files separated from the main problem files
blanchet
parents:
44423
diff
changeset

671 

44423
f74707e12d30
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents:
44416
diff
changeset

672 
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on 
43631
4144d7b4ec77
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents:
43626
diff
changeset

673 
Linux appears to be the only ATP that does not honor its time limit. *) 
43690  674 
val atp_timeout_slack = seconds 1.0 
43631
4144d7b4ec77
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents:
43626
diff
changeset

675 

48331
f190a6dbb29b
make the monomorphizer more predictable by making the cutoff independent on the number of facts
blanchet
parents:
48321
diff
changeset

676 
val mono_max_privileged_facts = 10 
f190a6dbb29b
make the monomorphizer more predictable by making the cutoff independent on the number of facts
blanchet
parents:
48321
diff
changeset

677 

51186
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

678 
(* For low values of "max_facts", this fudge value ensures that most slices are 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

679 
invoked with a nontrivial amount of facts. *) 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

680 
val max_fact_factor_fudge = 5 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

681 

43021  682 
fun run_atp mode name 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

683 
({exec, arguments, proof_delims, known_failures, prem_role, best_slices, 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

684 
best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) 
46301  685 
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, 
51024
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51014
diff
changeset

686 
uncurried_aliases, fact_filter, max_facts, max_mono_iters, 
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51024
diff
changeset

687 
max_new_mono_instances, isar_proofs, isar_compress, 
53137  688 
isar_compress_degree, merge_timeout_slack, isar_try0, 
689 
isar_minimize, slice, timeout, preplay_timeout, 

690 
preplay_trace, ...}) 

43037  691 
minimize_command 
51013  692 
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = 
38023  693 
let 
42182
a630978fc967
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents:
42181
diff
changeset

694 
val thy = Proof.theory_of state 
39318  695 
val ctxt = Proof.context_of state 
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
47934
diff
changeset

696 
val atp_mode = 
48143  697 
if Config.get ctxt completish then Sledgehammer_Completish 
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higherorder features without breaking "metis"
blanchet
parents:
47934
diff
changeset

698 
else Sledgehammer 
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof  have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52150
diff
changeset

699 
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

700 
val (dest_dir, problem_prefix) = 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

701 
if overlord then overlord_file_location_of_prover name 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

702 
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

703 
val problem_file_name = 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

704 
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

705 
suffix_of_mode mode ^ "_" ^ string_of_int subgoal) 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

706 
val prob_path = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

707 
if dest_dir = "" then 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

708 
File.tmp_path problem_file_name 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

709 
else if File.exists (Path.explode dest_dir) then 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

710 
Path.append (Path.explode dest_dir) problem_file_name 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

711 
else 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

712 
error ("No such directory: " ^ quote dest_dir ^ ".") 
52754
d9d90d29860e
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents:
52697
diff
changeset

713 
val exec = exec () 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

714 
val command0 = 
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47038
diff
changeset

715 
case find_first (fn var => getenv var <> "") (fst exec) of 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

716 
SOME var => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

717 
let 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

718 
val pref = getenv var ^ "/" 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

719 
val paths = map (Path.explode o prefix pref) (snd exec) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

720 
in 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

721 
case find_first File.exists paths of 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

722 
SOME path => path 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

723 
 NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".") 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

724 
end 
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47038
diff
changeset

725 
 NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^ 
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47038
diff
changeset

726 
" is not set.") 
38023  727 
fun split_time s = 
728 
let 

42448  729 
val split = String.tokens (fn c => str c = "\n") 
47737
63c939dcd055
made "split_last" more robust in the face of obscure lowlevel errors
blanchet
parents:
47606
diff
changeset

730 
val (output, t) = 
63c939dcd055
made "split_last" more robust in the face of obscure lowlevel errors
blanchet
parents:
47606
diff
changeset

731 
s > split > (try split_last #> the_default ([], "0")) 
63c939dcd055
made "split_last" more robust in the face of obscure lowlevel errors
blanchet
parents:
47606
diff
changeset

732 
>> cat_lines 
42448  733 
fun as_num f = f >> (fst o read_int) 
734 
val num = as_num (Scan.many1 Symbol.is_ascii_digit) 

735 
val digit = Scan.one Symbol.is_ascii_digit 

736 
val num3 = as_num (digit ::: digit ::: (digit >> single)) 

737 
val time = num  Scan.$$ "."  num3 >> (fn (a, b) => a * 1000 + b) 

45381  738 
val as_time = 
739 
raw_explode #> Scan.read Symbol.stopper time #> the_default 0 

47737
63c939dcd055
made "split_last" more robust in the face of obscure lowlevel errors
blanchet
parents:
47606
diff
changeset

740 
in (output, as_time t > Time.fromMilliseconds) end 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

741 
fun run () = 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

742 
let 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

743 
(* If slicing is disabled, we expand the last slice to fill the entire 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

744 
time available. *) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

745 
val actual_slices = get_slices slice (best_slices ctxt) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

746 
val num_actual_slices = length actual_slices 
51186
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

747 
val max_fact_factor = 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

748 
case max_facts of 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

749 
NONE => 1.0 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

750 
 SOME max => 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

751 
Real.fromInt max 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

752 
/ Real.fromInt (fold (Integer.max o slice_max_facts) 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

753 
actual_slices 0) 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

754 
fun monomorphize_facts facts = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

755 
let 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

756 
val ctxt = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

757 
ctxt 
53478  758 
> repair_monomorph_context max_mono_iters 
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

759 
best_max_mono_iters max_new_mono_instances 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

760 
best_max_new_mono_instances 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

761 
(* pseudotheorem involving the same constants as the subgoal *) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

762 
val subgoal_th = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

763 
Logic.list_implies (hyp_ts, concl_t) > Skip_Proof.make_thm thy 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

764 
val rths = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

765 
facts > chop mono_max_privileged_facts 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

766 
>> map (pair 1 o snd) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

767 
> map (pair 2 o snd) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

768 
> op @ 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

769 
> cons (0, subgoal_th) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

770 
in 
53478  771 
Monomorph.monomorph atp_schematic_consts_of ctxt rths 
772 
> tl > curry ListPair.zip (map fst facts) 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

773 
> maps (fn (name, rths) => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

774 
map (pair name o zero_var_indexes o snd) rths) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

775 
end 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

776 
fun run_slice time_left (cache_key, cache_value) 
48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48656
diff
changeset

777 
(slice, (time_frac, 
51011  778 
(key as ((best_max_facts, best_fact_filter), format, 
779 
best_type_enc, best_lam_trans, 

780 
best_uncurried_aliases), 

48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48656
diff
changeset

781 
extra))) = 
38032  782 
let 
51024
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51014
diff
changeset

783 
val effective_fact_filter = 
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51014
diff
changeset

784 
fact_filter > the_default best_fact_filter 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

785 
val facts = get_facts_of_filter effective_fact_filter factss 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

786 
val num_facts = 
51186
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

787 
Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

788 
max_fact_factor_fudge 
c8721406511a
interpret "max_facts" argument in a slicedependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents:
51181
diff
changeset

789 
> Integer.min (length facts) 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

790 
val soundness = if strict then Strict else Non_Strict 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

791 
val type_enc = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

792 
type_enc > choose_type_enc soundness best_type_enc format 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

793 
val sound = is_type_enc_sound type_enc 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

794 
val real_ms = Real.fromInt o Time.toMilliseconds 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

795 
val slice_timeout = 
50557  796 
case time_left of 
797 
SOME time_left => 

798 
((real_ms time_left 

799 
> (if slice < num_actual_slices  1 then 

800 
curry Real.min (time_frac * real_ms (the timeout)) 

801 
else 

802 
I)) 

803 
* 0.001) 

804 
> seconds > SOME 

805 
 NONE => NONE 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

806 
val generous_slice_timeout = 
50558
a719106124d8
avoid creating nested threads for MaSh  this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
blanchet
parents:
50557
diff
changeset

807 
if mode = MaSh then NONE 
a719106124d8
avoid creating nested threads for MaSh  this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
blanchet
parents:
50557
diff
changeset

808 
else Option.map (curry Time.+ atp_timeout_slack) slice_timeout 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

809 
val _ = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

810 
if debug then 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

811 
quote name ^ " slice #" ^ string_of_int (slice + 1) ^ 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

812 
" with " ^ string_of_int num_facts ^ " fact" ^ 
50557  813 
plural_s num_facts ^ 
814 
(case slice_timeout of 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

815 
SOME timeout => " for " ^ string_of_time timeout 
50557  816 
 NONE => "") ^ "..." 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

817 
> Output.urgent_message 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

818 
else 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

819 
() 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

820 
val readable_names = not (Config.get ctxt atp_full_names) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

821 
val lam_trans = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

822 
case lam_trans of 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

823 
SOME s => s 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

824 
 NONE => best_lam_trans 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

825 
val uncurried_aliases = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

826 
case uncurried_aliases of 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

827 
SOME b => b 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

828 
 NONE => best_uncurried_aliases 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

829 
val value as (atp_problem, _, fact_names, _, _) = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

830 
if cache_key = SOME key then 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

831 
cache_value 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

832 
else 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

833 
facts 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

834 
> not sound 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

835 
? filter_out (is_dangerous_prop ctxt o prop_of o snd) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

836 
> take num_facts 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

837 
> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

838 
> map (apsnd prop_of) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

839 
> prepare_atp_problem ctxt format prem_role type_enc atp_mode 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

840 
lam_trans uncurried_aliases 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

841 
readable_names true hyp_ts concl_t 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

842 
fun sel_weights () = atp_problem_selection_weights atp_problem 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

843 
fun ord_info () = atp_problem_term_order_info atp_problem 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

844 
val ord = effective_term_order ctxt name 
53492
c3d7d9911aae
since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
blanchet
parents:
53480
diff
changeset

845 
val full_proof = isar_proofs > the_default (mode = Minimize) 
50927  846 
val args = 
847 
arguments ctxt full_proof extra 

848 
(slice_timeout > the_default one_day) 

849 
(File.shell_path prob_path) (ord, ord_info, sel_weights) 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

850 
val command = 
50927  851 
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" 
48532
c0f44941e674
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers  no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents:
48392
diff
changeset

852 
> enclose "TIMEFORMAT='%3R'; { time " " ; }" 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

853 
val _ = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

854 
atp_problem 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

855 
> lines_of_atp_problem format ord ord_info 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

856 
> cons ("% " ^ command ^ "\n") 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

857 
> File.write_list prob_path 
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

858 
val ((output, run_time), (atp_proof, outcome)) = 
50557  859 
time_limit generous_slice_timeout Isabelle_System.bash_output 
860 
command 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

861 
>> (if overlord then 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

862 
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

863 
else 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

864 
I) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

865 
> fst > split_time 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

866 
> (fn accum as (output, _) => 
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

867 
(accum, 
48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48656
diff
changeset

868 
extract_tstplike_proof_and_outcome verbose proof_delims 
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48656
diff
changeset

869 
known_failures output 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

870 
>> atp_proof_of_tstplike_proof atp_problem 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

871 
handle UNRECOGNIZED_ATP_PROOF () => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

872 
([], SOME ProofIncomplete))) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

873 
handle TimeLimit.TimeOut => 
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

874 
(("", the slice_timeout), ([], SOME TimedOut)) 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

875 
val outcome = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

876 
case outcome of 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

877 
NONE => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

878 
(case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

879 
> Option.map (sort string_ord) of 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

880 
SOME facts => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

881 
let 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

882 
val failure = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

883 
UnsoundProof (is_type_enc_sound type_enc, facts) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

884 
in 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

885 
if debug then (warning (string_of_failure failure); NONE) 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

886 
else SOME failure 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

887 
end 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

888 
 NONE => NONE) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

889 
 _ => outcome 
51013  890 
in 
891 
((SOME key, value), (output, run_time, facts, atp_proof, outcome)) 

892 
end 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

893 
val timer = Timer.startRealTimer () 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

894 
fun maybe_run_slice slice 
51013  895 
(result as (cache, (_, run_time0, _, _, SOME _))) = 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

896 
let 
50557  897 
val time_left = 
898 
Option.map 

899 
(fn timeout => Time. (timeout, Timer.checkRealTimer timer)) 

900 
timeout 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

901 
in 
50557  902 
if time_left <> NONE andalso 
903 
Time.<= (the time_left, Time.zeroTime) then 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

904 
result 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

905 
else 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

906 
run_slice time_left cache slice 
51013  907 
> (fn (cache, (output, run_time, used_from, atp_proof, 
908 
outcome)) => 

909 
(cache, (output, Time.+ (run_time0, run_time), used_from, 

48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

910 
atp_proof, outcome))) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

911 
end 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

912 
 maybe_run_slice _ result = result 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

913 
in 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

914 
((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), 
51013  915 
("", Time.zeroTime, [], [], SOME InternalError)) 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

916 
> fold maybe_run_slice actual_slices 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

917 
end 
38023  918 
(* If the problem file has not been exported, remove it; otherwise, export 
919 
the proof file too. *) 

48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

920 
fun clean_up () = 
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

921 
if dest_dir = "" then (try File.rm prob_path; ()) else () 
51013  922 
fun export (_, (output, _, _, _, _)) = 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

923 
if dest_dir = "" then () 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

924 
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output 
52150
41c885784e04
handle lambdalifted problems in Isar construction code
blanchet
parents:
52125
diff
changeset

925 
val ((_, (_, pool, fact_names, lifted, sym_tab)), 
51013  926 
(output, run_time, used_from, atp_proof, outcome)) = 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

927 
with_cleanup clean_up run () > tap export 
39492  928 
val important_message = 
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset

929 
if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient  1) = 0 
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset

930 
then 
39492  931 
extract_important_message output 
932 
else 

933 
"" 

43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

934 
val (used_facts, preplay, message, message_tail) = 
38023  935 
case outcome of 
936 
NONE => 

43033  937 
let 
45551  938 
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof 
45590  939 
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof 
45521  940 
val reconstrs = 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45553
diff
changeset

941 
bunch_of_reconstructors needs_full_types 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

942 
(lam_trans_of_atp_proof atp_proof 
46405  943 
o (fn desperate => if desperate then hide_lamsN 
944 
else metis_default_lam_trans)) 

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

946 
(used_facts, 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

947 
Lazy.lazy (fn () => 
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

948 
let 
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

949 
val used_pairs = 
51013  950 
used_from > filter_used_facts false used_facts 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

951 
in 
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

952 
play_one_line_proof mode debug verbose preplay_timeout 
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

953 
used_pairs state subgoal (hd reconstrs) reconstrs 
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

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

955 
fn preplay => 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

956 
let 
49921  957 
val _ = 
958 
if verbose then 

51232  959 
Output.urgent_message "Generating proof text..." 
49921  960 
else 
961 
() 

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

962 
val isar_params = 
52754
d9d90d29860e
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents:
52697
diff
changeset

963 
(debug, verbose, preplay_timeout, preplay_trace, 
d9d90d29860e
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents:
52697
diff
changeset

964 
isar_compress, isar_compress_degree, merge_timeout_slack, 
53137  965 
isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab, 
966 
atp_proof, goal) 

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

967 
val one_line_params = 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

968 
(preplay, proof_banner mode name, used_facts, 
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

969 
choose_minimize_command ctxt params minimize_command name 
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset

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

971 
subgoal, subgoal_count) 
48799  972 
val num_chained = length (#facts (Proof.goal state)) 
973 
in 

53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset

974 
proof_text ctxt isar_proofs isar_params 
52754
d9d90d29860e
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents:
52697
diff
changeset

975 
num_chained one_line_params 
48799  976 
end, 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

977 
(if verbose then 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

978 
"\nATP real CPU time: " ^ string_of_time run_time ^ "." 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

979 
else 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

980 
"") ^ 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

981 
(if important_message <> "" then 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

982 
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

983 
important_message 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

984 
else 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

985 
"")) 
43033  986 
end 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

987 
 SOME failure => 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50667
diff
changeset

988 
([], Lazy.value (Failed_to_Play plain_metis), 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

989 
fn _ => string_of_failure failure, "") 
38023  990 
in 
51013  991 
{outcome = outcome, used_facts = used_facts, used_from = used_from, 
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset

992 
run_time = run_time, preplay = preplay, message = message, 
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset

993 
message_tail = message_tail} 
38023  994 
end 
995 

51014  996 
fun rotate_one (x :: xs) = xs @ [x] 
997 

40669  998 
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until 
999 
these are sorted out properly in the SMT module, we have to interpret these 

1000 
ourselves. *) 

40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

1001 
val remote_smt_failures = 
43631
4144d7b4ec77
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents:
43626
diff
changeset

1002 
[(2, NoLibwwwPerl), 
4144d7b4ec77
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents:
43626
diff
changeset

1003 
(22, CantConnect)] 
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

1004 
val z3_failures = 
41236  1005 
[(101, OutOfResources), 
1006 
(103, MalformedInput), 

50667  1007 
(110, MalformedInput), 
1008 
(112, TimedOut)] 

40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

1009 
val unix_failures = 
48797  1010 
[(138, Crashed), 
1011 
(139, Crashed)] 

43631
4144d7b4ec77
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents:
43626
diff
changeset

1012 
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures 
40555  1013 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

1014 
fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) = 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

1015 
if is_real_cex then Unprovable else GaveUp 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

1016 
 failure_of_smt_failure SMT_Failure.Time_Out = TimedOut 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

1017 
 failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = 
41222  1018 
(case AList.lookup (op =) smt_failures code of 
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

1019 
SOME failure => failure 
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset

1020 
 NONE => UnknownError ("Abnormal termination with exit code " ^ 
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41256
diff
changeset

1021 
string_of_int code ^ ".")) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

1022 
 failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources 
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

1023 
 failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

1024 

40698  1025 
(* FUDGE *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1026 
val smt_max_slices = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1027 
Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1028 
val smt_slice_fact_frac = 
51014  1029 
Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} 
1030 
(K 0.667) 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1031 
val smt_slice_time_frac = 
51014  1032 
Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1033 
val smt_slice_min_secs = 
51014  1034 
Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3) 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

1035 

50759  1036 
fun smt_filter_loop name 
42724
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42723
diff
changeset

1037 
({debug, verbose, overlord, max_mono_iters, 
45706  1038 
max_new_mono_instances, timeout, slice, ...} : params) 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
50020
diff
changeset

1039 
state goal i = 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

1040 
let 
50759  1041 
fun repair_context ctxt = 
1042 
ctxt > select_smt_solver name 

1043 
> Config.put SMT_Config.verbose debug 

1044 
> (if overlord then 

1045 
Config.put SMT_Config.debug_files 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51879
diff
changeset

1046 
(overlord_file_location_of_prover name 
50759  1047 
> (fn (path, name) => path ^ "/" ^ name)) 
1048 
else 

1049 
I) 

1050 
> Config.put SMT_Config.infer_triggers 

1051 
(Config.get ctxt smt_triggers) 

52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

1052 
> repair_monomorph_context max_mono_iters default_max_mono_iters 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

1053 
max_new_mono_instances default_max_new_mono_instances 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

1054 
val state = Proof.map_context (repair_context) state 
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset

1055 
val ctxt = Proof.context_of state 
45706  1056 
val max_slices = if slice then Config.get ctxt smt_max_slices else 1 
51024
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51014
diff
changeset

1057 
fun do_slice timeout slice outcome0 time_so_far 
98fb341d32e3
distinguish MeSh and smart  with smart, allow combinations of MaSh, MeSh, and MePo in different slices  and use MaSh also with SMT solvers, based on evaluation
blanchet
parents:
51014
diff
changeset

1058 
(weighted_factss as (fact_filter, weighted_facts) :: _) = 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1059 
let 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1060 
val timer = Timer.startRealTimer () 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

1061 
val slice_timeout = 
50557  1062 
if slice < max_slices andalso timeout <> NONE then 
1063 
let val ms = timeout > the > Time.toMilliseconds in 

1064 
Int.min (ms, 

1065 
Int.max (1000 * Config.get ctxt smt_slice_min_secs, 

1066 
Real.ceil (Config.get ctxt smt_slice_time_frac 

1067 
* Real.fromInt ms))) 

1068 
> Time.fromMilliseconds > SOME 

1069 
end 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1070 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1071 
timeout 
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset

1072 
val num_facts = length weighted_facts 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1073 
val _ = 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1074 
if debug then 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1075 
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ 
50557  1076 
string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ 
1077 
(case slice_timeout of 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

1078 
SOME timeout => " for " ^ string_of_time timeout 
50557  1079 
 NONE => "") ^ "..." 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1080 
> Output.urgent_message 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1081 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1082 
() 
41168  1083 
val birth = Timer.checkRealTimer timer 
41171  1084 
val _ = 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset

1085 
if debug then Output.urgent_message "Invoking SMT solver..." else () 
41209  1086 
val (outcome, used_facts) = 
51204
20f6d400cc68
don't pass chained facts directly to SMT solvers  this breaks various invariants and is never necessary
blanchet
parents:
51200
diff
changeset

1087 
SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i 
50557  1088 
> SMT_Solver.smt_filter_apply (slice_timeout > the_default one_day) 
41239  1089 
> (fn {outcome, used_facts} => (outcome, used_facts)) 
41209  1090 
handle exn => if Exn.is_interrupt exn then 
1091 
reraise exn 

1092 
else 

42061
71077681eaf6
let SMT errors through  the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
blanchet
parents:
42060
diff
changeset

1093 
(ML_Compiler.exn_message exn 
41209  1094 
> SMT_Failure.Other_Failure > SOME, []) 
41168  1095 
val death = Timer.checkRealTimer timer 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1096 
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 
41168  1097 
val time_so_far = Time.+ (time_so_far, Time. (death, birth)) 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1098 
val too_many_facts_perhaps = 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1099 
case outcome of 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1100 
NONE => false 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1101 
 SOME (SMT_Failure.Counterexample _) => false 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

1102 
 SOME SMT_Failure.Time_Out => slice_timeout <> timeout 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1103 
 SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1104 
 SOME SMT_Failure.Out_Of_Memory => true 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset

1105 
 SOME (SMT_Failure.Other_Failure _) => true 
50557 