1 (* Title: HOL/SMT/Tools/smt_solver.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 SMT solvers registry and SMT tactic. |
|
5 *) |
|
6 |
|
7 signature SMT_SOLVER = |
|
8 sig |
|
9 exception SMT of string |
|
10 exception SMT_COUNTEREXAMPLE of bool * term list |
|
11 |
|
12 type solver_config = { |
|
13 command: {env_var: string, remote_name: string option}, |
|
14 arguments: string list, |
|
15 interface: string list -> SMT_Translate.config, |
|
16 reconstruct: (string list * SMT_Translate.recon) -> Proof.context -> |
|
17 thm * Proof.context } |
|
18 |
|
19 (*options*) |
|
20 val timeout: int Config.T |
|
21 val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b |
|
22 val trace: bool Config.T |
|
23 val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit |
|
24 |
|
25 (*certificates*) |
|
26 val fixed_certificates: bool Config.T |
|
27 val select_certificates: string -> Context.generic -> Context.generic |
|
28 |
|
29 (*solvers*) |
|
30 type solver = Proof.context -> thm list -> thm |
|
31 type solver_info = Context.generic -> Pretty.T list |
|
32 val add_solver: string * (Proof.context -> solver_config) -> theory -> |
|
33 theory |
|
34 val all_solver_names_of: theory -> string list |
|
35 val add_solver_info: string * solver_info -> theory -> theory |
|
36 val solver_name_of: Context.generic -> string |
|
37 val select_solver: string -> Context.generic -> Context.generic |
|
38 val solver_of: Context.generic -> solver |
|
39 |
|
40 (*tactic*) |
|
41 val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic |
|
42 val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic |
|
43 |
|
44 (*setup*) |
|
45 val setup: theory -> theory |
|
46 val print_setup: Context.generic -> unit |
|
47 end |
|
48 |
|
49 structure SMT_Solver: SMT_SOLVER = |
|
50 struct |
|
51 |
|
52 exception SMT of string |
|
53 exception SMT_COUNTEREXAMPLE of bool * term list |
|
54 |
|
55 |
|
56 type solver_config = { |
|
57 command: {env_var: string, remote_name: string option}, |
|
58 arguments: string list, |
|
59 interface: string list -> SMT_Translate.config, |
|
60 reconstruct: (string list * SMT_Translate.recon) -> Proof.context -> |
|
61 thm * Proof.context } |
|
62 |
|
63 |
|
64 |
|
65 (* SMT options *) |
|
66 |
|
67 val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30) |
|
68 |
|
69 fun with_timeout ctxt f x = |
|
70 TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x |
|
71 handle TimeLimit.TimeOut => raise SMT "timeout" |
|
72 |
|
73 val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false) |
|
74 |
|
75 fun trace_msg ctxt f x = |
|
76 if Config.get ctxt trace then tracing (f x) else () |
|
77 |
|
78 |
|
79 |
|
80 (* SMT certificates *) |
|
81 |
|
82 val (fixed_certificates, setup_fixed_certificates) = |
|
83 Attrib.config_bool "smt_fixed" (K false) |
|
84 |
|
85 structure Certificates = Generic_Data |
|
86 ( |
|
87 type T = Cache_IO.cache option |
|
88 val empty = NONE |
|
89 val extend = I |
|
90 fun merge (s, _) = s |
|
91 ) |
|
92 |
|
93 fun select_certificates name = Certificates.put ( |
|
94 if name = "" then NONE |
|
95 else SOME (Cache_IO.make (Path.explode name))) |
|
96 |
|
97 |
|
98 |
|
99 (* interface to external solvers *) |
|
100 |
|
101 local |
|
102 |
|
103 fun choose {env_var, remote_name} = |
|
104 let |
|
105 val local_solver = getenv env_var |
|
106 val remote_solver = the_default "" remote_name |
|
107 val remote_url = getenv "REMOTE_SMT_URL" |
|
108 in |
|
109 if local_solver <> "" |
|
110 then |
|
111 (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ..."); |
|
112 [local_solver]) |
|
113 else if remote_solver <> "" |
|
114 then |
|
115 (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^ |
|
116 quote remote_url ^ " ..."); |
|
117 [getenv "REMOTE_SMT", remote_solver]) |
|
118 else error ("Undefined Isabelle environment variable: " ^ quote env_var) |
|
119 end |
|
120 |
|
121 fun make_cmd solver args problem_path proof_path = space_implode " " ( |
|
122 map File.shell_quote (solver @ args) @ |
|
123 [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
|
124 |
|
125 fun run ctxt cmd args input = |
|
126 (case Certificates.get (Context.Proof ctxt) of |
|
127 NONE => Cache_IO.run (make_cmd (choose cmd) args) input |
|
128 | SOME certs => |
|
129 (case Cache_IO.lookup certs input of |
|
130 (NONE, key) => |
|
131 if Config.get ctxt fixed_certificates |
|
132 then error ("Bad certificates cache: missing certificate") |
|
133 else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) |
|
134 input |
|
135 | (SOME output, _) => |
|
136 (tracing ("Using cached certificate from " ^ |
|
137 File.shell_path (Cache_IO.cache_path_of certs) ^ " ..."); |
|
138 output))) |
|
139 |
|
140 in |
|
141 |
|
142 fun run_solver ctxt cmd args input = |
|
143 let |
|
144 fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
145 (map Pretty.str ls)) |
|
146 |
|
147 val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input |
|
148 |
|
149 val (res, err) = with_timeout ctxt (run ctxt cmd args) input |
|
150 val _ = trace_msg ctxt (pretty "SMT solver:") err |
|
151 |
|
152 val ls = rev (dropwhile (equal "") (rev res)) |
|
153 val _ = trace_msg ctxt (pretty "SMT result:") ls |
|
154 in ls end |
|
155 |
|
156 end |
|
157 |
|
158 fun trace_recon_data ctxt {typs, terms, ...} = |
|
159 let |
|
160 fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] |
|
161 fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) |
|
162 fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
|
163 in |
|
164 trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [ |
|
165 Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)), |
|
166 Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) () |
|
167 end |
|
168 |
|
169 fun invoke translate_config command arguments thms ctxt = |
|
170 thms |
|
171 |> SMT_Translate.translate translate_config ctxt |
|
172 ||> tap (trace_recon_data ctxt) |
|
173 |>> run_solver ctxt command arguments |
|
174 |> rpair ctxt |
|
175 |
|
176 fun discharge_definitions thm = |
|
177 if Thm.nprems_of thm = 0 then thm |
|
178 else discharge_definitions (@{thm reflexive} RS thm) |
|
179 |
|
180 fun gen_solver name solver ctxt prems = |
|
181 let |
|
182 val {command, arguments, interface, reconstruct} = solver ctxt |
|
183 val comments = ("solver: " ^ name) :: |
|
184 ("timeout: " ^ string_of_int (Config.get ctxt timeout)) :: |
|
185 "arguments:" :: arguments |
|
186 in |
|
187 SMT_Additional_Facts.add_facts prems |
|
188 |> rpair ctxt |
|
189 |-> SMT_Normalize.normalize |
|
190 |-> invoke (interface comments) command arguments |
|
191 |-> reconstruct |
|
192 |-> (fn thm => fn ctxt' => thm |
|
193 |> singleton (ProofContext.export ctxt' ctxt) |
|
194 |> discharge_definitions) |
|
195 end |
|
196 |
|
197 |
|
198 |
|
199 (* solver store *) |
|
200 |
|
201 type solver = Proof.context -> thm list -> thm |
|
202 type solver_info = Context.generic -> Pretty.T list |
|
203 |
|
204 structure Solvers = Theory_Data |
|
205 ( |
|
206 type T = ((Proof.context -> solver_config) * solver_info) Symtab.table |
|
207 val empty = Symtab.empty |
|
208 val extend = I |
|
209 fun merge data = Symtab.merge (K true) data |
|
210 handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) |
|
211 ) |
|
212 |
|
213 val no_solver = "(none)" |
|
214 val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K [])) |
|
215 val all_solver_names_of = Symtab.keys o Solvers.get |
|
216 val lookup_solver = Symtab.lookup o Solvers.get |
|
217 fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i))) |
|
218 |
|
219 |
|
220 |
|
221 (* selected solver *) |
|
222 |
|
223 structure Selected_Solver = Generic_Data |
|
224 ( |
|
225 type T = string |
|
226 val empty = no_solver |
|
227 val extend = I |
|
228 fun merge (s, _) = s |
|
229 ) |
|
230 |
|
231 val solver_name_of = Selected_Solver.get |
|
232 |
|
233 fun select_solver name context = |
|
234 if is_none (lookup_solver (Context.theory_of context) name) |
|
235 then error ("SMT solver not registered: " ^ quote name) |
|
236 else Selected_Solver.map (K name) context |
|
237 |
|
238 fun raw_solver_of context name = |
|
239 (case lookup_solver (Context.theory_of context) name of |
|
240 NONE => error "No SMT solver selected" |
|
241 | SOME (s, _) => s) |
|
242 |
|
243 fun solver_of context = |
|
244 let val name = solver_name_of context |
|
245 in gen_solver name (raw_solver_of context name) end |
|
246 |
|
247 |
|
248 |
|
249 (* SMT tactic *) |
|
250 |
|
251 local |
|
252 fun pretty_cex ctxt (real, ex) = |
|
253 let |
|
254 val msg = if real then "SMT: counterexample found" |
|
255 else "SMT: potential counterexample found" |
|
256 in |
|
257 if null ex then msg ^ "." |
|
258 else Pretty.string_of (Pretty.big_list (msg ^ ":") |
|
259 (map (Syntax.pretty_term ctxt) ex)) |
|
260 end |
|
261 |
|
262 fun fail_tac f msg st = (f msg; Tactical.no_tac st) |
|
263 |
|
264 fun SAFE pass_exns tac ctxt i st = |
|
265 if pass_exns then tac ctxt i st |
|
266 else (tac ctxt i st |
|
267 handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st |
|
268 | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st) |
|
269 |
|
270 fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules |
|
271 |
|
272 val has_topsort = Term.exists_type (Term.exists_subtype (fn |
|
273 TFree (_, []) => true |
|
274 | TVar (_, []) => true |
|
275 | _ => false)) |
|
276 in |
|
277 fun smt_tac' pass_exns ctxt rules = |
|
278 Tactic.rtac @{thm ccontr} THEN' |
|
279 SUBPROOF (fn {context, prems, ...} => |
|
280 let val thms = rules @ prems |
|
281 in |
|
282 if exists (has_topsort o Thm.prop_of) thms |
|
283 then fail_tac (trace_msg context I) |
|
284 "SMT: proof state contains the universal sort {}" |
|
285 else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1 |
|
286 end) ctxt |
|
287 |
|
288 val smt_tac = smt_tac' false |
|
289 end |
|
290 |
|
291 val smt_method = |
|
292 Scan.optional Attrib.thms [] >> |
|
293 (fn thms => fn ctxt => METHOD (fn facts => |
|
294 HEADGOAL (smt_tac ctxt (thms @ facts)))) |
|
295 |
|
296 |
|
297 |
|
298 (* setup *) |
|
299 |
|
300 val setup = |
|
301 Attrib.setup (Binding.name "smt_solver") |
|
302 (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >> |
|
303 (Thm.declaration_attribute o K o select_solver)) |
|
304 "SMT solver configuration" #> |
|
305 setup_timeout #> |
|
306 setup_trace #> |
|
307 setup_fixed_certificates #> |
|
308 Attrib.setup (Binding.name "smt_certificates") |
|
309 (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >> |
|
310 (Thm.declaration_attribute o K o select_certificates)) |
|
311 "SMT certificates" #> |
|
312 Method.setup (Binding.name "smt") smt_method |
|
313 "Applies an SMT solver to the current goal." |
|
314 |
|
315 |
|
316 fun print_setup gen = |
|
317 let |
|
318 val t = string_of_int (Config.get_generic gen timeout) |
|
319 val names = sort_strings (all_solver_names_of (Context.theory_of gen)) |
|
320 val ns = if null names then [no_solver] else names |
|
321 val take_info = (fn (_, []) => NONE | info => SOME info) |
|
322 val infos = |
|
323 Context.theory_of gen |
|
324 |> Symtab.dest o Solvers.get |
|
325 |> map_filter (fn (n, (_, info)) => take_info (n, info gen)) |
|
326 |> sort (prod_ord string_ord (K EQUAL)) |
|
327 |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps) |
|
328 in |
|
329 Pretty.writeln (Pretty.big_list "SMT setup:" [ |
|
330 Pretty.str ("Current SMT solver: " ^ solver_name_of gen), |
|
331 Pretty.str_list "Available SMT solvers: " "" ns, |
|
332 Pretty.str ("Current timeout: " ^ t ^ " seconds"), |
|
333 Pretty.big_list "Solver-specific settings:" infos]) |
|
334 end |
|
335 |
|
336 val _ = OuterSyntax.improper_command "smt_status" |
|
337 "Show the available SMT solvers and the currently selected solver." |
|
338 OuterKeyword.diag |
|
339 (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => |
|
340 print_setup (Context.Proof (Toplevel.context_of state))))) |
|
341 |
|
342 end |
|