|
1 (* Title: HOL/Tools/SMT2/smt2_solver.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 SMT solvers registry and SMT tactic. |
|
5 *) |
|
6 |
|
7 signature SMT2_SOLVER = |
|
8 sig |
|
9 (*configuration*) |
|
10 datatype outcome = Unsat | Sat | Unknown |
|
11 type solver_config = { |
|
12 name: string, |
|
13 class: Proof.context -> SMT2_Utils.class, |
|
14 avail: unit -> bool, |
|
15 command: unit -> string list, |
|
16 options: Proof.context -> string list, |
|
17 default_max_relevant: int, |
|
18 supports_filter: bool, |
|
19 outcome: string -> string list -> outcome * string list, |
|
20 cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> |
|
21 term list * term list) option, |
|
22 replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option } |
|
23 |
|
24 (*registry*) |
|
25 val add_solver: solver_config -> theory -> theory |
|
26 val solver_name_of: Proof.context -> string |
|
27 val available_solvers_of: Proof.context -> string list |
|
28 val apply_solver: Proof.context -> (int * (int option * thm)) list -> |
|
29 int list * thm |
|
30 val default_max_relevant: Proof.context -> string -> int |
|
31 |
|
32 (*filter*) |
|
33 type 'a smt2_filter_data = |
|
34 ('a * thm) list * ((int * thm) list * Proof.context) |
|
35 val smt2_filter_preprocess: Proof.context -> thm list -> thm -> |
|
36 ('a * (int option * thm)) list -> int -> 'a smt2_filter_data |
|
37 val smt2_filter_apply: Time.time -> 'a smt2_filter_data -> |
|
38 {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list} |
|
39 |
|
40 (*tactic*) |
|
41 val smt2_tac: Proof.context -> thm list -> int -> tactic |
|
42 val smt2_tac': Proof.context -> thm list -> int -> tactic |
|
43 end |
|
44 |
|
45 structure SMT2_Solver: SMT2_SOLVER = |
|
46 struct |
|
47 |
|
48 |
|
49 (* interface to external solvers *) |
|
50 |
|
51 local |
|
52 |
|
53 fun make_cmd command options problem_path proof_path = space_implode " " ( |
|
54 "(exec 2>&1;" :: map File.shell_quote (command @ options) @ |
|
55 [File.shell_path problem_path, ")", ">", File.shell_path proof_path]) |
|
56 |
|
57 fun trace_and ctxt msg f x = |
|
58 let val _ = SMT2_Config.trace_msg ctxt (fn () => msg) () |
|
59 in f x end |
|
60 |
|
61 fun run ctxt name mk_cmd input = |
|
62 (case SMT2_Config.certificates_of ctxt of |
|
63 NONE => |
|
64 if not (SMT2_Config.is_available ctxt name) then |
|
65 error ("The SMT solver " ^ quote name ^ " is not installed.") |
|
66 else if Config.get ctxt SMT2_Config.debug_files = "" then |
|
67 trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") |
|
68 (Cache_IO.run mk_cmd) input |
|
69 else |
|
70 let |
|
71 val base_path = Path.explode (Config.get ctxt SMT2_Config.debug_files) |
|
72 val in_path = Path.ext "smt2_in" base_path |
|
73 val out_path = Path.ext "smt2_out" base_path |
|
74 in Cache_IO.raw_run mk_cmd input in_path out_path end |
|
75 | SOME certs => |
|
76 (case Cache_IO.lookup certs input of |
|
77 (NONE, key) => |
|
78 if Config.get ctxt SMT2_Config.read_only_certificates then |
|
79 error ("Bad certificate cache: missing certificate") |
|
80 else |
|
81 Cache_IO.run_and_cache certs key mk_cmd input |
|
82 | (SOME output, _) => |
|
83 trace_and ctxt ("Using cached certificate from " ^ |
|
84 File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") |
|
85 I output)) |
|
86 |
|
87 fun run_solver ctxt name mk_cmd input = |
|
88 let |
|
89 fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
90 (map Pretty.str ls)) |
|
91 |
|
92 val _ = SMT2_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input |
|
93 |
|
94 val {redirected_output=res, output=err, return_code} = |
|
95 SMT2_Config.with_timeout ctxt (run ctxt name mk_cmd) input |
|
96 val _ = SMT2_Config.trace_msg ctxt (pretty "Solver:") err |
|
97 |
|
98 val output = fst (take_suffix (equal "") res) |
|
99 val _ = SMT2_Config.trace_msg ctxt (pretty "Result:") output |
|
100 |
|
101 val _ = return_code <> 0 andalso |
|
102 raise SMT2_Failure.SMT (SMT2_Failure.Abnormal_Termination return_code) |
|
103 in output end |
|
104 |
|
105 fun trace_assms ctxt = |
|
106 SMT2_Config.trace_msg ctxt (Pretty.string_of o |
|
107 Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) |
|
108 |
|
109 fun trace_replay_data ({context=ctxt, typs, terms, ...} : SMT2_Translate.replay_data) = |
|
110 let |
|
111 fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] |
|
112 fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) |
|
113 fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
|
114 in |
|
115 SMT2_Config.trace_msg ctxt (fn () => |
|
116 Pretty.string_of (Pretty.big_list "Names:" [ |
|
117 Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), |
|
118 Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () |
|
119 end |
|
120 |
|
121 in |
|
122 |
|
123 fun invoke name command ithms ctxt = |
|
124 let |
|
125 val options = SMT2_Config.solver_options_of ctxt |
|
126 val cmd = command () |
|
127 val comments = [space_implode " " (cmd @ options)] |
|
128 |
|
129 val (str, replay_data as {context=ctxt', ...}) = |
|
130 ithms |
|
131 |> tap (trace_assms ctxt) |
|
132 |> SMT2_Translate.translate ctxt comments |
|
133 ||> tap trace_replay_data |
|
134 in (run_solver ctxt' name (make_cmd cmd options) str, replay_data) end |
|
135 |
|
136 end |
|
137 |
|
138 |
|
139 (* configuration *) |
|
140 |
|
141 datatype outcome = Unsat | Sat | Unknown |
|
142 |
|
143 type solver_config = { |
|
144 name: string, |
|
145 class: Proof.context -> SMT2_Utils.class, |
|
146 avail: unit -> bool, |
|
147 command: unit -> string list, |
|
148 options: Proof.context -> string list, |
|
149 default_max_relevant: int, |
|
150 supports_filter: bool, |
|
151 outcome: string -> string list -> outcome * string list, |
|
152 cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> |
|
153 term list * term list) option, |
|
154 replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option } |
|
155 |
|
156 |
|
157 (* registry *) |
|
158 |
|
159 type solver_info = { |
|
160 command: unit -> string list, |
|
161 default_max_relevant: int, |
|
162 supports_filter: bool, |
|
163 replay: Proof.context -> string list * SMT2_Translate.replay_data -> int list * thm } |
|
164 |
|
165 structure Solvers = Generic_Data |
|
166 ( |
|
167 type T = solver_info Symtab.table |
|
168 val empty = Symtab.empty |
|
169 val extend = I |
|
170 fun merge data = Symtab.merge (K true) data |
|
171 ) |
|
172 |
|
173 local |
|
174 fun finish outcome cex_parser replay ocl outer_ctxt |
|
175 (output, (replay_data as {context=ctxt, ...} : SMT2_Translate.replay_data)) = |
|
176 (case outcome output of |
|
177 (Unsat, ls) => |
|
178 if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay |
|
179 then the replay outer_ctxt replay_data ls |
|
180 else ([], ocl ()) |
|
181 | (result, ls) => |
|
182 let |
|
183 val (ts, us) = |
|
184 (case cex_parser of SOME f => f ctxt replay_data ls | _ => ([], [])) |
|
185 in |
|
186 raise SMT2_Failure.SMT (SMT2_Failure.Counterexample { |
|
187 is_real_cex = (result = Sat), |
|
188 free_constraints = ts, |
|
189 const_defs = us}) |
|
190 end) |
|
191 |
|
192 val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False}) |
|
193 in |
|
194 |
|
195 fun add_solver cfg = |
|
196 let |
|
197 val {name, class, avail, command, options, default_max_relevant, |
|
198 supports_filter, outcome, cex_parser, replay} = cfg |
|
199 |
|
200 fun core_oracle () = cfalse |
|
201 |
|
202 fun solver ocl = { |
|
203 command = command, |
|
204 default_max_relevant = default_max_relevant, |
|
205 supports_filter = supports_filter, |
|
206 replay = finish (outcome name) cex_parser replay ocl } |
|
207 |
|
208 val info = {name=name, class=class, avail=avail, options=options} |
|
209 in |
|
210 Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => |
|
211 Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> |
|
212 Context.theory_map (SMT2_Config.add_solver info) |
|
213 end |
|
214 |
|
215 end |
|
216 |
|
217 fun get_info ctxt name = |
|
218 the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) |
|
219 |
|
220 val solver_name_of = SMT2_Config.solver_of |
|
221 |
|
222 val available_solvers_of = SMT2_Config.available_solvers_of |
|
223 |
|
224 fun name_and_info_of ctxt = |
|
225 let val name = solver_name_of ctxt |
|
226 in (name, get_info ctxt name) end |
|
227 |
|
228 fun gen_preprocess ctxt iwthms = SMT2_Normalize.normalize iwthms ctxt |
|
229 |
|
230 fun gen_apply (ithms, ctxt) = |
|
231 let val (name, {command, replay, ...}) = name_and_info_of ctxt |
|
232 in |
|
233 (ithms, ctxt) |
|
234 |-> invoke name command |
|
235 |> replay ctxt |
|
236 |>> distinct (op =) |
|
237 end |
|
238 |
|
239 fun apply_solver ctxt = gen_apply o gen_preprocess ctxt |
|
240 |
|
241 val default_max_relevant = #default_max_relevant oo get_info |
|
242 |
|
243 val supports_filter = #supports_filter o snd o name_and_info_of |
|
244 |
|
245 |
|
246 (* check well-sortedness *) |
|
247 |
|
248 val has_topsort = Term.exists_type (Term.exists_subtype (fn |
|
249 TFree (_, []) => true |
|
250 | TVar (_, []) => true |
|
251 | _ => false)) |
|
252 |
|
253 (* without this test, we would run into problems when atomizing the rules: *) |
|
254 fun check_topsort ctxt thm = |
|
255 if has_topsort (Thm.prop_of thm) then |
|
256 (SMT2_Normalize.drop_fact_warning ctxt thm; TrueI) |
|
257 else |
|
258 thm |
|
259 |
|
260 fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms |
|
261 |
|
262 |
|
263 (* filter *) |
|
264 |
|
265 val cnot = Thm.cterm_of @{theory} @{const Not} |
|
266 |
|
267 fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } |
|
268 |
|
269 type 'a smt2_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) |
|
270 |
|
271 fun smt2_filter_preprocess ctxt facts goal xwthms i = |
|
272 let |
|
273 val ctxt = |
|
274 ctxt |
|
275 |> Config.put SMT2_Config.oracle false |
|
276 |> Config.put SMT2_Config.filter_only_facts true |
|
277 |
|
278 val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
|
279 fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply |
|
280 val cprop = |
|
281 (case try negate (Thm.rhs_of (SMT2_Normalize.atomize_conv ctxt' concl)) of |
|
282 SOME ct => ct |
|
283 | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ( |
|
284 "goal is not a HOL term"))) |
|
285 in |
|
286 map snd xwthms |
|
287 |> map_index I |
|
288 |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) |
|
289 |> check_topsorts ctxt' |
|
290 |> gen_preprocess ctxt' |
|
291 |> pair (map (apsnd snd) xwthms) |
|
292 end |
|
293 |
|
294 fun smt2_filter_apply time_limit (xthms, (ithms, ctxt)) = |
|
295 let |
|
296 val ctxt' = |
|
297 ctxt |
|
298 |> Config.put SMT2_Config.timeout (Time.toReal time_limit) |
|
299 |
|
300 fun filter_thms false = K xthms |
|
301 | filter_thms true = map_filter (try (nth xthms)) o fst |
|
302 in |
|
303 (ithms, ctxt') |
|
304 |> gen_apply |
|
305 |> filter_thms (supports_filter ctxt') |
|
306 |> mk_result NONE |
|
307 end |
|
308 handle SMT2_Failure.SMT fail => mk_result (SOME fail) [] |
|
309 |
|
310 |
|
311 (* SMT tactic *) |
|
312 |
|
313 local |
|
314 fun trace_assumptions ctxt iwthms idxs = |
|
315 let |
|
316 val wthms = |
|
317 idxs |
|
318 |> filter (fn i => i >= 0) |
|
319 |> map_filter (AList.lookup (op =) iwthms) |
|
320 in |
|
321 if Config.get ctxt SMT2_Config.trace_used_facts andalso length wthms > 0 |
|
322 then |
|
323 tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" |
|
324 (map (Display.pretty_thm ctxt o snd) wthms))) |
|
325 else () |
|
326 end |
|
327 |
|
328 fun solve ctxt iwthms = |
|
329 iwthms |
|
330 |> check_topsorts ctxt |
|
331 |> apply_solver ctxt |
|
332 |>> trace_assumptions ctxt iwthms |
|
333 |> snd |
|
334 |
|
335 fun str_of ctxt fail = |
|
336 SMT2_Failure.string_of_failure ctxt fail |
|
337 |> prefix ("Solver " ^ SMT2_Config.solver_of ctxt ^ ": ") |
|
338 |
|
339 fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) |
|
340 handle |
|
341 SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) => |
|
342 (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) |
|
343 | SMT2_Failure.SMT (fail as SMT2_Failure.Time_Out) => |
|
344 error ("SMT: Solver " ^ quote (SMT2_Config.solver_of ctxt) ^ ": " ^ |
|
345 SMT2_Failure.string_of_failure ctxt fail ^ " (setting the " ^ |
|
346 "configuration option " ^ quote (Config.name_of SMT2_Config.timeout) ^ " might help)") |
|
347 | SMT2_Failure.SMT fail => error (str_of ctxt fail) |
|
348 |
|
349 fun tag_rules thms = map_index (apsnd (pair NONE)) thms |
|
350 fun tag_prems thms = map (pair ~1 o pair NONE) thms |
|
351 |
|
352 fun resolve (SOME thm) = rtac thm 1 |
|
353 | resolve NONE = no_tac |
|
354 |
|
355 fun tac prove ctxt rules = |
|
356 CONVERSION (SMT2_Normalize.atomize_conv ctxt) |
|
357 THEN' rtac @{thm ccontr} |
|
358 THEN' SUBPROOF (fn {context, prems, ...} => |
|
359 resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt |
|
360 in |
|
361 |
|
362 val smt2_tac = tac safe_solve |
|
363 val smt2_tac' = tac (SOME oo solve) |
|
364 |
|
365 end |
|
366 |
|
367 end |