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_kind = ATP_Problem.formula_kind
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 conj_sym_kind : formula_kind,
26 prem_kind : formula_kind,
28 Proof.context -> (real * (bool * (slice_spec * string))) list}
30 val force_sos : bool Config.T
31 val term_order : string Config.T
34 val e_fun_weightN : string
35 val e_sym_offset_weightN : string
36 val e_selection_heuristic : string Config.T
37 val e_default_fun_weight : real Config.T
38 val e_fun_weight_base : real Config.T
39 val e_fun_weight_span : real Config.T
40 val e_default_sym_offs_weight : real Config.T
41 val e_sym_offs_weight_base : real Config.T
42 val e_sym_offs_weight_span : real Config.T
43 val alt_ergoN : string
44 val dummy_thfN : string
49 val iprover_eqN : string
51 val satallaxN : string
54 val spass_oldN : string
55 val spass_newN : string
57 val waldmeisterN : string
59 val remote_prefix : string
61 string -> string -> string list -> (string * string) list
62 -> (failure * string) list -> formula_kind -> formula_kind
63 -> (Proof.context -> slice_spec * string) -> string * atp_config
64 val add_atp : string * atp_config -> theory -> theory
65 val get_atp : theory -> string -> atp_config
66 val supported_atps : theory -> string list
67 val is_atp_installed : theory -> string -> bool
68 val refresh_systems_on_tptp : unit -> unit
69 val effective_term_order : Proof.context -> string -> term_order
70 val setup : theory -> theory
73 structure ATP_Systems : ATP_SYSTEMS =
78 open ATP_Problem_Generate
80 (* ATP configuration *)
82 type slice_spec = int * atp_format * string * string * bool
85 {exec : string list * string,
86 required_vars : string list list,
88 Proof.context -> bool -> string -> Time.time
89 -> term_order * (unit -> (string * int) list)
90 * (unit -> (string * real) list) -> string,
91 proof_delims : (string * string) list,
92 known_failures : (failure * string) list,
93 conj_sym_kind : formula_kind,
94 prem_kind : formula_kind,
95 best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
97 (* "best_slices" must be found empirically, taking a wholistic approach since
98 the ATPs are run in parallel. The "real" component gives the faction of the
99 time available given to the slice and should add up to 1.0. The first "bool"
100 component indicates whether the slice's strategy is complete; the "int", the
101 preferred number of facts to pass; the first "string", the preferred type
102 system (which should be sound or quasi-sound); the second "string", the
103 preferred lambda translation scheme; the second "bool", whether uncurried
104 aliased should be generated; the third "string", extra information to
105 the prover (e.g., SOS or no SOS).
107 The last slice should be the most "normal" one, because it will get all the
108 time available if the other slices fail early and also because it is used if
109 slicing is disabled (e.g., by the minimizer). *)
111 val known_perl_failures =
112 [(CantConnect, "HTTP error"),
113 (NoPerl, "env: perl"),
114 (NoLibwwwPerl, "Can't locate HTTP")]
116 fun known_szs_failures wrap =
117 [(Unprovable, wrap "CounterSatisfiable"),
118 (Unprovable, wrap "Satisfiable"),
119 (GaveUp, wrap "GaveUp"),
120 (GaveUp, wrap "Unknown"),
121 (GaveUp, wrap "Incomplete"),
122 (ProofMissing, wrap "Theorem"),
123 (ProofMissing, wrap "Unsatisfiable"),
124 (TimedOut, wrap "Timeout"),
125 (Inappropriate, wrap "Inappropriate"),
126 (OutOfResources, wrap "ResourceOut"),
127 (OutOfResources, wrap "MemoryOut"),
128 (Interrupted, wrap "Forced"),
129 (Interrupted, wrap "User")]
131 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
132 val known_says_failures = known_szs_failures (prefix " says ")
136 val alt_ergoN = "alt_ergo"
137 val dummy_thfN = "dummy_thf" (* for experiments *)
139 val e_sineN = "e_sine"
140 val e_tofofN = "e_tofof"
141 val iproverN = "iprover"
142 val iprover_eqN = "iprover_eq"
144 val satallaxN = "satallax"
147 val spass_oldN = "spass_old" (* for experiments *)
148 val spass_newN = "spass_new" (* for experiments *)
149 val vampireN = "vampire"
150 val waldmeisterN = "waldmeister"
151 val z3_tptpN = "z3_tptp"
152 val remote_prefix = "remote_"
154 structure Data = Theory_Data
156 type T = (atp_config * stamp) Symtab.table
157 val empty = Symtab.empty
160 Symtab.merge (eq_snd (op =)) data
161 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
164 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
167 val no_sosN = "no_sos"
169 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
172 (* val kboN = "kbo" *)
174 val xweightsN = "_weights"
176 val xsimpN = "_simp" (* SPASS-specific *)
178 (* Possible values for "atp_term_order":
179 "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
181 Attrib.setup_config_string @{binding atp_term_order} (K smartN)
185 val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit)
187 val alt_ergo_config : atp_config =
188 {exec = (["WHY3_HOME"], "why3"),
191 fn _ => fn _ => fn _ => fn timeout => fn _ =>
192 "--format tff1 --prover alt-ergo --timelimit " ^
193 string_of_int (to_secs 1 timeout),
196 [(ProofMissing, ": Valid"),
197 (TimedOut, ": Timeout"),
198 (GaveUp, ": Unknown")],
199 conj_sym_kind = Hypothesis,
200 prem_kind = Hypothesis,
201 best_slices = fn _ =>
203 [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))]}
205 val alt_ergo = (alt_ergoN, alt_ergo_config)
210 fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER)
212 val tstp_proof_delims =
213 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
214 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
216 val e_smartN = "smart"
218 val e_fun_weightN = "fun_weight"
219 val e_sym_offset_weightN = "sym_offset_weight"
221 val e_selection_heuristic =
222 Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
224 val e_default_fun_weight =
225 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
226 val e_fun_weight_base =
227 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
228 val e_fun_weight_span =
229 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
230 val e_default_sym_offs_weight =
231 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
232 val e_sym_offs_weight_base =
233 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
234 val e_sym_offs_weight_span =
235 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
237 fun e_selection_heuristic_case heuristic fw sow =
238 if heuristic = e_fun_weightN then fw
239 else if heuristic = e_sym_offset_weightN then sow
240 else raise Fail ("unexpected " ^ quote heuristic)
242 fun scaled_e_selection_weight ctxt heuristic w =
243 w * Config.get ctxt (e_selection_heuristic_case heuristic
244 e_fun_weight_span e_sym_offs_weight_span)
245 + Config.get ctxt (e_selection_heuristic_case heuristic
246 e_fun_weight_base e_sym_offs_weight_base)
247 |> Real.ceil |> signed_string_of_int
249 fun e_selection_weight_arguments ctxt heuristic sel_weights =
250 if heuristic = e_autoN then
253 (* supplied by Stephan Schulz *)
254 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
255 \--destructive-er-aggressive --destructive-er --presat-simplify \
256 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
257 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
259 e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
261 (e_selection_heuristic_case heuristic
262 e_default_fun_weight e_default_sym_offs_weight
263 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
266 |> map (fn (s, w) => "," ^ s ^ ":" ^
267 scaled_e_selection_weight ctxt heuristic w)
269 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
270 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
271 \FIFOWeight(PreferProcessed))'"
274 map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
275 fun e_ord_precedence [_] = ""
276 | e_ord_precedence info = info |> map fst |> space_implode "<"
278 fun e_term_order_info_arguments false false _ = ""
279 | e_term_order_info_arguments gen_weights gen_prec ord_info =
280 let val ord_info = ord_info () in
281 (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
283 (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
287 fun effective_e_selection_heuristic ctxt =
288 if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN
290 val e_config : atp_config =
291 {exec = (["E_HOME"], "eproof"),
294 fn ctxt => fn _ => fn heuristic => fn timeout =>
295 fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
296 "--tstp-in --tstp-out --output-level=5 --silent " ^
297 e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
298 e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
299 "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
300 "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
301 proof_delims = tstp_proof_delims,
303 known_szs_status_failures @
304 [(TimedOut, "Failure: Resource limit exceeded (time)"),
305 (TimedOut, "time limit exceeded"),
306 (OutOfResources, "# Cannot determine problem status")],
307 conj_sym_kind = Hypothesis,
308 prem_kind = Conjecture,
309 best_slices = fn ctxt =>
310 let val heuristic = effective_e_selection_heuristic ctxt in
312 if heuristic = e_smartN then
313 [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),
314 (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))),
315 (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))]
317 [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))]
320 val e = (eN, e_config)
325 val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
327 val leo2_config : atp_config =
328 {exec = (["LEO2_HOME"], "leo"),
331 fn _ => fn _ => fn sos => fn timeout => fn _ =>
332 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
333 |> sos = sosN ? prefix "--sos ",
334 proof_delims = tstp_proof_delims,
336 known_szs_status_failures @
337 [(TimedOut, "CPU time limit exceeded, terminating"),
338 (GaveUp, "No.of.Axioms")],
339 conj_sym_kind = Axiom,
340 prem_kind = Hypothesis,
341 best_slices = fn ctxt =>
343 [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), sosN))),
344 (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), no_sosN)))]
345 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
348 val leo2 = (leo2N, leo2_config)
353 val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
355 val satallax_config : atp_config =
356 {exec = (["SATALLAX_HOME"], "satallax"),
359 fn _ => fn _ => fn _ => fn timeout => fn _ =>
360 "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
362 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
363 known_failures = known_szs_status_failures,
364 conj_sym_kind = Axiom,
365 prem_kind = Hypothesis,
368 K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
370 val satallax = (satallaxN, satallax_config)
375 fun is_new_spass_version () =
376 string_ord (getenv "SPASS_VERSION", "3.7") = GREATER orelse
377 getenv "SPASS_NEW_HOME" <> ""
379 (* TODO: Legacy: Remove after planned Isabelle2012 release (and don't forget
380 "required_vars" and "script/spass"). *)
381 val spass_old_config : atp_config =
382 {exec = (["ISABELLE_ATP"], "scripts/spass"),
383 required_vars = [["SPASS_OLD_HOME", "SPASS_HOME"]],
384 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
385 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
386 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
387 |> sos = sosN ? prefix "-SOS=1 ",
388 proof_delims = [("Here is a proof", "Formulae used in the proof")],
390 known_perl_failures @
391 [(GaveUp, "SPASS beiseite: Completion found"),
392 (TimedOut, "SPASS beiseite: Ran out of time"),
393 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
394 (MalformedInput, "Undefined symbol"),
395 (MalformedInput, "Free Variable"),
396 (Unprovable, "No formulae and clauses found in input file"),
397 (InternalError, "Please report this error")],
398 conj_sym_kind = Hypothesis,
399 prem_kind = Conjecture,
400 best_slices = fn ctxt =>
402 [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))),
403 (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))),
404 (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
405 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
407 val spass_old = (spass_oldN, spass_old_config)
409 val spass_new_H2 = "-Heuristic=2"
410 val spass_new_H2SOS = "-Heuristic=2 -SOS"
411 val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
412 val spass_new_H2NuVS0Red2 =
413 "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
415 val spass_new_config : atp_config =
416 {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
418 arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
419 ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
420 |> extra_options <> "" ? prefix (extra_options ^ " "),
421 proof_delims = #proof_delims spass_old_config,
422 known_failures = #known_failures spass_old_config,
423 conj_sym_kind = #conj_sym_kind spass_old_config,
424 prem_kind = #prem_kind spass_old_config,
425 best_slices = fn _ =>
427 [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
428 (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
429 (0.1666, (false, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))),
430 (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
431 (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
432 (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
433 (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
434 (0.1000, (false, ((400, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2)))]}
436 val spass_new = (spass_newN, spass_new_config)
439 (spassN, if is_new_spass_version () then spass_new_config
440 else spass_old_config)
444 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
446 fun is_new_vampire_version () =
447 string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
449 val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
451 val vampire_config : atp_config =
452 {exec = (["VAMPIRE_HOME"], "vampire"),
454 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
455 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
456 " --proof tptp --output_axiom_names on\
457 \ --forced_options propositional_to_bdd=off\
458 \ --thanks \"Andrei and Krystof\" --input_file"
459 |> sos = sosN ? prefix "--sos on ",
461 [("=========== Refutation ==========",
462 "======= End of refutation ======="),
463 ("% SZS output start Refutation", "% SZS output end Refutation"),
464 ("% SZS output start Proof", "% SZS output end Proof")],
466 known_szs_status_failures @
467 [(GaveUp, "UNPROVABLE"),
468 (GaveUp, "CANNOT PROVE"),
469 (Unprovable, "Satisfiability detected"),
470 (Unprovable, "Termination reason: Satisfiable"),
471 (Interrupted, "Aborted by signal SIGINT")],
472 conj_sym_kind = Conjecture,
473 prem_kind = Conjecture,
474 best_slices = fn ctxt =>
476 (if is_new_vampire_version () then
477 [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
478 (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
479 (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]
481 [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))),
482 (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
483 (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))])
484 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
487 val vampire = (vampireN, vampire_config)
490 (* Z3 with TPTP syntax *)
492 val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
494 val z3_tptp_config : atp_config =
495 {exec = (["Z3_HOME"], "z3"),
497 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
498 "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
500 known_failures = known_szs_status_failures,
501 conj_sym_kind = Hypothesis,
502 prem_kind = Hypothesis,
505 K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
506 (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
507 (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
508 (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]}
510 val z3_tptp = (z3_tptpN, z3_tptp_config)
513 (* Not really a prover: Experimental Polymorphic TFF and THF output *)
515 fun dummy_config format type_enc : atp_config =
516 {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
518 arguments = K (K (K (K (K "")))),
520 known_failures = known_szs_status_failures,
521 conj_sym_kind = Hypothesis,
522 prem_kind = Hypothesis,
524 K [(1.0, (false, ((200, format, type_enc,
525 if is_format_higher_order format then keep_lamsN
526 else combsN, false), "")))]}
528 val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
529 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
530 val dummy_thf = (dummy_thfN, dummy_thf_config)
533 (* Remote ATP invocation via SystemOnTPTP *)
535 val systems = Synchronized.var "atp_systems" ([] : string list)
538 case Isabelle_System.bash_output
539 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
540 (output, 0) => split_lines output
542 error (case extract_known_failure known_perl_failures output of
543 SOME failure => string_for_failure failure
544 | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
546 fun find_system name [] systems =
547 find_first (String.isPrefix (name ^ "---")) systems
548 | find_system name (version :: versions) systems =
549 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
550 NONE => find_system name versions systems
553 fun get_system name versions =
554 Synchronized.change_result systems
555 (fn systems => (if null systems then get_systems () else systems)
556 |> `(`(find_system name versions)))
558 fun the_system name versions =
559 case get_system name versions of
561 | (NONE, []) => error ("SystemOnTPTP is not available.")
563 case syss |> filter_out (String.isPrefix "%")
564 |> filter_out (curry (op =) "") of
565 [] => error ("SystemOnTPTP is not available.")
566 | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".")
568 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
569 "(Available systems: " ^ commas_quote syss ^ ".)")
571 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
573 fun remote_config system_name system_versions proof_delims known_failures
574 conj_sym_kind prem_kind best_slice : atp_config =
575 {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
577 arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
578 (if command <> "" then "-c " ^ quote command ^ " " else "") ^
579 "-s " ^ the_system system_name system_versions ^ " " ^
580 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
581 proof_delims = union (op =) tstp_proof_delims proof_delims,
582 known_failures = known_failures @ known_perl_failures @ known_says_failures,
583 conj_sym_kind = conj_sym_kind,
584 prem_kind = prem_kind,
585 best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
587 fun remotify_config system_name system_versions best_slice
588 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
589 : atp_config) : atp_config =
590 remote_config system_name system_versions proof_delims known_failures
591 conj_sym_kind prem_kind best_slice
593 fun remote_atp name system_name system_versions proof_delims known_failures
594 conj_sym_kind prem_kind best_slice =
595 (remote_prefix ^ name,
596 remote_config system_name system_versions proof_delims known_failures
597 conj_sym_kind prem_kind best_slice)
598 fun remotify_atp (name, config) system_name system_versions best_slice =
599 (remote_prefix ^ name,
600 remotify_config system_name system_versions best_slice config)
602 val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
605 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
606 (K ((750, FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
608 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
609 (K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
610 val remote_satallax =
611 remotify_atp satallax "Satallax" ["2.3", "2.2", "2"]
612 (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "satallax.opt -p hocore -t %d %s") (* FUDGE *))
614 remotify_atp vampire "Vampire" ["1.8"]
615 (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
617 remotify_atp z3_tptp "Z3" ["3.0"]
618 (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
620 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture
621 (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
623 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
624 (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
625 val remote_iprover_eq =
626 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
627 (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
629 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
630 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
631 (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
633 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
635 (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
636 val remote_waldmeister =
637 remote_atp waldmeisterN "Waldmeister" ["710"]
638 [("#START OF PROOF", "Proved Goals:")]
639 [(OutOfResources, "Too many function symbols"),
640 (Crashed, "Unrecoverable Segmentation Fault")]
641 Hypothesis Hypothesis
642 (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))
646 fun add_atp (name, config) thy =
647 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
648 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
650 fun get_atp thy name =
651 the (Symtab.lookup (Data.get thy) name) |> fst
652 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
654 val supported_atps = Symtab.keys o Data.get
656 fun is_atp_installed thy name =
657 let val {exec, required_vars, ...} = get_atp thy name in
658 forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars)
661 fun refresh_systems_on_tptp () =
662 Synchronized.change systems (fn _ => get_systems ())
664 fun effective_term_order ctxt atp =
665 let val ord = Config.get ctxt term_order in
667 if atp = spass_newN orelse
668 (atp = spassN andalso is_new_spass_version ()) then
669 {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
671 {is_lpo = false, gen_weights = false, gen_prec = false,
674 let val is_lpo = String.isSubstring lpoN ord in
676 gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
677 gen_prec = String.isSubstring xprecN ord,
678 gen_simp = String.isSubstring xsimpN ord}
683 [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass (),
684 vampire, z3_tptp, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
685 remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
686 remote_z3_tptp, remote_snark, remote_waldmeister]
688 fun setup thy = fold add_atp (atps ()) thy