4 Wrapper functions for external ATPs. |
4 Wrapper functions for external ATPs. |
5 *) |
5 *) |
6 |
6 |
7 signature ATP_WRAPPER = |
7 signature ATP_WRAPPER = |
8 sig |
8 sig |
9 (*hooks for problem files*) |
9 type prover = ATP_Manager.prover |
10 val destdir: string Config.T |
10 |
11 val problem_prefix: string Config.T |
11 (* hooks for problem files *) |
12 val measure_runtime: bool Config.T |
12 val destdir : string Config.T |
13 val setup: theory -> theory |
13 val problem_prefix : string Config.T |
14 |
14 val measure_runtime : bool Config.T |
15 (*prover configuration, problem format, and prover result*) |
15 |
16 type prover_config = |
16 val refresh_systems_on_tptp : unit -> unit |
17 {command: Path.T, |
17 val setup : theory -> theory |
18 arguments: int -> string, |
|
19 failure_strs: string list, |
|
20 max_new_clauses: int, |
|
21 insert_theory_const: bool, |
|
22 emit_structured_proof: bool} |
|
23 type problem = |
|
24 {with_full_types: bool, |
|
25 subgoal: int, |
|
26 goal: Proof.context * (thm list * thm), |
|
27 axiom_clauses: (thm * (string * int)) list option, |
|
28 filtered_clauses: (thm * (string * int)) list option} |
|
29 val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem |
|
30 type prover_result = |
|
31 {success: bool, |
|
32 message: string, |
|
33 theorem_names: string list, |
|
34 runtime: int, |
|
35 proof: string, |
|
36 internal_thm_names: string Vector.vector, |
|
37 filtered_clauses: (thm * (string * int)) list} |
|
38 type prover = int -> problem -> prover_result |
|
39 |
|
40 (*common provers*) |
|
41 val vampire: string * prover |
|
42 val vampire_full: string * prover |
|
43 val eprover: string * prover |
|
44 val eprover_full: string * prover |
|
45 val spass: string * prover |
|
46 val spass_no_tc: string * prover |
|
47 val remote_vampire: string * prover |
|
48 val remote_eprover: string * prover |
|
49 val remote_spass: string * prover |
|
50 val refresh_systems: unit -> unit |
|
51 end; |
18 end; |
52 |
19 |
53 structure ATP_Wrapper : ATP_WRAPPER = |
20 structure ATP_Wrapper : ATP_WRAPPER = |
54 struct |
21 struct |
55 |
22 |
56 open Sledgehammer_HOL_Clause |
23 open Sledgehammer_HOL_Clause |
57 open Sledgehammer_Fact_Filter |
24 open Sledgehammer_Fact_Filter |
58 open Sledgehammer_Proof_Reconstruct |
25 open Sledgehammer_Proof_Reconstruct |
|
26 open ATP_Manager |
59 |
27 |
60 (** generic ATP wrapper **) |
28 (** generic ATP wrapper **) |
61 |
29 |
62 (* external problem files *) |
30 (* external problem files *) |
63 |
31 |
68 Attrib.config_string "atp_problem_prefix" "prob"; |
36 Attrib.config_string "atp_problem_prefix" "prob"; |
69 |
37 |
70 val (measure_runtime, measure_runtime_setup) = |
38 val (measure_runtime, measure_runtime_setup) = |
71 Attrib.config_bool "atp_measure_runtime" false; |
39 Attrib.config_bool "atp_measure_runtime" false; |
72 |
40 |
73 val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup; |
41 |
74 |
42 (* prover configuration *) |
75 |
|
76 (* prover configuration, problem format, and prover result *) |
|
77 |
43 |
78 type prover_config = |
44 type prover_config = |
79 {command: Path.T, |
45 {command: Path.T, |
80 arguments: int -> string, |
46 arguments: int -> string, |
81 failure_strs: string list, |
47 failure_strs: string list, |
82 max_new_clauses: int, |
48 max_new_clauses: int, |
83 insert_theory_const: bool, |
49 insert_theory_const: bool, |
84 emit_structured_proof: bool}; |
50 emit_structured_proof: bool}; |
85 |
|
86 type problem = |
|
87 {with_full_types: bool, |
|
88 subgoal: int, |
|
89 goal: Proof.context * (thm list * thm), |
|
90 axiom_clauses: (thm * (string * int)) list option, |
|
91 filtered_clauses: (thm * (string * int)) list option}; |
|
92 |
|
93 fun problem_of_goal with_full_types subgoal goal : problem = |
|
94 {with_full_types = with_full_types, |
|
95 subgoal = subgoal, |
|
96 goal = goal, |
|
97 axiom_clauses = NONE, |
|
98 filtered_clauses = NONE}; |
|
99 |
|
100 type prover_result = |
|
101 {success: bool, |
|
102 message: string, |
|
103 theorem_names: string list, (*relevant theorems*) |
|
104 runtime: int, (*user time of the ATP, in milliseconds*) |
|
105 proof: string, |
|
106 internal_thm_names: string Vector.vector, |
|
107 filtered_clauses: (thm * (string * int)) list}; |
|
108 |
|
109 type prover = int -> problem -> prover_result; |
|
110 |
51 |
111 |
52 |
112 (* basic template *) |
53 (* basic template *) |
113 |
54 |
114 fun with_path cleanup after f path = |
55 fun with_path cleanup after f path = |
314 in |
255 in |
315 if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) |
256 if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) |
316 else split_lines answer |
257 else split_lines answer |
317 end; |
258 end; |
318 |
259 |
319 fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ()); |
260 fun refresh_systems_on_tptp () = |
|
261 Synchronized.change systems (fn _ => get_systems ()); |
320 |
262 |
321 fun get_system prefix = Synchronized.change_result systems (fn systems => |
263 fun get_system prefix = Synchronized.change_result systems (fn systems => |
322 (if null systems then get_systems () else systems) |
264 (if null systems then get_systems () else systems) |
323 |> `(find_first (String.isPrefix prefix))); |
265 |> `(find_first (String.isPrefix prefix))); |
324 |
266 |
345 "EP---" "" eprover_max_new_clauses eprover_insert_theory_const); |
287 "EP---" "" eprover_max_new_clauses eprover_insert_theory_const); |
346 |
288 |
347 val remote_spass = tptp_prover ("remote_spass", remote_prover_config |
289 val remote_spass = tptp_prover ("remote_spass", remote_prover_config |
348 "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const); |
290 "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const); |
349 |
291 |
|
292 val provers = |
|
293 [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc, |
|
294 remote_vampire, remote_spass, remote_eprover] |
|
295 val prover_setup = fold add_prover provers |
|
296 |
|
297 val setup = |
|
298 destdir_setup |
|
299 #> problem_prefix_setup |
|
300 #> measure_runtime_setup |
|
301 #> prover_setup; |
|
302 |
350 end; |
303 end; |