specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
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 tptp_format = ATP_Problem.tptp_format
11 type formula_kind = ATP_Problem.formula_kind
12 type failure = ATP_Proof.failure
15 {exec : string * string,
16 required_execs : (string * string) list,
18 Proof.context -> bool -> string -> Time.time
19 -> (unit -> (string * real) list) -> string,
20 proof_delims : (string * string) list,
21 known_failures : (failure * string) list,
22 conj_sym_kind : formula_kind,
23 prem_kind : formula_kind,
26 -> (real * (bool * (int * tptp_format * string * string))) list}
28 val force_sos : bool Config.T
31 val e_fun_weightN : string
32 val e_sym_offset_weightN : string
33 val e_weight_method : string Config.T
34 val e_default_fun_weight : real Config.T
35 val e_fun_weight_base : real Config.T
36 val e_fun_weight_span : real Config.T
37 val e_default_sym_offs_weight : real Config.T
38 val e_sym_offs_weight_base : real Config.T
39 val e_sym_offs_weight_span : real Config.T
46 val satallaxN : string
50 val waldmeisterN : string
52 val remote_prefix : string
54 string -> string -> string list -> (string * string) list
55 -> (failure * string) list -> formula_kind -> formula_kind
56 -> (Proof.context -> int * tptp_format * string) -> string * atp_config
57 val add_atp : string * atp_config -> theory -> theory
58 val get_atp : theory -> string -> atp_config
59 val supported_atps : theory -> string list
60 val is_atp_installed : theory -> string -> bool
61 val refresh_systems_on_tptp : unit -> unit
62 val setup : theory -> theory
65 structure ATP_Systems : ATP_SYSTEMS =
71 (* ATP configuration *)
74 {exec : string * string,
75 required_execs : (string * string) list,
77 Proof.context -> bool -> string -> Time.time
78 -> (unit -> (string * real) list) -> string,
79 proof_delims : (string * string) list,
80 known_failures : (failure * string) list,
81 conj_sym_kind : formula_kind,
82 prem_kind : formula_kind,
85 -> (real * (bool * (int * tptp_format * string * string))) list}
87 (* "best_slices" must be found empirically, taking a wholistic approach since
88 the ATPs are run in parallel. The "real" components give the faction of the
89 time available given to the slice and should add up to 1.0. The "bool"
90 component indicates whether the slice's strategy is complete; the "int", the
91 preferred number of facts to pass; the first "string", the preferred type
92 system (which should be sound or quasi-sound); the second "string", extra
93 information to the prover (e.g., SOS or no SOS).
95 The last slice should be the most "normal" one, because it will get all the
96 time available if the other slices fail early and also because it is used if
97 slicing is disabled (e.g., by the minimizer). *)
99 val known_perl_failures =
100 [(CantConnect, "HTTP error"),
101 (NoPerl, "env: perl"),
102 (NoLibwwwPerl, "Can't locate HTTP")]
104 fun known_szs_failures wrap =
105 [(Unprovable, wrap "CounterSatisfiable"),
106 (Unprovable, wrap "Satisfiable"),
107 (GaveUp, wrap "GaveUp"),
108 (GaveUp, wrap "Unknown"),
109 (GaveUp, wrap "Incomplete"),
110 (ProofMissing, wrap "Theorem"),
111 (ProofMissing, wrap "Unsatisfiable"),
112 (TimedOut, wrap "Timeout"),
113 (Inappropriate, wrap "Inappropriate"),
114 (OutOfResources, wrap "ResourceOut"),
115 (OutOfResources, wrap "MemoryOut"),
116 (Interrupted, wrap "Forced"),
117 (Interrupted, wrap "User")]
119 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
120 val known_says_failures = known_szs_failures (prefix " says ")
125 val e_sineN = "e_sine"
126 val e_tofofN = "e_tofof"
130 val satallaxN = "satallax"
133 val vampireN = "vampire"
134 val waldmeisterN = "waldmeister"
135 val z3_tptpN = "z3_tptp"
136 val remote_prefix = "remote_"
138 structure Data = Theory_Data
140 type T = (atp_config * stamp) Symtab.table
141 val empty = Symtab.empty
143 fun merge data : T = Symtab.merge (eq_snd op =) data
144 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
147 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
150 val no_sosN = "no_sos"
152 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
157 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
159 val tstp_proof_delims =
160 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
161 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
163 val e_smartN = "smart"
165 val e_fun_weightN = "fun_weight"
166 val e_sym_offset_weightN = "sym_offset_weight"
168 val e_weight_method =
169 Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
171 val e_default_fun_weight =
172 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
173 val e_fun_weight_base =
174 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
175 val e_fun_weight_span =
176 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
177 val e_default_sym_offs_weight =
178 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
179 val e_sym_offs_weight_base =
180 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
181 val e_sym_offs_weight_span =
182 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
184 fun e_weight_method_case method fw sow =
185 if method = e_fun_weightN then fw
186 else if method = e_sym_offset_weightN then sow
187 else raise Fail ("unexpected " ^ quote method)
189 fun scaled_e_weight ctxt method w =
191 (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
193 (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
194 |> Real.ceil |> signed_string_of_int
196 fun e_weight_arguments ctxt method weights =
197 if method = e_autoN then
200 (* supplied by Stephan Schulz *)
201 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
202 \--destructive-er-aggressive --destructive-er --presat-simplify \
203 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
204 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
205 \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
207 (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
208 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
211 |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
213 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
214 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
215 \FIFOWeight(PreferProcessed))'"
217 fun effective_e_weight_method ctxt =
218 if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
220 val e_config : atp_config =
221 {exec = ("E_HOME", "eproof"),
224 fn ctxt => fn _ => fn method => fn timeout => fn weights =>
225 "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
226 " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
227 proof_delims = tstp_proof_delims,
229 known_szs_status_failures @
230 [(TimedOut, "Failure: Resource limit exceeded (time)"),
231 (TimedOut, "time limit exceeded"),
232 (OutOfResources, "# Cannot determine problem status")],
233 conj_sym_kind = Hypothesis,
234 prem_kind = Conjecture,
235 best_slices = fn ctxt =>
236 let val method = effective_e_weight_method ctxt in
238 if method = e_smartN then
239 [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))),
240 (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))),
241 (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))]
243 [(1.0, (true, (500, FOF, "mono_tags??", method)))]
246 val e = (eN, e_config)
251 val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
253 val leo2_config : atp_config =
254 {exec = ("LEO2_HOME", "leo"),
257 fn _ => fn _ => fn sos => fn timeout => fn _ =>
258 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
259 |> sos = sosN ? prefix "--sos ",
260 proof_delims = tstp_proof_delims,
262 known_szs_status_failures @
263 [(TimedOut, "CPU time limit exceeded, terminating")],
264 conj_sym_kind = Axiom,
265 prem_kind = Hypothesis,
266 best_slices = fn ctxt =>
268 [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
269 (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
270 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
273 val leo2 = (leo2N, leo2_config)
278 val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
280 val satallax_config : atp_config =
281 {exec = ("SATALLAX_HOME", "satallax"),
284 fn _ => fn _ => fn _ => fn timeout => fn _ =>
285 "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
287 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
288 known_failures = known_szs_status_failures,
289 conj_sym_kind = Axiom,
290 prem_kind = Hypothesis,
293 K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
295 val satallax = (satallaxN, satallax_config)
300 (* The "-VarWeight=3" option helps the higher-order problems, probably by
301 counteracting the presence of explicit application operators. *)
302 val spass_config : atp_config =
303 {exec = ("ISABELLE_ATP", "scripts/spass"),
304 required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
305 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
306 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
307 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
308 |> sos = sosN ? prefix "-SOS=1 ",
309 proof_delims = [("Here is a proof", "Formulae used in the proof")],
311 known_perl_failures @
312 [(GaveUp, "SPASS beiseite: Completion found"),
313 (TimedOut, "SPASS beiseite: Ran out of time"),
314 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
315 (MalformedInput, "Undefined symbol"),
316 (MalformedInput, "Free Variable"),
317 (Unprovable, "No formulae and clauses found in input file"),
318 (SpassTooOld, "tptp2dfg"),
319 (InternalError, "Please report this error")],
320 conj_sym_kind = Hypothesis,
321 prem_kind = Conjecture,
322 best_slices = fn ctxt =>
324 [(0.333, (false, (150, FOF, "mono_tags??", sosN))),
325 (0.333, (false, (300, FOF, "poly_tags??", sosN))),
326 (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
327 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
330 val spass = (spassN, spass_config)
335 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
337 fun is_old_vampire_version () =
338 string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
340 val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
342 val vampire_config : atp_config =
343 {exec = ("VAMPIRE_HOME", "vampire"),
345 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
346 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
347 " --proof tptp --output_axiom_names on\
348 \ --forced_options propositional_to_bdd=off\
349 \ --thanks \"Andrei and Krystof\" --input_file"
350 |> sos = sosN ? prefix "--sos on ",
352 [("=========== Refutation ==========",
353 "======= End of refutation ======="),
354 ("% SZS output start Refutation", "% SZS output end Refutation"),
355 ("% SZS output start Proof", "% SZS output end Proof")],
357 known_szs_status_failures @
358 [(GaveUp, "UNPROVABLE"),
359 (GaveUp, "CANNOT PROVE"),
360 (Unprovable, "Satisfiability detected"),
361 (Unprovable, "Termination reason: Satisfiable"),
362 (VampireTooOld, "not a valid option"),
363 (Interrupted, "Aborted by signal SIGINT")],
364 conj_sym_kind = Conjecture,
365 prem_kind = Conjecture,
366 best_slices = fn ctxt =>
368 (if is_old_vampire_version () then
369 [(0.333, (false, (150, FOF, "poly_guards??", sosN))),
370 (0.333, (false, (500, FOF, "mono_tags??", sosN))),
371 (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))]
373 [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))),
374 (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
375 (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
376 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
379 val vampire = (vampireN, vampire_config)
382 (* Z3 with TPTP syntax *)
384 val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
386 val z3_tptp_config : atp_config =
387 {exec = ("Z3_HOME", "z3"),
389 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
390 "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
392 known_failures = known_szs_status_failures,
393 conj_sym_kind = Hypothesis,
394 prem_kind = Hypothesis,
397 K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
398 (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
399 (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
400 (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
402 val z3_tptp = (z3_tptpN, z3_tptp_config)
405 (* Not really a prover: Experimental Polymorphic TFF and THF output *)
407 fun dummy_config format type_enc : atp_config =
408 {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
410 arguments = K (K (K (K (K "")))),
412 known_failures = known_szs_status_failures,
413 conj_sym_kind = Hypothesis,
414 prem_kind = Hypothesis,
415 best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
417 val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
418 val pff_config = dummy_config pff_format "poly_simple"
419 val pff = (pffN, pff_config)
421 val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
422 val phf_config = dummy_config phf_format "poly_simple_higher"
423 val phf = (phfN, phf_config)
426 (* Remote ATP invocation via SystemOnTPTP *)
428 val systems = Synchronized.var "atp_systems" ([] : string list)
431 case Isabelle_System.bash_output
432 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
433 (output, 0) => split_lines output
435 error (case extract_known_failure known_perl_failures output of
436 SOME failure => string_for_failure failure
437 | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
439 fun find_system name [] systems =
440 find_first (String.isPrefix (name ^ "---")) systems
441 | find_system name (version :: versions) systems =
442 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
443 NONE => find_system name versions systems
446 fun get_system name versions =
447 Synchronized.change_result systems
448 (fn systems => (if null systems then get_systems () else systems)
449 |> `(`(find_system name versions)))
451 fun the_system name versions =
452 case get_system name versions of
454 | (NONE, []) => error ("SystemOnTPTP is currently not available.")
456 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
457 "(Available systems: " ^ commas_quote syss ^ ".)")
459 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
461 fun remote_config system_name system_versions proof_delims known_failures
462 conj_sym_kind prem_kind best_slice : atp_config =
463 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
465 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
466 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
467 ^ " -s " ^ the_system system_name system_versions,
468 proof_delims = union (op =) tstp_proof_delims proof_delims,
469 known_failures = known_failures @ known_perl_failures @ known_says_failures,
470 conj_sym_kind = conj_sym_kind,
471 prem_kind = prem_kind,
472 best_slices = fn ctxt =>
473 let val (max_relevant, format, type_enc) = best_slice ctxt in
474 [(1.0, (false, (max_relevant, format, type_enc, "")))]
477 fun remotify_config system_name system_versions best_slice
478 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
479 : atp_config) : atp_config =
480 remote_config system_name system_versions proof_delims known_failures
481 conj_sym_kind prem_kind best_slice
483 fun remote_atp name system_name system_versions proof_delims known_failures
484 conj_sym_kind prem_kind best_slice =
485 (remote_prefix ^ name,
486 remote_config system_name system_versions proof_delims known_failures
487 conj_sym_kind prem_kind best_slice)
488 fun remotify_atp (name, config) system_name system_versions best_slice =
489 (remote_prefix ^ name,
490 remotify_config system_name system_versions best_slice config)
492 val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
495 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
496 (K (750, FOF, "mono_tags??") (* FUDGE *))
498 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
499 (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
500 val remote_satallax =
501 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
502 (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
504 remotify_atp vampire "Vampire" ["1.8"]
505 (K (250, FOF, "mono_guards??") (* FUDGE *))
507 remotify_atp z3_tptp "Z3" ["3.0"]
508 (K (250, z3_tff0, "mono_simple") (* FUDGE *))
510 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
511 Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
513 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
514 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
515 (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
517 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
518 Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
519 val remote_waldmeister =
520 remote_atp waldmeisterN "Waldmeister" ["710"]
521 [("#START OF PROOF", "Proved Goals:")]
522 [(OutOfResources, "Too many function symbols"),
523 (Crashed, "Unrecoverable Segmentation Fault")]
524 Hypothesis Hypothesis
525 (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *))
529 fun add_atp (name, config) thy =
530 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
531 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
533 fun get_atp thy name =
534 the (Symtab.lookup (Data.get thy) name) |> fst
535 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
537 val supported_atps = Symtab.keys o Data.get
539 fun is_atp_installed thy name =
540 let val {exec, required_execs, ...} = get_atp thy name in
541 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
544 fun refresh_systems_on_tptp () =
545 Synchronized.change systems (fn _ => get_systems ())
548 [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
549 remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
550 remote_e_tofof, remote_waldmeister]
551 val setup = fold add_atp atps