author  blanchet 
Thu, 18 Oct 2012 15:41:15 +0200  
changeset 49921  073d69478207 
parent 49918  cf441f4a358b 
child 50004  c96e8e40d789 
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, 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

37 
isar_shrinkage : real, 
48321  38 
slice : bool, 
39 
minimize : bool option, 

40 
timeout : Time.time, 

41 
preplay_timeout : Time.time, 

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, 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

330 
isar_shrinkage : real, 
48321  331 
slice : bool, 
332 
minimize : bool option, 

333 
timeout : Time.time, 

334 
preplay_timeout : Time.time, 

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 

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

482 
in TimeLimit.timeLimit 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 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

503 
val _ = 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

504 
if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

505 
Output.urgent_message "Preplaying proof..." 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

506 
else 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

507 
() 
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

508 
val ths = pairs > sort_wrt (fst o fst) > map snd 
45520  509 
fun get_preferred reconstrs = 
510 
if member (op =) reconstrs preferred then preferred 

511 
else List.last reconstrs 

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

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

513 
 play timed_outs [] = 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

514 
Trust_Playable (get_preferred timed_outs, SOME timeout) 
45520  515 
 play timed_out (reconstr :: reconstrs) = 
45378  516 
let 
517 
val _ = 

518 
if verbose then 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45553
diff
changeset

519 
"Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^ 
45378  520 
string_from_time timeout ^ "..." 
521 
> Output.urgent_message 

522 
else 

523 
() 

524 
val timer = Timer.startRealTimer () 

525 
in 

45520  526 
case timed_reconstructor reconstr debug timeout ths state i of 
527 
SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer) 

528 
 _ => play timed_out reconstrs 

43044
5945375700aa
always check plain "metis" even if the ATP proof seems to require "metisFT"  maybe the proof is needlessly complicated
blanchet
parents:
43037
diff
changeset

529 
end 
45520  530 
handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs 
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset

531 
in 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

532 
if timeout = Time.zeroTime then 
45520  533 
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

534 
else 
45520  535 
play [] reconstrs 
43033  536 
end 
537 

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

538 

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

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

540 

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

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

542 
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

543 
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

544 
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

545 

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

547 
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

548 
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

549 
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

550 
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

551 
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

552 
 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

553 
 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

554 
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

555 
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

556 
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

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

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

559 
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

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

561 
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

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

563 
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

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

565 
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

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

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

568 
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

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

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

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

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

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

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

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

576 
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

577 

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

579 
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

580 
 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

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

582 

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

584 
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

585 
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

586 
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

587 
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

588 

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

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

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

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

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

595 
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

596 

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

44649  599 
val atp_important_message_keep_quotient = 25 
39492  600 

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

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

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

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

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

605 

43051  606 
val metis_minimize_max_time = seconds 2.0 
607 

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

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

611 
case preplay of 

612 
Played (reconstr, time) => 

613 
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

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

617 
 _ => (name, []) 

618 
in minimize_command override_params name end 

43051  619 

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

620 
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

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

622 
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

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

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

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

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

627 
fun suffix_for_mode Auto_Try = "_auto_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

628 
 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

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

630 
 suffix_for_mode MaSh = "_mash" 
45574  631 
 suffix_for_mode Auto_Minimize = "_auto_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

632 
 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

633 

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

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

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

637 

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

638 
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

639 

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

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

642 
best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) 
46301  643 
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, 
48293  644 
uncurried_aliases, max_facts, max_mono_iters, 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49914
diff
changeset

645 
max_new_mono_instances, isar_proofs, isar_shrinkage, 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46407
diff
changeset

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

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

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

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

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

655 
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

656 
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

657 
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

658 
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

659 
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

660 
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

661 
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

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

663 
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

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

665 
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

666 
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

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

668 
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

669 
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

670 
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

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

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

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

674 
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

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

676 
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

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

678 
 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

679 
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

680 
 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

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

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

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

686 
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

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

690 
val digit = Scan.one Symbol.is_ascii_digit 

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

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

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

695 
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

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

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

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

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

700 
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

701 
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

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

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

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

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

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

707 
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

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

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

710 
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

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

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

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

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

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

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

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

718 
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

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

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

721 
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

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

723 
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

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

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

726 
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

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

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

730 
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

731 
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

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

733 
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

734 
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

735 
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

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

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

738 
> (if slice < num_actual_slices  1 then 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

739 
curry Real.min (time_frac * real_ms timeout) 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

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

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

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

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

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

747 
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

748 
" with " ^ string_of_int num_facts ^ " fact" ^ 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

750 
string_from_time slice_timeout ^ "..." 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

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

754 
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

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

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

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

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

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

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

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

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

763 
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

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

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

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

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

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

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

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

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

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

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

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

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

776 
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

777 
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

778 
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

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

780 
val full_proof = debug orelse isar_proofs 
48376
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

781 
val args = arguments ctxt full_proof extra slice_timeout 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

783 
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

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

785 
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

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

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

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

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

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

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

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

793 
TimeLimit.timeLimit generous_slice_timeout 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

794 
Isabelle_System.bash_output command 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

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

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

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

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

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

802 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

817 
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

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

819 
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

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

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

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

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

824 
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

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

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

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

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

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

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

831 
if Time.<= (time_left, Time.zeroTime) then 
416e4123baf3
use "eproof_ram" script if available (plugin replacement for "eproof", but faster)
blanchet
parents:
48331
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

844 
end 
38023  845 
(* If the problem file has not been exported, remove it; otherwise, export 
846 
the proof file too. *) 

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

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

848 
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

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

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

851 
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

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

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

854 
with_cleanup clean_up run () > tap export 
39492  855 
val important_message = 
43021  856 
if mode = Normal andalso 
42609  857 
random_range 0 (atp_important_message_keep_quotient  1) = 0 then 
39492  858 
extract_important_message output 
859 
else 

860 
"" 

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

861 
val (used_facts, preplay, message, message_tail) = 
38023  862 
case outcome of 
863 
NONE => 

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

868 
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

869 
(lam_trans_from_atp_proof atp_proof 
46405  870 
o (fn desperate => if desperate then hide_lamsN 
871 
else metis_default_lam_trans)) 

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

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

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

875 
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

876 
val used_pairs = 
48798  877 
facts > map untranslated_fact 
878 
> 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

879 
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

880 
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

881 
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

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

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

884 
let 
49921  885 
val _ = 
886 
if verbose then 

887 
Output.urgent_message "Generating proof text..." 

888 
else 

889 
() 

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

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

891 
(debug, verbose, isar_shrinkage, pool, fact_names, sym_tab, 
45552  892 
atp_proof, goal) 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

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

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

895 
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

896 
subgoal, subgoal_count) 
48799  897 
val num_chained = length (#facts (Proof.goal state)) 
898 
in 

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

899 
proof_text ctxt isar_proofs isar_params num_chained 
48799  900 
one_line_params 
901 
end, 

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

902 
(if verbose then 
45381  903 
"\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

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

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

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

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

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

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

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

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

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

914 
fn _ => string_for_failure failure, "") 
38023  915 
in 
45381  916 
{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

917 
preplay = preplay, message = message, message_tail = message_tail} 
38023  918 
end 
919 

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

922 
ourselves. *) 

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

923 
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

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

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

926 
val z3_failures = 
41236  927 
[(101, OutOfResources), 
928 
(103, MalformedInput), 

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

930 
val unix_failures = 
48797  931 
[(138, Crashed), 
932 
(139, Crashed)] 

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

933 
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures 
40555  934 

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

935 
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

936 
if is_real_cex then Unprovable else GaveUp 
41222  937 
 failure_from_smt_failure SMT_Failure.Time_Out = TimedOut 
938 
 failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = 

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

940 
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

941 
 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

942 
string_of_int code ^ ".")) 
41222  943 
 failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources 
944 
 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

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

946 

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

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

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

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

951 
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

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

953 
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

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

955 
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

956 

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

957 
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

958 
({debug, verbose, overlord, max_mono_iters, 
45706  959 
max_new_mono_instances, timeout, slice, ...} : params) 
47531
7fe7c7419489
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents:
47055
diff
changeset

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

961 
let 
45706  962 
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

963 
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

964 
select_smt_solver name 
45557  965 
#> 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

966 
#> (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

967 
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

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

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

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

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

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

973 
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

974 
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

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

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

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

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

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

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

982 
val ms = timeout > Time.toMilliseconds 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

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

984 
if slice < max_slices then 
41169  985 
Int.min (ms, 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

986 
Int.max (1000 * Config.get ctxt smt_slice_min_secs, 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

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

988 
* Real.fromInt ms))) 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

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

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

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

992 
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

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

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

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

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

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

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

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

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

1003 
if debug then Output.urgent_message "Invoking SMT solver..." else () 
41209  1004 
val (outcome, used_facts) = 
47531
7fe7c7419489
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents:
47055
diff
changeset

1005 
SMT_Solver.smt_filter_preprocess state facts i 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

1006 
> SMT_Solver.smt_filter_apply slice_timeout 
41239  1007 
> (fn {outcome, used_facts} => (outcome, used_facts)) 
41209  1008 
handle exn => if Exn.is_interrupt exn then 
1009 
reraise exn 

1010 
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

1011 
(ML_Compiler.exn_message exn 
41209  1012 
> SMT_Failure.Other_Failure > SOME, []) 
41168  1013 
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

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

1016 
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

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

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

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

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

1021 
 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

1022 
 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

1023 
 SOME (SMT_Failure.Other_Failure _) => true 
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

1024 
val timeout = Time. (timeout, Timer.checkRealTimer timer) 
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40471
diff
changeset

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

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

1027 
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then 
41169  1028 
let 
42614
81953e554197
make "debug" more verbose and "verbose" less verbose
blanchet
parents:
42613
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1048 
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

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

1050 
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

1051 

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

1052 
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

1053 
minimize_command 
47531
7fe7c7419489
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents:
47055
diff
changeset

1054 
({state, 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

1055 
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

1056 
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

1057 
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

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

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

1060 
val {outcome, used_facts = used_pairs, run_time} = 
47531
7fe7c7419489
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents:
47055
diff
changeset

1061 
smt_filter_loop ctxt name params state 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

1062 
val used_facts = used_pairs > map fst 
41222  1063 
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

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

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

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

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

1068 
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

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

1070 
(bunch_of_reconstructors false 
48800  1071 
(fn desperate => 
1072 
if desperate then liftingN 

1073 
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

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

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

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

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

1078 
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

1079 
subgoal, subgoal_count) 
48799  1080 
val num_chained = length (#facts (Proof.goal state)) 
1081 
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

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

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

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

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

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

1088 
in 
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset

1089 
{outcome = outcome, used_facts = used_facts, run_time = run_time, 
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset

1090 
preplay = preplay, message = message, message_tail = message_tail} 
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset

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

1092 

45520  1093 
fun run_reconstructor mode name 
45561
57227eedce81
don't propagate userset "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset

1094 
(params as {debug, verbose, timeout, type_enc, lam_trans, ...}) 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

1095 
minimize_command 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset

1096 
({state, subgoal, subgoal_count, facts, ...} : prover_problem) = 
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset

1097 
let 
45520  1098 
val reconstr = 
1099 
if name = metisN then 

1100 
Metis (type_enc > the_default (hd partial_type_encs), 

1101 
lam_trans > the_default metis_default_lam_trans) 

1102 
else if name = smtN then 

1103 
SMT 

1104 
else 

1105 
raise Fail ("unknown reconstructor: " ^ quote name) 

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 fa 