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,
24 formats : format list,
26 Proof.context -> (real * (bool * (int * string * string))) list}
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
39 val spass_force_sos : bool Config.T
40 val vampire_force_sos : bool Config.T
45 val satallaxN : string
49 val waldmeisterN : string
51 val remote_prefix : string
53 string -> string -> string list -> (string * string) list
54 -> (failure * string) list -> formula_kind -> formula_kind -> format list
55 -> (Proof.context -> int * string) -> string * atp_config
56 val add_atp : string * atp_config -> theory -> theory
57 val get_atp : theory -> string -> atp_config
58 val supported_atps : theory -> string list
59 val is_atp_installed : theory -> string -> bool
60 val refresh_systems_on_tptp : unit -> unit
61 val setup : theory -> theory
64 structure ATP_Systems : ATP_SYSTEMS =
70 (* ATP configuration *)
73 {exec : string * string,
74 required_execs : (string * string) list,
76 Proof.context -> bool -> string -> Time.time
77 -> (unit -> (string * real) list) -> string,
78 proof_delims : (string * string) list,
79 known_failures : (failure * string) list,
80 conj_sym_kind : formula_kind,
81 prem_kind : formula_kind,
82 formats : format list,
84 Proof.context -> (real * (bool * (int * string * string))) list}
86 (* "best_slices" must be found empirically, taking a wholistic approach since
87 the ATPs are run in parallel. The "real" components give the faction of the
88 time available given to the slice and should add up to 1.0. The "bool"
89 component indicates whether the slice's strategy is complete; the "int", the
90 preferred number of facts to pass; the first "string", the preferred type
91 system (which should be sound or quasi-sound); the second "string", extra
92 information to the prover (e.g., SOS or no SOS).
94 The last slice should be the most "normal" one, because it will get all the
95 time available if the other slices fail early and also because it is used if
96 slicing is disabled (e.g., by the minimizer). *)
98 val known_perl_failures =
99 [(CantConnect, "HTTP error"),
100 (NoPerl, "env: perl"),
101 (NoLibwwwPerl, "Can't locate HTTP")]
107 val vampireN = "vampire"
108 val z3_atpN = "z3_atp"
110 val satallaxN = "satallax"
111 val sine_eN = "sine_e"
113 val tofof_eN = "tofof_e"
114 val waldmeisterN = "waldmeister"
115 val remote_prefix = "remote_"
117 structure Data = Theory_Data
119 type T = (atp_config * stamp) Symtab.table
120 val empty = Symtab.empty
122 fun merge data : T = Symtab.merge (eq_snd op =) data
123 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
126 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
129 val no_sosN = "no_sos"
134 val tstp_proof_delims =
135 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
136 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
138 val e_smartN = "smart"
140 val e_fun_weightN = "fun_weight"
141 val e_sym_offset_weightN = "sym_offset_weight"
143 val e_weight_method =
144 Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
146 val e_default_fun_weight =
147 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
148 val e_fun_weight_base =
149 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
150 val e_fun_weight_span =
151 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
152 val e_default_sym_offs_weight =
153 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
154 val e_sym_offs_weight_base =
155 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
156 val e_sym_offs_weight_span =
157 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
159 fun e_weight_method_case method fw sow =
160 if method = e_fun_weightN then fw
161 else if method = e_sym_offset_weightN then sow
162 else raise Fail ("unexpected " ^ quote method)
164 fun scaled_e_weight ctxt method w =
166 (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
168 (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
169 |> Real.ceil |> signed_string_of_int
171 fun e_weight_arguments ctxt method weights =
172 if method = e_autoN then
175 (* supplied by Stephan Schulz *)
176 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
177 \--destructive-er-aggressive --destructive-er --presat-simplify \
178 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
179 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
180 \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
182 (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
183 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
186 |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
188 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
189 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
190 \FIFOWeight(PreferProcessed))'"
192 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
194 fun effective_e_weight_method ctxt =
195 if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
197 val e_config : atp_config =
198 {exec = ("E_HOME", "eproof"),
201 fn ctxt => fn _ => fn method => fn timeout => fn weights =>
202 "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
203 " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
204 proof_delims = tstp_proof_delims,
206 [(Unprovable, "SZS status: CounterSatisfiable"),
207 (Unprovable, "SZS status CounterSatisfiable"),
208 (ProofMissing, "SZS status Theorem"),
209 (TimedOut, "Failure: Resource limit exceeded (time)"),
210 (TimedOut, "time limit exceeded"),
211 (OutOfResources, "# Cannot determine problem status"),
212 (OutOfResources, "SZS status: ResourceOut"),
213 (OutOfResources, "SZS status ResourceOut")],
214 conj_sym_kind = Hypothesis,
215 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, "mangled_tags?", e_fun_weightN))),
222 (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
223 (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
225 [(1.0, (true, (500, "mangled_tags?", method)))]
228 val e = (eN, e_config)
233 val spass_force_sos =
234 Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
236 (* The "-VarWeight=3" option helps the higher-order problems, probably by
237 counteracting the presence of "hAPP". *)
238 val spass_config : atp_config =
239 {exec = ("ISABELLE_ATP", "scripts/spass"),
240 required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
241 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
242 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
243 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
244 |> sos = sosN ? prefix "-SOS=1 ",
245 proof_delims = [("Here is a proof", "Formulae used in the proof")],
247 known_perl_failures @
248 [(GaveUp, "SPASS beiseite: Completion found"),
249 (TimedOut, "SPASS beiseite: Ran out of time"),
250 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
251 (MalformedInput, "Undefined symbol"),
252 (MalformedInput, "Free Variable"),
253 (SpassTooOld, "tptp2dfg"),
254 (InternalError, "Please report this error")],
255 conj_sym_kind = Hypothesis,
256 prem_kind = Conjecture,
258 best_slices = fn ctxt =>
260 [(0.333, (false, (150, "mangled_tags", sosN))),
261 (0.333, (false, (300, "poly_tags?", sosN))),
262 (0.334, (true, (50, "mangled_tags?", no_sosN)))]
263 |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
266 val spass = (spassN, spass_config)
271 val vampire_force_sos =
272 Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
274 val vampire_config : atp_config =
275 {exec = ("VAMPIRE_HOME", "vampire"),
277 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
278 "--proof tptp --mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
279 " --thanks \"Andrei and Krystof\" --input_file"
280 |> sos = sosN ? prefix "--sos on ",
282 [("=========== Refutation ==========",
283 "======= End of refutation ======="),
284 ("% SZS output start Refutation", "% SZS output end Refutation"),
285 ("% SZS output start Proof", "% SZS output end Proof")],
287 [(GaveUp, "UNPROVABLE"),
288 (GaveUp, "CANNOT PROVE"),
289 (GaveUp, "SZS status GaveUp"),
290 (ProofIncomplete, "predicate_definition_introduction,[]"),
291 (TimedOut, "SZS status Timeout"),
292 (Unprovable, "Satisfiability detected"),
293 (Unprovable, "Termination reason: Satisfiable"),
294 (VampireTooOld, "not a valid option"),
295 (Interrupted, "Aborted by signal SIGINT")],
296 conj_sym_kind = Conjecture,
297 prem_kind = Conjecture,
299 best_slices = fn ctxt =>
301 [(0.333, (false, (150, "poly_guards", sosN))),
302 (0.334, (true, (50, "mangled_guards?", no_sosN))),
303 (0.333, (false, (500, "mangled_tags?", sosN)))]
304 |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
307 val vampire = (vampireN, vampire_config)
310 (* Z3 with TPTP syntax *)
312 val z3_atp_config : atp_config =
313 {exec = ("Z3_HOME", "z3"),
315 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
316 "MBQI=true -p -t:" ^ string_of_int (to_secs 1 timeout),
319 [(Unprovable, "\nsat"),
320 (GaveUp, "\nunknown"),
321 (GaveUp, "SZS status Satisfiable"),
322 (ProofMissing, "\nunsat"),
323 (ProofMissing, "SZS status Unsatisfiable")],
324 conj_sym_kind = Hypothesis,
325 prem_kind = Hypothesis,
329 K [(0.5, (false, (250, "mangled_guards?", ""))),
330 (0.25, (false, (125, "mangled_guards?", ""))),
331 (0.125, (false, (62, "mangled_guards?", ""))),
332 (0.125, (false, (31, "mangled_guards?", "")))]}
334 val z3_atp = (z3_atpN, z3_atp_config)
337 (* Remote ATP invocation via SystemOnTPTP *)
339 val systems = Synchronized.var "atp_systems" ([] : string list)
342 case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
343 (output, 0) => split_lines output
345 error (case extract_known_failure known_perl_failures output of
346 SOME failure => string_for_failure failure
347 | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
349 fun find_system name [] systems =
350 find_first (String.isPrefix (name ^ "---")) systems
351 | find_system name (version :: versions) systems =
352 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
353 NONE => find_system name versions systems
356 fun get_system name versions =
357 Synchronized.change_result systems
358 (fn systems => (if null systems then get_systems () else systems)
359 |> `(`(find_system name versions)))
361 fun the_system name versions =
362 case get_system name versions of
364 | (NONE, []) => error ("SystemOnTPTP is currently not available.")
366 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
367 "(Available systems: " ^ commas_quote syss ^ ".)")
369 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
371 fun remote_config system_name system_versions proof_delims known_failures
372 conj_sym_kind prem_kind formats best_slice : atp_config =
373 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
375 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
376 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
377 ^ " -s " ^ the_system system_name system_versions,
378 proof_delims = union (op =) tstp_proof_delims proof_delims,
379 known_failures = known_failures @ known_perl_failures @
380 [(Unprovable, "says Satisfiable"),
381 (Unprovable, "says CounterSatisfiable"),
382 (GaveUp, "says Unknown"),
383 (GaveUp, "says GaveUp"),
384 (ProofMissing, "says Theorem"),
385 (ProofMissing, "says Unsatisfiable"),
386 (TimedOut, "says Timeout"),
387 (Inappropriate, "says Inappropriate")],
388 conj_sym_kind = conj_sym_kind,
389 prem_kind = prem_kind,
391 best_slices = fn ctxt =>
392 let val (max_relevant, type_enc) = best_slice ctxt in
393 [(1.0, (false, (max_relevant, type_enc, "")))]
396 fun remotify_config system_name system_versions best_slice
397 ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...}
398 : atp_config) : atp_config =
399 remote_config system_name system_versions proof_delims known_failures
400 conj_sym_kind prem_kind formats best_slice
402 fun remote_atp name system_name system_versions proof_delims known_failures
403 conj_sym_kind prem_kind formats best_slice =
404 (remote_prefix ^ name,
405 remote_config system_name system_versions proof_delims known_failures
406 conj_sym_kind prem_kind formats best_slice)
407 fun remotify_atp (name, config) system_name system_versions best_slice =
408 (remote_prefix ^ name,
409 remotify_config system_name system_versions best_slice config)
412 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
413 (K (750, "mangled_tags?") (* FUDGE *))
415 remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
416 (K (200, "mangled_guards?") (* FUDGE *))
418 remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
420 remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
421 (K (100, "simple_higher") (* FUDGE *))
422 val remote_satallax =
423 remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
424 (K (64, "simple_higher") (* FUDGE *))
426 remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
427 Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
429 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
430 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
431 [TFF, FOF] (K (100, "simple") (* FUDGE *))
433 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
434 Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
435 val remote_waldmeister =
436 remote_atp waldmeisterN "Waldmeister" ["710"]
437 [("#START OF PROOF", "Proved Goals:")]
438 [(OutOfResources, "Too many function symbols"),
439 (Crashed, "Unrecoverable Segmentation Fault")]
440 Hypothesis Hypothesis [CNF_UEQ]
441 (K (50, "mangled_tags?") (* FUDGE *))
445 fun add_atp (name, config) thy =
446 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
447 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
449 fun get_atp thy name =
450 the (Symtab.lookup (Data.get thy) name) |> fst
451 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
453 val supported_atps = Symtab.keys o Data.get
455 fun is_atp_installed thy name =
456 let val {exec, required_execs, ...} = get_atp thy name in
457 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
460 fun refresh_systems_on_tptp () =
461 Synchronized.change systems (fn _ => get_systems ())
464 [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
465 remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
467 val setup = fold add_atp atps