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 format = ATP_Problem.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,
25 Proof.context -> (real * (bool * (int * format * string * string))) list}
27 val force_sos : bool Config.T
30 val e_fun_weightN : string
31 val e_sym_offset_weightN : string
32 val e_weight_method : string Config.T
33 val e_default_fun_weight : real Config.T
34 val e_fun_weight_base : real Config.T
35 val e_fun_weight_span : real Config.T
36 val e_default_sym_offs_weight : real Config.T
37 val e_sym_offs_weight_base : real Config.T
38 val e_sym_offs_weight_span : real Config.T
44 val satallaxN : string
48 val waldmeisterN : string
50 val remote_prefix : string
52 string -> string -> string list -> (string * string) list
53 -> (failure * string) list -> formula_kind -> formula_kind
54 -> (Proof.context -> int * format * string) -> string * atp_config
55 val add_atp : string * atp_config -> theory -> theory
56 val get_atp : theory -> string -> 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 setup : theory -> theory
63 structure ATP_Systems : ATP_SYSTEMS =
69 (* ATP configuration *)
72 {exec : string * string,
73 required_execs : (string * string) list,
75 Proof.context -> bool -> string -> Time.time
76 -> (unit -> (string * real) list) -> string,
77 proof_delims : (string * string) list,
78 known_failures : (failure * string) list,
79 conj_sym_kind : formula_kind,
80 prem_kind : formula_kind,
82 Proof.context -> (real * (bool * (int * format * string * string))) list}
84 (* "best_slices" must be found empirically, taking a wholistic approach since
85 the ATPs are run in parallel. The "real" components give the faction of the
86 time available given to the slice and should add up to 1.0. The "bool"
87 component indicates whether the slice's strategy is complete; the "int", the
88 preferred number of facts to pass; the first "string", the preferred type
89 system (which should be sound or quasi-sound); the second "string", extra
90 information to the prover (e.g., SOS or no SOS).
92 The last slice should be the most "normal" one, because it will get all the
93 time available if the other slices fail early and also because it is used if
94 slicing is disabled (e.g., by the minimizer). *)
96 val known_perl_failures =
97 [(CantConnect, "HTTP error"),
98 (NoPerl, "env: perl"),
99 (NoLibwwwPerl, "Can't locate HTTP")]
104 val e_sineN = "e_sine"
105 val e_tofofN = "e_tofof"
108 val satallaxN = "satallax"
111 val vampireN = "vampire"
112 val waldmeisterN = "waldmeister"
113 val z3_tptpN = "z3_tptp"
114 val remote_prefix = "remote_"
116 structure Data = Theory_Data
118 type T = (atp_config * stamp) Symtab.table
119 val empty = Symtab.empty
121 fun merge data : T = Symtab.merge (eq_snd op =) data
122 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
125 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
128 val no_sosN = "no_sos"
130 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
135 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
137 val tstp_proof_delims =
138 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
139 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
141 val e_smartN = "smart"
143 val e_fun_weightN = "fun_weight"
144 val e_sym_offset_weightN = "sym_offset_weight"
146 val e_weight_method =
147 Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
149 val e_default_fun_weight =
150 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
151 val e_fun_weight_base =
152 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
153 val e_fun_weight_span =
154 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
155 val e_default_sym_offs_weight =
156 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
157 val e_sym_offs_weight_base =
158 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
159 val e_sym_offs_weight_span =
160 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
162 fun e_weight_method_case method fw sow =
163 if method = e_fun_weightN then fw
164 else if method = e_sym_offset_weightN then sow
165 else raise Fail ("unexpected " ^ quote method)
167 fun scaled_e_weight ctxt method w =
169 (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
171 (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
172 |> Real.ceil |> signed_string_of_int
174 fun e_weight_arguments ctxt method weights =
175 if method = e_autoN then
178 (* supplied by Stephan Schulz *)
179 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
180 \--destructive-er-aggressive --destructive-er --presat-simplify \
181 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
182 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
183 \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
185 (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
186 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
189 |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
191 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
192 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
193 \FIFOWeight(PreferProcessed))'"
195 fun effective_e_weight_method ctxt =
196 if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
198 val e_config : atp_config =
199 {exec = ("E_HOME", "eproof"),
202 fn ctxt => fn _ => fn method => fn timeout => fn weights =>
203 "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
204 " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
205 proof_delims = tstp_proof_delims,
207 [(Unprovable, "SZS status: CounterSatisfiable"),
208 (Unprovable, "SZS status CounterSatisfiable"),
209 (ProofMissing, "SZS status Theorem"),
210 (TimedOut, "Failure: Resource limit exceeded (time)"),
211 (TimedOut, "time limit exceeded"),
212 (OutOfResources, "# Cannot determine problem status"),
213 (OutOfResources, "SZS status: ResourceOut"),
214 (OutOfResources, "SZS status ResourceOut")],
215 conj_sym_kind = Hypothesis,
216 prem_kind = Conjecture,
217 best_slices = fn ctxt =>
218 let val method = effective_e_weight_method ctxt in
220 if method = e_smartN then
221 [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
222 (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
223 (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
225 [(1.0, (true, (500, FOF, "mono_tags?", method)))]
228 val e = (eN, e_config)
233 val leo2_config : atp_config =
234 {exec = ("LEO2_HOME", "leo"),
237 fn _ => fn _ => fn sos => fn timeout => fn _ =>
238 "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
239 |> sos = sosN ? prefix "--sos ",
240 proof_delims = tstp_proof_delims,
242 conj_sym_kind = Axiom,
243 prem_kind = Hypothesis,
244 best_slices = fn ctxt =>
246 [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))),
247 (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))]
248 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
251 val leo2 = (leo2N, leo2_config)
256 val satallax_config : atp_config =
257 {exec = ("SATALLAX_HOME", "satallax"),
260 fn _ => fn _ => fn _ => fn timeout => fn _ =>
261 "-t " ^ string_of_int (to_secs 1 timeout),
262 proof_delims = tstp_proof_delims,
263 known_failures = [(ProofMissing, "SZS status Theorem")],
264 conj_sym_kind = Axiom,
265 prem_kind = Hypothesis,
267 K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))]
270 val satallax = (satallaxN, satallax_config)
275 (* The "-VarWeight=3" option helps the higher-order problems, probably by
276 counteracting the presence of explicit application operators. *)
277 val spass_config : atp_config =
278 {exec = ("ISABELLE_ATP", "scripts/spass"),
279 required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
280 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
281 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
282 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
283 |> sos = sosN ? prefix "-SOS=1 ",
284 proof_delims = [("Here is a proof", "Formulae used in the proof")],
286 known_perl_failures @
287 [(GaveUp, "SPASS beiseite: Completion found"),
288 (TimedOut, "SPASS beiseite: Ran out of time"),
289 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
290 (MalformedInput, "Undefined symbol"),
291 (MalformedInput, "Free Variable"),
292 (Unprovable, "No formulae and clauses found in input file"),
293 (SpassTooOld, "tptp2dfg"),
294 (InternalError, "Please report this error")],
295 conj_sym_kind = Hypothesis,
296 prem_kind = Conjecture,
297 best_slices = fn ctxt =>
299 [(0.333, (false, (150, FOF, "mono_tags", sosN))),
300 (0.333, (false, (300, FOF, "poly_tags?", sosN))),
301 (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
302 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
305 val spass = (spassN, spass_config)
310 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
312 fun is_old_vampire_version () =
313 string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
315 val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
317 val vampire_config : atp_config =
318 {exec = ("VAMPIRE_HOME", "vampire"),
320 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
321 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
322 " --proof tptp --output_axiom_names on \
323 \ --thanks \"Andrei and Krystof\" --input_file"
324 |> sos = sosN ? prefix "--sos on ",
326 [("=========== Refutation ==========",
327 "======= End of refutation ======="),
328 ("% SZS output start Refutation", "% SZS output end Refutation"),
329 ("% SZS output start Proof", "% SZS output end Proof")],
331 [(GaveUp, "UNPROVABLE"),
332 (GaveUp, "CANNOT PROVE"),
333 (GaveUp, "SZS status GaveUp"),
334 (TimedOut, "SZS status Timeout"),
335 (Unprovable, "Satisfiability detected"),
336 (Unprovable, "Termination reason: Satisfiable"),
337 (VampireTooOld, "not a valid option"),
338 (Interrupted, "Aborted by signal SIGINT")],
339 conj_sym_kind = Conjecture,
340 prem_kind = Conjecture,
341 best_slices = fn ctxt =>
343 (if is_old_vampire_version () then
344 [(0.333, (false, (150, FOF, "poly_guards", sosN))),
345 (0.333, (false, (500, FOF, "mono_tags?", sosN))),
346 (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
348 [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
349 (0.333, (false, (500, vampire_tff, "simple", sosN))),
350 (0.334, (true, (50, vampire_tff, "simple", no_sosN)))])
351 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
354 val vampire = (vampireN, vampire_config)
357 (* Z3 with TPTP syntax *)
359 val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
361 val z3_tptp_config : atp_config =
362 {exec = ("Z3_HOME", "z3"),
364 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
365 "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
368 [(GaveUp, "SZS status Satisfiable"),
369 (GaveUp, "SZS status CounterSatisfiable"),
370 (GaveUp, "SZS status GaveUp"),
371 (GaveUp, "SZS status Unknown"),
372 (ProofMissing, "SZS status Unsatisfiable"),
373 (ProofMissing, "SZS status Theorem")],
374 conj_sym_kind = Hypothesis,
375 prem_kind = Hypothesis,
378 K [(0.5, (false, (250, z3_tff, "simple", ""))),
379 (0.25, (false, (125, z3_tff, "simple", ""))),
380 (0.125, (false, (62, z3_tff, "simple", ""))),
381 (0.125, (false, (31, z3_tff, "simple", "")))]}
383 val z3_tptp = (z3_tptpN, z3_tptp_config)
385 (* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
387 val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
389 val pff_config : atp_config =
390 {exec = ("HOME", ""), (* dummy *)
392 arguments = K (K (K (K (K "")))),
395 conj_sym_kind = Hypothesis,
396 prem_kind = Hypothesis,
397 best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
399 val pff = (pffN, pff_config)
402 (* Remote ATP invocation via SystemOnTPTP *)
404 val systems = Synchronized.var "atp_systems" ([] : string list)
407 case Isabelle_System.bash_output
408 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
409 (output, 0) => split_lines output
411 error (case extract_known_failure known_perl_failures output of
412 SOME failure => string_for_failure failure
413 | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
415 fun find_system name [] systems =
416 find_first (String.isPrefix (name ^ "---")) systems
417 | find_system name (version :: versions) systems =
418 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
419 NONE => find_system name versions systems
422 fun get_system name versions =
423 Synchronized.change_result systems
424 (fn systems => (if null systems then get_systems () else systems)
425 |> `(`(find_system name versions)))
427 fun the_system name versions =
428 case get_system name versions of
430 | (NONE, []) => error ("SystemOnTPTP is currently not available.")
432 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
433 "(Available systems: " ^ commas_quote syss ^ ".)")
435 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
437 fun remote_config system_name system_versions proof_delims known_failures
438 conj_sym_kind prem_kind best_slice : atp_config =
439 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
441 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
442 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
443 ^ " -s " ^ the_system system_name system_versions,
444 proof_delims = union (op =) tstp_proof_delims proof_delims,
445 known_failures = known_failures @ known_perl_failures @
446 [(Unprovable, "says Satisfiable"),
447 (Unprovable, "says CounterSatisfiable"),
448 (GaveUp, "says Unknown"),
449 (GaveUp, "says GaveUp"),
450 (ProofMissing, "says Theorem"),
451 (ProofMissing, "says Unsatisfiable"),
452 (TimedOut, "says Timeout"),
453 (Inappropriate, "says Inappropriate")],
454 conj_sym_kind = conj_sym_kind,
455 prem_kind = prem_kind,
456 best_slices = fn ctxt =>
457 let val (max_relevant, format, type_enc) = best_slice ctxt in
458 [(1.0, (false, (max_relevant, format, type_enc, "")))]
461 fun remotify_config system_name system_versions best_slice
462 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
463 : atp_config) : atp_config =
464 remote_config system_name system_versions proof_delims known_failures
465 conj_sym_kind prem_kind best_slice
467 fun remote_atp name system_name system_versions proof_delims known_failures
468 conj_sym_kind prem_kind best_slice =
469 (remote_prefix ^ name,
470 remote_config system_name system_versions proof_delims known_failures
471 conj_sym_kind prem_kind best_slice)
472 fun remotify_atp (name, config) system_name system_versions best_slice =
473 (remote_prefix ^ name,
474 remotify_config system_name system_versions best_slice config)
476 val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
479 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
480 (K (750, FOF, "mono_tags?") (* FUDGE *))
482 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
483 (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *))
484 val remote_satallax =
485 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
486 (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *))
488 remotify_atp vampire "Vampire" ["1.8"]
489 (K (250, FOF, "mono_guards?") (* FUDGE *))
491 remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *))
493 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
494 Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
496 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
497 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
498 (K (100, dumb_tff, "simple") (* FUDGE *))
500 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
501 Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *))
502 val remote_waldmeister =
503 remote_atp waldmeisterN "Waldmeister" ["710"]
504 [("#START OF PROOF", "Proved Goals:")]
505 [(OutOfResources, "Too many function symbols"),
506 (Crashed, "Unrecoverable Segmentation Fault")]
507 Hypothesis Hypothesis
508 (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
512 fun add_atp (name, config) thy =
513 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
514 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
516 fun get_atp thy name =
517 the (Symtab.lookup (Data.get thy) name) |> fst
518 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
520 val supported_atps = Symtab.keys o Data.get
522 fun is_atp_installed thy name =
523 let val {exec, required_execs, ...} = get_atp thy name in
524 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
527 fun refresh_systems_on_tptp () =
528 Synchronized.change systems (fn _ => get_systems ())
531 [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
532 remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
533 remote_e_tofof, remote_waldmeister]
534 val setup = fold add_atp atps