1 (* Title: HOL/SMT/Tools/z3_interface.ML
2 Author: Sascha Boehme, TU Muenchen
4 Interface to Z3 based on a relaxed version of SMT-LIB.
7 signature Z3_INTERFACE =
9 val interface: SMT_Solver.interface
12 structure Z3_Interface: Z3_INTERFACE =
15 structure T = SMT_Translate
17 fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]"
18 fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
21 @{typ int} => SOME "Int"
22 | @{typ real} => SOME "Real"
23 | Type (@{type_name word}, [T]) =>
24 Option.map (mk_name1 "BitVec") (try T.dest_binT T)
28 (i, @{typ int}) => SOME (string_of_int i)
29 | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
30 | (i, Type (@{type_name word}, [T])) =>
31 Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T)
34 val builtin_funcs = T.builtin_make [
36 (@{term "uminus :: int => _"}, "~"),
37 (@{term "plus :: int => _"}, "+"),
38 (@{term "minus :: int => _"}, "-"),
39 (@{term "times :: int => _"}, "*"),
40 (@{term "op div :: int => _"}, "div"),
41 (@{term "op mod :: int => _"}, "mod"),
42 (@{term "op rem"}, "rem"),
43 (@{term "uminus :: real => _"}, "~"),
44 (@{term "plus :: real => _"}, "+"),
45 (@{term "minus :: real => _"}, "-"),
46 (@{term "times :: real => _"}, "*"),
47 (@{term "op / :: real => _"}, "/"),
48 (@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"),
49 (@{term "op AND :: 'a::len0 word => _"}, "bvand"),
50 (@{term "op OR :: 'a::len0 word => _"}, "bvor"),
51 (@{term "op XOR :: 'a::len0 word => _"}, "bvxor"),
52 (@{term "uminus :: 'a::len0 word => _"}, "bvneg"),
53 (@{term "op + :: 'a::len0 word => _"}, "bvadd"),
54 (@{term "op - :: 'a::len0 word => _"}, "bvsub"),
55 (@{term "op * :: 'a::len0 word => _"}, "bvmul"),
56 (@{term "op div :: 'a::len0 word => _"}, "bvudiv"),
57 (@{term "op mod :: 'a::len0 word => _"}, "bvurem"),
58 (@{term "op sdiv"}, "bvsdiv"),
59 (@{term "op smod"}, "bvsmod"),
60 (@{term "op srem"}, "bvsrem"),
61 (@{term word_cat}, "concat"),
62 (@{term bv_shl}, "bvshl"),
63 (@{term bv_lshr}, "bvlshr"),
64 (@{term bv_ashr}, "bvashr")]
65 |> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract"))
66 |> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend"))
67 |> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend"))
68 |> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left"))
69 |> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right"))
71 val builtin_preds = T.builtin_make [
72 (@{term True}, "true"),
73 (@{term False}, "false"),
75 (@{term "op &"}, "and"),
76 (@{term "op |"}, "or"),
77 (@{term "op -->"}, "implies"),
78 (@{term "op iff"}, "iff"),
79 (@{term If}, "if_then_else"),
80 (@{term distinct}, "distinct"),
81 (@{term "op ="}, "="),
82 (@{term "op < :: int => _"}, "<"),
83 (@{term "op <= :: int => _"}, "<="),
84 (@{term "op < :: real => _"}, "<"),
85 (@{term "op <= :: real => _"}, "<="),
86 (@{term "op < :: 'a::len0 word => _"}, "bvult"),
87 (@{term "op <= :: 'a::len0 word => _"}, "bvule"),
88 (@{term word_sless}, "bvslt"),
89 (@{term word_sle}, "bvsle")]
91 val builtins = T.Builtins {
92 builtin_typ = builtin_typ,
93 builtin_num = builtin_num,
94 builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
96 val interface = SMTLIB_Interface.gen_interface builtins []