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