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