1 (* Title: HOL/Tools/ATP/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 atp_format = ATP_Problem.atp_format
11 type formula_kind = ATP_Problem.formula_kind
12 type failure = ATP_Proof.failure
14 type slice_spec = int * atp_format * string * string * bool
16 {exec : string * string,
17 required_execs : (string * string) list,
19 Proof.context -> bool -> string -> Time.time
20 -> (unit -> (string * real) list) -> string,
21 proof_delims : (string * string) list,
22 known_failures : (failure * string) list,
23 conj_sym_kind : formula_kind,
24 prem_kind : formula_kind,
26 Proof.context -> (real * (bool * (slice_spec * string))) list}
28 val force_sos : bool Config.T
29 val term_order : string Config.T
32 val e_fun_weightN : string
33 val e_sym_offset_weightN : string
34 val e_selection_heuristic : string Config.T
35 val e_default_fun_weight : real Config.T
36 val e_fun_weight_base : real Config.T
37 val e_fun_weight_span : real Config.T
38 val e_default_sym_offs_weight : real Config.T
39 val e_sym_offs_weight_base : real Config.T
40 val e_sym_offs_weight_span : real Config.T
41 val alt_ergoN : string
42 val dummy_thfN : string
47 val iprover_eqN : string
49 val satallaxN : string
52 val spass_newN : string
54 val waldmeisterN : string
56 val remote_prefix : string
58 string -> string -> string list -> (string * string) list
59 -> (failure * string) list -> formula_kind -> formula_kind
60 -> (Proof.context -> slice_spec) -> string * atp_config
61 val add_atp : string * atp_config -> theory -> theory
62 val get_atp : theory -> string -> atp_config
63 val supported_atps : theory -> string list
64 val is_atp_installed : theory -> string -> bool
65 val refresh_systems_on_tptp : unit -> unit
66 val setup : theory -> theory
69 structure ATP_Systems : ATP_SYSTEMS =
74 open ATP_Problem_Generate
76 (* ATP configuration *)
78 type slice_spec = int * atp_format * string * string * bool
81 {exec : string * string,
82 required_execs : (string * string) list,
84 Proof.context -> bool -> string -> Time.time
85 -> (unit -> (string * real) list) -> string,
86 proof_delims : (string * string) list,
87 known_failures : (failure * string) list,
88 conj_sym_kind : formula_kind,
89 prem_kind : formula_kind,
90 best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
92 (* "best_slices" must be found empirically, taking a wholistic approach since
93 the ATPs are run in parallel. The "real" component gives the faction of the
94 time available given to the slice and should add up to 1.0. The first "bool"
95 component indicates whether the slice's strategy is complete; the "int", the
96 preferred number of facts to pass; the first "string", the preferred type
97 system (which should be sound or quasi-sound); the second "string", the
98 preferred lambda translation scheme; the second "bool", whether uncurried
99 aliased should be generated; the third "string", extra information to
100 the prover (e.g., SOS or no SOS).
102 The last slice should be the most "normal" one, because it will get all the
103 time available if the other slices fail early and also because it is used if
104 slicing is disabled (e.g., by the minimizer). *)
106 val known_perl_failures =
107 [(CantConnect, "HTTP error"),
108 (NoPerl, "env: perl"),
109 (NoLibwwwPerl, "Can't locate HTTP")]
111 fun known_szs_failures wrap =
112 [(Unprovable, wrap "CounterSatisfiable"),
113 (Unprovable, wrap "Satisfiable"),
114 (GaveUp, wrap "GaveUp"),
115 (GaveUp, wrap "Unknown"),
116 (GaveUp, wrap "Incomplete"),
117 (ProofMissing, wrap "Theorem"),
118 (ProofMissing, wrap "Unsatisfiable"),
119 (TimedOut, wrap "Timeout"),
120 (Inappropriate, wrap "Inappropriate"),
121 (OutOfResources, wrap "ResourceOut"),
122 (OutOfResources, wrap "MemoryOut"),
123 (Interrupted, wrap "Forced"),
124 (Interrupted, wrap "User")]
126 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
127 val known_says_failures = known_szs_failures (prefix " says ")
131 val alt_ergoN = "alt_ergo"
132 val dummy_thfN = "dummy_thf" (* experimental *)
134 val e_sineN = "e_sine"
135 val e_tofofN = "e_tofof"
136 val iproverN = "iprover"
137 val iprover_eqN = "iprover_eq"
139 val satallaxN = "satallax"
142 val spass_newN = "spass_new" (* experimental *)
143 val vampireN = "vampire"
144 val waldmeisterN = "waldmeister"
145 val z3_tptpN = "z3_tptp"
146 val remote_prefix = "remote_"
148 structure Data = Theory_Data
150 type T = (atp_config * stamp) Symtab.table
151 val empty = Symtab.empty
154 Symtab.merge (eq_snd (op =)) data
155 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
158 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
161 val no_sosN = "no_sos"
163 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
168 val weightsN = "_weights"
169 val precsN = "_precs"
170 val lrN = "_lr" (* SPASS-specific *)
173 Attrib.setup_config_string @{binding atp_term_order} (K smartN)
178 val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit)
180 val alt_ergo_config : atp_config =
181 {exec = ("WHY3_HOME", "why3"),
184 fn _ => fn _ => fn _ => fn timeout => fn _ =>
185 "--format tff1 --prover alt-ergo --timelimit " ^
186 string_of_int (to_secs 1 timeout),
189 [(ProofMissing, ": Valid"),
190 (TimedOut, ": Timeout"),
191 (GaveUp, ": Unknown")],
192 conj_sym_kind = Hypothesis,
193 prem_kind = Hypothesis,
194 best_slices = fn _ =>
196 [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))]}
198 val alt_ergo = (alt_ergoN, alt_ergo_config)
203 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
205 val tstp_proof_delims =
206 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
207 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
209 val e_smartN = "smart"
211 val e_fun_weightN = "fun_weight"
212 val e_sym_offset_weightN = "sym_offset_weight"
214 val e_selection_heuristic =
215 Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
217 val e_default_fun_weight =
218 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
219 val e_fun_weight_base =
220 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
221 val e_fun_weight_span =
222 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
223 val e_default_sym_offs_weight =
224 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
225 val e_sym_offs_weight_base =
226 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
227 val e_sym_offs_weight_span =
228 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
230 fun e_selection_heuristic_case method fw sow =
231 if method = e_fun_weightN then fw
232 else if method = e_sym_offset_weightN then sow
233 else raise Fail ("unexpected " ^ quote method)
235 fun scaled_e_selection_weight ctxt method w =
236 w * Config.get ctxt (e_selection_heuristic_case method
237 e_fun_weight_span e_sym_offs_weight_span)
238 + Config.get ctxt (e_selection_heuristic_case method
239 e_fun_weight_base e_sym_offs_weight_base)
240 |> Real.ceil |> signed_string_of_int
242 fun e_selection_weight_arguments ctxt method sel_weights =
243 if method = e_autoN then
246 (* supplied by Stephan Schulz *)
247 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
248 \--destructive-er-aggressive --destructive-er --presat-simplify \
249 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
250 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
251 \-H'(4*" ^ e_selection_heuristic_case method "FunWeight" "SymOffsetWeight" ^
253 (e_selection_heuristic_case method
254 e_default_fun_weight e_default_sym_offs_weight
255 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
258 |> map (fn (s, w) => "," ^ s ^ ":" ^
259 scaled_e_selection_weight ctxt method w)
261 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
262 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
263 \FIFOWeight(PreferProcessed))'"
265 fun effective_e_selection_heuristic ctxt =
266 if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic
268 val e_config : atp_config =
269 {exec = ("E_HOME", "eproof"),
272 fn ctxt => fn _ => fn method => fn timeout => fn sel_weights =>
273 "--tstp-in --tstp-out -l5 " ^
274 e_selection_weight_arguments ctxt method sel_weights ^
275 " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
276 proof_delims = tstp_proof_delims,
278 known_szs_status_failures @
279 [(TimedOut, "Failure: Resource limit exceeded (time)"),
280 (TimedOut, "time limit exceeded"),
281 (OutOfResources, "# Cannot determine problem status")],
282 conj_sym_kind = Hypothesis,
283 prem_kind = Conjecture,
284 best_slices = fn ctxt =>
285 let val method = effective_e_selection_heuristic ctxt in
287 if method = e_smartN then
288 [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),
289 (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))),
290 (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))]
292 [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
295 val e = (eN, e_config)
300 val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
302 val leo2_config : atp_config =
303 {exec = ("LEO2_HOME", "leo"),
306 fn _ => fn _ => fn sos => fn timeout => fn _ =>
307 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
308 |> sos = sosN ? prefix "--sos ",
309 proof_delims = tstp_proof_delims,
311 known_szs_status_failures @
312 [(TimedOut, "CPU time limit exceeded, terminating"),
313 (GaveUp, "No.of.Axioms")],
314 conj_sym_kind = Axiom,
315 prem_kind = Hypothesis,
316 best_slices = fn ctxt =>
318 [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), sosN))),
319 (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), no_sosN)))]
320 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
323 val leo2 = (leo2N, leo2_config)
328 val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
330 val satallax_config : atp_config =
331 {exec = ("SATALLAX_HOME", "satallax"),
334 fn _ => fn _ => fn _ => fn timeout => fn _ =>
335 "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
337 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
338 known_failures = known_szs_status_failures,
339 conj_sym_kind = Axiom,
340 prem_kind = Hypothesis,
343 K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
345 val satallax = (satallaxN, satallax_config)
350 (* The "-VarWeight=3" option helps the higher-order problems, probably by
351 counteracting the presence of explicit application operators. *)
352 val spass_config : atp_config =
353 {exec = ("ISABELLE_ATP", "scripts/spass"),
354 required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
355 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
356 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
357 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
358 |> sos = sosN ? prefix "-SOS=1 ",
359 proof_delims = [("Here is a proof", "Formulae used in the proof")],
361 known_perl_failures @
362 [(GaveUp, "SPASS beiseite: Completion found"),
363 (TimedOut, "SPASS beiseite: Ran out of time"),
364 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
365 (MalformedInput, "Undefined symbol"),
366 (MalformedInput, "Free Variable"),
367 (Unprovable, "No formulae and clauses found in input file"),
368 (InternalError, "Please report this error")],
369 conj_sym_kind = Hypothesis,
370 prem_kind = Conjecture,
371 best_slices = fn ctxt =>
373 [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))),
374 (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))),
375 (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
376 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
378 val spass = (spassN, spass_config)
380 val spass_new_H2 = "-Heuristic=2"
381 val spass_new_H2SOS = "-Heuristic=2 -SOS"
382 val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
383 val spass_new_H2NuVS0Red2 =
384 "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
387 val spass_new_config : atp_config =
388 {exec = ("SPASS_NEW_HOME", "SPASS"),
390 arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
391 ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
392 |> extra_options <> "" ? prefix (extra_options ^ " "),
393 proof_delims = #proof_delims spass_config,
394 known_failures = #known_failures spass_config,
395 conj_sym_kind = #conj_sym_kind spass_config,
396 prem_kind = #prem_kind spass_config,
397 best_slices = fn _ =>
399 [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
400 (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
401 (0.1666, (false, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
402 (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
403 (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
404 (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
405 (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
406 (0.1000, (false, ((400, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2)))]}
408 val spass_new = (spass_newN, spass_new_config)
413 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
415 fun is_old_vampire_version () =
416 string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
418 val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
420 val vampire_config : atp_config =
421 {exec = ("VAMPIRE_HOME", "vampire"),
423 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
424 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
425 " --proof tptp --output_axiom_names on\
426 \ --forced_options propositional_to_bdd=off\
427 \ --thanks \"Andrei and Krystof\" --input_file"
428 |> sos = sosN ? prefix "--sos on ",
430 [("=========== Refutation ==========",
431 "======= End of refutation ======="),
432 ("% SZS output start Refutation", "% SZS output end Refutation"),
433 ("% SZS output start Proof", "% SZS output end Proof")],
435 known_szs_status_failures @
436 [(GaveUp, "UNPROVABLE"),
437 (GaveUp, "CANNOT PROVE"),
438 (Unprovable, "Satisfiability detected"),
439 (Unprovable, "Termination reason: Satisfiable"),
440 (Interrupted, "Aborted by signal SIGINT")],
441 conj_sym_kind = Conjecture,
442 prem_kind = Conjecture,
443 best_slices = fn ctxt =>
445 (if is_old_vampire_version () then
446 [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))),
447 (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
448 (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))]
450 [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
451 (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
452 (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))])
453 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
456 val vampire = (vampireN, vampire_config)
459 (* Z3 with TPTP syntax *)
461 val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
463 val z3_tptp_config : atp_config =
464 {exec = ("Z3_HOME", "z3"),
466 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
467 "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
469 known_failures = known_szs_status_failures,
470 conj_sym_kind = Hypothesis,
471 prem_kind = Hypothesis,
474 K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
475 (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
476 (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
477 (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]}
479 val z3_tptp = (z3_tptpN, z3_tptp_config)
482 (* Not really a prover: Experimental Polymorphic TFF and THF output *)
484 fun dummy_config format type_enc : atp_config =
485 {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
487 arguments = K (K (K (K (K "")))),
489 known_failures = known_szs_status_failures,
490 conj_sym_kind = Hypothesis,
491 prem_kind = Hypothesis,
493 K [(1.0, (false, ((200, format, type_enc,
494 if is_format_higher_order format then keep_lamsN
495 else combsN, false), "")))]}
497 val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
498 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
499 val dummy_thf = (dummy_thfN, dummy_thf_config)
502 (* Remote ATP invocation via SystemOnTPTP *)
504 val systems = Synchronized.var "atp_systems" ([] : string list)
507 case Isabelle_System.bash_output
508 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
509 (output, 0) => split_lines output
511 error (case extract_known_failure known_perl_failures output of
512 SOME failure => string_for_failure failure
513 | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
515 fun find_system name [] systems =
516 find_first (String.isPrefix (name ^ "---")) systems
517 | find_system name (version :: versions) systems =
518 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
519 NONE => find_system name versions systems
522 fun get_system name versions =
523 Synchronized.change_result systems
524 (fn systems => (if null systems then get_systems () else systems)
525 |> `(`(find_system name versions)))
527 fun the_system name versions =
528 case get_system name versions of
530 | (NONE, []) => error ("SystemOnTPTP is not available.")
532 case syss |> filter_out (String.isPrefix "%")
533 |> filter_out (curry (op =) "") of
534 [] => error ("SystemOnTPTP is not available.")
535 | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".")
537 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
538 "(Available systems: " ^ commas_quote syss ^ ".)")
540 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
542 fun remote_config system_name system_versions proof_delims known_failures
543 conj_sym_kind prem_kind best_slice : atp_config =
544 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
546 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
547 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
548 " -s " ^ the_system system_name system_versions,
549 proof_delims = union (op =) tstp_proof_delims proof_delims,
550 known_failures = known_failures @ known_perl_failures @ known_says_failures,
551 conj_sym_kind = conj_sym_kind,
552 prem_kind = prem_kind,
553 best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
555 fun remotify_config system_name system_versions best_slice
556 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
557 : atp_config) : atp_config =
558 remote_config system_name system_versions proof_delims known_failures
559 conj_sym_kind prem_kind best_slice
561 fun remote_atp name system_name system_versions proof_delims known_failures
562 conj_sym_kind prem_kind best_slice =
563 (remote_prefix ^ name,
564 remote_config system_name system_versions proof_delims known_failures
565 conj_sym_kind prem_kind best_slice)
566 fun remotify_atp (name, config) system_name system_versions best_slice =
567 (remote_prefix ^ name,
568 remotify_config system_name system_versions best_slice config)
570 val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
573 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
574 (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
576 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
577 (K (100, leo2_thf0, "mono_native_higher", liftingN, false) (* FUDGE *))
578 val remote_satallax =
579 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
580 (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false)
583 remotify_atp vampire "Vampire" ["1.8"]
584 (K (250, vampire_tff0, "mono_native", combs_or_liftingN, false) (* FUDGE *))
586 remotify_atp z3_tptp "Z3" ["3.0"]
587 (K (250, z3_tff0, "mono_native", combsN, false) (* FUDGE *))
589 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
590 Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
592 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
593 (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
594 val remote_iprover_eq =
595 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
596 (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
598 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
599 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
600 (K (100, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
602 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
604 (K (150, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
605 val remote_waldmeister =
606 remote_atp waldmeisterN "Waldmeister" ["710"]
607 [("#START OF PROOF", "Proved Goals:")]
608 [(OutOfResources, "Too many function symbols"),
609 (Crashed, "Unrecoverable Segmentation Fault")]
610 Hypothesis Hypothesis
611 (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
615 fun add_atp (name, config) thy =
616 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
617 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
619 fun get_atp thy name =
620 the (Symtab.lookup (Data.get thy) name) |> fst
621 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
623 val supported_atps = Symtab.keys o Data.get
625 fun is_atp_installed thy name =
626 let val {exec, required_execs, ...} = get_atp thy name in
627 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
630 fun refresh_systems_on_tptp () =
631 Synchronized.change systems (fn _ => get_systems ())
634 [alt_ergo, e, leo2, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
635 remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
636 remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
638 val setup = fold add_atp atps