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 atp_formula_role = ATP_Problem.atp_formula_role
13 type atp_failure = ATP_Proof.atp_failure
15 type slice_spec = (int * string) * atp_format * string * string * bool
17 {exec : unit -> string list * string list,
19 Proof.context -> bool -> string -> Time.time -> string
20 -> term_order * (unit -> (string * int) list)
21 * (unit -> (string * real) list) -> string,
22 proof_delims : (string * string) list,
23 known_failures : (atp_failure * string) list,
24 prem_role : atp_formula_role,
25 best_slices : Proof.context -> (real * (slice_spec * string)) list,
26 best_max_mono_iters : int,
27 best_max_new_mono_instances : int}
29 val default_max_mono_iters : int
30 val default_max_new_mono_instances : int
31 val force_sos : bool Config.T
32 val term_order : string Config.T
35 val e_fun_weightN : string
36 val e_sym_offset_weightN : string
37 val e_selection_heuristic : string Config.T
38 val e_default_fun_weight : real Config.T
39 val e_fun_weight_base : real Config.T
40 val e_fun_weight_span : real Config.T
41 val e_default_sym_offs_weight : real Config.T
42 val e_sym_offs_weight_base : real Config.T
43 val e_sym_offs_weight_span : real Config.T
44 val spass_H1SOS : string
46 val spass_H2LR0LT0 : string
47 val spass_H2NuVS0 : string
48 val spass_H2NuVS0Red2 : string
49 val spass_H2SOS : string
50 val spass_extra_options : string Config.T
52 string -> string -> string list -> (string * string) list
53 -> (atp_failure * string) list -> atp_formula_role
54 -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
55 val add_atp : string * (unit -> atp_config) -> theory -> theory
56 val get_atp : theory -> string -> (unit -> atp_config)
57 val supported_atps : theory -> string list
58 val is_atp_installed : theory -> string -> bool
59 val refresh_systems_on_tptp : unit -> unit
60 val effective_term_order : Proof.context -> string -> term_order
63 structure ATP_Systems : ATP_SYSTEMS =
68 open ATP_Problem_Generate
71 (* ATP configuration *)
73 val default_max_mono_iters = 3 (* FUDGE *)
74 val default_max_new_mono_instances = 100 (* FUDGE *)
76 type slice_spec = (int * string) * atp_format * string * string * bool
79 {exec : unit -> string list * string list,
81 Proof.context -> bool -> string -> Time.time -> string
82 -> term_order * (unit -> (string * int) list)
83 * (unit -> (string * real) list) -> string,
84 proof_delims : (string * string) list,
85 known_failures : (atp_failure * string) list,
86 prem_role : atp_formula_role,
87 best_slices : Proof.context -> (real * (slice_spec * string)) list,
88 best_max_mono_iters : int,
89 best_max_new_mono_instances : int}
91 (* "best_slices" must be found empirically, taking a wholistic approach since
92 the ATPs are run in parallel. Each slice has the format
94 (time_frac, ((max_facts, fact_filter), format, type_enc,
95 lam_trans, uncurried_aliases), extra)
99 time_frac = faction of the time available given to the slice (which should
102 extra = extra information to the prover (e.g., SOS or no SOS).
104 The last slice should be the most "normal" one, because it will get all the
105 time available if the other slices fail early and also because it is used if
106 slicing is disabled (e.g., by the minimizer). *)
112 val tstp_proof_delims =
113 [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"),
114 ("% SZS output start Refutation", "% SZS output end Refutation"),
115 ("% SZS output start Proof", "% SZS output end Proof")]
117 val known_perl_failures =
118 [(CantConnect, "HTTP error"),
119 (NoPerl, "env: perl"),
120 (NoLibwwwPerl, "Can't locate HTTP")]
122 fun known_szs_failures wrap =
123 [(Unprovable, wrap "CounterSatisfiable"),
124 (Unprovable, wrap "Satisfiable"),
125 (GaveUp, wrap "GaveUp"),
126 (GaveUp, wrap "Unknown"),
127 (GaveUp, wrap "Incomplete"),
128 (ProofMissing, wrap "Theorem"),
129 (ProofMissing, wrap "Unsatisfiable"),
130 (TimedOut, wrap "Timeout"),
131 (Inappropriate, wrap "Inappropriate"),
132 (OutOfResources, wrap "ResourceOut"),
133 (OutOfResources, wrap "MemoryOut"),
134 (Interrupted, wrap "Forced"),
135 (Interrupted, wrap "User")]
137 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
138 val known_says_failures = known_szs_failures (prefix " says ")
140 structure Data = Theory_Data
142 type T = ((unit -> atp_config) * stamp) Symtab.table
143 val empty = Symtab.empty
146 Symtab.merge (eq_snd (op =)) data
147 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
150 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
153 val no_sosN = "no_sos"
155 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
158 (* val kboN = "kbo" *)
160 val xweightsN = "_weights"
162 val xsimpN = "_simp" (* SPASS-specific *)
164 (* Possible values for "atp_term_order":
165 "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
167 Attrib.setup_config_string @{binding atp_term_order} (K smartN)
172 val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice)
174 val agsyhol_config : atp_config =
175 {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
176 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
177 "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^
179 proof_delims = tstp_proof_delims,
180 known_failures = known_szs_status_failures,
181 prem_role = Hypothesis,
184 K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
185 best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
186 best_max_new_mono_instances = default_max_new_mono_instances}
188 val agsyhol = (agsyholN, fn () => agsyhol_config)
193 val alt_ergo_tff1 = TFF Polymorphic
195 val alt_ergo_config : atp_config =
196 {exec = K (["WHY3_HOME"], ["why3"]),
197 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
198 "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^
199 string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
202 [(ProofMissing, ": Valid"),
203 (TimedOut, ": Timeout"),
204 (GaveUp, ": Unknown")],
205 prem_role = Hypothesis,
206 best_slices = fn _ =>
208 [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
209 best_max_mono_iters = default_max_mono_iters,
210 best_max_new_mono_instances = default_max_new_mono_instances}
212 val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
217 fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
218 fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
219 fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
221 val e_smartN = "smart"
223 val e_fun_weightN = "fun_weight"
224 val e_sym_offset_weightN = "sym_offset_weight"
226 val e_selection_heuristic =
227 Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
229 val e_default_fun_weight =
230 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
231 val e_fun_weight_base =
232 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
233 val e_fun_weight_span =
234 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
235 val e_default_sym_offs_weight =
236 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
237 val e_sym_offs_weight_base =
238 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
239 val e_sym_offs_weight_span =
240 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
242 fun e_selection_heuristic_case heuristic fw sow =
243 if heuristic = e_fun_weightN then fw
244 else if heuristic = e_sym_offset_weightN then sow
245 else raise Fail ("unexpected " ^ quote heuristic)
247 fun scaled_e_selection_weight ctxt heuristic w =
248 w * Config.get ctxt (e_selection_heuristic_case heuristic
249 e_fun_weight_span e_sym_offs_weight_span)
250 + Config.get ctxt (e_selection_heuristic_case heuristic
251 e_fun_weight_base e_sym_offs_weight_base)
252 |> Real.ceil |> signed_string_of_int
254 fun e_selection_weight_arguments ctxt heuristic sel_weights =
255 if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then
256 (* supplied by Stephan Schulz *)
257 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
258 \--destructive-er-aggressive --destructive-er --presat-simplify \
259 \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
260 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
261 e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
263 (e_selection_heuristic_case heuristic
264 e_default_fun_weight e_default_sym_offs_weight
265 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
268 |> map (fn (s, w) => "," ^ s ^ ":" ^
269 scaled_e_selection_weight ctxt heuristic w)
271 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
272 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
273 \FIFOWeight(PreferProcessed))'"
278 map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
279 fun e_ord_precedence [_] = ""
280 | e_ord_precedence info = info |> map fst |> space_implode "<"
282 fun e_term_order_info_arguments false false _ = ""
283 | e_term_order_info_arguments gen_weights gen_prec ord_info =
284 let val ord_info = ord_info () in
285 (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
287 (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
291 fun effective_e_selection_heuristic ctxt =
292 if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
295 fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
297 val e_config : atp_config =
298 {exec = (fn () => (["E_HOME"],
299 if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
300 arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
301 fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
302 (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
303 "--tstp-in --tstp-out --silent " ^
304 e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
305 e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
306 "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
307 "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
308 (if is_e_at_least_1_8 () then
311 " --output-level=5" ^
312 (if is_e_at_least_1_6 () then " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
316 [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
319 [(TimedOut, "Failure: Resource limit exceeded (time)"),
320 (TimedOut, "time limit exceeded")] @
321 known_szs_status_failures,
322 prem_role = Conjecture,
323 best_slices = fn ctxt =>
324 let val heuristic = effective_e_selection_heuristic ctxt in
326 if heuristic = e_smartN then
327 [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
328 (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
329 (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
330 (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
331 (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
332 (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
334 [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
336 best_max_mono_iters = default_max_mono_iters,
337 best_max_new_mono_instances = default_max_new_mono_instances}
339 val e = (eN, fn () => e_config)
344 val e_males_config : atp_config =
345 {exec = K (["E_MALES_HOME"], ["emales.py"]),
346 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
347 "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
348 proof_delims = tstp_proof_delims,
349 known_failures = #known_failures e_config,
350 prem_role = Conjecture,
353 K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
354 (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
355 (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
356 (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
357 best_max_mono_iters = default_max_mono_iters,
358 best_max_new_mono_instances = default_max_new_mono_instances}
360 val e_males = (e_malesN, fn () => e_males_config)
365 val e_par_config : atp_config =
366 {exec = K (["E_HOME"], ["runepar.pl"]),
367 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
368 string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
370 proof_delims = tstp_proof_delims,
371 known_failures = #known_failures e_config,
372 prem_role = Conjecture,
373 best_slices = #best_slices e_males_config,
374 best_max_mono_iters = default_max_mono_iters,
375 best_max_new_mono_instances = default_max_new_mono_instances}
377 val e_par = (e_parN, fn () => e_par_config)
382 val iprover_config : atp_config =
383 {exec = K (["IPROVER_HOME"], ["iprover"]),
384 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
385 "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
386 string_of_real (Time.toReal timeout) ^ " " ^ file_name,
387 proof_delims = tstp_proof_delims,
389 [(ProofIncomplete, "% SZS output start CNFRefutation")] @
390 known_szs_status_failures,
391 prem_role = Hypothesis,
394 K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))],
395 best_max_mono_iters = default_max_mono_iters,
396 best_max_new_mono_instances = default_max_new_mono_instances}
398 val iprover = (iproverN, fn () => iprover_config)
403 val iprover_eq_config : atp_config =
404 {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
405 arguments = #arguments iprover_config,
406 proof_delims = #proof_delims iprover_config,
407 known_failures = #known_failures iprover_config,
408 prem_role = #prem_role iprover_config,
409 best_slices = #best_slices iprover_config,
410 best_max_mono_iters = #best_max_mono_iters iprover_config,
411 best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
413 val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
418 (* LEO-II supports definitions, but it performs significantly better on our
419 benchmarks when they are not used. *)
420 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
422 val leo2_config : atp_config =
423 {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
424 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
425 "--foatp e --atp e=\"$E_HOME\"/eprover \
426 \--atp epclextract=\"$E_HOME\"/epclextract \
427 \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
429 proof_delims = tstp_proof_delims,
431 [(TimedOut, "CPU time limit exceeded, terminating"),
432 (GaveUp, "No.of.Axioms")] @
433 known_szs_status_failures,
434 prem_role = Hypothesis,
437 K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
438 best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
439 best_max_new_mono_instances = default_max_new_mono_instances}
441 val leo2 = (leo2N, fn () => leo2_config)
446 (* Choice is disabled until there is proper reconstruction for it. *)
447 val satallax_thf0 = THF (Monomorphic, THF_Without_Choice)
449 val satallax_config : atp_config =
450 {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
451 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
452 "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
454 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
455 known_failures = known_szs_status_failures,
456 prem_role = Hypothesis,
459 K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
460 best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
461 best_max_new_mono_instances = default_max_new_mono_instances}
463 val satallax = (satallaxN, fn () => satallax_config)
468 val spass_H1SOS = "-Heuristic=1 -SOS"
469 val spass_H2 = "-Heuristic=2"
470 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
471 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
472 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
473 val spass_H2SOS = "-Heuristic=2 -SOS"
475 val spass_extra_options =
476 Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
478 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
479 val spass_config : atp_config =
480 {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
481 arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
482 fn file_name => fn _ =>
483 "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
484 "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
485 |> extra_options <> "" ? prefix (extra_options ^ " "),
486 proof_delims = [("Here is a proof", "Formulae used in the proof")],
488 [(GaveUp, "SPASS beiseite: Completion found"),
489 (TimedOut, "SPASS beiseite: Ran out of time"),
490 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
491 (MalformedInput, "Undefined symbol"),
492 (MalformedInput, "Free Variable"),
493 (Unprovable, "No formulae and clauses found in input file"),
494 (InternalError, "Please report this error")] @
496 prem_role = Conjecture,
497 best_slices = fn ctxt =>
499 [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
500 (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
501 (0.1666, (((50, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)),
502 (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
503 (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
504 (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
505 (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
506 (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
507 |> (case Config.get ctxt spass_extra_options of
509 | opts => map (apsnd (apsnd (K opts)))),
510 best_max_mono_iters = default_max_mono_iters,
511 best_max_new_mono_instances = default_max_new_mono_instances}
513 val spass = (spassN, fn () => spass_config)
518 (* Vampire 1.8 has TFF0 support, but the support was buggy until revision
519 1435 (or shortly before). *)
520 fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
521 fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
523 val vampire_tff0 = TFF Monomorphic
525 val vampire_config : atp_config =
526 {exec = K (["VAMPIRE_HOME"], ["vampire"]),
527 arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name =>
529 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
530 " --proof tptp --output_axiom_names on" ^
531 (if is_vampire_at_least_1_8 () then
532 (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
534 " --forced_options splitting=off:equality_proxy=off:general_splitting=off\
535 \:inequality_splitting=0:naming=0"
540 " --thanks \"Andrei and Krystof\" --input_file " ^ file_name
541 |> sos = sosN ? prefix "--sos on ",
543 [("=========== Refutation ==========",
544 "======= End of refutation =======")] @
547 [(GaveUp, "UNPROVABLE"),
548 (GaveUp, "CANNOT PROVE"),
549 (Unprovable, "Satisfiability detected"),
550 (Unprovable, "Termination reason: Satisfiable"),
551 (Interrupted, "Aborted by signal SIGINT")] @
552 known_szs_status_failures,
553 prem_role = Conjecture,
554 best_slices = fn ctxt =>
556 (if is_vampire_beyond_1_8 () then
557 [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
558 (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
559 (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
561 [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
562 (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
563 (0.334, (((50, meshN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
564 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
566 best_max_mono_iters = default_max_mono_iters,
567 best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
569 val vampire = (vampireN, fn () => vampire_config)
571 (* Z3 with TPTP syntax (half experimental, half legacy) *)
573 val z3_tff0 = TFF Monomorphic
575 val z3_tptp_config : atp_config =
576 {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
577 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
578 "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
579 proof_delims = [("SZS status Theorem", "")],
580 known_failures = known_szs_status_failures,
581 prem_role = Hypothesis,
584 K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")),
585 (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")),
586 (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
587 (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
588 best_max_mono_iters = default_max_mono_iters,
589 best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
591 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
596 val zipperposition_tff1 = TFF Polymorphic
598 val zipperposition_config : atp_config =
599 {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
600 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
601 "-print none -proof tstp -print-types -timeout " ^
602 string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
603 proof_delims = tstp_proof_delims,
604 known_failures = known_szs_status_failures,
605 prem_role = Hypothesis,
606 best_slices = fn _ =>
608 [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
609 best_max_mono_iters = default_max_mono_iters,
610 best_max_new_mono_instances = default_max_new_mono_instances}
612 val zipperposition = (zipperpositionN, fn () => zipperposition_config)
615 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
617 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
618 {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
619 arguments = K (K (K (K (K (K ""))))),
621 known_failures = known_szs_status_failures,
622 prem_role = prem_role,
624 K [(1.0, (((200, ""), format, type_enc,
625 if is_format_higher_order format then keep_lamsN
626 else combsN, uncurried_aliases), ""))],
627 best_max_mono_iters = default_max_mono_iters,
628 best_max_new_mono_instances = default_max_new_mono_instances}
630 val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
631 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
632 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
634 val spass_pirate_format = DFG Polymorphic
635 val remote_spass_pirate_config : atp_config =
636 {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
637 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
638 string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
639 proof_delims = [("Involved clauses:", "Involved clauses:")],
640 known_failures = known_szs_status_failures,
641 prem_role = #prem_role spass_config,
642 best_slices = K [(1.0, (((200, ""), spass_pirate_format, "tc_native", combsN, true), ""))],
643 best_max_mono_iters = default_max_mono_iters,
644 best_max_new_mono_instances = default_max_new_mono_instances}
645 val remote_spass_pirate = (remote_prefix ^ spass_pirateN, fn () => remote_spass_pirate_config)
648 (* Remote ATP invocation via SystemOnTPTP *)
650 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
652 fun get_remote_systems () =
653 TimeLimit.timeLimit (seconds 10.0)
655 case Isabelle_System.bash_output
656 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
657 (output, 0) => split_lines output
659 (warning (case extract_known_atp_failure known_perl_failures output of
660 SOME failure => string_of_atp_failure failure
661 | NONE => trim_line output ^ "."); [])) ()
662 handle TimeLimit.TimeOut => []
664 fun find_remote_system name [] systems =
665 find_first (String.isPrefix (name ^ "---")) systems
666 | find_remote_system name (version :: versions) systems =
667 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
668 NONE => find_remote_system name versions systems
671 fun get_remote_system name versions =
672 Synchronized.change_result remote_systems
673 (fn systems => (if null systems then get_remote_systems () else systems)
674 |> `(`(find_remote_system name versions)))
676 fun the_remote_system name versions =
677 (case get_remote_system name versions of
679 | (NONE, []) => error "SystemOnTPTP is not available."
681 (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
682 [] => error "SystemOnTPTP is currently not available."
683 | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
685 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
686 commas_quote syss ^ ".)")))
688 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
690 fun remote_config system_name system_versions proof_delims known_failures
691 prem_role best_slice : atp_config =
692 {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
693 arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
694 (if command <> "" then "-c " ^ quote command ^ " " else "") ^
695 "-s " ^ the_remote_system system_name system_versions ^ " " ^
696 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
698 proof_delims = union (op =) tstp_proof_delims proof_delims,
699 known_failures = known_failures @ known_perl_failures @ known_says_failures,
700 prem_role = prem_role,
701 best_slices = fn ctxt => [(1.0, best_slice ctxt)],
702 best_max_mono_iters = default_max_mono_iters,
703 best_max_new_mono_instances = default_max_new_mono_instances}
705 fun remotify_config system_name system_versions best_slice
706 ({proof_delims, known_failures, prem_role, ...} : atp_config)
708 remote_config system_name system_versions proof_delims known_failures
711 fun remote_atp name system_name system_versions proof_delims known_failures
712 prem_role best_slice =
713 (remote_prefix ^ name,
714 fn () => remote_config system_name system_versions proof_delims
715 known_failures prem_role best_slice)
716 fun remotify_atp (name, config) system_name system_versions best_slice =
717 (remote_prefix ^ name,
718 remotify_config system_name system_versions best_slice o config)
720 fun gen_remote_waldmeister name =
721 remote_atp name "Waldmeister" ["710"]
722 [("#START OF PROOF", "Proved Goals:")]
723 [(OutOfResources, "Too many function symbols"),
724 (Inappropriate, "**** Unexpected end of file."),
725 (Crashed, "Unrecoverable Segmentation Fault")]
727 (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
729 val explicit_tff0 = TFF Monomorphic
732 remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
733 (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
735 remotify_atp e "EP" ["1.7", "1.6", "1.5", "1"]
736 (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
738 remotify_atp iprover "iProver" ["0.99"]
739 (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
740 val remote_iprover_eq =
741 remotify_atp iprover_eq "iProver-Eq" ["0.8"]
742 (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
744 remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
745 (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
746 val remote_satallax =
747 remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
748 (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
750 remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
751 (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
753 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
754 (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
756 remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
757 [("refutation.", "end_refutation.")] [] Hypothesis
758 (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
760 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
761 (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
762 val remote_waldmeister = gen_remote_waldmeister waldmeisterN
763 val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN
768 fun add_atp (name, config) thy =
769 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
770 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
772 fun get_atp thy name =
773 fst (the (Symtab.lookup (Data.get thy) name))
774 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
776 val supported_atps = Symtab.keys o Data.get
778 fun is_atp_installed thy name =
779 let val {exec, ...} = get_atp thy name () in
780 exists (fn var => getenv var <> "") (fst (exec ()))
783 fun refresh_systems_on_tptp () =
784 Synchronized.change remote_systems (fn _ => get_remote_systems ())
786 fun effective_term_order ctxt atp =
787 let val ord = Config.get ctxt term_order in
789 {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
790 gen_simp = String.isSuffix spass_pirateN atp}
792 let val is_lpo = String.isSubstring lpoN ord in
793 {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
794 gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord}
799 [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
800 z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
801 remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
802 remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
804 val _ = Theory.setup (fold add_atp atps)