1 (* Title: HOL/Tools/ATP_Manager/atp_systems.ML |
|
2 Author: Fabian Immler, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Setup for supported ATPs. |
|
6 *) |
|
7 |
|
8 signature ATP_SYSTEMS = |
|
9 sig |
|
10 datatype failure = |
|
11 Unprovable | IncompleteUnprovable | CantConnect | TimedOut | |
|
12 OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError |
|
13 |
|
14 type prover_config = |
|
15 {executable: string * string, |
|
16 required_executables: (string * string) list, |
|
17 arguments: bool -> Time.time -> string, |
|
18 proof_delims: (string * string) list, |
|
19 known_failures: (failure * string) list, |
|
20 max_new_relevant_facts_per_iter: int, |
|
21 prefers_theory_relevant: bool, |
|
22 explicit_forall: bool} |
|
23 |
|
24 val add_prover: string * prover_config -> theory -> theory |
|
25 val get_prover: theory -> string -> prover_config |
|
26 val available_atps: theory -> unit |
|
27 val refresh_systems_on_tptp : unit -> unit |
|
28 val default_atps_param_value : unit -> string |
|
29 val setup : theory -> theory |
|
30 end; |
|
31 |
|
32 structure ATP_Systems : ATP_SYSTEMS = |
|
33 struct |
|
34 |
|
35 (* prover configuration *) |
|
36 |
|
37 datatype failure = |
|
38 Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | |
|
39 OldSpass | MalformedInput | MalformedOutput | UnknownError |
|
40 |
|
41 type prover_config = |
|
42 {executable: string * string, |
|
43 required_executables: (string * string) list, |
|
44 arguments: bool -> Time.time -> string, |
|
45 proof_delims: (string * string) list, |
|
46 known_failures: (failure * string) list, |
|
47 max_new_relevant_facts_per_iter: int, |
|
48 prefers_theory_relevant: bool, |
|
49 explicit_forall: bool} |
|
50 |
|
51 |
|
52 (* named provers *) |
|
53 |
|
54 structure Data = Theory_Data |
|
55 ( |
|
56 type T = (prover_config * stamp) Symtab.table |
|
57 val empty = Symtab.empty |
|
58 val extend = I |
|
59 fun merge data : T = Symtab.merge (eq_snd op =) data |
|
60 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
|
61 ) |
|
62 |
|
63 fun add_prover (name, config) thy = |
|
64 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
|
65 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") |
|
66 |
|
67 fun get_prover thy name = |
|
68 the (Symtab.lookup (Data.get thy) name) |> fst |
|
69 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") |
|
70 |
|
71 fun available_atps thy = |
|
72 priority ("Available ATPs: " ^ |
|
73 commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") |
|
74 |
|
75 fun available_atps thy = |
|
76 priority ("Available ATPs: " ^ |
|
77 commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") |
|
78 |
|
79 fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 |
|
80 |
|
81 (* E prover *) |
|
82 |
|
83 val tstp_proof_delims = |
|
84 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
|
85 |
|
86 val e_config : prover_config = |
|
87 {executable = ("E_HOME", "eproof"), |
|
88 required_executables = [], |
|
89 arguments = fn _ => fn timeout => |
|
90 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ |
|
91 string_of_int (to_generous_secs timeout), |
|
92 proof_delims = [tstp_proof_delims], |
|
93 known_failures = |
|
94 [(Unprovable, "SZS status: CounterSatisfiable"), |
|
95 (Unprovable, "SZS status CounterSatisfiable"), |
|
96 (TimedOut, "Failure: Resource limit exceeded (time)"), |
|
97 (TimedOut, "time limit exceeded"), |
|
98 (OutOfResources, |
|
99 "# Cannot determine problem status within resource limit"), |
|
100 (OutOfResources, "SZS status: ResourceOut"), |
|
101 (OutOfResources, "SZS status ResourceOut")], |
|
102 max_new_relevant_facts_per_iter = 80 (* FIXME *), |
|
103 prefers_theory_relevant = false, |
|
104 explicit_forall = false} |
|
105 val e = ("e", e_config) |
|
106 |
|
107 |
|
108 (* The "-VarWeight=3" option helps the higher-order problems, probably by |
|
109 counteracting the presence of "hAPP". *) |
|
110 val spass_config : prover_config = |
|
111 {executable = ("ISABELLE_ATP_MANAGER", "scripts/spass"), |
|
112 required_executables = [("SPASS_HOME", "SPASS")], |
|
113 (* "div 2" accounts for the fact that SPASS is often run twice. *) |
|
114 arguments = fn complete => fn timeout => |
|
115 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ |
|
116 \-VarWeight=3 -TimeLimit=" ^ |
|
117 string_of_int (to_generous_secs timeout div 2)) |
|
118 |> not complete ? prefix "-SOS=1 ", |
|
119 proof_delims = [("Here is a proof", "Formulae used in the proof")], |
|
120 known_failures = |
|
121 [(IncompleteUnprovable, "SPASS beiseite: Completion found"), |
|
122 (TimedOut, "SPASS beiseite: Ran out of time"), |
|
123 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), |
|
124 (MalformedInput, "Undefined symbol"), |
|
125 (MalformedInput, "Free Variable"), |
|
126 (OldSpass, "tptp2dfg")], |
|
127 max_new_relevant_facts_per_iter = 26 (* FIXME *), |
|
128 prefers_theory_relevant = true, |
|
129 explicit_forall = true} |
|
130 val spass = ("spass", spass_config) |
|
131 |
|
132 (* Vampire *) |
|
133 |
|
134 val vampire_config : prover_config = |
|
135 {executable = ("VAMPIRE_HOME", "vampire"), |
|
136 required_executables = [], |
|
137 arguments = fn _ => fn timeout => |
|
138 "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ |
|
139 " --input_file ", |
|
140 proof_delims = |
|
141 [("=========== Refutation ==========", |
|
142 "======= End of refutation ======="), |
|
143 ("% SZS output start Refutation", "% SZS output end Refutation"), |
|
144 ("% SZS output start Proof", "% SZS output end Proof")], |
|
145 known_failures = |
|
146 [(Unprovable, "UNPROVABLE"), |
|
147 (IncompleteUnprovable, "CANNOT PROVE"), |
|
148 (Unprovable, "Satisfiability detected"), |
|
149 (OutOfResources, "Refutation not found")], |
|
150 max_new_relevant_facts_per_iter = 40 (* FIXME *), |
|
151 prefers_theory_relevant = false, |
|
152 explicit_forall = false} |
|
153 val vampire = ("vampire", vampire_config) |
|
154 |
|
155 (* Remote prover invocation via SystemOnTPTP *) |
|
156 |
|
157 val systems = Synchronized.var "atp_systems" ([]: string list) |
|
158 |
|
159 fun get_systems () = |
|
160 case bash_output "\"$ISABELLE_ATP_MANAGER/scripts/remote_atp\" -w" of |
|
161 (answer, 0) => split_lines answer |
|
162 | (answer, _) => |
|
163 error ("Failed to get available systems at SystemOnTPTP:\n" ^ |
|
164 perhaps (try (unsuffix "\n")) answer) |
|
165 |
|
166 fun refresh_systems_on_tptp () = |
|
167 Synchronized.change systems (fn _ => get_systems ()) |
|
168 |
|
169 fun get_system prefix = Synchronized.change_result systems (fn systems => |
|
170 (if null systems then get_systems () else systems) |
|
171 |> `(find_first (String.isPrefix prefix))); |
|
172 |
|
173 fun the_system prefix = |
|
174 (case get_system prefix of |
|
175 NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.") |
|
176 | SOME sys => sys); |
|
177 |
|
178 val remote_known_failures = |
|
179 [(CantConnect, "HTTP-Error"), |
|
180 (TimedOut, "says Timeout"), |
|
181 (MalformedOutput, "Remote script could not extract proof")] |
|
182 |
|
183 fun remote_config atp_prefix |
|
184 ({proof_delims, known_failures, max_new_relevant_facts_per_iter, |
|
185 prefers_theory_relevant, explicit_forall, ...} : prover_config) |
|
186 : prover_config = |
|
187 {executable = ("ISABELLE_ATP_MANAGER", "scripts/remote_atp"), |
|
188 required_executables = [], |
|
189 arguments = fn _ => fn timeout => |
|
190 " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ |
|
191 the_system atp_prefix, |
|
192 proof_delims = insert (op =) tstp_proof_delims proof_delims, |
|
193 known_failures = remote_known_failures @ known_failures, |
|
194 max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, |
|
195 prefers_theory_relevant = prefers_theory_relevant, |
|
196 explicit_forall = explicit_forall} |
|
197 |
|
198 val remote_name = prefix "remote_" |
|
199 |
|
200 fun remote_prover (name, config) atp_prefix = |
|
201 (remote_name name, remote_config atp_prefix config) |
|
202 |
|
203 val remote_e = remote_prover e "EP---" |
|
204 val remote_vampire = remote_prover vampire "Vampire---9" |
|
205 |
|
206 fun is_installed ({executable, required_executables, ...} : prover_config) = |
|
207 forall (curry (op <>) "" o getenv o fst) (executable :: required_executables) |
|
208 fun maybe_remote (name, config) = |
|
209 name |> not (is_installed config) ? remote_name |
|
210 |
|
211 fun default_atps_param_value () = |
|
212 space_implode " " ([maybe_remote e] @ |
|
213 (if is_installed (snd spass) then [fst spass] else []) @ |
|
214 [remote_name (fst vampire)]) |
|
215 |
|
216 val provers = [e, spass, vampire, remote_e, remote_vampire] |
|
217 val setup = fold add_prover provers |
|
218 |
|
219 end; |
|