author  blanchet 
Thu, 26 Jul 2012 11:07:27 +0200  
changeset 48533  5ada9fd7507b 
parent 48433  9e9b6e363859 
child 49365  8aebe857aaaa 
permissions  rwrr 
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36373
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

3 

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

4 
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

5 
*) 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

6 

35963  7 
signature SLEDGEHAMMER_ISAR = 
8 
sig 

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

9 
type params = Sledgehammer_Provers.params 
35963  10 

39318  11 
val auto : bool Unsynchronized.ref 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

12 
val provers : string Unsynchronized.ref 
39318  13 
val timeout : int Unsynchronized.ref 
40069  14 
val default_params : Proof.context > (string * string) list > params 
39318  15 
val setup : theory > theory 
35963  16 
end; 
17 

35971  18 
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

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

20 

44784  21 
open ATP_Util 
38028  22 
open ATP_Systems 
46320  23 
open ATP_Problem_Generate 
24 
open ATP_Proof_Reconstruct 

35971  25 
open Sledgehammer_Util 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
47962
diff
changeset

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

27 
open Sledgehammer_Provers 
38988  28 
open Sledgehammer_Minimize 
48381  29 
open Sledgehammer_MaSh 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40941
diff
changeset

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

31 

48433  32 
(* val cvc3N = "cvc3" *) 
48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48400
diff
changeset

33 
val yicesN = "yices" 
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48400
diff
changeset

34 
val z3N = "z3" 
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48400
diff
changeset

35 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

36 
val runN = "run" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

37 
val minN = "min" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

38 
val messagesN = "messages" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

39 
val supported_proversN = "supported_provers" 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

40 
val kill_proversN = "kill_provers" 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

41 
val running_proversN = "running_provers" 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

42 
val kill_learnersN = "kill_learners" 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

43 
val running_learnersN = "running_learners" 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

44 
val refresh_tptpN = "refresh_tptp" 
48301  45 

39318  46 
val auto = Unsynchronized.ref false 
47 

48 
val _ = 

49 
ProofGeneralPgip.add_preference Preferences.category_tracing 

50 
(Preferences.bool_pref auto "autosledgehammer" 

39327  51 
"Run Sledgehammer automatically.") 
39318  52 

36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

53 
(** Sledgehammer commands **) 
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

54 

48292  55 
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} 
56 
fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} 

57 
fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} 

58 
fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

59 
{add = #add r1 @ #add r2, del = #del r1 @ #del r2, 
36183
f723348b2231
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
blanchet
parents:
36143
diff
changeset

60 
only = #only r1 andalso #only r2} 
48292  61 
fun merge_fact_overrides rs = 
62 
fold merge_fact_override_pairwise rs (only_fact_override []) 

35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

63 

36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

64 
(*** parameters ***) 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

65 

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

66 
val provers = Unsynchronized.ref "" 
39335
87a9ff4d5817
use 30 s instead of 60 s as the default Sledgehammer timeout;
blanchet
parents:
39327
diff
changeset

67 
val timeout = Unsynchronized.ref 30 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

68 

8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

69 
val _ = 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

70 
ProofGeneralPgip.add_preference Preferences.category_proof 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

71 
(Preferences.string_pref provers 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

72 
"Sledgehammer: Provers" 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

73 
"Default automatic provers (separated by whitespace)") 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

74 

8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

75 
val _ = 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

76 
ProofGeneralPgip.add_preference Preferences.category_proof 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

77 
(Preferences.int_pref timeout 
36373
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset

78 
"Sledgehammer: Time Limit" 
36371
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

79 
"ATPs will be interrupted after this time (in seconds)") 
8c83ea1a7740
move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents:
36290
diff
changeset

80 

35963  81 
type raw_param = string * string list 
82 

83 
val default_default_params = 

41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

84 
[("debug", "false"), 
35963  85 
("verbose", "false"), 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

86 
("overlord", "false"), 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

87 
("blocking", "false"), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

88 
("type_enc", "smart"), 
46301  89 
("strict", "false"), 
45514  90 
("lam_trans", "smart"), 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

91 
("uncurried_aliases", "smart"), 
48321  92 
("learn", "true"), 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

93 
("fact_filter", "smart"), 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

94 
("max_facts", "smart"), 
48293  95 
("fact_thresholds", "0.45 0.85"), 
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

96 
("max_mono_iters", "smart"), 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

97 
("max_new_mono_instances", "smart"), 
35963  98 
("isar_proof", "false"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

99 
("isar_shrink_factor", "1"), 
45706  100 
("slice", "true"), 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

101 
("minimize", "smart"), 
46297
0a4907baf9db
lower timeout for preplay, now that we have more preplay methods
blanchet
parents:
45707
diff
changeset

102 
("preplay_timeout", "3")] 
35963  103 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

104 
val alias_params = 
48293  105 
[("prover", ("provers", [])), (* legacy *) 
106 
("max_relevant", ("max_facts", [])), (* legacy *) 

47037  107 
("dont_preplay", ("preplay_timeout", ["0"]))] 
36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

108 
val negated_alias_params = 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

109 
[("no_debug", "debug"), 
35963  110 
("quiet", "verbose"), 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

111 
("no_overlord", "overlord"), 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

112 
("non_blocking", "blocking"), 
46301  113 
("non_strict", "strict"), 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

114 
("no_uncurried_aliases", "uncurried_aliases"), 
48321  115 
("dont_learn", "learn"), 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

116 
("no_isar_proof", "isar_proof"), 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

117 
("dont_slice", "slice"), 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

118 
("dont_minimize", "minimize")] 
35963  119 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

120 
val params_for_minimize = 
46301  121 
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans", 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

122 
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances", 
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

123 
"isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"] 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

124 

43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43353
diff
changeset

125 
val property_dependent_params = ["provers", "timeout"] 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

126 

35963  127 
fun is_known_raw_param s = 
128 
AList.defined (op =) default_default_params s orelse 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

129 
AList.defined (op =) alias_params s orelse 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

130 
AList.defined (op =) negated_alias_params s orelse 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

131 
member (op =) property_dependent_params s orelse s = "expect" 
35963  132 

41258
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

133 
fun is_prover_list ctxt s = 
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

134 
case space_explode " " s of 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

135 
ss as _ :: _ => forall (is_prover_supported ctxt) ss 
41258
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

136 
 _ => false 
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

137 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

138 
fun unalias_raw_param (name, value) = 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

139 
case AList.lookup (op =) alias_params name of 
47037  140 
SOME (name', []) => (name', value) 
141 
 SOME (param' as (name', _)) => 

142 
if value <> ["false"] then 

143 
param' 

144 
else 

145 
error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \ 

146 
\(cf. " ^ quote name' ^ ").") 

36140
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

147 
 NONE => 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

148 
case AList.lookup (op =) negated_alias_params name of 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

149 
SOME name' => (name', case value of 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

150 
["false"] => ["true"] 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

151 
 ["true"] => ["false"] 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

152 
 [] => ["false"] 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

153 
 _ => value) 
08b2a7ecb6c3
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
blanchet
parents:
36064
diff
changeset

154 
 NONE => (name, value) 
35963  155 

46301  156 
val any_type_enc = type_enc_from_string Strict "erased" 
45514  157 

48397  158 
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" 
159 
can be omitted. For the last four, this is a secret feature. *) 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

160 
fun normalize_raw_param ctxt = 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

161 
unalias_raw_param 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

162 
#> (fn (name, value) => 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

163 
if is_known_raw_param name then 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

164 
(name, value) 
48533  165 
else if null value then 
166 
if is_prover_list ctxt name then 

167 
("provers", [name]) 

168 
else if can (type_enc_from_string Strict) name then 

169 
("type_enc", [name]) 

170 
else if can (trans_lams_from_string ctxt any_type_enc) name then 

171 
("lam_trans", [name]) 

172 
else if member (op =) fact_filters name then 

173 
("fact_filter", [name]) 

174 
else if is_some (Int.fromString name) then 

175 
("max_facts", [name]) 

176 
else 

177 
error ("Unknown parameter: " ^ quote name ^ ".") 

48400  178 
else 
179 
error ("Unknown parameter: " ^ quote name ^ ".")) 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

180 

46435  181 
(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are 
44785  182 
read correctly. *) 
44784  183 
val implode_param = strip_spaces_except_between_idents o space_implode " " 
43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

184 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset

185 
structure Data = Theory_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset

186 
( 
35963  187 
type T = raw_param list 
188 
val empty = default_default_params > map (apsnd single) 

189 
val extend = I 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset

190 
fun merge data : T = AList.merge (op =) (K true) data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41258
diff
changeset

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

192 

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

193 
fun remotify_prover_if_supported_and_not_already_remote ctxt name = 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

194 
if String.isPrefix remote_prefix name then 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

195 
SOME name 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

196 
else 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

197 
let val remote_name = remote_prefix ^ name in 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

198 
if is_prover_supported ctxt remote_name then SOME remote_name else NONE 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

199 
end 
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

200 

27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

201 
fun remotify_prover_if_not_installed ctxt name = 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

202 
if is_prover_supported ctxt name andalso is_prover_installed ctxt name then 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40931
diff
changeset

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

204 
else 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

205 
remotify_prover_if_supported_and_not_already_remote ctxt name 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40069
diff
changeset

206 

43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

207 
fun avoid_too_many_threads _ _ [] = [] 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

208 
 avoid_too_many_threads _ (0, 0) _ = [] 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

209 
 avoid_too_many_threads ctxt (0, max_remote) provers = 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

210 
provers 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

211 
> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt) 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

212 
> take max_remote 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

213 
 avoid_too_many_threads _ (max_local, 0) provers = 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

214 
provers 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

215 
> filter_out (String.isPrefix remote_prefix) 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

216 
> take max_local 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

217 
 avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) = 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

218 
let 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

219 
val max_local_and_remote = 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

220 
max_local_and_remote 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

221 
> (if String.isPrefix remote_prefix prover then apsnd else apfst) 
48406  222 
(Integer.add ~1) 
43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

223 
in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

224 

43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

225 
val max_default_remote_threads = 4 
42688
097a61baeca9
smoother handling of ! and ? in type system names
blanchet
parents:
42613
diff
changeset

226 

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

227 
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low 
48405
7682bc885e8a
use CVC3 and Yices by default if they are available and there are enough cores
blanchet
parents:
48400
diff
changeset

228 
timeout, it makes sense to put E first. *) 
40069  229 
fun default_provers_param_value ctxt = 
48432
60759d07df24
took out CVC3 again  there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48406
diff
changeset

230 
[eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN] 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40931
diff
changeset

231 
> map_filter (remotify_prover_if_not_installed ctxt) 
43009
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

232 
> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), 
f58bab6be6a9
reintroduced Waldmeister but limit the number of remote threads created
blanchet
parents:
43008
diff
changeset

233 
max_default_remote_threads) 
42776  234 
> implode_param 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

235 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

236 
fun set_default_raw_param param thy = 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

237 
let val ctxt = Proof_Context.init_global thy in 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

238 
thy > Data.map (AList.update (op =) (normalize_raw_param ctxt param)) 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

239 
end 
40069  240 
fun default_raw_params ctxt = 
42361  241 
let val thy = Proof_Context.theory_of ctxt in 
40069  242 
Data.get thy 
243 
> fold (AList.default (op =)) 

244 
[("provers", [case !provers of 

245 
"" => default_provers_param_value ctxt 

246 
 s => s]), 

247 
("timeout", let val timeout = !timeout in 

248 
[if timeout <= 0 then "none" 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40181
diff
changeset

249 
else string_of_int timeout] 
40069  250 
end)] 
251 
end 

35963  252 

48383  253 
val the_timeout = the_default infinite_timeout 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

254 

43021  255 
fun extract_params mode default_params override_params = 
35963  256 
let 
257 
val raw_params = rev override_params @ rev default_params 

42776  258 
val lookup = Option.map implode_param o AList.lookup (op =) raw_params 
35963  259 
val lookup_string = the_default "" o lookup 
260 
fun general_lookup_bool option default_value name = 

261 
case lookup name of 

35970
3d41a2a490f0
revert debugging output that shouldn't have been submitted in the first place
blanchet
parents:
35966
diff
changeset

262 
SOME s => parse_bool_option option name s 
35963  263 
 NONE => default_value 
264 
val lookup_bool = the o general_lookup_bool false (SOME false) 

265 
fun lookup_time name = 

39318  266 
case lookup name of 
267 
SOME s => parse_time_option name s 

268 
 NONE => NONE 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

269 
fun lookup_int name = 
35963  270 
case lookup name of 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

271 
NONE => 0 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

272 
 SOME s => case Int.fromString s of 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

273 
SOME n => n 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

274 
 NONE => error ("Parameter " ^ quote name ^ 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

275 
" must be assigned an integer value.") 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

276 
fun lookup_real_pair name = 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

277 
case lookup name of 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

278 
NONE => (0.0, 0.0) 
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

279 
 SOME s => case s > space_explode " " > map Real.fromString of 
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

280 
[SOME r1, SOME r2] => (r1, r2) 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

281 
 _ => error ("Parameter " ^ quote name ^ 
40343
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

282 
"must be assigned a pair of floatingpoint \ 
4521d56aef63
use floatingpoint numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet
parents:
40341
diff
changeset

283 
\values (e.g., \"0.6 0.95\")") 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43057
diff
changeset

284 
fun lookup_option lookup' name = 
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38282
diff
changeset

285 
case lookup name of 
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38282
diff
changeset

286 
SOME "smart" => NONE 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43057
diff
changeset

287 
 _ => SOME (lookup' name) 
43021  288 
val debug = mode <> Auto_Try andalso lookup_bool "debug" 
289 
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") 

36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

290 
val overlord = lookup_bool "overlord" 
42995
e23f61546cf0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents:
42944
diff
changeset

291 
val blocking = 
43021  292 
Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse 
42995
e23f61546cf0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
blanchet
parents:
42944
diff
changeset

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

294 
val provers = lookup_string "provers" > space_explode " " 
43021  295 
> mode = Auto_Try ? single o hd 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

296 
val type_enc = 
43021  297 
if mode = Auto_Try then 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43353
diff
changeset

298 
NONE 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43572
diff
changeset

299 
else case lookup_string "type_enc" of 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43353
diff
changeset

300 
"smart" => NONE 
46301  301 
 s => (type_enc_from_string Strict s; SOME s) 
302 
val strict = mode = Auto_Try orelse lookup_bool "strict" 

45520  303 
val lam_trans = lookup_option lookup_string "lam_trans" 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

304 
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" 
48321  305 
val learn = lookup_bool "learn" 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

306 
val fact_filter = lookup_option lookup_string "fact_filter" 
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

307 
val max_facts = lookup_option lookup_int "max_facts" 
48293  308 
val fact_thresholds = lookup_real_pair "fact_thresholds" 
47962
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

309 
val max_mono_iters = lookup_option lookup_int "max_mono_iters" 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

310 
val max_new_mono_instances = 
137883567114
lower the monomorphization thresholds for less scalable provers
blanchet
parents:
47642
diff
changeset

311 
lookup_option lookup_int "max_new_mono_instances" 
35963  312 
val isar_proof = lookup_bool "isar_proof" 
36924  313 
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") 
45706  314 
val slice = mode <> Auto_Try andalso lookup_bool "slice" 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

315 
val minimize = 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

316 
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" 
43021  317 
val timeout = 
318 
(if mode = Auto_Try then NONE else lookup_time "timeout") > the_timeout 

43015
21b6baec55b1
renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents:
43013
diff
changeset

319 
val preplay_timeout = 
43021  320 
if mode = Auto_Try then Time.zeroTime 
43015
21b6baec55b1
renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents:
43013
diff
changeset

321 
else lookup_time "preplay_timeout" > the_timeout 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

322 
val expect = lookup_string "expect" 
35963  323 
in 
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41153
diff
changeset

324 
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, 
46301  325 
provers = provers, type_enc = type_enc, strict = strict, 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46398
diff
changeset

326 
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, 
48321  327 
learn = learn, fact_filter = fact_filter, max_facts = max_facts, 
48314
ee33ba3c0e05
added option to control which fact filter is used
blanchet
parents:
48308
diff
changeset

328 
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, 
48388  329 
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, 
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

330 
isar_shrink_factor = isar_shrink_factor, slice = slice, 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

331 
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, 
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset

332 
expect = expect} 
35963  333 
end 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

334 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

335 
fun get_params mode = extract_params mode o default_raw_params 
43021  336 
fun default_params thy = get_params Normal thy o map (apsnd single) 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
diff
changeset

337 

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

338 
(* Sledgehammer the given subgoal *) 
66af0a49de39
move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents:
36371
diff
changeset

339 

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

340 
val default_minimize_prover = metisN 
43051  341 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

342 
fun is_raw_param_relevant_for_minimize (name, _) = 
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

343 
member (op =) params_for_minimize name 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

344 
fun string_for_raw_param (key, values) = 
42776  345 
key ^ (case implode_param values of "" => ""  value => " = " ^ value) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

346 

45520  347 
fun minimize_command override_params i more_override_params prover_name 
348 
fact_names = 

43057  349 
let 
350 
val params = 

45520  351 
(override_params 
352 
> filter_out (AList.defined (op =) more_override_params o fst)) @ 

353 
more_override_params 

43057  354 
> filter is_raw_param_relevant_for_minimize 
355 
> map string_for_raw_param 

356 
> (if prover_name = default_minimize_prover then I else cons prover_name) 

357 
> space_implode ", " 

358 
in 

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

359 
sledgehammerN ^ " " ^ minN ^ 
43057  360 
(if params = "" then "" else enclose " [" "]" params) ^ 
361 
" (" ^ space_implode " " fact_names ^ ")" ^ 

362 
(if i = 1 then "" else " " ^ string_of_int i) 

363 
end 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

364 

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

365 
val default_learn_atp_timeout = 0.5 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

366 

48292  367 
fun hammer_away override_params subcommand opt_i fact_override state = 
35963  368 
let 
40069  369 
val ctxt = Proof.context_of state 
44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

370 
val override_params = override_params > map (normalize_raw_param ctxt) 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

371 
in 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

372 
if subcommand = runN then 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

373 
let val i = the_default 1 opt_i in 
43021  374 
run_sledgehammer (get_params Normal ctxt override_params) Normal i 
48292  375 
fact_override (minimize_command override_params i) 
39318  376 
state 
377 
> K () 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

378 
end 
43008
bb212c2ad238
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet
parents:
42997
diff
changeset

379 
else if subcommand = minN then 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

380 
let 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

381 
val ctxt = ctxt > Config.put instantiate_inducts false 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

382 
val i = the_default 1 opt_i 
48400  383 
val params = 
48384
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

384 
get_params Minimize ctxt (("provers", [default_minimize_prover]) :: 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

385 
override_params) 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

386 
val goal = prop_of (#goal (Proof.goal state)) 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

387 
val facts = nearly_all_facts ctxt false fact_override Symtab.empty 
83dc102041e6
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents:
48383
diff
changeset

388 
Termtab.empty [] [] goal 
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48397
diff
changeset

389 
fun learn prover = mash_learn_proof ctxt params prover goal facts 
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48397
diff
changeset

390 
in run_minimize params learn i (#add fact_override) state end 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

391 
else if subcommand = messagesN then 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

392 
messages opt_i 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

393 
else if subcommand = supported_proversN then 
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41472
diff
changeset

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

395 
else if subcommand = kill_proversN then 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39335
diff
changeset

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

397 
else if subcommand = running_proversN then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

398 
running_provers () 
48383  399 
else if subcommand = unlearnN then 
400 
mash_unlearn ctxt 

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

401 
else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

402 
subcommand = relearn_isarN orelse subcommand = relearn_atpN then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

403 
(if subcommand = relearn_isarN orelse subcommand = relearn_atpN then 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

404 
mash_unlearn ctxt 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

405 
else 
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

406 
(); 
48383  407 
mash_learn ctxt (get_params Normal ctxt 
48432
60759d07df24
took out CVC3 again  there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48406
diff
changeset

408 
([("timeout", 
60759d07df24
took out CVC3 again  there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48406
diff
changeset

409 
[string_of_real default_learn_atp_timeout]), 
60759d07df24
took out CVC3 again  there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48406
diff
changeset

410 
("slice", ["false"])] @ 
48392
ca998fa08cd9
added "learn_from_atp" command to MaSh, for patient users
blanchet
parents:
48388
diff
changeset

411 
override_params @ 
48432
60759d07df24
took out CVC3 again  there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48406
diff
changeset

412 
[("minimize", ["true"]), 
48395
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

413 
("preplay_timeout", ["0"])])) 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

414 
fact_override (#facts (Proof.goal state)) 
85a7fb65507a
learning should honor the fact override and the chained facts
blanchet
parents:
48392
diff
changeset

415 
(subcommand = learn_atpN orelse subcommand = relearn_atpN)) 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

416 
else if subcommand = kill_learnersN then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

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

418 
else if subcommand = running_learnersN then 
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset

419 
running_learners () 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

420 
else if subcommand = refresh_tptpN then 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

421 
refresh_systems_on_tptp () 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

422 
else 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

423 
error ("Unknown subcommand: " ^ quote subcommand ^ ".") 
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

424 
end 
35963  425 

48292  426 
fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = 
427 
Toplevel.keep (hammer_away params subcommand opt_i fact_override 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35965
diff
changeset

428 
o Toplevel.proof_of) 
35963  429 

42776  430 
fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value 
35963  431 

35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

432 
fun sledgehammer_params_trans params = 
35963  433 
Toplevel.theory 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

434 
(fold set_default_raw_param params 
39318  435 
#> tap (fn thy => 
42361  436 
let val ctxt = Proof_Context.init_global thy in 
40069  437 
writeln ("Default parameters for Sledgehammer:\n" ^ 
438 
(case default_raw_params ctxt > rev of 

439 
[] => "none" 

440 
 params => 

44720
f3a8c19708c8
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
blanchet
parents:
44651
diff
changeset

441 
params > map string_for_raw_param 
41258
73401632a80c
convenient syntax for setting provers  useful for debugging, not for general consumption and hence not documented
blanchet
parents:
41208
diff
changeset

442 
> sort_strings > cat_lines)) 
40069  443 
end)) 
35963  444 

46949  445 
val parse_query_bang = @{keyword "?"}  @{keyword "!"}  @{keyword "!!"} 
42776  446 
val parse_key = 
44768  447 
Scan.repeat1 (Parse.typ_group  parse_query_bang) >> implode_param 
42581
398fff2c6b8f
use ! for mildly unsound and !! for very unsound encodings
blanchet
parents:
42579
diff
changeset

448 
val parse_value = 
44768  449 
Scan.repeat1 (Parse.xname  Parse.float_number  parse_query_bang) 
46949  450 
val parse_param = parse_key  Scan.optional (@{keyword "="}  parse_value) [] 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36924
diff
changeset

451 
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] 
35965
0fce6db7babd
added a syntax for specifying facts to Sledgehammer;
blanchet
parents:
35963
diff
changeset

452 
val parse_fact_refs = 
38996  453 
Scan.repeat1 (Scan.unless (Parse.name  Args.colon) Parse_Spec.xthm) 
48293  454 
val parse_fact_override_chunk = 
48292  455 
(Args.add  Args.colon  parse_fact_refs >> add_fact_override) 
456 
 (Args.del  Args.colon  parse_fact_refs >> del_fact_override) 

457 
 (parse_fact_refs >> only_fact_override) 

458 
val parse_fact_override = 

48293  459 
Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk 
48292  460 
>> merge_fact_overrides)) 
461 
no_fact_override 

35963  462 

463 
val _ = 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

464 
Outer_Syntax.improper_command @{command_spec "sledgehammer"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

465 
"search for firstorder proof using automatic theorem provers" 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

466 
((Scan.optional Parse.short_ident runN  parse_params 
48292  467 
 parse_fact_override  Scan.option Parse.nat) #>> sledgehammer_trans) 
35963  468 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

469 
Outer_Syntax.command @{command_spec "sledgehammer_params"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

470 
"set and display the default parameters for Sledgehammer" 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

471 
(parse_params #>> sledgehammer_params_trans) 
36394
1a48d18449d8
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
blanchet
parents:
36378
diff
changeset

472 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

473 
fun try_sledgehammer auto state = 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

474 
let 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

475 
val ctxt = Proof.context_of state 
43021  476 
val mode = if auto then Auto_Try else Try 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

477 
val i = 1 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

478 
in 
48292  479 
run_sledgehammer (get_params mode ctxt []) mode i no_fact_override 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset

480 
(minimize_command [] i) state 
40931  481 
end 
39318  482 

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

483 
val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer)) 
39318  484 

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

485 
end; 