5 Setup for supported ATPs. |
5 Setup for supported ATPs. |
6 *) |
6 *) |
7 |
7 |
8 signature ATP_SYSTEMS = |
8 signature ATP_SYSTEMS = |
9 sig |
9 sig |
10 type tptp_format = ATP_Problem.tptp_format |
10 type atp_format = ATP_Problem.atp_format |
11 type formula_kind = ATP_Problem.formula_kind |
11 type formula_kind = ATP_Problem.formula_kind |
12 type failure = ATP_Proof.failure |
12 type failure = ATP_Proof.failure |
13 |
13 |
14 type atp_config = |
14 type atp_config = |
15 {exec : string * string, |
15 {exec : string * string, |
21 known_failures : (failure * string) list, |
21 known_failures : (failure * string) list, |
22 conj_sym_kind : formula_kind, |
22 conj_sym_kind : formula_kind, |
23 prem_kind : formula_kind, |
23 prem_kind : formula_kind, |
24 best_slices : |
24 best_slices : |
25 Proof.context |
25 Proof.context |
26 -> (real * (bool * (int * tptp_format * string * string))) list} |
26 -> (real * (bool * (int * atp_format * string * string))) list} |
27 |
27 |
28 val force_sos : bool Config.T |
28 val force_sos : bool Config.T |
29 val e_smartN : string |
29 val e_smartN : string |
30 val e_autoN : string |
30 val e_autoN : string |
31 val e_fun_weightN : string |
31 val e_fun_weightN : string |
44 val pffN : string |
44 val pffN : string |
45 val phfN : string |
45 val phfN : string |
46 val satallaxN : string |
46 val satallaxN : string |
47 val snarkN : string |
47 val snarkN : string |
48 val spassN : string |
48 val spassN : string |
|
49 val spass_newN : string |
49 val vampireN : string |
50 val vampireN : string |
50 val waldmeisterN : string |
51 val waldmeisterN : string |
51 val z3_tptpN : string |
52 val z3_tptpN : string |
52 val remote_prefix : string |
53 val remote_prefix : string |
53 val remote_atp : |
54 val remote_atp : |
54 string -> string -> string list -> (string * string) list |
55 string -> string -> string list -> (string * string) list |
55 -> (failure * string) list -> formula_kind -> formula_kind |
56 -> (failure * string) list -> formula_kind -> formula_kind |
56 -> (Proof.context -> int * tptp_format * string) -> string * atp_config |
57 -> (Proof.context -> int * atp_format * string) -> string * atp_config |
57 val add_atp : string * atp_config -> theory -> theory |
58 val add_atp : string * atp_config -> theory -> theory |
58 val get_atp : theory -> string -> atp_config |
59 val get_atp : theory -> string -> atp_config |
59 val supported_atps : theory -> string list |
60 val supported_atps : theory -> string list |
60 val is_atp_installed : theory -> string -> bool |
61 val is_atp_installed : theory -> string -> bool |
61 val refresh_systems_on_tptp : unit -> unit |
62 val refresh_systems_on_tptp : unit -> unit |
80 known_failures : (failure * string) list, |
81 known_failures : (failure * string) list, |
81 conj_sym_kind : formula_kind, |
82 conj_sym_kind : formula_kind, |
82 prem_kind : formula_kind, |
83 prem_kind : formula_kind, |
83 best_slices : |
84 best_slices : |
84 Proof.context |
85 Proof.context |
85 -> (real * (bool * (int * tptp_format * string * string))) list} |
86 -> (real * (bool * (int * atp_format * string * string))) list} |
86 |
87 |
87 (* "best_slices" must be found empirically, taking a wholistic approach since |
88 (* "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 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 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 component indicates whether the slice's strategy is complete; the "int", the |
128 val pffN = "pff" |
129 val pffN = "pff" |
129 val phfN = "phf" |
130 val phfN = "phf" |
130 val satallaxN = "satallax" |
131 val satallaxN = "satallax" |
131 val snarkN = "snark" |
132 val snarkN = "snark" |
132 val spassN = "spass" |
133 val spassN = "spass" |
|
134 val spass_newN = "spass_new" |
133 val vampireN = "vampire" |
135 val vampireN = "vampire" |
134 val waldmeisterN = "waldmeister" |
136 val waldmeisterN = "waldmeister" |
135 val z3_tptpN = "z3_tptp" |
137 val z3_tptpN = "z3_tptp" |
136 val remote_prefix = "remote_" |
138 val remote_prefix = "remote_" |
137 |
139 |
313 (TimedOut, "SPASS beiseite: Ran out of time"), |
315 (TimedOut, "SPASS beiseite: Ran out of time"), |
314 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
316 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
315 (MalformedInput, "Undefined symbol"), |
317 (MalformedInput, "Undefined symbol"), |
316 (MalformedInput, "Free Variable"), |
318 (MalformedInput, "Free Variable"), |
317 (Unprovable, "No formulae and clauses found in input file"), |
319 (Unprovable, "No formulae and clauses found in input file"), |
318 (SpassTooOld, "tptp2dfg"), |
|
319 (InternalError, "Please report this error")], |
320 (InternalError, "Please report this error")], |
320 conj_sym_kind = Hypothesis, |
321 conj_sym_kind = Hypothesis, |
321 prem_kind = Conjecture, |
322 prem_kind = Conjecture, |
322 best_slices = fn ctxt => |
323 best_slices = fn ctxt => |
323 (* FUDGE *) |
324 (* FUDGE *) |
326 (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))] |
327 (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))] |
327 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |
328 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |
328 else I)} |
329 else I)} |
329 |
330 |
330 val spass = (spassN, spass_config) |
331 val spass = (spassN, spass_config) |
|
332 |
|
333 (* Experimental *) |
|
334 val spass_new_config : atp_config = |
|
335 {exec = ("SPASS_HOME", "SPASS"), |
|
336 required_execs = [], |
|
337 arguments = #arguments spass_config, |
|
338 proof_delims = #proof_delims spass_config, |
|
339 known_failures = #known_failures spass_config, |
|
340 conj_sym_kind = #conj_sym_kind spass_config, |
|
341 prem_kind = #prem_kind spass_config, |
|
342 best_slices = fn ctxt => |
|
343 (* FUDGE *) |
|
344 [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*, |
|
345 (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))), |
|
346 (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)] |
|
347 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |
|
348 else I)} |
|
349 |
|
350 val spass_new = (spass_newN, spass_new_config) |
331 |
351 |
332 |
352 |
333 (* Vampire *) |
353 (* Vampire *) |
334 |
354 |
335 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on |
355 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on |
357 known_szs_status_failures @ |
377 known_szs_status_failures @ |
358 [(GaveUp, "UNPROVABLE"), |
378 [(GaveUp, "UNPROVABLE"), |
359 (GaveUp, "CANNOT PROVE"), |
379 (GaveUp, "CANNOT PROVE"), |
360 (Unprovable, "Satisfiability detected"), |
380 (Unprovable, "Satisfiability detected"), |
361 (Unprovable, "Termination reason: Satisfiable"), |
381 (Unprovable, "Termination reason: Satisfiable"), |
362 (VampireTooOld, "not a valid option"), |
|
363 (Interrupted, "Aborted by signal SIGINT")], |
382 (Interrupted, "Aborted by signal SIGINT")], |
364 conj_sym_kind = Conjecture, |
383 conj_sym_kind = Conjecture, |
365 prem_kind = Conjecture, |
384 prem_kind = Conjecture, |
366 best_slices = fn ctxt => |
385 best_slices = fn ctxt => |
367 (* FUDGE *) |
386 (* FUDGE *) |
543 |
562 |
544 fun refresh_systems_on_tptp () = |
563 fun refresh_systems_on_tptp () = |
545 Synchronized.change systems (fn _ => get_systems ()) |
564 Synchronized.change systems (fn _ => get_systems ()) |
546 |
565 |
547 val atps = |
566 val atps = |
548 [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, |
567 [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e, |
549 remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark, |
568 remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, |
550 remote_e_tofof, remote_waldmeister] |
569 remote_snark, remote_e_tofof, remote_waldmeister] |
551 val setup = fold add_atp atps |
570 val setup = fold add_atp atps |
552 |
571 |
553 end; |
572 end; |