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