|
1 (* Title: HOL/Tools/SMT/smt_translate.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Translate theorems into an SMT intermediate format and serialize them. |
|
5 *) |
|
6 |
|
7 signature SMT_TRANSLATE = |
|
8 sig |
|
9 (* intermediate term structure *) |
|
10 datatype squant = SForall | SExists |
|
11 datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
|
12 datatype sterm = |
|
13 SVar of int | |
|
14 SApp of string * sterm list | |
|
15 SLet of string * sterm * sterm | |
|
16 SQua of squant * string list * sterm spattern list * sterm |
|
17 |
|
18 (* configuration options *) |
|
19 type prefixes = {sort_prefix: string, func_prefix: string} |
|
20 type strict = { |
|
21 is_builtin_conn: string * typ -> bool, |
|
22 is_builtin_pred: string * typ -> bool, |
|
23 is_builtin_distinct: bool} |
|
24 type builtins = { |
|
25 builtin_typ: typ -> string option, |
|
26 builtin_num: typ -> int -> string option, |
|
27 builtin_fun: string * typ -> term list -> (string * term list) option } |
|
28 datatype smt_theory = Integer | Real | Bitvector |
|
29 type sign = { |
|
30 theories: smt_theory list, |
|
31 sorts: string list, |
|
32 funcs: (string * (string list * string)) list } |
|
33 type config = { |
|
34 prefixes: prefixes, |
|
35 strict: strict option, |
|
36 builtins: builtins, |
|
37 serialize: string list -> sign -> sterm list -> string } |
|
38 type recon = { |
|
39 typs: typ Symtab.table, |
|
40 terms: term Symtab.table, |
|
41 unfolds: thm list, |
|
42 assms: thm list option } |
|
43 |
|
44 val translate: config -> Proof.context -> string list -> thm list -> |
|
45 string * recon |
|
46 end |
|
47 |
|
48 structure SMT_Translate: SMT_TRANSLATE = |
|
49 struct |
|
50 |
|
51 (* intermediate term structure *) |
|
52 |
|
53 datatype squant = SForall | SExists |
|
54 |
|
55 datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
|
56 |
|
57 datatype sterm = |
|
58 SVar of int | |
|
59 SApp of string * sterm list | |
|
60 SLet of string * sterm * sterm | |
|
61 SQua of squant * string list * sterm spattern list * sterm |
|
62 |
|
63 |
|
64 |
|
65 (* configuration options *) |
|
66 |
|
67 type prefixes = {sort_prefix: string, func_prefix: string} |
|
68 |
|
69 type strict = { |
|
70 is_builtin_conn: string * typ -> bool, |
|
71 is_builtin_pred: string * typ -> bool, |
|
72 is_builtin_distinct: bool} |
|
73 |
|
74 type builtins = { |
|
75 builtin_typ: typ -> string option, |
|
76 builtin_num: typ -> int -> string option, |
|
77 builtin_fun: string * typ -> term list -> (string * term list) option } |
|
78 |
|
79 datatype smt_theory = Integer | Real | Bitvector |
|
80 |
|
81 type sign = { |
|
82 theories: smt_theory list, |
|
83 sorts: string list, |
|
84 funcs: (string * (string list * string)) list } |
|
85 |
|
86 type config = { |
|
87 prefixes: prefixes, |
|
88 strict: strict option, |
|
89 builtins: builtins, |
|
90 serialize: string list -> sign -> sterm list -> string } |
|
91 |
|
92 type recon = { |
|
93 typs: typ Symtab.table, |
|
94 terms: term Symtab.table, |
|
95 unfolds: thm list, |
|
96 assms: thm list option } |
|
97 |
|
98 |
|
99 |
|
100 (* utility functions *) |
|
101 |
|
102 val dest_funT = |
|
103 let |
|
104 fun dest Ts 0 T = (rev Ts, T) |
|
105 | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U |
|
106 | dest _ _ T = raise TYPE ("dest_funT", [T], []) |
|
107 in dest [] end |
|
108 |
|
109 val quantifier = (fn |
|
110 @{const_name All} => SOME SForall |
|
111 | @{const_name Ex} => SOME SExists |
|
112 | _ => NONE) |
|
113 |
|
114 fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = |
|
115 if q = qname then group_quant qname (T :: Ts) u else (Ts, t) |
|
116 | group_quant _ Ts t = (Ts, t) |
|
117 |
|
118 fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts)) |
|
119 | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts)) |
|
120 | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p |
|
121 | dest_pat _ t = raise TERM ("dest_pat", [t]) |
|
122 |
|
123 fun dest_trigger (@{term trigger} $ tl $ t) = |
|
124 (map (dest_pat []) (HOLogic.dest_list tl), t) |
|
125 | dest_trigger t = ([], t) |
|
126 |
|
127 fun dest_quant qn T t = quantifier qn |> Option.map (fn q => |
|
128 let |
|
129 val (Ts, u) = group_quant qn [T] t |
|
130 val (ps, b) = dest_trigger u |
|
131 in (q, rev Ts, ps, b) end) |
|
132 |
|
133 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
|
134 | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
|
135 |
|
136 fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm) |
|
137 |
|
138 |
|
139 |
|
140 (* enforce a strict separation between formulas and terms *) |
|
141 |
|
142 val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)} |
|
143 |
|
144 val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)} |
|
145 val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool |
|
146 |
|
147 |
|
148 val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn |
|
149 Const (@{const_name Let}, _) => true |
|
150 | @{term "op = :: bool => _"} $ _ $ @{term True} => true |
|
151 | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true |
|
152 | _ => false) |
|
153 |
|
154 val rewrite_rules = [ |
|
155 Let_def, |
|
156 @{lemma "P = True == P" by (rule eq_reflection) simp}, |
|
157 @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] |
|
158 |
|
159 fun rewrite ctxt = Simplifier.full_rewrite |
|
160 (Simplifier.context ctxt empty_ss addsimps rewrite_rules) |
|
161 |
|
162 fun normalize ctxt thm = |
|
163 if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm |
|
164 |
|
165 val unfold_rules = term_eq_rewr :: rewrite_rules |
|
166 |
|
167 |
|
168 val revert_types = |
|
169 let |
|
170 fun revert @{typ prop} = @{typ bool} |
|
171 | revert (Type (n, Ts)) = Type (n, map revert Ts) |
|
172 | revert T = T |
|
173 in Term.map_types revert end |
|
174 |
|
175 |
|
176 fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt = |
|
177 let |
|
178 |
|
179 fun is_builtin_conn' (@{const_name True}, _) = false |
|
180 | is_builtin_conn' (@{const_name False}, _) = false |
|
181 | is_builtin_conn' c = is_builtin_conn c |
|
182 |
|
183 val propT = @{typ prop} and boolT = @{typ bool} |
|
184 val as_propT = (fn @{typ bool} => propT | T => T) |
|
185 fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T) |
|
186 fun conn (n, T) = (n, mapTs as_propT as_propT T) |
|
187 fun pred (n, T) = (n, mapTs I as_propT T) |
|
188 |
|
189 val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred |
|
190 fun as_term t = Const term_eq $ t $ @{term True} |
|
191 |
|
192 val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT) |
|
193 fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False} |
|
194 |
|
195 fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) |
|
196 |
|
197 fun in_term t = |
|
198 (case Term.strip_comb t of |
|
199 (c as Const (@{const_name If}, _), [t1, t2, t3]) => |
|
200 c $ in_form t1 $ in_term t2 $ in_term t3 |
|
201 | (h as Const c, ts) => |
|
202 if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c) |
|
203 then wrap_in_if (in_form t) |
|
204 else Term.list_comb (h, map in_term ts) |
|
205 | (h as Free _, ts) => Term.list_comb (h, map in_term ts) |
|
206 | _ => t) |
|
207 |
|
208 and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t |
|
209 | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t |
|
210 | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) = |
|
211 c $ in_pat p $ in_term t |
|
212 | in_pat t = raise TERM ("in_pat", [t]) |
|
213 |
|
214 and in_pats p = in_list @{typ pattern} in_pat p |
|
215 |
|
216 and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t |
|
217 | in_trig t = in_form t |
|
218 |
|
219 and in_form t = |
|
220 (case Term.strip_comb t of |
|
221 (q as Const (qn, _), [Abs (n, T, t')]) => |
|
222 if is_some (quantifier qn) then q $ Abs (n, T, in_trig t') |
|
223 else as_term (in_term t) |
|
224 | (Const (c as (@{const_name distinct}, T)), [t']) => |
|
225 if is_builtin_distinct then Const (pred c) $ in_list T in_term t' |
|
226 else as_term (in_term t) |
|
227 | (Const c, ts) => |
|
228 if is_builtin_conn (conn c) |
|
229 then Term.list_comb (Const (conn c), map in_form ts) |
|
230 else if is_builtin_pred (pred c) |
|
231 then Term.list_comb (Const (pred c), map in_term ts) |
|
232 else as_term (in_term t) |
|
233 | _ => as_term (in_term t)) |
|
234 in |
|
235 map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms), |
|
236 map (in_form o prop_of) (term_bool :: thms))) |
|
237 end |
|
238 |
|
239 |
|
240 |
|
241 (* translation from Isabelle terms into SMT intermediate terms *) |
|
242 |
|
243 val empty_context = (1, Typtab.empty, 1, Termtab.empty, []) |
|
244 |
|
245 fun make_sign (_, typs, _, terms, thys) = { |
|
246 theories = thys, |
|
247 sorts = Typtab.fold (cons o snd) typs [], |
|
248 funcs = Termtab.fold (cons o snd) terms [] } |
|
249 |
|
250 fun make_recon (unfolds, assms) (_, typs, _, terms, _) = { |
|
251 typs = Symtab.make (map swap (Typtab.dest typs)), |
|
252 terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)), |
|
253 unfolds = unfolds, |
|
254 assms = SOME assms } |
|
255 |
|
256 fun string_of_index pre i = pre ^ string_of_int i |
|
257 |
|
258 fun add_theory T (Tidx, typs, idx, terms, thys) = |
|
259 let |
|
260 fun add @{typ int} = insert (op =) Integer |
|
261 | add @{typ real} = insert (op =) Real |
|
262 | add (Type (@{type_name word}, _)) = insert (op =) Bitvector |
|
263 | add (Type (_, Ts)) = fold add Ts |
|
264 | add _ = I |
|
265 in (Tidx, typs, idx, terms, add T thys) end |
|
266 |
|
267 fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) = |
|
268 (case Typtab.lookup typs T of |
|
269 SOME s => (s, cx) |
|
270 | NONE => |
|
271 let |
|
272 val s = string_of_index sort_prefix Tidx |
|
273 val typs' = Typtab.update (T, s) typs |
|
274 in (s, (Tidx+1, typs', idx, terms, thys)) end) |
|
275 |
|
276 fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) = |
|
277 (case Termtab.lookup terms t of |
|
278 SOME (f, _) => (f, cx) |
|
279 | NONE => |
|
280 let |
|
281 val f = string_of_index func_prefix idx |
|
282 val terms' = Termtab.update (revert_types t, (f, ss)) terms |
|
283 in (f, (Tidx, typs, idx+1, terms', thys)) end) |
|
284 |
|
285 fun relaxed thms = (([], thms), map prop_of thms) |
|
286 |
|
287 fun with_context f (ths, ts) = |
|
288 let val (us, context) = fold_map f ts empty_context |
|
289 in ((make_sign context, us), make_recon ths context) end |
|
290 |
|
291 |
|
292 fun translate {prefixes, strict, builtins, serialize} ctxt comments = |
|
293 let |
|
294 val {sort_prefix, func_prefix} = prefixes |
|
295 val {builtin_typ, builtin_num, builtin_fun} = builtins |
|
296 |
|
297 fun transT T = add_theory T #> |
|
298 (case builtin_typ T of |
|
299 SOME n => pair n |
|
300 | NONE => fresh_typ sort_prefix T) |
|
301 |
|
302 fun app n ts = SApp (n, ts) |
|
303 |
|
304 fun trans t = |
|
305 (case Term.strip_comb t of |
|
306 (Const (qn, _), [Abs (_, T, t1)]) => |
|
307 (case dest_quant qn T t1 of |
|
308 SOME (q, Ts, ps, b) => |
|
309 fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
|
310 trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) |
|
311 | NONE => raise TERM ("intermediate", [t])) |
|
312 | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
|
313 transT T ##>> trans t1 ##>> trans t2 #>> |
|
314 (fn ((U, u1), u2) => SLet (U, u1, u2)) |
|
315 | (h as Const (c as (@{const_name distinct}, T)), [t1]) => |
|
316 (case builtin_fun c (HOLogic.dest_list t1) of |
|
317 SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n |
|
318 | NONE => transs h T [t1]) |
|
319 | (h as Const (c as (_, T)), ts) => |
|
320 (case try HOLogic.dest_number t of |
|
321 SOME (T, i) => |
|
322 (case builtin_num T i of |
|
323 SOME n => add_theory T #> pair (SApp (n, [])) |
|
324 | NONE => transs t T []) |
|
325 | NONE => |
|
326 (case builtin_fun c ts of |
|
327 SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n |
|
328 | NONE => transs h T ts)) |
|
329 | (h as Free (_, T), ts) => transs h T ts |
|
330 | (Bound i, []) => pair (SVar i) |
|
331 | _ => raise TERM ("intermediate", [t])) |
|
332 |
|
333 and transs t T ts = |
|
334 let val (Us, U) = dest_funT (length ts) T |
|
335 in |
|
336 fold_map transT Us ##>> transT U #-> (fn Up => |
|
337 fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp) |
|
338 end |
|
339 in |
|
340 (if is_some strict then strictify (the strict) ctxt else relaxed) #> |
|
341 with_context trans #>> uncurry (serialize comments) |
|
342 end |
|
343 |
|
344 end |