1 (* Title: HOL/Tools/ATP_Manager/atp_wrapper.ML |
|
2 Author: Fabian Immler, TU Muenchen |
|
3 |
|
4 Wrapper functions for external ATPs. |
|
5 *) |
|
6 |
|
7 signature ATP_WRAPPER = |
|
8 sig |
|
9 type prover = ATP_Manager.prover |
|
10 |
|
11 (* hooks for problem files *) |
|
12 val destdir : string Config.T |
|
13 val problem_prefix : string Config.T |
|
14 val measure_runtime : bool Config.T |
|
15 |
|
16 val refresh_systems_on_tptp : unit -> unit |
|
17 val setup : theory -> theory |
|
18 end; |
|
19 |
|
20 structure ATP_Wrapper : ATP_WRAPPER = |
|
21 struct |
|
22 |
|
23 open Sledgehammer_Util |
|
24 open Sledgehammer_Fact_Preprocessor |
|
25 open Sledgehammer_HOL_Clause |
|
26 open Sledgehammer_Fact_Filter |
|
27 open Sledgehammer_Proof_Reconstruct |
|
28 open ATP_Manager |
|
29 |
|
30 (** generic ATP wrapper **) |
|
31 |
|
32 (* external problem files *) |
|
33 |
|
34 val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K ""); |
|
35 (*Empty string means create files in Isabelle's temporary files directory.*) |
|
36 |
|
37 val (problem_prefix, problem_prefix_setup) = |
|
38 Attrib.config_string "atp_problem_prefix" (K "prob"); |
|
39 |
|
40 val (measure_runtime, measure_runtime_setup) = |
|
41 Attrib.config_bool "atp_measure_runtime" (K false); |
|
42 |
|
43 |
|
44 (* prover configuration *) |
|
45 |
|
46 val remotify = prefix "remote_" |
|
47 |
|
48 type prover_config = |
|
49 {home: string, |
|
50 executable: string, |
|
51 arguments: Time.time -> string, |
|
52 known_failures: (string list * string) list, |
|
53 max_new_clauses: int, |
|
54 prefers_theory_relevant: bool}; |
|
55 |
|
56 |
|
57 (* basic template *) |
|
58 |
|
59 fun with_path cleanup after f path = |
|
60 Exn.capture f path |
|
61 |> tap (fn _ => cleanup path) |
|
62 |> Exn.release |
|
63 |> tap (after path); |
|
64 |
|
65 fun find_known_failure known_failures proof = |
|
66 case map_filter (fn (patterns, message) => |
|
67 if exists (fn pattern => String.isSubstring pattern proof) |
|
68 patterns then |
|
69 SOME message |
|
70 else |
|
71 NONE) known_failures of |
|
72 [] => if is_proof_well_formed proof then "" |
|
73 else "Error: The ATP output is ill-formed." |
|
74 | (message :: _) => message |
|
75 |
|
76 fun generic_prover overlord get_facts prepare write_file home executable args |
|
77 known_failures name |
|
78 ({debug, full_types, explicit_apply, isar_proof, modulus, sorts, ...} |
|
79 : params) minimize_command |
|
80 ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} |
|
81 : problem) = |
|
82 let |
|
83 (* get clauses and prepare them for writing *) |
|
84 val (ctxt, (chain_ths, th)) = goal; |
|
85 val thy = ProofContext.theory_of ctxt; |
|
86 val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; |
|
87 val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal); |
|
88 val the_filtered_clauses = |
|
89 (case filtered_clauses of |
|
90 NONE => get_facts relevance_override goal goal_cls |
|
91 | SOME fcls => fcls); |
|
92 val the_axiom_clauses = |
|
93 (case axiom_clauses of |
|
94 NONE => the_filtered_clauses |
|
95 | SOME axcls => axcls); |
|
96 val (internal_thm_names, clauses) = |
|
97 prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; |
|
98 |
|
99 (* path to unique problem file *) |
|
100 val destdir' = if overlord then getenv "ISABELLE_HOME_USER" |
|
101 else Config.get ctxt destdir; |
|
102 val problem_prefix' = Config.get ctxt problem_prefix; |
|
103 fun prob_pathname nr = |
|
104 let |
|
105 val probfile = |
|
106 Path.basic (problem_prefix' ^ |
|
107 (if overlord then "_" ^ name else serial_string ()) |
|
108 ^ "_" ^ string_of_int nr) |
|
109 in |
|
110 if destdir' = "" then File.tmp_path probfile |
|
111 else if File.exists (Path.explode destdir') |
|
112 then Path.append (Path.explode destdir') probfile |
|
113 else error ("No such directory: " ^ destdir' ^ ".") |
|
114 end; |
|
115 |
|
116 val command = Path.explode (home ^ "/" ^ executable) |
|
117 (* write out problem file and call prover *) |
|
118 fun command_line probfile = |
|
119 (if Config.get ctxt measure_runtime then |
|
120 "TIMEFORMAT='%3U'; { time " ^ |
|
121 space_implode " " [File.shell_path command, args, |
|
122 File.shell_path probfile] ^ " ; } 2>&1" |
|
123 else |
|
124 space_implode " " ["exec", File.shell_path command, args, |
|
125 File.shell_path probfile, "2>&1"]) ^ |
|
126 (if overlord then |
|
127 " | sed 's/,/, /g' \ |
|
128 \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \ |
|
129 \| sed 's/! =/ !=/g' \ |
|
130 \| sed 's/ / /g' | sed 's/| |/||/g' \ |
|
131 \| sed 's/ = = =/===/g' \ |
|
132 \| sed 's/= = /== /g'" |
|
133 else |
|
134 "") |
|
135 fun split_time s = |
|
136 let |
|
137 val split = String.tokens (fn c => str c = "\n"); |
|
138 val (proof, t) = s |> split |> split_last |> apfst cat_lines; |
|
139 fun as_num f = f >> (fst o read_int); |
|
140 val num = as_num (Scan.many1 Symbol.is_ascii_digit); |
|
141 val digit = Scan.one Symbol.is_ascii_digit; |
|
142 val num3 = as_num (digit ::: digit ::: (digit >> single)); |
|
143 val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
|
144 val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; |
|
145 in (proof, as_time t) end; |
|
146 fun split_time' s = |
|
147 if Config.get ctxt measure_runtime then split_time s else (s, 0) |
|
148 fun run_on probfile = |
|
149 if File.exists command then |
|
150 write_file full_types explicit_apply probfile clauses |
|
151 |> pair (apfst split_time' (bash_output (command_line probfile))) |
|
152 else error ("Bad executable: " ^ Path.implode command ^ "."); |
|
153 |
|
154 (* If the problem file has not been exported, remove it; otherwise, export |
|
155 the proof file too. *) |
|
156 fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE; |
|
157 fun export probfile (((proof, _), _), _) = |
|
158 if destdir' = "" then |
|
159 () |
|
160 else |
|
161 File.write (Path.explode (Path.implode probfile ^ "_proof")) |
|
162 ((if overlord then |
|
163 "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^ |
|
164 "\n" |
|
165 else |
|
166 "") ^ proof) |
|
167 |
|
168 val (((proof, atp_run_time_in_msecs), rc), _) = |
|
169 with_path cleanup export run_on (prob_pathname subgoal); |
|
170 |
|
171 (* Check for success and print out some information on failure. *) |
|
172 val failure = find_known_failure known_failures proof; |
|
173 val success = rc = 0 andalso failure = ""; |
|
174 val (message, relevant_thm_names) = |
|
175 if success then |
|
176 proof_text isar_proof debug modulus sorts ctxt |
|
177 (minimize_command, proof, internal_thm_names, th, subgoal) |
|
178 else if failure <> "" then |
|
179 (failure ^ "\n", []) |
|
180 else |
|
181 ("Unknown ATP error: " ^ proof ^ ".\n", []) |
|
182 in |
|
183 {success = success, message = message, |
|
184 relevant_thm_names = relevant_thm_names, |
|
185 atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, |
|
186 internal_thm_names = internal_thm_names, |
|
187 filtered_clauses = the_filtered_clauses} |
|
188 end; |
|
189 |
|
190 |
|
191 (* generic TPTP-based provers *) |
|
192 |
|
193 fun generic_tptp_prover |
|
194 (name, {home, executable, arguments, known_failures, max_new_clauses, |
|
195 prefers_theory_relevant}) |
|
196 (params as {debug, overlord, respect_no_atp, relevance_threshold, |
|
197 convergence, theory_relevant, higher_order, follow_defs, |
|
198 isar_proof, ...}) |
|
199 minimize_command timeout = |
|
200 generic_prover overlord |
|
201 (get_relevant_facts respect_no_atp relevance_threshold convergence |
|
202 higher_order follow_defs max_new_clauses |
|
203 (the_default prefers_theory_relevant theory_relevant)) |
|
204 (prepare_clauses higher_order false) |
|
205 (write_tptp_file (debug andalso overlord andalso not isar_proof)) home |
|
206 executable (arguments timeout) known_failures name params minimize_command |
|
207 |
|
208 fun tptp_prover name p = (name, generic_tptp_prover (name, p)); |
|
209 |
|
210 |
|
211 (** common provers **) |
|
212 |
|
213 fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000 |
|
214 |
|
215 (* Vampire *) |
|
216 |
|
217 (* Vampire requires an explicit time limit. *) |
|
218 |
|
219 val vampire_config : prover_config = |
|
220 {home = getenv "VAMPIRE_HOME", |
|
221 executable = "vampire", |
|
222 arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^ |
|
223 string_of_int (generous_to_secs timeout)), |
|
224 known_failures = |
|
225 [(["Satisfiability detected", "CANNOT PROVE"], |
|
226 "The ATP problem is unprovable."), |
|
227 (["Refutation not found"], |
|
228 "The ATP failed to determine the problem's status.")], |
|
229 max_new_clauses = 60, |
|
230 prefers_theory_relevant = false} |
|
231 val vampire = tptp_prover "vampire" vampire_config |
|
232 |
|
233 |
|
234 (* E prover *) |
|
235 |
|
236 val e_config : prover_config = |
|
237 {home = getenv "E_HOME", |
|
238 executable = "eproof", |
|
239 arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \ |
|
240 \-tAutoDev --silent --cpu-limit=" ^ |
|
241 string_of_int (generous_to_secs timeout)), |
|
242 known_failures = |
|
243 [(["SZS status: Satisfiable", "SZS status Satisfiable"], |
|
244 "The ATP problem is unprovable."), |
|
245 (["SZS status: ResourceOut", "SZS status ResourceOut"], |
|
246 "The ATP ran out of resources."), |
|
247 (["# Cannot determine problem status"], |
|
248 "The ATP failed to determine the problem's status.")], |
|
249 max_new_clauses = 100, |
|
250 prefers_theory_relevant = false} |
|
251 val e = tptp_prover "e" e_config |
|
252 |
|
253 |
|
254 (* SPASS *) |
|
255 |
|
256 fun generic_dfg_prover |
|
257 (name, {home, executable, arguments, known_failures, max_new_clauses, |
|
258 prefers_theory_relevant}) |
|
259 (params as {overlord, respect_no_atp, relevance_threshold, convergence, |
|
260 theory_relevant, higher_order, follow_defs, ...}) |
|
261 minimize_command timeout = |
|
262 generic_prover overlord |
|
263 (get_relevant_facts respect_no_atp relevance_threshold convergence |
|
264 higher_order follow_defs max_new_clauses |
|
265 (the_default prefers_theory_relevant theory_relevant)) |
|
266 (prepare_clauses higher_order true) write_dfg_file home executable |
|
267 (arguments timeout) known_failures name params minimize_command |
|
268 |
|
269 fun dfg_prover name p = (name, generic_dfg_prover (name, p)) |
|
270 |
|
271 (* The "-VarWeight=3" option helps the higher-order problems, probably by |
|
272 counteracting the presence of "hAPP". *) |
|
273 val spass_config : prover_config = |
|
274 {home = getenv "SPASS_HOME", |
|
275 executable = "SPASS", |
|
276 arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ |
|
277 " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^ |
|
278 string_of_int (generous_to_secs timeout)), |
|
279 known_failures = |
|
280 [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."), |
|
281 (["SPASS beiseite: Ran out of time."], "The ATP timed out."), |
|
282 (["SPASS beiseite: Maximal number of loops exceeded."], |
|
283 "The ATP hit its loop limit.")], |
|
284 max_new_clauses = 40, |
|
285 prefers_theory_relevant = true} |
|
286 val spass = dfg_prover "spass" spass_config |
|
287 |
|
288 (* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0 |
|
289 supports only the DFG syntax. As soon as all Isabelle repository/snapshot |
|
290 users have upgraded to 3.7, we can kill "spass" (and all DFG support in |
|
291 Sledgehammer) and rename "spass_tptp" "spass". *) |
|
292 |
|
293 (* FIXME: Change the error message below to point to the Isabelle download |
|
294 page once the package is there (around the Isabelle2010 release). *) |
|
295 |
|
296 val spass_tptp_config = |
|
297 {home = #home spass_config, |
|
298 executable = #executable spass_config, |
|
299 arguments = prefix "-TPTP " o #arguments spass_config, |
|
300 known_failures = |
|
301 #known_failures spass_config @ |
|
302 [(["unrecognized option `-TPTP'", "Unrecognized option TPTP"], |
|
303 "Warning: Sledgehammer requires a more recent version of SPASS with \ |
|
304 \support for the TPTP syntax. To install it, download and untar the \ |
|
305 \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add \ |
|
306 \the \"spass-3.7\" directory's full path to \"" ^ |
|
307 Path.implode (Path.expand (Path.appends |
|
308 (Path.variable "ISABELLE_HOME_USER" :: |
|
309 map Path.basic ["etc", "components"]))) ^ |
|
310 "\" on a line of its own.")], |
|
311 max_new_clauses = #max_new_clauses spass_config, |
|
312 prefers_theory_relevant = #prefers_theory_relevant spass_config} |
|
313 val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config |
|
314 |
|
315 (* remote prover invocation via SystemOnTPTP *) |
|
316 |
|
317 val systems = Synchronized.var "atp_wrapper_systems" ([]: string list); |
|
318 |
|
319 fun get_systems () = |
|
320 let |
|
321 val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" |
|
322 in |
|
323 if rc <> 0 then |
|
324 error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) |
|
325 else |
|
326 split_lines answer |
|
327 end; |
|
328 |
|
329 fun refresh_systems_on_tptp () = |
|
330 Synchronized.change systems (fn _ => get_systems ()); |
|
331 |
|
332 fun get_system prefix = Synchronized.change_result systems (fn systems => |
|
333 (if null systems then get_systems () else systems) |
|
334 |> `(find_first (String.isPrefix prefix))); |
|
335 |
|
336 fun the_system prefix = |
|
337 (case get_system prefix of |
|
338 NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") |
|
339 | SOME sys => sys); |
|
340 |
|
341 val remote_known_failures = |
|
342 [(["Remote-script could not extract proof"], |
|
343 "Error: The remote ATP proof is ill-formed.")] |
|
344 |
|
345 fun remote_prover_config prover_prefix args |
|
346 ({known_failures, max_new_clauses, prefers_theory_relevant, ...} |
|
347 : prover_config) : prover_config = |
|
348 {home = getenv "ISABELLE_ATP_MANAGER", |
|
349 executable = "SystemOnTPTP", |
|
350 arguments = (fn timeout => |
|
351 args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^ |
|
352 the_system prover_prefix), |
|
353 known_failures = remote_known_failures @ known_failures, |
|
354 max_new_clauses = max_new_clauses, |
|
355 prefers_theory_relevant = prefers_theory_relevant} |
|
356 |
|
357 val remote_vampire = |
|
358 tptp_prover (remotify (fst vampire)) |
|
359 (remote_prover_config "Vampire---9" "" vampire_config) |
|
360 |
|
361 val remote_e = |
|
362 tptp_prover (remotify (fst e)) |
|
363 (remote_prover_config "EP---" "" e_config) |
|
364 |
|
365 val remote_spass = |
|
366 tptp_prover (remotify (fst spass)) |
|
367 (remote_prover_config "SPASS---" "-x" spass_config) |
|
368 |
|
369 val provers = |
|
370 [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e] |
|
371 val prover_setup = fold add_prover provers |
|
372 |
|
373 val setup = |
|
374 destdir_setup |
|
375 #> problem_prefix_setup |
|
376 #> measure_runtime_setup |
|
377 #> prover_setup; |
|
378 |
|
379 fun maybe_remote (name, _) ({home, ...} : prover_config) = |
|
380 name |> home = "" ? remotify |
|
381 |
|
382 val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config, |
|
383 remotify (fst vampire)] |> space_implode " ") |
|
384 end; |
|