36898
|
1 |
(* Title: HOL/Tools/SMT/smtlib_interface.ML
|
|
2 |
Author: Sascha Boehme, TU Muenchen
|
|
3 |
|
|
4 |
Interface to SMT solvers based on the SMT-LIB format.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature SMTLIB_INTERFACE =
|
|
8 |
sig
|
|
9 |
val interface: SMT_Solver.interface
|
|
10 |
end
|
|
11 |
|
|
12 |
structure SMTLIB_Interface: SMTLIB_INTERFACE =
|
|
13 |
struct
|
|
14 |
|
|
15 |
structure N = SMT_Normalize
|
|
16 |
structure T = SMT_Translate
|
|
17 |
|
|
18 |
|
|
19 |
|
|
20 |
(** facts about uninterpreted constants **)
|
|
21 |
|
|
22 |
infix 2 ??
|
|
23 |
fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms
|
|
24 |
|
|
25 |
|
|
26 |
(* pairs *)
|
|
27 |
|
|
28 |
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
|
|
29 |
|
|
30 |
val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
|
|
31 |
val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
|
|
32 |
|
|
33 |
val add_pair_rules = exists_pair_type ?? append pair_rules
|
|
34 |
|
|
35 |
|
|
36 |
(* function update *)
|
|
37 |
|
|
38 |
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
|
|
39 |
|
|
40 |
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
|
|
41 |
val exists_fun_upd = Term.exists_subterm is_fun_upd
|
|
42 |
|
|
43 |
val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules
|
|
44 |
|
|
45 |
|
|
46 |
(* abs/min/max *)
|
|
47 |
|
|
48 |
val exists_abs_min_max = Term.exists_subterm (fn
|
|
49 |
Const (@{const_name abs}, _) => true
|
|
50 |
| Const (@{const_name min}, _) => true
|
|
51 |
| Const (@{const_name max}, _) => true
|
|
52 |
| _ => false)
|
|
53 |
|
|
54 |
val unfold_abs_conv = Conv.rewr_conv @{thm abs_if[THEN eq_reflection]}
|
|
55 |
val unfold_min_conv = Conv.rewr_conv @{thm min_def[THEN eq_reflection]}
|
|
56 |
val unfold_max_conv = Conv.rewr_conv @{thm max_def[THEN eq_reflection]}
|
|
57 |
|
|
58 |
fun expand_conv cv = N.eta_expand_conv (K cv)
|
|
59 |
fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv))
|
|
60 |
|
|
61 |
fun unfold_def_conv ctxt ct =
|
|
62 |
(case Thm.term_of ct of
|
|
63 |
Const (@{const_name abs}, _) $ _ => unfold_abs_conv
|
|
64 |
| Const (@{const_name abs}, _) => expand_conv unfold_abs_conv ctxt
|
|
65 |
| Const (@{const_name min}, _) $ _ $ _ => unfold_min_conv
|
|
66 |
| Const (@{const_name min}, _) $ _ => expand_conv unfold_min_conv ctxt
|
|
67 |
| Const (@{const_name min}, _) => expand2_conv unfold_min_conv ctxt
|
|
68 |
| Const (@{const_name max}, _) $ _ $ _ => unfold_max_conv
|
|
69 |
| Const (@{const_name max}, _) $ _ => expand_conv unfold_max_conv ctxt
|
|
70 |
| Const (@{const_name max}, _) => expand2_conv unfold_max_conv ctxt
|
|
71 |
| _ => Conv.all_conv) ct
|
|
72 |
|
|
73 |
fun unfold_abs_min_max_defs ctxt thm =
|
|
74 |
if exists_abs_min_max (Thm.prop_of thm)
|
|
75 |
then Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt) thm
|
|
76 |
else thm
|
|
77 |
|
|
78 |
|
|
79 |
(* include additional facts *)
|
|
80 |
|
|
81 |
fun extra_norm thms ctxt =
|
|
82 |
thms
|
|
83 |
|> add_pair_rules
|
|
84 |
|> add_fun_upd_rules
|
|
85 |
|> map (unfold_abs_min_max_defs ctxt)
|
|
86 |
|> rpair ctxt
|
|
87 |
|
|
88 |
|
|
89 |
|
|
90 |
(** builtins **)
|
|
91 |
|
|
92 |
fun dest_binT T =
|
|
93 |
(case T of
|
|
94 |
Type (@{type_name "Numeral_Type.num0"}, _) => 0
|
|
95 |
| Type (@{type_name "Numeral_Type.num1"}, _) => 1
|
|
96 |
| Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
|
|
97 |
| Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
|
|
98 |
| _ => raise TYPE ("dest_binT", [T], []))
|
|
99 |
|
|
100 |
fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
|
|
101 |
| dest_wordT T = raise TYPE ("dest_wordT", [T], [])
|
|
102 |
|
|
103 |
fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
|
|
104 |
fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
|
|
105 |
|
|
106 |
fun builtin_typ @{typ int} = SOME "Int"
|
|
107 |
| builtin_typ @{typ real} = SOME "Real"
|
|
108 |
| builtin_typ (Type (@{type_name word}, [T])) =
|
|
109 |
Option.map (index1 "BitVec") (try dest_binT T)
|
|
110 |
| builtin_typ _ = NONE
|
|
111 |
|
|
112 |
fun builtin_num @{typ int} i = SOME (string_of_int i)
|
|
113 |
| builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
|
|
114 |
| builtin_num (Type (@{type_name word}, [T])) i =
|
|
115 |
Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
|
|
116 |
| builtin_num _ _ = NONE
|
|
117 |
|
|
118 |
val is_propT = (fn @{typ prop} => true | _ => false)
|
|
119 |
fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
|
|
120 |
fun is_predT T = is_propT (Term.body_type T)
|
|
121 |
|
|
122 |
fun just c ts = SOME (c, ts)
|
|
123 |
|
|
124 |
val is_arith_type = member (op =) [@{typ int}, @{typ real}] o Term.domain_type
|
|
125 |
|
|
126 |
fun fixed_bvT (Ts, T) x =
|
|
127 |
if forall (can dest_wordT) (T :: Ts) then SOME x else NONE
|
|
128 |
|
|
129 |
fun if_fixed_bvT' T = fixed_bvT ([], Term.domain_type T)
|
|
130 |
fun if_fixed_bvT T = curry (fixed_bvT ([], Term.domain_type T))
|
|
131 |
fun if_full_fixed_bvT T = curry (fixed_bvT (Term.strip_type T))
|
|
132 |
|
|
133 |
fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
|
|
134 |
| dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
|
|
135 |
fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
|
|
136 |
| dest_nat ts = raise TERM ("dest_nat", ts)
|
|
137 |
fun dest_nat_word_funT (T, ts) =
|
|
138 |
(dest_word_funT (Term.range_type T), dest_nat ts)
|
|
139 |
|
|
140 |
fun bv_extend n T ts =
|
|
141 |
(case try dest_word_funT T of
|
|
142 |
SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
|
|
143 |
| _ => NONE)
|
|
144 |
|
|
145 |
fun bv_rotate n T ts =
|
|
146 |
try dest_nat ts
|
|
147 |
|> Option.map (fn (i, ts') => (index1 n i, ts'))
|
|
148 |
|
|
149 |
fun bv_extract n T ts =
|
|
150 |
try dest_nat_word_funT (T, ts)
|
|
151 |
|> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
|
|
152 |
|
|
153 |
|
|
154 |
fun conn @{const_name True} = SOME "true"
|
|
155 |
| conn @{const_name False} = SOME "false"
|
|
156 |
| conn @{const_name Not} = SOME "not"
|
|
157 |
| conn @{const_name "op &"} = SOME "and"
|
|
158 |
| conn @{const_name "op |"} = SOME "or"
|
|
159 |
| conn @{const_name "op -->"} = SOME "implies"
|
|
160 |
| conn @{const_name "op ="} = SOME "iff"
|
|
161 |
| conn @{const_name If} = SOME "if_then_else"
|
|
162 |
| conn _ = NONE
|
|
163 |
|
|
164 |
fun pred @{const_name distinct} _ = SOME "distinct"
|
|
165 |
| pred @{const_name "op ="} _ = SOME "="
|
|
166 |
| pred @{const_name term_eq} _ = SOME "="
|
|
167 |
| pred @{const_name less} T =
|
|
168 |
if is_arith_type T then SOME "<"
|
|
169 |
else if_fixed_bvT' T "bvult"
|
|
170 |
| pred @{const_name less_eq} T =
|
|
171 |
if is_arith_type T then SOME "<="
|
|
172 |
else if_fixed_bvT' T "bvule"
|
|
173 |
| pred @{const_name word_sless} T = if_fixed_bvT' T "bvslt"
|
|
174 |
| pred @{const_name word_sle} T = if_fixed_bvT' T "bvsle"
|
|
175 |
| pred _ _ = NONE
|
|
176 |
|
|
177 |
fun func @{const_name If} _ = just "ite"
|
|
178 |
| func @{const_name uminus} T =
|
|
179 |
if is_arith_type T then just "~"
|
|
180 |
else if_fixed_bvT T "bvneg"
|
|
181 |
| func @{const_name plus} T =
|
|
182 |
if is_arith_type T then just "+"
|
|
183 |
else if_fixed_bvT T "bvadd"
|
|
184 |
| func @{const_name minus} T =
|
|
185 |
if is_arith_type T then just "-"
|
|
186 |
else if_fixed_bvT T "bvsub"
|
|
187 |
| func @{const_name times} T =
|
|
188 |
if is_arith_type T then just "*"
|
|
189 |
else if_fixed_bvT T "bvmul"
|
|
190 |
| func @{const_name bitNOT} T = if_fixed_bvT T "bvnot"
|
|
191 |
| func @{const_name bitAND} T = if_fixed_bvT T "bvand"
|
|
192 |
| func @{const_name bitOR} T = if_fixed_bvT T "bvor"
|
|
193 |
| func @{const_name bitXOR} T = if_fixed_bvT T "bvxor"
|
|
194 |
| func @{const_name div} T = if_fixed_bvT T "bvudiv"
|
|
195 |
| func @{const_name mod} T = if_fixed_bvT T "bvurem"
|
|
196 |
| func @{const_name sdiv} T = if_fixed_bvT T "bvsdiv"
|
|
197 |
| func @{const_name smod} T = if_fixed_bvT T "bvsmod"
|
|
198 |
| func @{const_name srem} T = if_fixed_bvT T "bvsrem"
|
|
199 |
| func @{const_name word_cat} T = if_full_fixed_bvT T "concat"
|
|
200 |
| func @{const_name bv_shl} T = if_full_fixed_bvT T "bvshl"
|
|
201 |
| func @{const_name bv_lshr} T = if_full_fixed_bvT T "bvlshr"
|
|
202 |
| func @{const_name bv_ashr} T = if_full_fixed_bvT T "bvashr"
|
|
203 |
| func @{const_name slice} T = bv_extract "extract" T
|
|
204 |
| func @{const_name ucast} T = bv_extend "zero_extend" T
|
|
205 |
| func @{const_name scast} T = bv_extend "sign_extend" T
|
|
206 |
| func @{const_name word_rotl} T = bv_rotate "rotate_left" T
|
|
207 |
| func @{const_name word_rotr} T = bv_rotate "rotate_right" T
|
|
208 |
| func _ _ = K NONE
|
|
209 |
|
|
210 |
fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
|
|
211 |
fun is_builtin_pred (n, T) = is_predT T andalso is_some (pred n T)
|
|
212 |
|
|
213 |
fun builtin_fun (n, T) ts =
|
|
214 |
if is_connT T then conn n |> Option.map (rpair ts)
|
|
215 |
else if is_predT T then pred n T |> Option.map (rpair ts)
|
|
216 |
else func n T ts
|
|
217 |
|
|
218 |
|
|
219 |
|
|
220 |
(** serialization **)
|
|
221 |
|
|
222 |
val add = Buffer.add
|
|
223 |
fun sep f = add " " #> f
|
|
224 |
fun enclose l r f = sep (add l #> f #> add r)
|
|
225 |
val par = enclose "(" ")"
|
|
226 |
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
|
|
227 |
fun line f = f #> add "\n"
|
|
228 |
|
|
229 |
fun var i = add "?v" #> add (string_of_int i)
|
|
230 |
|
|
231 |
fun sterm l (T.SVar i) = sep (var (l - i - 1))
|
|
232 |
| sterm l (T.SApp (n, ts)) = app n (sterm l) ts
|
|
233 |
| sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
|
|
234 |
| sterm l (T.SQua (q, ss, ps, t)) =
|
|
235 |
let
|
|
236 |
val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
|
|
237 |
val vs = map_index (apfst (Integer.add l)) ss
|
|
238 |
fun var_decl (i, s) = par (var i #> sep (add s))
|
|
239 |
val sub = sterm (l + length ss)
|
|
240 |
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
|
|
241 |
fun pats (T.SPat ts) = pat ":pat" ts
|
|
242 |
| pats (T.SNoPat ts) = pat ":nopat" ts
|
|
243 |
in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
|
|
244 |
|
|
245 |
fun choose_logic theories =
|
|
246 |
if member (op =) theories T.Bitvector then "QF_AUFBV"
|
|
247 |
else if member (op =) theories T.Real then "AUFLIRA"
|
|
248 |
else "AUFLIA"
|
|
249 |
|
|
250 |
fun serialize comments {theories, sorts, funcs} ts =
|
|
251 |
Buffer.empty
|
|
252 |
|> line (add "(benchmark Isabelle")
|
|
253 |
|> line (add ":status unknown")
|
|
254 |
|> line (add ":logic " #> add (choose_logic theories))
|
|
255 |
|> length sorts > 0 ?
|
|
256 |
line (add ":extrasorts" #> par (fold (sep o add) sorts))
|
|
257 |
|> length funcs > 0 ? (
|
|
258 |
line (add ":extrafuns" #> add " (") #>
|
|
259 |
fold (fn (f, (ss, s)) =>
|
|
260 |
line (sep (app f (sep o add) (ss @ [s])))) funcs #>
|
|
261 |
line (add ")"))
|
|
262 |
|> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
|
|
263 |
|> line (add ":formula true)")
|
|
264 |
|> fold (fn str => line (add "; " #> add str)) comments
|
|
265 |
|> Buffer.content
|
|
266 |
|
|
267 |
|
|
268 |
|
|
269 |
(** interface **)
|
|
270 |
|
|
271 |
val interface = {
|
|
272 |
extra_norm = extra_norm,
|
|
273 |
translate = {
|
|
274 |
prefixes = {
|
|
275 |
sort_prefix = "S",
|
|
276 |
func_prefix = "f"},
|
|
277 |
strict = SOME {
|
|
278 |
is_builtin_conn = is_builtin_conn,
|
|
279 |
is_builtin_pred = is_builtin_pred,
|
|
280 |
is_builtin_distinct = true},
|
|
281 |
builtins = {
|
|
282 |
builtin_typ = builtin_typ,
|
|
283 |
builtin_num = builtin_num,
|
|
284 |
builtin_fun = builtin_fun},
|
|
285 |
serialize = serialize}}
|
|
286 |
|
|
287 |
end
|