author  blanchet 
Mon, 09 Aug 2010 14:08:30 +0200  
changeset 38290  581a402a80f0 
parent 38282  319c59682c51 
child 38455  131f7c46cf2c 
permissions  rwrr 
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer.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 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

6 
Sledgehammer's heart. 
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 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

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

10 
sig 
38023  11 
type failure = ATP_Systems.failure 
35969  12 
type relevance_override = Sledgehammer_Fact_Filter.relevance_override 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

13 
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command 
35969  14 
type params = 
15 
{debug: bool, 

16 
verbose: bool, 

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:
36064
diff
changeset

17 
overlord: bool, 
35969  18 
atps: string list, 
19 
full_types: bool, 

36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

20 
explicit_apply: bool, 
35969  21 
relevance_threshold: real, 
36922  22 
relevance_convergence: real, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36184
diff
changeset

23 
theory_relevant: bool option, 
36922  24 
defs_relevant: bool, 
35969  25 
isar_proof: bool, 
36924  26 
isar_shrink_factor: int, 
35969  27 
timeout: Time.time, 
28 
minimize_timeout: Time.time} 

35867  29 
type problem = 
35969  30 
{subgoal: int, 
31 
goal: Proof.context * (thm list * thm), 

32 
relevance_override: relevance_override, 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

33 
axioms: (string * thm) list option} 
35867  34 
type prover_result = 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

35 
{outcome: failure option, 
35969  36 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

37 
pool: string Symtab.table, 
38015  38 
used_thm_names: string list, 
35969  39 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

40 
output: string, 
35969  41 
proof: string, 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

42 
axiom_names: string Vector.vector, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

43 
conjecture_shape: int list list} 
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

44 
type prover = params > minimize_command > problem > prover_result 
35867  45 

38023  46 
val dest_dir : string Config.T 
47 
val problem_prefix : string Config.T 

48 
val measure_runtime : bool Config.T 

35969  49 
val kill_atps: unit > unit 
50 
val running_atps: unit > unit 

29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28835
diff
changeset

51 
val messages: int option > unit 
38023  52 
val get_prover_fun : theory > string > prover 
38044  53 
val run_sledgehammer : 
54 
params > int > relevance_override > (string > minimize_command) 

55 
> Proof.state > unit 

38023  56 
val setup : theory > theory 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

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

58 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

59 
structure Sledgehammer : SLEDGEHAMMER = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

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

61 

38028  62 
open ATP_Problem 
63 
open ATP_Systems 

37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

64 
open Metis_Clauses 
38023  65 
open Sledgehammer_Util 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36059
diff
changeset

66 
open Sledgehammer_Fact_Filter 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

67 
open Sledgehammer_Translate 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36059
diff
changeset

68 
open Sledgehammer_Proof_Reconstruct 
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

69 

38023  70 

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

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

72 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

73 
(* Identifier to distinguish Sledgehammer from other tools using 
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

74 
"Async_Manager". *) 
37585  75 
val das_Tool = "Sledgehammer" 
76 

77 
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" 

78 
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" 

79 
val messages = Async_Manager.thread_messages das_Tool "ATP" 

35969  80 

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

81 
(** problems, results, provers, etc. **) 
35969  82 

83 
type params = 

84 
{debug: bool, 

85 
verbose: bool, 

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:
36064
diff
changeset

86 
overlord: bool, 
35969  87 
atps: string list, 
88 
full_types: bool, 

36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

89 
explicit_apply: bool, 
35969  90 
relevance_threshold: real, 
36922  91 
relevance_convergence: real, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36184
diff
changeset

92 
theory_relevant: bool option, 
36922  93 
defs_relevant: bool, 
35969  94 
isar_proof: bool, 
36924  95 
isar_shrink_factor: int, 
35969  96 
timeout: Time.time, 
97 
minimize_timeout: Time.time} 

35867  98 

99 
type problem = 

35969  100 
{subgoal: int, 
101 
goal: Proof.context * (thm list * thm), 

102 
relevance_override: relevance_override, 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

103 
axioms: (string * thm) list option} 
35867  104 

105 
type prover_result = 

36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

106 
{outcome: failure option, 
35969  107 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

108 
pool: string Symtab.table, 
38015  109 
used_thm_names: string list, 
35969  110 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

111 
output: string, 
35969  112 
proof: string, 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

113 
axiom_names: string Vector.vector, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

114 
conjecture_shape: int list list} 
35867  115 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

116 
type prover = params > minimize_command > problem > prover_result 
35867  117 

38023  118 
(* configuration attributes *) 
119 

120 
val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); 

121 
(*Empty string means create files in Isabelle's temporary files directory.*) 

122 

123 
val (problem_prefix, problem_prefix_setup) = 

124 
Attrib.config_string "atp_problem_prefix" (K "prob"); 

125 

126 
val (measure_runtime, measure_runtime_setup) = 

127 
Attrib.config_bool "atp_measure_runtime" (K false); 

28484  128 

38023  129 
fun with_path cleanup after f path = 
130 
Exn.capture f path 

131 
> tap (fn _ => cleanup path) 

132 
> Exn.release 

133 
> tap (after path) 

134 

135 
(* Splits by the first possible of a list of delimiters. *) 

136 
fun extract_proof delims output = 

137 
case pairself (find_first (fn s => String.isSubstring s output)) 

138 
(ListPair.unzip delims) of 

139 
(SOME begin_delim, SOME end_delim) => 

140 
(output > first_field begin_delim > the > snd 

141 
> first_field end_delim > the > fst 

142 
> first_field "\n" > the > snd 

143 
handle Option.Option => "") 

144 
 _ => "" 

28484  145 

38023  146 
fun extract_proof_and_outcome complete res_code proof_delims known_failures 
147 
output = 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

148 
case known_failure_in_output output known_failures of 
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

149 
NONE => (case extract_proof proof_delims output of 
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

150 
"" => ("", SOME MalformedOutput) 
38023  151 
 proof => if res_code = 0 then (proof, NONE) 
152 
else ("", SOME UnknownError)) 

38061
685d1f0f75b3
handle Perl and "libwwwperl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents:
38044
diff
changeset

153 
 SOME failure => 
38023  154 
("", SOME (if failure = IncompleteUnprovable andalso complete then 
155 
Unprovable 

156 
else 

157 
failure)) 

28582  158 

38023  159 
fun extract_clause_sequence output = 
160 
let 

161 
val tokens_of = String.tokens (not o Char.isAlphaNum) 

162 
fun extract_num ("clause" :: (ss as _ :: _)) = 

163 
Int.fromString (List.last ss) 

164 
 extract_num _ = NONE 

165 
in output > split_lines > map_filter (extract_num o tokens_of) end 

166 

167 
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" 

168 

169 
val parse_clause_formula_pair = 

38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38102
diff
changeset

170 
$$ "("  scan_integer  $$ ","  Symbol.scan_id 
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38102
diff
changeset

171 
 Scan.repeat ($$ ","  Symbol.scan_id)  $$ ")" 
38023  172 
 Scan.option ($$ ",") 
173 
val parse_clause_formula_relation = 

174 
Scan.this_string set_ClauseFormulaRelationN  $$ "(" 

175 
 Scan.repeat parse_clause_formula_pair 

176 
val extract_clause_formula_relation = 

177 
Substring.full 

178 
#> Substring.position set_ClauseFormulaRelationN 

179 
#> snd #> Substring.string #> strip_spaces #> explode 

180 
#> parse_clause_formula_relation #> fst 

181 

182 
fun repair_conjecture_shape_and_theorem_names output conjecture_shape 

183 
thm_names = 

184 
if String.isSubstring set_ClauseFormulaRelationN output then 

185 
(* This is a hack required for keeping track of axioms after they have been 

186 
clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part 

187 
of this hack. *) 

188 
let 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

189 
val j0 = hd (hd conjecture_shape) 
38023  190 
val seq = extract_clause_sequence output 
191 
val name_map = extract_clause_formula_relation output 

192 
fun renumber_conjecture j = 

193 
AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j  j0)) 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

194 
> map (fn s => find_index (curry (op =) s) seq + 1) 
38023  195 
in 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

196 
(conjecture_shape > map (maps renumber_conjecture), 
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38102
diff
changeset

197 
seq > map (fn j => case j > AList.lookup (op =) name_map > the 
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38102
diff
changeset

198 
> try (unprefix axiom_prefix) of 
38023  199 
SOME s' => undo_ascii_of s' 
200 
 NONE => "") 

201 
> Vector.fromList) 

202 
end 

203 
else 

204 
(conjecture_shape, thm_names) 

205 

206 

207 
(* generic TPTPbased provers *) 

208 

209 
fun prover_fun name 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

210 
{exec, required_execs, arguments, proof_delims, known_failures, 
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

211 
max_new_relevant_facts_per_iter, prefers_theory_relevant, 
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

212 
explicit_forall} 
38023  213 
({debug, overlord, full_types, explicit_apply, relevance_threshold, 
214 
relevance_convergence, theory_relevant, defs_relevant, isar_proof, 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

215 
isar_shrink_factor, timeout, ...} : params) 
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

216 
minimize_command 
38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

217 
({subgoal, goal, relevance_override, axioms} : problem) = 
38023  218 
let 
219 
val (ctxt, (_, th)) = goal; 

220 
val thy = ProofContext.theory_of ctxt 

221 
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

222 
val the_axioms = 
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

223 
case axioms of 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

224 
SOME axioms => axioms 
38023  225 
 NONE => relevant_facts full_types relevance_threshold 
226 
relevance_convergence defs_relevant 

227 
max_new_relevant_facts_per_iter 

228 
(the_default prefers_theory_relevant theory_relevant) 

229 
relevance_override goal hyp_ts concl_t 

230 

231 
(* path to unique problem file *) 

232 
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" 

233 
else Config.get ctxt dest_dir; 

234 
val the_problem_prefix = Config.get ctxt problem_prefix; 

235 
fun prob_pathname nr = 

236 
let 

237 
val probfile = 

238 
Path.basic ((if overlord then "prob_" ^ name 

239 
else the_problem_prefix ^ serial_string ()) 

240 
^ "_" ^ string_of_int nr) 

241 
in 

242 
if the_dest_dir = "" then File.tmp_path probfile 

243 
else if File.exists (Path.explode the_dest_dir) 

244 
then Path.append (Path.explode the_dest_dir) probfile 

245 
else error ("No such directory: " ^ the_dest_dir ^ ".") 

246 
end; 

247 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

248 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
38023  249 
(* write out problem file and call prover *) 
250 
fun command_line complete probfile = 

251 
let 

252 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

253 
" " ^ File.shell_path probfile 

254 
in 

255 
(if Config.get ctxt measure_runtime then 

256 
"TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" 

257 
else 

258 
"exec " ^ core) ^ " 2>&1" 

259 
end 

260 
fun split_time s = 

261 
let 

262 
val split = String.tokens (fn c => str c = "\n"); 

263 
val (output, t) = s > split > split_last > apfst cat_lines; 

264 
fun as_num f = f >> (fst o read_int); 

265 
val num = as_num (Scan.many1 Symbol.is_ascii_digit); 

266 
val digit = Scan.one Symbol.is_ascii_digit; 

267 
val num3 = as_num (digit ::: digit ::: (digit >> single)); 

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

269 
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; 

270 
in (output, as_time t) end; 

271 
fun run_on probfile = 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

272 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  273 
(home_var, _) :: _ => 
38023  274 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  275 
 [] => 
276 
if File.exists command then 

277 
let 

278 
fun do_run complete = 

279 
let 

280 
val command = command_line complete probfile 

281 
val ((output, msecs), res_code) = 

282 
bash_output command 

283 
>> (if overlord then 

284 
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") 

285 
else 

286 
I) 

287 
>> (if Config.get ctxt measure_runtime then split_time 

288 
else rpair 0) 

289 
val (proof, outcome) = 

290 
extract_proof_and_outcome complete res_code proof_delims 

291 
known_failures output 

292 
in (output, msecs, proof, outcome) end 

293 
val readable_names = debug andalso overlord 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

294 
val (problem, pool, conjecture_offset, axiom_names) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

295 
prepare_problem ctxt readable_names explicit_forall full_types 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

296 
explicit_apply hyp_ts concl_t the_axioms 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

297 
val _ = File.write_list probfile (strings_for_tptp_problem problem) 
38032  298 
val conjecture_shape = 
299 
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

300 
> map single 
38032  301 
val result = 
302 
do_run false 

303 
> (fn (_, msecs0, _, SOME _) => 

304 
do_run true 

305 
> (fn (output, msecs, proof, outcome) => 

306 
(output, msecs0 + msecs, proof, outcome)) 

307 
 result => result) 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

308 
in ((pool, conjecture_shape, axiom_names), result) end 
38032  309 
else 
310 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  311 

312 
(* If the problem file has not been exported, remove it; otherwise, export 

313 
the proof file too. *) 

314 
fun cleanup probfile = 

315 
if the_dest_dir = "" then try File.rm probfile else NONE 

316 
fun export probfile (_, (output, _, _, _)) = 

317 
if the_dest_dir = "" then 

318 
() 

319 
else 

320 
File.write (Path.explode (Path.implode probfile ^ "_proof")) output 

321 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

322 
val ((pool, conjecture_shape, axiom_names), 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

323 
(output, msecs, proof, outcome)) = 
38023  324 
with_path cleanup export run_on (prob_pathname subgoal) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

325 
val (conjecture_shape, axiom_names) = 
38023  326 
repair_conjecture_shape_and_theorem_names output conjecture_shape 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

327 
axiom_names 
38023  328 

329 
val (message, used_thm_names) = 

330 
case outcome of 

331 
NONE => 

332 
proof_text isar_proof 

333 
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

334 
(full_types, minimize_command, proof, axiom_names, th, subgoal) 
38023  335 
 SOME failure => (string_for_failure failure ^ "\n", []) 
336 
in 

337 
{outcome = outcome, message = message, pool = pool, 

338 
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

339 
output = output, proof = proof, axiom_names = axiom_names, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

340 
conjecture_shape = conjecture_shape} 
38023  341 
end 
342 

343 
fun get_prover_fun thy name = prover_fun name (get_prover thy name) 

344 

37584  345 
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n 
346 
relevance_override minimize_command proof_state name = 

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

347 
let 
38023  348 
val thy = Proof.theory_of proof_state 
37584  349 
val birth_time = Time.now () 
350 
val death_time = Time.+ (birth_time, timeout) 

38023  351 
val prover = get_prover_fun thy name 
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

352 
val {context = ctxt, facts, goal} = Proof.goal proof_state; 
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

353 
val desc = 
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

354 
"ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ 
36392  355 
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); 
37584  356 
in 
37585  357 
Async_Manager.launch das_Tool verbose birth_time death_time desc 
37584  358 
(fn () => 
359 
let 

360 
val problem = 

361 
{subgoal = i, goal = (ctxt, (facts, goal)), 

38084
e2aac207d13b
"axiom_clauses" > "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset

362 
relevance_override = relevance_override, axioms = NONE} 
37584  363 
in 
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

364 
prover params (minimize_command name) problem > #message 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37926
diff
changeset

365 
handle ERROR message => "Error: " ^ message ^ "\n" 
38290
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38282
diff
changeset

366 
 exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^ 
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38282
diff
changeset

367 
"\n" 
37584  368 
end) 
369 
end 

28582  370 

38044  371 
fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set." 
372 
 run_sledgehammer (params as {atps, ...}) i relevance_override 

373 
minimize_command state = 

374 
case subgoal_count state of 

375 
0 => priority "No subgoal!" 

376 
 n => 

377 
let 

378 
val _ = kill_atps () 

379 
val _ = priority "Sledgehammering..." 

380 
val _ = app (start_prover_thread params i n relevance_override 

381 
minimize_command state) atps 

382 
in () end 

383 

38023  384 
val setup = 
385 
dest_dir_setup 

386 
#> problem_prefix_setup 

387 
#> measure_runtime_setup 

388 

28582  389 
end; 