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 term_order = ATP_Problem.term_order
11 type atp_format = ATP_Problem.atp_format
12 type formula_role = ATP_Problem.formula_role
13 type failure = ATP_Proof.failure
15 type slice_spec = int * atp_format * string * string * bool
17 {exec : string list * string,
18 required_vars : string list list,
20 Proof.context -> bool -> string -> Time.time
21 -> term_order * (unit -> (string * int) list)
22 * (unit -> (string * real) list) -> string,
23 proof_delims : (string * string) list,
24 known_failures : (failure * string) list,
25 prem_role : formula_role,
27 Proof.context -> (real * (bool * (slice_spec * string))) list,
28 best_max_mono_iters : int,
29 best_max_new_mono_instances : int}
31 val default_max_mono_iters : int
32 val default_max_new_mono_instances : int
33 val force_sos : bool Config.T
34 val term_order : string Config.T
37 val e_fun_weightN : string
38 val e_sym_offset_weightN : string
39 val e_selection_heuristic : string Config.T
40 val e_default_fun_weight : real Config.T
41 val e_fun_weight_base : real Config.T
42 val e_fun_weight_span : real Config.T
43 val e_default_sym_offs_weight : real Config.T
44 val e_sym_offs_weight_base : real Config.T
45 val e_sym_offs_weight_span : real Config.T
46 val alt_ergoN : string
47 val dummy_thfN : string
52 val iprover_eqN : string
54 val satallaxN : string
58 val waldmeisterN : string
60 val remote_prefix : string
62 string -> string -> string list -> (string * string) list
63 -> (failure * string) list -> formula_role
64 -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
65 val add_atp : string * (unit -> atp_config) -> theory -> theory
66 val get_atp : theory -> string -> (unit -> atp_config)
67 val supported_atps : theory -> string list
68 val is_atp_installed : theory -> string -> bool
69 val refresh_systems_on_tptp : unit -> unit
70 val effective_term_order : Proof.context -> string -> term_order
71 val setup : theory -> theory
74 structure ATP_Systems : ATP_SYSTEMS =
79 open ATP_Problem_Generate
81 (* ATP configuration *)
83 val default_max_mono_iters = 3 (* FUDGE *)
84 val default_max_new_mono_instances = 200 (* FUDGE *)
86 type slice_spec = int * atp_format * string * string * bool
89 {exec : string list * string,
90 required_vars : string list list,
92 Proof.context -> bool -> string -> Time.time
93 -> term_order * (unit -> (string * int) list)
94 * (unit -> (string * real) list) -> string,
95 proof_delims : (string * string) list,
96 known_failures : (failure * string) list,
97 prem_role : formula_role,
98 best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list,
99 best_max_mono_iters : int,
100 best_max_new_mono_instances : int}
102 (* "best_slices" must be found empirically, taking a wholistic approach since
103 the ATPs are run in parallel. The "real" component gives the faction of the
104 time available given to the slice and should add up to 1.0. The first "bool"
105 component indicates whether the slice's strategy is complete; the "int", the
106 preferred number of facts to pass; the first "string", the preferred type
107 system (which should be sound or quasi-sound); the second "string", the
108 preferred lambda translation scheme; the second "bool", whether uncurried
109 aliased should be generated; the third "string", extra information to
110 the prover (e.g., SOS or no SOS).
112 The last slice should be the most "normal" one, because it will get all the
113 time available if the other slices fail early and also because it is used if
114 slicing is disabled (e.g., by the minimizer). *)
116 val known_perl_failures =
117 [(CantConnect, "HTTP error"),
118 (NoPerl, "env: perl"),
119 (NoLibwwwPerl, "Can't locate HTTP")]
121 fun known_szs_failures wrap =
122 [(Unprovable, wrap "CounterSatisfiable"),
123 (Unprovable, wrap "Satisfiable"),
124 (GaveUp, wrap "GaveUp"),
125 (GaveUp, wrap "Unknown"),
126 (GaveUp, wrap "Incomplete"),
127 (ProofMissing, wrap "Theorem"),
128 (ProofMissing, wrap "Unsatisfiable"),
129 (TimedOut, wrap "Timeout"),
130 (Inappropriate, wrap "Inappropriate"),
131 (OutOfResources, wrap "ResourceOut"),
132 (OutOfResources, wrap "MemoryOut"),
133 (Interrupted, wrap "Forced"),
134 (Interrupted, wrap "User")]
136 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
137 val known_says_failures = known_szs_failures (prefix " says ")
141 val alt_ergoN = "alt_ergo"
142 val dummy_thfN = "dummy_thf" (* for experiments *)
144 val e_sineN = "e_sine"
145 val e_tofofN = "e_tofof"
146 val iproverN = "iprover"
147 val iprover_eqN = "iprover_eq"
149 val satallaxN = "satallax"
152 val vampireN = "vampire"
153 val waldmeisterN = "waldmeister"
154 val z3_tptpN = "z3_tptp"
155 val remote_prefix = "remote_"
157 structure Data = Theory_Data
159 type T = ((unit -> atp_config) * stamp) Symtab.table
160 val empty = Symtab.empty
163 Symtab.merge (eq_snd (op =)) data
164 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
167 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
170 val no_sosN = "no_sos"
172 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
175 (* val kboN = "kbo" *)
177 val xweightsN = "_weights"
179 val xsimpN = "_simp" (* SPASS-specific *)
181 (* Possible values for "atp_term_order":
182 "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
184 Attrib.setup_config_string @{binding atp_term_order} (K smartN)
188 val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
190 val alt_ergo_config : atp_config =
191 {exec = (["WHY3_HOME"], "why3"),
194 fn _ => fn _ => fn _ => fn timeout => fn _ =>
195 "--format tff1 --prover alt-ergo --timelimit " ^
196 string_of_int (to_secs 1 timeout),
199 [(ProofMissing, ": Valid"),
200 (TimedOut, ": Timeout"),
201 (GaveUp, ": Unknown")],
202 prem_role = Hypothesis,
203 best_slices = fn _ =>
205 [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))],
206 best_max_mono_iters = default_max_mono_iters,
207 best_max_new_mono_instances = default_max_new_mono_instances}
209 val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
214 fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER)
216 val tstp_proof_delims =
217 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
218 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
220 val e_smartN = "smart"
222 val e_fun_weightN = "fun_weight"
223 val e_sym_offset_weightN = "sym_offset_weight"
225 val e_selection_heuristic =
226 Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
228 val e_default_fun_weight =
229 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
230 val e_fun_weight_base =
231 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
232 val e_fun_weight_span =
233 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
234 val e_default_sym_offs_weight =
235 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
236 val e_sym_offs_weight_base =
237 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
238 val e_sym_offs_weight_span =
239 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
241 fun e_selection_heuristic_case heuristic fw sow =
242 if heuristic = e_fun_weightN then fw
243 else if heuristic = e_sym_offset_weightN then sow
244 else raise Fail ("unexpected " ^ quote heuristic)
246 fun scaled_e_selection_weight ctxt heuristic w =
247 w * Config.get ctxt (e_selection_heuristic_case heuristic
248 e_fun_weight_span e_sym_offs_weight_span)
249 + Config.get ctxt (e_selection_heuristic_case heuristic
250 e_fun_weight_base e_sym_offs_weight_base)
251 |> Real.ceil |> signed_string_of_int
253 fun e_selection_weight_arguments ctxt heuristic sel_weights =
254 if heuristic = e_autoN then
257 (* supplied by Stephan Schulz *)
258 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
259 \--destructive-er-aggressive --destructive-er --presat-simplify \
260 \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
261 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
262 e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
264 (e_selection_heuristic_case heuristic
265 e_default_fun_weight e_default_sym_offs_weight
266 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
269 |> map (fn (s, w) => "," ^ s ^ ":" ^
270 scaled_e_selection_weight ctxt heuristic w)
272 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
273 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
274 \FIFOWeight(PreferProcessed))'"
277 map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
278 fun e_ord_precedence [_] = ""
279 | e_ord_precedence info = info |> map fst |> space_implode "<"
281 fun e_term_order_info_arguments false false _ = ""
282 | e_term_order_info_arguments gen_weights gen_prec ord_info =
283 let val ord_info = ord_info () in
284 (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
286 (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
290 fun effective_e_selection_heuristic ctxt =
291 if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN
293 fun e_kbo () = if is_new_e_version () then "KBO6" else "KBO"
295 val e_config : atp_config =
296 {exec = (["E_HOME"], "eproof"),
299 fn ctxt => fn _ => fn heuristic => fn timeout =>
300 fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
301 "--tstp-in --tstp-out --output-level=5 --silent " ^
302 e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
303 e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
304 "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
305 "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
306 proof_delims = tstp_proof_delims,
308 [(TimedOut, "Failure: Resource limit exceeded (time)"),
309 (TimedOut, "time limit exceeded")] @
310 known_szs_status_failures,
311 prem_role = Conjecture,
312 best_slices = fn ctxt =>
313 let val heuristic = effective_e_selection_heuristic ctxt in
315 if heuristic = e_smartN then
316 [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),
317 (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))),
318 (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))]
320 [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))]
322 best_max_mono_iters = default_max_mono_iters,
323 best_max_new_mono_instances = default_max_new_mono_instances}
325 val e = (eN, fn () => e_config)
330 (* LEO-II supports definitions, but it performs significantly better on our
331 benchmarks when they are not used. *)
333 THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
335 val leo2_config : atp_config =
336 {exec = (["LEO2_HOME"], "leo"),
339 fn _ => fn _ => fn _ => fn timeout => fn _ =>
340 "--foatp e --atp e=\"$E_HOME\"/eprover \
341 \--atp epclextract=\"$E_HOME\"/epclextract \
342 \--proofoutput 1 --timeout " ^
343 string_of_int (to_secs 1 timeout),
344 proof_delims = tstp_proof_delims,
346 [(TimedOut, "CPU time limit exceeded, terminating"),
347 (GaveUp, "No.of.Axioms")] @
348 known_szs_status_failures,
349 prem_role = Hypothesis,
352 K [(1.0, (true, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))],
353 best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
354 best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
356 val leo2 = (leo2N, fn () => leo2_config)
362 THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
364 val satallax_config : atp_config =
365 {exec = (["SATALLAX_HOME"], "satallax"),
368 fn _ => fn _ => fn _ => fn timeout => fn _ =>
369 "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
371 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
372 known_failures = known_szs_status_failures,
373 prem_role = Hypothesis,
376 K [(1.0, (true, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
377 best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
378 best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
380 val satallax = (satallaxN, fn () => satallax_config)
385 val spass_H1SOS = "-Heuristic=1 -SOS"
386 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
387 val spass_H2SOS = "-Heuristic=2 -SOS"
388 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
389 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
391 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
392 val spass_config : atp_config =
393 {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
395 arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
396 ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
397 |> extra_options <> "" ? prefix (extra_options ^ " "),
398 proof_delims = [("Here is a proof", "Formulae used in the proof")],
400 [(OldSPASS, "Unrecognized option Isabelle"),
401 (GaveUp, "SPASS beiseite: Completion found"),
402 (TimedOut, "SPASS beiseite: Ran out of time"),
403 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
404 (MalformedInput, "Undefined symbol"),
405 (MalformedInput, "Free Variable"),
406 (Unprovable, "No formulae and clauses found in input file"),
407 (InternalError, "Please report this error")] @
409 prem_role = Conjecture,
410 best_slices = fn _ =>
412 [(0.1667, (false, ((150, DFG, "mono_native", combsN, true), ""))),
413 (0.1667, (false, ((500, DFG, "mono_native", liftingN, true), spass_H2SOS))),
414 (0.1666, (false, ((50, DFG, "mono_native", liftingN, true), spass_H2LR0LT0))),
415 (0.1000, (false, ((250, DFG, "mono_native", combsN, true), spass_H2NuVS0))),
416 (0.1000, (false, ((1000, DFG, "mono_native", liftingN, true), spass_H1SOS))),
417 (0.1000, (false, ((150, DFG, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
418 (0.1000, (false, ((300, DFG, "mono_native", combsN, true), spass_H2SOS))),
419 (0.1000, (false, ((100, DFG, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
420 best_max_mono_iters = default_max_mono_iters,
421 best_max_new_mono_instances = default_max_new_mono_instances}
423 val spass = (spassN, fn () => spass_config)
427 (* Vampire 1.8 has TFF support, but the support was buggy until revision
428 1435 (or shortly before). *)
429 fun is_new_vampire_version () =
430 string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
432 val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
434 val vampire_config : atp_config =
435 {exec = (["VAMPIRE_HOME"], "vampire"),
437 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
438 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
439 " --proof tptp --output_axiom_names on\
440 \ --forced_options propositional_to_bdd=off\
441 \ --thanks \"Andrei and Krystof\" --input_file"
442 |> sos = sosN ? prefix "--sos on ",
444 [("=========== Refutation ==========",
445 "======= End of refutation ======="),
446 ("% SZS output start Refutation", "% SZS output end Refutation"),
447 ("% SZS output start Proof", "% SZS output end Proof")],
449 [(GaveUp, "UNPROVABLE"),
450 (GaveUp, "CANNOT PROVE"),
451 (Unprovable, "Satisfiability detected"),
452 (Unprovable, "Termination reason: Satisfiable"),
453 (Interrupted, "Aborted by signal SIGINT")] @
454 known_szs_status_failures,
455 prem_role = Conjecture,
456 best_slices = fn ctxt =>
458 (if is_new_vampire_version () then
459 [(0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
460 (0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
461 (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]
463 [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))),
464 (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
465 (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))])
466 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
468 best_max_mono_iters = default_max_mono_iters,
469 best_max_new_mono_instances = default_max_new_mono_instances}
471 val vampire = (vampireN, fn () => vampire_config)
474 (* Z3 with TPTP syntax *)
476 val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
478 val z3_tptp_config : atp_config =
479 {exec = (["Z3_HOME"], "z3"),
481 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
482 "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
484 known_failures = known_szs_status_failures,
485 prem_role = Hypothesis,
488 K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
489 (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
490 (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
491 (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))],
492 best_max_mono_iters = default_max_mono_iters,
493 best_max_new_mono_instances = default_max_new_mono_instances}
495 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
498 (* Not really a prover: Experimental Polymorphic TFF and THF output *)
500 fun dummy_config format type_enc : atp_config =
501 {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
503 arguments = K (K (K (K (K "")))),
505 known_failures = known_szs_status_failures,
506 prem_role = Hypothesis,
508 K [(1.0, (false, ((200, format, type_enc,
509 if is_format_higher_order format then keep_lamsN
510 else combsN, false), "")))],
511 best_max_mono_iters = default_max_mono_iters,
512 best_max_new_mono_instances = default_max_new_mono_instances}
514 val dummy_thf_format =
515 THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
516 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
517 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
520 (* Remote ATP invocation via SystemOnTPTP *)
522 val systems = Synchronized.var "atp_systems" ([] : string list)
525 case Isabelle_System.bash_output
526 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
527 (output, 0) => split_lines output
529 error (case extract_known_failure known_perl_failures output of
530 SOME failure => string_for_failure failure
531 | NONE => trim_line output ^ ".")
533 fun find_system name [] systems =
534 find_first (String.isPrefix (name ^ "---")) systems
535 | find_system name (version :: versions) systems =
536 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
537 NONE => find_system name versions systems
540 fun get_system name versions =
541 Synchronized.change_result systems
542 (fn systems => (if null systems then get_systems () else systems)
543 |> `(`(find_system name versions)))
545 fun the_system name versions =
546 case get_system name versions of
548 | (NONE, []) => error ("SystemOnTPTP is not available.")
550 case syss |> filter_out (String.isPrefix "%")
551 |> filter_out (curry (op =) "") of
552 [] => error ("SystemOnTPTP is not available.")
553 | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".")
555 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
556 "(Available systems: " ^ commas_quote syss ^ ".)")
558 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
560 fun remote_config system_name system_versions proof_delims known_failures
561 prem_role best_slice : atp_config =
562 {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
564 arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
565 (if command <> "" then "-c " ^ quote command ^ " " else "") ^
566 "-s " ^ the_system system_name system_versions ^ " " ^
567 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
568 proof_delims = union (op =) tstp_proof_delims proof_delims,
569 known_failures = known_failures @ known_perl_failures @ known_says_failures,
570 prem_role = prem_role,
571 best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))],
572 best_max_mono_iters = default_max_mono_iters,
573 best_max_new_mono_instances = default_max_new_mono_instances}
575 fun remotify_config system_name system_versions best_slice
576 ({proof_delims, known_failures, prem_role, ...} : atp_config)
578 remote_config system_name system_versions proof_delims known_failures
581 fun remote_atp name system_name system_versions proof_delims known_failures
582 prem_role best_slice =
583 (remote_prefix ^ name,
584 fn () => remote_config system_name system_versions proof_delims
585 known_failures prem_role best_slice)
586 fun remotify_atp (name, config) system_name system_versions best_slice =
587 (remote_prefix ^ name,
588 remotify_config system_name system_versions best_slice o config)
590 val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
593 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
594 (K ((750, FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
596 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
597 (K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
598 val remote_satallax =
599 remotify_atp satallax "Satallax" ["2.3", "2.2", "2"]
600 (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
602 remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
603 (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
605 remotify_atp z3_tptp "Z3" ["3.0"]
606 (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
608 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
609 (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
611 remote_atp iproverN "iProver" [] [] [] Conjecture
612 (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
613 val remote_iprover_eq =
614 remote_atp iprover_eqN "iProver-Eq" [] [] [] Conjecture
615 (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
617 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
618 [("refutation.", "end_refutation.")] [] Hypothesis
619 (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
621 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
622 (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
623 val remote_waldmeister =
624 remote_atp waldmeisterN "Waldmeister" ["710"]
625 [("#START OF PROOF", "Proved Goals:")]
626 [(OutOfResources, "Too many function symbols"),
627 (Inappropriate, "**** Unexpected end of file."),
628 (Crashed, "Unrecoverable Segmentation Fault")]
630 (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
634 fun add_atp (name, config) thy =
635 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
636 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
638 fun get_atp thy name =
639 the (Symtab.lookup (Data.get thy) name) |> fst
640 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
642 val supported_atps = Symtab.keys o Data.get
644 fun is_atp_installed thy name =
645 let val {exec, required_vars, ...} = get_atp thy name () in
646 forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars)
649 fun refresh_systems_on_tptp () =
650 Synchronized.change systems (fn _ => get_systems ())
652 fun effective_term_order ctxt atp =
653 let val ord = Config.get ctxt term_order in
656 {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
658 {is_lpo = false, gen_weights = false, gen_prec = false,
661 let val is_lpo = String.isSubstring lpoN ord in
663 gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
664 gen_prec = String.isSubstring xprecN ord,
665 gen_simp = String.isSubstring xsimpN ord}
670 [alt_ergo, e, leo2, dummy_thf, satallax, spass, vampire, z3_tptp, remote_e,
671 remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
672 remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
675 val setup = fold add_atp atps