1(* Copyright (c) 2010-2011 Tjark Weber. All rights reserved. *)
2
3(* SMT-LIB 2 theories *)
4
5structure SmtLib_Theories =
6struct
7
8local
9
10  local open HolSmtTheory in end
11
12  val ERR = Feedback.mk_HOL_ERR "SmtLib_Theories"
13
14in
15
16  fun zero_args x xs =
17    if List.null xs then
18      x
19    else
20      raise ERR "zero_args" "no arguments expected"
21
22  fun one_arg f xs =
23    f (Lib.singleton_of_list xs handle Feedback.HOL_ERR _ =>
24      raise ERR "one_arg" "one argument expected")
25
26  fun two_args f xs =
27    f (Lib.pair_of_list xs handle Feedback.HOL_ERR _ =>
28      raise ERR "two_args" "two arguments expected")
29
30  fun three_args f xs =
31    f (Lib.triple_of_list xs handle Feedback.HOL_ERR _ =>
32      raise ERR "three_args" "three arguments expected")
33
34  fun list_args f xs =
35    if List.null xs then
36      raise ERR "list_args" "non-empty argument list expected"
37    else
38      f xs
39
40  fun zero_zero f x = zero_args (zero_args (f x))
41  fun zero_one f x = zero_args (one_arg (f x))
42  fun zero_two f x = zero_args (two_args (f x))
43
44  fun one_zero f x = zero_args o (one_arg (f x))
45  fun one_one f x = one_arg o (one_arg (f x))
46
47  fun K_zero_zero x = Lib.K (zero_args (zero_args x))
48  fun K_zero_one f = Lib.K (zero_args (one_arg f))
49  fun K_zero_two f = Lib.K (zero_args (two_args f))
50  fun K_zero_three f = Lib.K (zero_args (three_args f))
51  fun K_zero_list f = Lib.K (zero_args (list_args f))
52
53  fun K_one_zero f = Lib.K (zero_args o one_arg f)
54  fun K_one_one f = Lib.K (one_arg o one_arg f)
55
56  fun K_two_one f = Lib.K (one_arg o two_args f)
57
58  fun chainable f =
59  let
60    fun aux t [] = raise Match  (* should never happen *)
61      | aux t [_] = t
62      | aux t (x::y::zs) = aux (boolSyntax.mk_conj (t, f (x, y))) (y::zs)
63  in
64    Lib.K (zero_args (list_args
65      (fn x::y::zs => aux (f (x, y)) (y::zs)
66        | _ => raise ERR "chainable" "at least two arguments expected")))
67  end
68
69  fun leftassoc f =
70  let
71    fun aux t [] = t
72      | aux t (y::zs) = aux (f (t, y)) zs
73  in
74    Lib.K (zero_args (list_args
75      (fn x::y::zs => aux x (y::zs)
76        | _ => raise ERR "leftassoc" "at least two arguments expected")))
77  end
78
79  fun rightassoc f =
80  let
81    fun aux _ [] = raise Match  (* should never happen *)
82      | aux cont [y] = cont y
83      | aux cont (x::y::zs) = aux (fn t => cont (f (x, t))) (y::zs)
84  in
85    Lib.K (zero_args (list_args
86      (fn x::y::zs => aux Lib.I (x::y::zs)
87        | _ => raise ERR "rightassoc" "at least two arguments expected")))
88  end
89
90  (* A <numeral> is the digit 0 or a non-empty sequence of digits not
91     starting with 0. *)
92  fun is_numeral token =
93  let
94    val cs = String.explode token
95  in
96    cs = [#"0"] orelse
97      (not (List.null cs) andalso List.all Char.isDigit cs andalso
98        List.hd cs <> #"0")
99  end
100
101  (* A <decimal> is a token of the form <numeral>.0*<numeral>. *)
102  fun real_of_decimal token =
103  let
104    val (left, right) = Lib.pair_of_list (String.fields (Lib.equal #".") token)
105    val _ = is_numeral left orelse
106      raise ERR "real_of_decimal" "not a decimal"
107    val right = String.explode right
108    fun is_zerostar_numeral (#"0" :: c :: cs) = is_zerostar_numeral (c :: cs)
109      | is_zerostar_numeral cs                = is_numeral (String.implode cs)
110    val _ = is_zerostar_numeral right orelse
111      raise ERR "real_of_decimal" "not a decimal"
112    (* drop trailing 0's *)
113    fun drop_zeros (#"0" :: cs) = drop_zeros cs
114      | drop_zeros cs           = cs
115    val right = String.implode (List.rev (drop_zeros (List.rev right)))
116    val numerator = Arbint.fromString (left ^ right)
117    val ten = Arbint.fromInt 10
118    val denominator = Lib.funpow (String.size right)
119      (fn i => Arbint.* (ten, i)) Arbint.one
120  in
121    if denominator = Arbint.one then
122      realSyntax.term_of_int numerator
123    else
124      realSyntax.mk_div (realSyntax.term_of_int numerator,
125        realSyntax.term_of_int denominator)
126  end
127  handle Feedback.HOL_ERR _ =>
128    raise ERR "real_of_decimal" "not a decimal"
129
130  (* ArraysEx *)
131
132  structure ArraysEx =
133  struct
134
135    val tydict = Library.dict_from_list [
136      (* arrays are translated as functions *)
137      ("Array", K_zero_two Type.-->)
138    ]
139
140    val tmdict = Library.dict_from_list [
141      (* array lookup is translated as function application *)
142      ("select", K_zero_two Term.mk_comb),
143      (* array update is translated as function update *)
144      ("store", K_zero_three (fn (array, index, value) =>
145        Term.mk_comb (combinSyntax.mk_update (index, value), array)))
146    ]
147
148  end
149
150  (* Fixed_Size_BitVectors *)
151
152  structure Fixed_Size_BitVectors =
153  struct
154
155    val tydict = Library.dict_from_list [
156      ("BitVec", K_one_zero (wordsSyntax.mk_word_type o fcpLib.index_type))
157    ]
158
159    val tmdict = Library.dict_from_list [
160      (* bit-vector constants *)
161      ("_", zero_zero (fn token =>
162        if String.isPrefix "#b" token then
163          let
164            val binary = String.extract (token, 2, NONE)
165            val value = Arbnum.fromBinString binary
166            val size = Arbnum.fromInt (String.size binary)
167          in
168            wordsSyntax.mk_word (value, size)
169          end
170        else if String.isPrefix "#x" token then
171          let
172            val hex = String.extract (token, 2, NONE)
173            val value = Arbnum.fromHexString hex
174            val size = Arbnum.times2 (Arbnum.times2 (Arbnum.fromInt
175              (String.size hex)))
176          in
177            wordsSyntax.mk_word (value, size)
178          end
179        else
180          raise ERR "<Fixed_Size_BitVectors.tmdict._>"
181            "not a bit-vector constant")),
182      ("concat", K_zero_two wordsSyntax.mk_word_concat),
183      ("extract", K_two_one (fn (m, n) =>
184        let
185          val index_type = fcpLib.index_type (Arbnum.plus1 (Arbnum.- (m, n)))
186          val m = numSyntax.mk_numeral m
187          val n = numSyntax.mk_numeral n
188        in
189          fn t => wordsSyntax.mk_word_extract (m, n, t, index_type)
190        end)),
191      ("bvnot", K_zero_one wordsSyntax.mk_word_1comp),
192      ("bvneg", K_zero_one wordsSyntax.mk_word_2comp),
193      ("bvand", K_zero_two wordsSyntax.mk_word_and),
194      ("bvor", K_zero_two wordsSyntax.mk_word_or),
195      ("bvadd", K_zero_two wordsSyntax.mk_word_add),
196      ("bvmul", K_zero_two wordsSyntax.mk_word_mul),
197      (* SMT-LIB states that division by 0w is unspecified. Thus, any
198         proof (of unsatisfiability) should also be valid in HOL,
199         regardless of how division by 0w is defined in HOL. *)
200      ("bvudiv", K_zero_two wordsSyntax.mk_word_div),
201      ("bvurem", K_zero_two wordsSyntax.mk_word_mod),
202      ("bvshl", K_zero_two wordsSyntax.mk_word_lsl_bv),
203      ("bvlshr", K_zero_two wordsSyntax.mk_word_lsr_bv),
204      ("bvult", K_zero_two wordsSyntax.mk_word_lo)
205    ]
206
207  end
208
209  (* Core *)
210
211  structure Core =
212  struct
213
214    val tydict = Library.dict_from_list [
215      ("Bool", K_zero_zero Type.bool)
216    ]
217
218    val tmdict = Library.dict_from_list [
219      ("true", K_zero_zero boolSyntax.T),
220      ("false", K_zero_zero boolSyntax.F),
221      ("not", K_zero_one boolSyntax.mk_neg),
222      ("=>", rightassoc boolSyntax.mk_imp),
223      (* FIXME: SMT-LIB declares "and" and "or" as left-assoc. This
224         interacts badly with HOL4, where they are right-assoc.  In
225         particular, it breaks our proof reconstruction implementation
226         (Z3_ProofReplay.sml) in a few places that are not prepared to
227         handle the additional parentheses. For now, we parse "and"
228         and "or" as rightassoc. Since conjunction and disjunction are
229         associative, this does not change the meaning of formulas. *)
230      ("and", rightassoc boolSyntax.mk_conj),
231      ("or", rightassoc boolSyntax.mk_disj),
232      ("xor", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
233          (Term.prim_mk_const {Thy="HolSmt", Name="xor"}, t1), t2))),
234      ("=", chainable boolSyntax.mk_eq),
235      (* "distinct" is declared as :pairwise in SMT-LIB, but rather
236         than unfolding the definition of :pairwise, we use
237         'mk_all_distinct' *)
238      ("distinct", K_zero_list (fn ts => listSyntax.mk_all_distinct
239        (listSyntax.mk_list (ts, Term.type_of (List.hd ts))))),
240      ("ite", K_zero_three boolSyntax.mk_cond)
241    ]
242
243  end
244
245  (* Ints *)
246
247  structure Ints =
248  struct
249
250    val tydict = Library.dict_from_list [
251      ("Int", K_zero_zero intSyntax.int_ty)
252    ]
253
254    val tmdict = Library.dict_from_list [
255      (* numerals *)
256      ("_", zero_zero (fn token =>
257        if is_numeral token then
258          intSyntax.term_of_int (Arbint.fromString token)
259        else
260          raise ERR "<Ints.tmdict._>" "not a numeral")),
261      ("-", K_zero_one intSyntax.mk_negated),
262      ("-", leftassoc intSyntax.mk_minus),
263      ("+", leftassoc intSyntax.mk_plus),
264      ("*", leftassoc intSyntax.mk_mult),
265      (* FIXME: add parsing of div and mod *)
266      ("abs", K_zero_one intSyntax.mk_absval),
267      ("<=", chainable intSyntax.mk_leq),
268      ("<", chainable intSyntax.mk_less),
269      (">=", chainable intSyntax.mk_geq),
270      (">", chainable intSyntax.mk_great)
271    ]
272
273  end
274
275  (* Reals *)
276
277  structure Reals =
278  struct
279
280    val tydict = Library.dict_from_list [
281      ("Real", K_zero_zero realSyntax.real_ty)
282    ]
283
284    val tmdict = Library.dict_from_list [
285      (* numerals *)
286      ("_", zero_zero (fn token =>
287        if is_numeral token then
288          realSyntax.term_of_int (Arbint.fromString token)
289        else
290          raise ERR "<Reals.tmdict._>" "not a numeral")),
291      (* decimals *)
292      ("_", zero_zero real_of_decimal),
293      ("-", K_zero_one realSyntax.mk_negated),
294      ("-", leftassoc realSyntax.mk_minus),
295      ("+", leftassoc realSyntax.mk_plus),
296      ("*", leftassoc realSyntax.mk_mult),
297      ("/", leftassoc realSyntax.mk_div),
298      ("<=", chainable realSyntax.mk_leq),
299      ("<", chainable realSyntax.mk_less),
300      (">=", chainable realSyntax.mk_geq),
301      (">", chainable realSyntax.mk_great)
302    ]
303
304  end
305
306  (* Reals_Ints *)
307
308  structure Reals_Ints =
309  struct
310
311    val tydict = Library.dict_from_list [
312      ("Int", K_zero_zero intSyntax.int_ty),
313      ("Real", K_zero_zero realSyntax.real_ty)
314    ]
315
316    val tmdict = Library.dict_from_list [
317      (* numerals *)
318      ("_", zero_zero (fn token =>
319        if is_numeral token then
320          intSyntax.term_of_int (Arbint.fromString token)
321        else
322          raise ERR "<Reals_Ints.tmdict._>" "not a numeral")),
323      ("-", K_zero_one intSyntax.mk_negated),
324      ("-", leftassoc intSyntax.mk_minus),
325      ("+", leftassoc intSyntax.mk_plus),
326      ("*", leftassoc intSyntax.mk_mult),
327      (* FIXME: add parsing of div and mod *)
328      ("abs", K_zero_one intSyntax.mk_absval),
329      ("<=", chainable intSyntax.mk_leq),
330      ("<", chainable intSyntax.mk_less),
331      (">=", chainable intSyntax.mk_geq),
332      (">", chainable intSyntax.mk_great),
333      (* decimals *)
334      ("_", zero_zero real_of_decimal),
335      ("-", K_zero_one realSyntax.mk_negated),
336      ("-", leftassoc realSyntax.mk_minus),
337      ("+", leftassoc realSyntax.mk_plus),
338      ("*", leftassoc realSyntax.mk_mult),
339      ("/", leftassoc realSyntax.mk_div),
340      ("<=", chainable realSyntax.mk_leq),
341      ("<", chainable realSyntax.mk_less),
342      (">=", chainable realSyntax.mk_geq),
343      (">", chainable realSyntax.mk_great),
344      ("to_real", K_zero_one intrealSyntax.mk_real_of_int),
345      ("to_int", K_zero_one intrealSyntax.mk_INT_FLOOR),
346      ("is_int", K_zero_one intrealSyntax.mk_is_int)
347    ]
348
349  end
350
351end  (* local *)
352
353end
354