1 (* Title: HOL/Tools/ATP_Manager/atp_systems.ML
2 Author: Fabian Immler, TU Muenchen
3 Author: Jasmin Blanchette, TU Muenchen
5 Setup for supported ATPs.
8 signature ATP_SYSTEMS =
10 type prover = ATP_Manager.prover
12 (* hooks for problem files *)
13 val dest_dir : string Config.T
14 val problem_prefix : string Config.T
15 val measure_runtime : bool Config.T
17 val refresh_systems_on_tptp : unit -> unit
18 val default_atps_param_value : unit -> string
19 val setup : theory -> theory
22 structure ATP_Systems : ATP_SYSTEMS =
25 open Sledgehammer_Util
26 open Sledgehammer_Fact_Preprocessor
27 open Sledgehammer_HOL_Clause
28 open Sledgehammer_Fact_Filter
29 open Sledgehammer_Proof_Reconstruct
34 (* external problem files *)
36 val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
37 (*Empty string means create files in Isabelle's temporary files directory.*)
39 val (problem_prefix, problem_prefix_setup) =
40 Attrib.config_string "atp_problem_prefix" (K "prob");
42 val (measure_runtime, measure_runtime_setup) =
43 Attrib.config_bool "atp_measure_runtime" (K false);
46 (* prover configuration *)
51 arguments: Time.time -> string,
52 proof_delims: (string * string) list,
53 known_failures: (failure * string) list,
54 max_axiom_clauses: int,
55 prefers_theory_relevant: bool};
60 val remotify = prefix "remote_"
62 fun with_path cleanup after f path =
64 |> tap (fn _ => cleanup path)
68 (* Splits by the first possible of a list of delimiters. *)
69 fun extract_proof delims output =
70 case pairself (find_first (fn s => String.isSubstring s output))
71 (ListPair.unzip delims) of
72 (SOME begin_delim, SOME end_delim) =>
73 (output |> first_field begin_delim |> the |> snd
74 |> first_field end_delim |> the |> fst
75 |> first_field "\n" |> the |> snd
76 handle Option.Option => "")
79 fun extract_proof_and_outcome res_code proof_delims known_failures output =
80 case map_filter (fn (failure, pattern) =>
81 if String.isSubstring pattern output then SOME failure
82 else NONE) known_failures of
83 [] => (case extract_proof proof_delims output of
84 "" => ("", SOME UnknownError)
85 | proof => if res_code = 0 then (proof, NONE)
86 else ("", SOME UnknownError))
87 | (failure :: _) => ("", SOME failure)
89 fun string_for_failure Unprovable = "The ATP problem is unprovable."
90 | string_for_failure IncompleteUnprovable =
91 "The ATP cannot prove the problem."
92 | string_for_failure TimedOut = "Timed out."
93 | string_for_failure OutOfResources = "The ATP ran out of resources."
94 | string_for_failure OldSpass =
95 (* FIXME: Change the error message below to point to the Isabelle download
96 page once the package is there (around the Isabelle2010 release). *)
97 "Warning: Sledgehammer requires a more recent version of SPASS with \
98 \support for the TPTP syntax. To install it, download and untar the \
99 \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
100 \\"spass-3.7\" directory's full path to \"" ^
101 Path.implode (Path.expand (Path.appends
102 (Path.variable "ISABELLE_HOME_USER" ::
103 map Path.basic ["etc", "components"]))) ^
104 "\" on a line of its own."
105 | string_for_failure MalformedInput =
106 "Internal Sledgehammer error: The ATP problem is malformed. Please report \
107 \this to the Isabelle developers."
108 | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
109 | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
111 fun shape_of_clauses _ [] = []
112 | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
113 | shape_of_clauses j ((lit :: lits) :: clauses) =
114 let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
115 (j :: hd shape) :: tl shape
118 fun generic_prover overlord get_facts prepare write_file home_var executable
119 args proof_delims known_failures name
120 ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
121 ...} : params) minimize_command
122 ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
125 (* get clauses and prepare them for writing *)
126 val (ctxt, (chained_ths, th)) = goal;
127 val thy = ProofContext.theory_of ctxt;
128 val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
129 val goal_cls = List.concat goal_clss
130 val the_filtered_clauses =
131 (case filtered_clauses of
132 NONE => get_facts relevance_override goal goal_cls
133 | SOME fcls => fcls);
134 val the_axiom_clauses =
135 (case axiom_clauses of
136 NONE => the_filtered_clauses
137 | SOME axcls => axcls);
138 val (internal_thm_names, clauses) =
139 prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy;
141 (* path to unique problem file *)
142 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
143 else Config.get ctxt dest_dir;
144 val the_problem_prefix = Config.get ctxt problem_prefix;
145 fun prob_pathname nr =
148 Path.basic ((if overlord then "prob_" ^ name
149 else the_problem_prefix ^ serial_string ())
150 ^ "_" ^ string_of_int nr)
152 if the_dest_dir = "" then File.tmp_path probfile
153 else if File.exists (Path.explode the_dest_dir)
154 then Path.append (Path.explode the_dest_dir) probfile
155 else error ("No such directory: " ^ the_dest_dir ^ ".")
158 val home = getenv home_var
159 val command = Path.explode (home ^ "/" ^ executable)
160 (* write out problem file and call prover *)
161 fun command_line probfile =
162 (if Config.get ctxt measure_runtime then
163 "TIMEFORMAT='%3U'; { time " ^
164 space_implode " " [File.shell_path command, args,
165 File.shell_path probfile] ^ " ; } 2>&1"
167 space_implode " " ["exec", File.shell_path command, args,
168 File.shell_path probfile, "2>&1"]) ^
171 \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \
172 \| sed 's/ / /g' | sed 's/| |/||/g' \
173 \| sed 's/ = = =/===/g' \
174 \| sed 's/= = /== /g'"
179 val split = String.tokens (fn c => str c = "\n");
180 val (output, t) = s |> split |> split_last |> apfst cat_lines;
181 fun as_num f = f >> (fst o read_int);
182 val num = as_num (Scan.many1 Symbol.is_ascii_digit);
183 val digit = Scan.one Symbol.is_ascii_digit;
184 val num3 = as_num (digit ::: digit ::: (digit >> single));
185 val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
186 val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
187 in (output, as_time t) end;
189 if Config.get ctxt measure_runtime then split_time s else (s, 0)
190 fun run_on probfile =
191 if File.exists command then
192 write_file full_types explicit_apply probfile clauses
193 |> pair (apfst split_time' (bash_output (command_line probfile)))
194 else if home = "" then
195 error ("The environment variable " ^ quote home_var ^ " is not set.")
197 error ("Bad executable: " ^ Path.implode command ^ ".");
199 (* If the problem file has not been exported, remove it; otherwise, export
200 the proof file too. *)
201 fun cleanup probfile =
202 if the_dest_dir = "" then try File.rm probfile else NONE
203 fun export probfile (((output, _), _), _) =
204 if the_dest_dir = "" then
207 File.write (Path.explode (Path.implode probfile ^ "_proof"))
209 "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^
214 val (((output, atp_run_time_in_msecs), res_code),
215 (pool, conjecture_offset)) =
216 with_path cleanup export run_on (prob_pathname subgoal);
217 val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
218 (* Check for success and print out some information on failure. *)
219 val (proof, outcome) =
220 extract_proof_and_outcome res_code proof_delims known_failures output
221 val (message, relevant_thm_names) =
224 proof_text isar_proof
225 (pool, debug, full_types, isar_shrink_factor, ctxt,
227 (minimize_command, proof, internal_thm_names, th, subgoal)
228 | SOME failure => (string_for_failure failure ^ "\n", [])
230 {outcome = outcome, message = message, pool = pool,
231 relevant_thm_names = relevant_thm_names,
232 atp_run_time_in_msecs = atp_run_time_in_msecs, output = output,
233 proof = proof, internal_thm_names = internal_thm_names,
234 conjecture_shape = conjecture_shape,
235 filtered_clauses = the_filtered_clauses}
239 (* generic TPTP-based provers *)
241 fun generic_tptp_prover
242 (name, {home_var, executable, arguments, proof_delims, known_failures,
243 max_axiom_clauses, prefers_theory_relevant})
244 (params as {debug, overlord, full_types, respect_no_atp,
245 relevance_threshold, relevance_convergence, theory_relevant,
246 defs_relevant, isar_proof, ...})
247 minimize_command timeout =
248 generic_prover overlord
249 (relevant_facts full_types respect_no_atp relevance_threshold
250 relevance_convergence defs_relevant max_axiom_clauses
251 (the_default prefers_theory_relevant theory_relevant))
252 (prepare_clauses false)
253 (write_tptp_file (debug andalso overlord)) home_var
254 executable (arguments timeout) proof_delims known_failures name params
257 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
260 (** common provers **)
262 fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
266 (* Vampire requires an explicit time limit. *)
268 val vampire_config : prover_config =
269 {home_var = "VAMPIRE_HOME",
270 executable = "vampire",
271 arguments = fn timeout =>
272 "--output_syntax tptp --mode casc -t " ^
273 string_of_int (to_generous_secs timeout),
275 [("=========== Refutation ==========",
276 "======= End of refutation ======="),
277 ("% SZS output start Refutation", "% SZS output end Refutation")],
279 [(Unprovable, "Satisfiability detected"),
280 (Unprovable, "UNPROVABLE"),
281 (Unprovable, "CANNOT PROVE"),
282 (OutOfResources, "Refutation not found")],
283 max_axiom_clauses = 60,
284 prefers_theory_relevant = false}
285 val vampire = tptp_prover "vampire" vampire_config
290 val tstp_proof_delims =
291 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
293 val e_config : prover_config =
294 {home_var = "E_HOME",
295 executable = "eproof",
296 arguments = fn timeout =>
297 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
298 string_of_int (to_generous_secs timeout),
299 proof_delims = [tstp_proof_delims],
301 [(Unprovable, "SZS status: Satisfiable"),
302 (Unprovable, "SZS status Satisfiable"),
303 (TimedOut, "Failure: Resource limit exceeded (time)"),
304 (TimedOut, "time limit exceeded"),
306 "# Cannot determine problem status within resource limit"),
307 (OutOfResources, "SZS status: ResourceOut"),
308 (OutOfResources, "SZS status ResourceOut")],
309 max_axiom_clauses = 100,
310 prefers_theory_relevant = false}
311 val e = tptp_prover "e" e_config
316 fun generic_dfg_prover
317 (name, {home_var, executable, arguments, proof_delims, known_failures,
318 max_axiom_clauses, prefers_theory_relevant})
319 (params as {overlord, full_types, respect_no_atp, relevance_threshold,
320 relevance_convergence, theory_relevant, defs_relevant, ...})
321 minimize_command timeout =
322 generic_prover overlord
323 (relevant_facts full_types respect_no_atp relevance_threshold
324 relevance_convergence defs_relevant max_axiom_clauses
325 (the_default prefers_theory_relevant theory_relevant))
326 (prepare_clauses true) write_dfg_file home_var executable
327 (arguments timeout) proof_delims known_failures name params
330 fun dfg_prover name p = (name, generic_dfg_prover (name, p))
332 (* The "-VarWeight=3" option helps the higher-order problems, probably by
333 counteracting the presence of "hAPP". *)
334 fun generic_spass_config dfg : prover_config =
335 {home_var = "SPASS_HOME",
336 executable = "SPASS",
337 arguments = fn timeout =>
338 "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
339 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
340 |> not dfg ? prefix "-TPTP ",
341 proof_delims = [("Here is a proof", "Formulae used in the proof")],
343 [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
344 (TimedOut, "SPASS beiseite: Ran out of time"),
345 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
346 (MalformedInput, "Undefined symbol"),
347 (MalformedInput, "Free Variable"),
348 (OldSpass, "unrecognized option `-TPTP'"),
349 (OldSpass, "Unrecognized option TPTP")],
350 max_axiom_clauses = 40,
351 prefers_theory_relevant = true}
352 val spass_dfg_config = generic_spass_config true
353 val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
355 val spass_config = generic_spass_config false
356 val spass = tptp_prover "spass" spass_config
358 (* remote prover invocation via SystemOnTPTP *)
360 val systems = Synchronized.var "atp_systems" ([]: string list);
363 case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
364 (answer, 0) => split_lines answer
366 error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
368 fun refresh_systems_on_tptp () =
369 Synchronized.change systems (fn _ => get_systems ());
371 fun get_system prefix = Synchronized.change_result systems (fn systems =>
372 (if null systems then get_systems () else systems)
373 |> `(find_first (String.isPrefix prefix)));
375 fun the_system prefix =
376 (case get_system prefix of
377 NONE => error ("System " ^ quote prefix ^
378 " not available at SystemOnTPTP.")
381 val remote_known_failures =
382 [(TimedOut, "says Timeout"),
383 (MalformedOutput, "Remote script could not extract proof")]
385 fun remote_prover_config atp_prefix args
386 ({proof_delims, known_failures, max_axiom_clauses,
387 prefers_theory_relevant, ...} : prover_config) : prover_config =
388 {home_var = "ISABELLE_ATP_MANAGER",
389 executable = "SystemOnTPTP",
390 arguments = fn timeout =>
391 args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
392 the_system atp_prefix,
393 proof_delims = insert (op =) tstp_proof_delims proof_delims,
394 known_failures = remote_known_failures @ known_failures,
395 max_axiom_clauses = max_axiom_clauses,
396 prefers_theory_relevant = prefers_theory_relevant}
399 tptp_prover (remotify (fst vampire))
400 (remote_prover_config "Vampire---9" "" vampire_config)
403 tptp_prover (remotify (fst e))
404 (remote_prover_config "EP---" "" e_config)
407 tptp_prover (remotify (fst spass))
408 (remote_prover_config "SPASS---" "-x" spass_config)
410 fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
411 name |> getenv home_var = "" ? remotify
413 fun default_atps_param_value () =
414 space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
415 remotify (fst vampire)]
418 [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
419 val prover_setup = fold add_prover provers
423 #> problem_prefix_setup
424 #> measure_runtime_setup