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