author  blanchet 
Sat, 15 Dec 2012 19:57:12 +0100  
changeset 50557  31313171deb5 
parent 50494  06b199a042ff 
child 50558  a719106124d8 
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 
49914  14 
type reconstructor = Sledgehammer_Reconstruct.reconstructor 
15 
type play = Sledgehammer_Reconstruct.play 

16 
type minimize_command = Sledgehammer_Reconstruct.minimize_command 

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

17 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48376
diff
changeset

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

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

23 
overlord : bool, 

24 
blocking : bool, 

25 
provers : string list, 

26 
type_enc : string option, 

27 
strict : bool, 

28 
lam_trans : string option, 

29 
uncurried_aliases : bool option, 

30 
learn : bool, 

31 
fact_filter : string option, 

32 
max_facts : int option, 

33 
fact_thresholds : real * real, 

34 
max_mono_iters : int option, 

35 
max_new_mono_instances : int option, 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

36 
isar_proofs : bool, 
50020  37 
isar_shrink : real, 
48321  38 
slice : bool, 
39 
minimize : bool option, 

50557  40 
timeout : Time.time option, 
41 
preplay_timeout : Time.time option, 

48321  42 
expect : string} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

43 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

64 

41090  65 
datatype prover_fact = 
46340  66 
Untranslated_Fact of (string * stature) * thm  
67 
SMT_Weighted_Fact of (string * stature) * (int option * thm) 

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

68 

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

69 
type prover_problem = 
48321  70 
{state : Proof.state, 
71 
goal : thm, 

72 
subgoal : int, 

73 
subgoal_count : int, 

74 
facts : prover_fact list} 

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

75 

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

76 
type prover_result = 
48321  77 
{outcome : failure option, 
78 
used_facts : (string * stature) list, 

79 
run_time : Time.time, 

80 
preplay : unit > play, 

81 
message : play > string, 

82 
message_tail : string} 

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

83 

43051  84 
type prover = 
45520  85 
params > ((string * string list) list > string > minimize_command) 
86 
> prover_problem > prover_result 

35867  87 

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

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

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

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

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

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

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

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

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

97 
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

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

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

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

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

102 
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

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

104 
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

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

107 
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

108 
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

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

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

111 
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

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

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

114 
val is_prover_installed : Proof.context > string > bool 
48293  115 
val default_max_facts_for_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

116 
val is_unit_equality : term > bool 
42952
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset

117 
val is_appropriate_prop_for_prover : Proof.context > string > term > bool 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

118 
val is_built_in_const_for_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

119 
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

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

121 
val smt_relevance_fudge : relevance_fudge 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

122 
val relevance_fudge_for_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

123 
val weight_smt_fact : 
46340  124 
Proof.context > int > ((string * stature) * thm) * int 
125 
> (string * stature) * (int option * thm) 

126 
val untranslated_fact : prover_fact > (string * stature) * thm 

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

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

128 
Proof.context > int > prover_fact * int 
46340  129 
> (string * stature) * (int option * thm) 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41723
diff
changeset

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

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

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

133 
val messages : int option > unit 
48798  134 
val is_fact_chained : (('a * stature) * 'b) > bool 
135 
val filter_used_facts : 

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

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

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

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

140 

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

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

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

143 

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

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

146 
open ATP_Proof 
38028  147 
open ATP_Systems 
46320  148 
open ATP_Problem_Generate 
149 
open ATP_Proof_Reconstruct 

45521  150 
open Metis_Tactic 
38023  151 
open Sledgehammer_Util 
49881
d9d73ebf9274
added proof minimization code from Steffen Smolka
blanchet
parents:
48802
diff
changeset

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

153 

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

154 

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

155 
(** 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

156 

48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48376
diff
changeset

157 
datatype mode = Auto_Try  Try  Normal  MaSh  Auto_Minimize  Minimize 
43021  158 

45376  159 
(* 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

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

161 
val SledgehammerN = "Sledgehammer" 
37585  162 

45520  163 
val reconstructor_names = [metisN, smtN] 
46365  164 
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

165 
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

166 

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

167 
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

168 

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

169 
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

170 

45376  171 
fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt) 
40062  172 

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

174 
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

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

176 
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

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

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

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

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

181 

44597  182 
val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ) 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

183 
val is_ho_atp = is_atp_for_format is_format_higher_order 
44597  184 

45376  185 
fun is_prover_supported ctxt = 
42361  186 
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

187 
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

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

189 

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

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

191 
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

192 
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

193 

45706  194 
fun get_slices slice slices = 
195 
(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

196 

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

198 

48293  199 
fun default_max_facts_for_prover ctxt slice name = 
42361  200 
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

201 
if is_reconstructor name then 
48293  202 
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

203 
else if is_atp thy name then 
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

204 
fold (Integer.max o #1 o fst o snd o snd) 
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47531
diff
changeset

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

206 
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

207 
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

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

209 

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

210 
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

211 
 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

212 

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

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

214 
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

215 
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

216 
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

217 

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

218 
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

219 
 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

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

221 
 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

222 
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

223 
 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

224 
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

225 
 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

226 
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

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

228 

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

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

230 
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

231 

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

232 
fun is_built_in_const_for_prover ctxt name = 
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

233 
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

234 
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

235 
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

236 
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

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

238 
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

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

240 
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

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

242 
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

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

244 
fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts 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

245 

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

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

247 
val atp_relevance_fudge = 
42738  248 
{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

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

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

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

252 
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

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

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

255 
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

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

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

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

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

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

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

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

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

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

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

267 

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

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

269 
val smt_relevance_fudge = 
42738  270 
{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

271 
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

272 
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

273 
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

274 
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

275 
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

276 
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

277 
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

278 
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

279 
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

280 
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

281 
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

282 
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

283 
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

284 
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

285 
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

286 
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

287 
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

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

289 

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

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

291 
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

292 

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

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

294 
let 
42361  295 
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

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

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

299 
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

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

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

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

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

304 
end 
35969  305 

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

306 
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

307 
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

308 
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

309 

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

310 

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

311 
(** problems, results, ATPs, etc. **) 
35969  312 

313 
type params = 

48321  314 
{debug : bool, 
315 
verbose : bool, 

316 
overlord : bool, 

317 
blocking : bool, 

318 
provers : string list, 

319 
type_enc : string option, 

320 
strict : bool, 

321 
lam_trans : string option, 

322 
uncurried_aliases : bool option, 

323 
learn : bool, 

324 
fact_filter : string option, 

325 
max_facts : int option, 

326 
fact_thresholds : real * real, 

327 
max_mono_iters : int option, 

328 
max_new_mono_instances : int option, 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

329 
isar_proofs : bool, 
50020  330 
isar_shrink : real, 
48321  331 
slice : bool, 
332 
minimize : bool option, 

50557  333 
timeout : Time.time option, 
334 
preplay_timeout : Time.time option, 

48321  335 
expect : string} 
35867  336 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

357 

41090  358 
datatype prover_fact = 
46340  359 
Untranslated_Fact of (string * stature) * thm  
360 
SMT_Weighted_Fact of (string * stature) * (int option * thm) 

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

361 

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

362 
type prover_problem = 
48321  363 
{state : Proof.state, 
364 
goal : thm, 

365 
subgoal : int, 

366 
subgoal_count : int, 

367 
facts : prover_fact list} 

35867  368 

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

369 
type prover_result = 
48321  370 
{outcome : failure option, 
371 
used_facts : (string * stature) list, 

372 
run_time : Time.time, 

373 
preplay : unit > play, 

374 
message : play > string, 

375 
message_tail : string} 

35867  376 

43051  377 
type prover = 
45520  378 
params > ((string * string list) list > string > minimize_command) 
379 
> prover_problem > prover_result 

35867  380 

38023  381 
(* configuration attributes *) 
382 

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

383 
(* 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

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

385 
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

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

387 
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") 
48143  388 
val completish = 
389 
Attrib.setup_config_bool @{binding sledgehammer_completish} (K false) 

28484  390 

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

391 
(* 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

392 
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

393 
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

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

395 
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

396 

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

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

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

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

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

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

402 
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

403 

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

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

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

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

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

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

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

410 
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

411 
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

412 

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

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

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

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

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

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

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

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

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

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

422 
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

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

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

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

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

427 

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

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

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

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

431 
end 
38023  432 

41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

433 
fun untranslated_fact (Untranslated_Fact p) = p 
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

434 
 untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

435 
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

436 
 smt_weighted_fact ctxt num_facts (fact, j) = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

437 
(untranslated_fact fact, j) > weight_smt_fact ctxt num_facts 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

438 

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

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

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

441 

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

442 
fun proof_banner mode name = 
43033  443 
case mode of 
444 
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" 

445 
 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

446 
 _ => "Try this" 
43033  447 

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

448 
fun bunch_of_reconstructors needs_full_types lam_trans = 
48800  449 
if needs_full_types then 
48802  450 
[Metis (full_type_enc, lam_trans false), 
451 
Metis (really_full_type_enc, lam_trans false), 

452 
Metis (full_type_enc, lam_trans true), 

453 
Metis (really_full_type_enc, lam_trans true), 

454 
SMT] 

455 
else 

48800  456 
[Metis (partial_type_enc, lam_trans false), 
457 
Metis (full_type_enc, lam_trans false), 

458 
Metis (no_typesN, lam_trans true), 

459 
Metis (really_full_type_enc, lam_trans true), 

460 
SMT] 

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

461 

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

462 
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

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

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

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

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

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

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

469 
[("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

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

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

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

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

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

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

476 

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

478 
fun timed_apply timeout tac state i = 
43033  479 
let 
480 
val {context = ctxt, facts, goal} = Proof.goal state 

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

50557  482 
in time_limit timeout (try (Seq.pull o full_tac)) goal end 
43033  483 

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

484 
fun tac_for_reconstructor (Metis (type_enc, lam_trans)) = 
45521  485 
metis_tac [type_enc] lam_trans 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

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

487 

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

489 
(Config.put Metis_Tactic.verbose debug 
45557  490 
#> Config.put SMT_Config.verbose debug 
45520  491 
#> (fn ctxt => tac_for_reconstructor reconstr ctxt ths)) 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

492 
> timed_apply timeout 
43033  493 

48798  494 
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained 
495 

496 
fun filter_used_facts keep_chained used = 

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

498 
(if keep_chained then is_fact_chained else K false)) 

43033  499 

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

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

502 
let 
45520  503 
fun get_preferred reconstrs = 
504 
if member (op =) reconstrs preferred then preferred 

505 
else List.last reconstrs 

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

506 
in 
50557  507 
if timeout = SOME Time.zeroTime then 
45520  508 
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

509 
else 
50557  510 
let 
511 
val _ = 

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

513 
else () 

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

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

516 
 play timed_outs [] = 

517 
Trust_Playable (get_preferred timed_outs, timeout) 

518 
 play timed_out (reconstr :: reconstrs) = 

519 
let 

520 
val _ = 

521 
if verbose then 

522 
"Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^ 

523 
(case timeout of 

524 
SOME timeout => " for " ^ string_from_time timeout 

525 
 NONE => "") ^ "..." 

526 
> Output.urgent_message 

527 
else 

528 
() 

529 
val timer = Timer.startRealTimer () 

530 
in 

531 
case timed_reconstructor reconstr debug timeout ths state i of 

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

533 
 _ => play timed_out reconstrs 

534 
end 

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

536 
in play [] reconstrs end 

43033  537 
end 
538 

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

539 

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

540 
(* 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

541 

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

542 
(* 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

543 
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

544 
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

545 
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

546 

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

547 
(* 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

548 
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

549 
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

550 
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

551 
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

552 
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

553 
 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

554 
 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

555 
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

556 
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

557 
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

558 
(_, @{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

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

560 
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

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

562 
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

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

564 
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

565 
 (_, @{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

566 
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

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

568 
 (_, @{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

569 
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

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

571 
 (_, @{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

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

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

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

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

576 
 _ => 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

577 
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

578 

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

580 
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

581 
 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

582 
 _ => 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 

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

585 
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

586 
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

587 
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

588 
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

589 

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

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

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

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

594 
transform_elim_prop 
44393  595 
#> (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

596 
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

597 

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

44649  600 
val atp_important_message_keep_quotient = 25 
39492  601 

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

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

603 
the_default best_type_enc 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44394
diff
changeset

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

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

606 

43051  607 
val metis_minimize_max_time = seconds 2.0 
608 

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

609 
fun choose_minimize_command params minimize_command name preplay = 
45520  610 
let 
611 
val (name, override_params) = 

612 
case preplay of 

613 
Played (reconstr, time) => 

614 
if Time.<= (time, metis_minimize_max_time) then 

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

615 
extract_reconstructor params reconstr 
45520  616 
else 
617 
(name, []) 

618 
 _ => (name, []) 

619 
in minimize_command override_params name end 

43051  620 

47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

621 
fun repair_monomorph_context max_iters best_max_iters max_new_instances 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

622 
best_max_new_instances = 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

623 
Config.put Monomorph.max_rounds (max_iters > the_default best_max_iters) 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

624 
#> Config.put Monomorph.max_new_instances 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

625 
(max_new_instances > the_default best_max_new_instances) 
43230
dabf6e311213
clarified meaning of monomorphization configuration option by renaming it
boehmes
parents:
43228
diff
changeset

626 
#> Config.put Monomorph.keep_partial_instances false 
43226  627 

50494  628 
fun suffix_for_mode Auto_Try = "_try" 
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

629 
 suffix_for_mode Try = "_try" 
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

630 
 suffix_for_mode Normal = "" 
50494  631 
 suffix_for_mode MaSh = "" 
632 
 suffix_for_mode Auto_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

633 
 suffix_for_mode Minimize = "_min" 
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

634 

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

635 
(* 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

636 
Linux appears to be the only ATP that does not honor its time limit. *) 
43690  637 
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

638 

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

639 
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

640 

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

642 
({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

643 
best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) 
46301  644 
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, 
48293  645 
uncurried_aliases, max_facts, max_mono_iters, 
50020  646 
max_new_mono_instances, isar_proofs, isar_shrink, 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset

647 
slice, timeout, preplay_timeout, ...}) 
43037  648 
minimize_command 
649 
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = 

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

651 
val thy = Proof.theory_of state 
39318  652 
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

653 
val atp_mode = 
48143  654 
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

655 
else Sledgehammer 
43004
20e9caff1f86
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents:
42998
diff
changeset

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

657 
val (dest_dir, problem_prefix) = 
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41152
diff
changeset

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

659 
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

660 
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

661 
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ 
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

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

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

664 
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

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

666 
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

667 
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

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

669 
error ("No such directory: " ^ quote dest_dir ^ ".") 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

670 
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

671 
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

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

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

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

675 
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

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

677 
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

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

679 
 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

680 
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

681 
 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

682 
" is not set.") 
38023  683 
fun split_time s = 
684 
let 

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

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

687 
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

688 
>> cat_lines 
42448  689 
fun as_num f = f >> (fst o read_int) 
690 
val num = as_num (Scan.many1 Symbol.is_ascii_digit) 

691 
val digit = Scan.one Symbol.is_ascii_digit 

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

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

45381  694 
val as_time = 
695 
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

696 
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

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

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

699 
(* 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

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

701 
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

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

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

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

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

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

707 
> repair_monomorph_context max_mono_iters best_max_mono_iters 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

709 
(* 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

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

711 
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

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

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

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

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

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

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

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

719 
Monomorph.monomorph atp_schematic_consts_of rths ctxt > fst > tl 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

720 
> curry ListPair.zip (map fst facts) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

722 
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

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

724 
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

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

726 
(key as (best_max_facts, format, best_type_enc, 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

727 
best_lam_trans, 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

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

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

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

732 
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

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

734 
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

735 
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

736 
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

737 
val slice_timeout = 
50557  738 
case time_left of 
739 
SOME time_left => 

740 
((real_ms time_left 

741 
> (if slice < num_actual_slices  1 then 

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

743 
else 

744 
I)) 

745 
* 0.001) 

746 
> seconds > SOME 

747 
 NONE => NONE 

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

748 
val generous_slice_timeout = 
50557  749 
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

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

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

752 
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

753 
" with " ^ string_of_int num_facts ^ " fact" ^ 
50557  754 
plural_s num_facts ^ 
755 
(case slice_timeout of 

756 
SOME timeout => " for " ^ string_from_time timeout 

757 
 NONE => "") ^ "..." 

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

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

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

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

761 
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

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

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

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

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

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

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

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

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

770 
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

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

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

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

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

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

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

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

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

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

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

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

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

783 
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

784 
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

785 
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

786 
val ord = effective_term_order ctxt name 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

787 
val full_proof = debug orelse isar_proofs 
50557  788 
val args = arguments ctxt full_proof extra 
789 
(slice_timeout > the_default one_day) 

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

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

791 
val command = 
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

792 
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

793 
File.shell_path prob_path ^ ")" 
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

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

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

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

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

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

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

800 
val ((output, run_time), (atp_proof, outcome)) = 
50557  801 
time_limit generous_slice_timeout Isabelle_System.bash_output 
802 
command 

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

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

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

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

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

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

808 
> (fn accum as (output, _) => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

810 
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

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

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

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

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

815 
handle TimeLimit.TimeOut => 
50557  816 
(("", the slice_timeout), ([], SOME TimedOut)) 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

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

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

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

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

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

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

825 
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

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

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

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

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

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

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

832 
in ((SOME key, value), (output, run_time, atp_proof, outcome)) end 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

835 
(result as (cache, (_, run_time0, _, SOME _))) = 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

836 
let 
50557  837 
val time_left = 
838 
Option.map 

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

840 
timeout 

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

841 
in 
50557  842 
if time_left <> NONE andalso 
843 
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

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

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

846 
run_slice time_left cache slice 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

847 
> (fn (cache, (output, run_time, atp_proof, outcome)) => 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

848 
(cache, (output, Time.+ (run_time0, run_time), 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

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

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

853 
((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

854 
("", Time.zeroTime, [], SOME InternalError)) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

856 
end 
38023  857 
(* If the problem file has not been exported, remove it; otherwise, export 
858 
the proof file too. *) 

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

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

860 
if dest_dir = "" then (try File.rm prob_path; ()) else () 
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

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

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

863 
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output 
46407
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46405
diff
changeset

864 
val ((_, (_, pool, fact_names, _, sym_tab)), 
30e9720cc0b9
optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents:
46405
diff
changeset

865 
(output, run_time, atp_proof, outcome)) = 
48656
5caa414ce9a2
cleaner temporary file cleanup for MaSh, based on triedandtrusted code
blanchet
parents:
48532
diff
changeset

866 
with_cleanup clean_up run () > tap export 
39492  867 
val important_message = 
43021  868 
if mode = Normal andalso 
42609  869 
random_range 0 (atp_important_message_keep_quotient  1) = 0 then 
39492  870 
extract_important_message output 
871 
else 

872 
"" 

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

873 
val (used_facts, preplay, message, message_tail) = 
38023  874 
case outcome of 
875 
NONE => 

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

880 
bunch_of_reconstructors needs_full_types 
45560
1606122a2d0f
don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
blanchet
parents:
45557
diff
changeset

881 
(lam_trans_from_atp_proof atp_proof 
46405  882 
o (fn desperate => if desperate then hide_lamsN 
883 
else metis_default_lam_trans)) 

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

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

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

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

888 
val used_pairs = 
48798  889 
facts > map untranslated_fact 
890 
> filter_used_facts false used_facts 

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

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

892 
play_one_line_proof mode debug verbose preplay_timeout 
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

893 
used_pairs state subgoal (hd reconstrs) reconstrs 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

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

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

896 
let 
49921  897 
val _ = 
898 
if verbose then 

899 
Output.urgent_message "Generating proof text..." 

900 
else 

901 
() 

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

902 
val isar_params = 
50020  903 
(debug, verbose, preplay_timeout, isar_shrink, 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49921
diff
changeset

904 
pool, fact_names, sym_tab, atp_proof, goal) 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

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

906 
(preplay, proof_banner mode name, used_facts, 
45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

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

908 
subgoal, subgoal_count) 
48799  909 
val num_chained = length (#facts (Proof.goal state)) 
910 
in 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

911 
proof_text ctxt isar_proofs isar_params num_chained 
48799  912 
one_line_params 
913 
end, 

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

914 
(if verbose then 
45381  915 
"\nATP real CPU time: " ^ string_from_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

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

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

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

919 
"\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

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

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

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

924 
 SOME failure => 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

925 
([], K (Failed_to_Play plain_metis), 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

926 
fn _ => string_for_failure failure, "") 
38023  927 
in 
45381  928 
{outcome = outcome, used_facts = used_facts, run_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

929 
preplay = preplay, message = message, message_tail = message_tail} 
38023  930 
end 
931 

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

934 
ourselves. *) 

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

935 
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

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

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

938 
val z3_failures = 
41236  939 
[(101, OutOfResources), 
940 
(103, MalformedInput), 

41222  941 
(110, MalformedInput)] 
40684
c7ba327eb58c
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents:
40669
diff
changeset

942 
val unix_failures = 
48797  943 
[(138, Crashed), 
944 
(139, Crashed)] 

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

945 
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures 
40555  946 

42100
062381c5f9f8
more precise failure reporting in Sledgehammer/SMT
blanchet
parents:
42061
diff
changeset

947 
fun failure_from_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

948 
if is_real_cex then Unprovable else GaveUp 
41222  949 
 failure_from_smt_failure SMT_Failure.Time_Out = TimedOut 
950 
 failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = 

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

952 
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

953 
 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

954 
string_of_int code ^ ".")) 
41222  955 
 failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources 
956 
 failure_from_smt_failure (SMT_Failure.Other_Failure msg) = 

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

957 
UnknownError msg 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

958 

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

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

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

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

963 
Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

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

965 
Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

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

967 
Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5) 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

968 

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

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

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

972 
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

973 
let 
45706  974 
val max_slices = if slice then Config.get ctxt smt_max_slices else 1 
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

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

976 
select_smt_solver name 
45557  977 
#> Config.put SMT_Config.verbose debug 
43233
2749c357f865
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents:
43232
diff
changeset

978 
#> (if overlord then 
2749c357f865
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents:
43232
diff
changeset

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

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

981 
> (fn (path, name) => path ^ "/" ^ name)) 
2749c357f865
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents:
43232
diff
changeset

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

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

984 
#> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) 
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

985 
val state = state > Proof.map_context repair_context 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

986 
fun do_slice timeout slice outcome0 time_so_far facts = 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

987 
let 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

988 
val timer = Timer.startRealTimer () 
42724
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42723
diff
changeset

989 
val state = 
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42723
diff
changeset

990 
state > Proof.map_context 
43267  991 
(repair_monomorph_context max_mono_iters 
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

992 
default_max_mono_iters max_new_mono_instances 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47946
diff
changeset

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

994 
val slice_timeout = 
50557  995 
if slice < max_slices andalso timeout <> NONE then 
996 
let val ms = timeout > the > Time.toMilliseconds in 

997 
Int.min (ms, 

998 
Int.max (1000 * Config.get ctxt smt_slice_min_secs, 

999 
Real.ceil (Config.get ctxt smt_slice_time_frac 

1000 
* Real.fromInt ms))) 

1001 
> Time.fromMilliseconds > SOME 

1002 
end 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1003 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1004 
timeout 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1005 
val num_facts = length facts 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1006 
val _ = 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1007 
if debug then 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1008 
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ 
50557  1009 
string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ 
1010 
(case slice_timeout of 

1011 
SOME timeout => " for " ^ string_from_time timeout 

1012 
 NONE => "") ^ "..." 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1013 
> Output.urgent_message 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1014 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1015 
() 
41168  1016 
val birth = Timer.checkRealTimer timer 
41171  1017 
val _ = 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41209
diff
changeset

1018 
if debug then Output.urgent_message "Invoking SMT solver..." else () 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
50020
diff
changeset

1019 
val state_facts = these (try (#facts o Proof.goal) state) 
41209  1020 
val (outcome, used_facts) = 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
50020
diff
changeset

1021 
SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i 
50557  1022 
> SMT_Solver.smt_filter_apply (slice_timeout > the_default one_day) 
41239  1023 
> (fn {outcome, used_facts} => (outcome, used_facts)) 
41209  1024 
handle exn => if Exn.is_interrupt exn then 
1025 
reraise exn 

1026 
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

1027 
(ML_Compiler.exn_message exn 
41209  1028 
> SMT_Failure.Other_Failure > SOME, []) 
41168  1029 
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

1030 
val outcome0 = if is_none outcome0 then SOME outcome else outcome0 
41168  1031 
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

1032 
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

1033 
case outcome of 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1034 
NONE => false 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1035 
 SOME (SMT_Failure.Counterexample _) => false 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

1036 
 SOME SMT_Failure.Time_Out => slice_timeout <> timeout 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1037 
 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

1038 
 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

1039 
 SOME (SMT_Failure.Other_Failure _) => true 
50557  1040 
val timeout = 
1041 
Option.map 

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

1043 
timeout 

40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

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

1045 
if too_many_facts_perhaps andalso slice < max_slices andalso 
50557  1046 
num_facts > 0 andalso 
1047 
(timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then 

41169  1048 
let 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

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

1050 
Real.ceil (Config.get ctxt smt_slice_fact_frac 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1051 
* Real.fromInt num_facts) 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1052 
val _ = 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1053 
if verbose andalso is_some outcome then 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1054 
quote name ^ " invoked with " ^ string_of_int num_facts ^ 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1055 
" fact" ^ plural_s num_facts ^ ": " ^ 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1056 
string_for_failure (failure_from_smt_failure (the outcome)) ^ 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1057 
" Retrying with " ^ string_of_int new_num_facts ^ " fact" ^ 
42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42623
diff
changeset

1058 
plural_s new_num_facts ^ "..." 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1059 
> Output.urgent_message 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1060 
else 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

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

1062 
in 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1063 
facts > take new_num_facts 
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

1064 
> do_slice timeout (slice + 1) outcome0 time_so_far 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

1065 
end 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1066 
else 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1067 
{outcome = if is_none outcome then NONE else the outcome0, 
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset

1068 
used_facts = used_facts, run_time = time_so_far} 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

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

1070 
in do_slice timeout 1 NONE Time.zeroTime end 
40409
3642dc3b72e8
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents:
40370
diff
changeset

1071 

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

1072 
fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) 
43011
5f8d74d3b297
added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents:
43006
diff
changeset

1073 
minimize_command 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
50020
diff
changeset

1074 
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = 
36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

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

1076 
val ctxt = Proof.context_of state 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41242
diff
changeset

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

1078 
val facts = facts ~~ (0 upto num_facts  1) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

1079 
> map (smt_weighted_fact ctxt num_facts) 
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

1080 
val {outcome, used_facts = used_pairs, run_time} = 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
50020
diff
changeset

1081 
smt_filter_loop ctxt name params state goal subgoal facts 
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

1082 
val used_facts = used_pairs > map fst 
41222  1083 
val outcome = outcome > Option.map failure_from_smt_failure 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset

1084 
val (preplay, message, message_tail) = 
40184
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset

1085 
case outcome of 
91b4b73dbafb
proper error handling for SMT solvers in Sledgehammer
blanchet
parents:
40181
diff
changeset

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

1087 
(fn () => 
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

1088 
play_one_line_proof mode debug verbose preplay_timeout used_pairs 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45553
diff
changeset

1089 
state subgoal SMT 
45560
1606122a2d0f
don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
blanchet
parents:
45557
diff
changeset

1090 
(bunch_of_reconstructors false 
48800  1091 
(fn desperate => 
1092 
if desperate then liftingN 

1093 
else metis_default_lam_trans)), 

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

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

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

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

1097 
(preplay, proof_banner mode name, used_facts, 
45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

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

1099 
subgoal, subgoal_count) 
48799  1100 
val num_chained = length (#facts (Proof.goal state)) 
1101 
in one_line_proof_text num_chained one_line_params end, 

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

1102 
if verbose then 
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset

1103 
"\nSMT solver real CPU time: " ^ string_from_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

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

1105 
"") 
43166  1106 
 SOME failure => 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

1107 
(K (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "") 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

1108 
in 