src/HOL/SMT/Tools/z3_interface.ML

tuned

(*  Title:      HOL/SMT/Tools/z3_interface.ML
    Author:     Sascha Boehme, TU Muenchen

Interface to Z3 based on a relaxed version of SMT-LIB.
*)

signature Z3_INTERFACE =
sig
  val interface: string list -> SMT_Translate.config
end

structure Z3_Interface: Z3_INTERFACE =
struct

structure T = SMT_Translate

fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]"
fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"

val builtin_typ = (fn
    @{typ int} => SOME "Int"
  | @{typ real} => SOME "Real"
  | Type (@{type_name word}, [T]) =>
      Option.map (mk_name1 "BitVec") (try T.dest_binT T)
  | _ => NONE)

val builtin_num = (fn
    (i, @{typ int}) => SOME (string_of_int i)
  | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
  | (i, Type (@{type_name word}, [T])) =>
      Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T)
  | _ => NONE)

val builtin_funcs = T.builtin_make [
  (@{term If}, "ite"),
  (@{term "uminus :: int => _"}, "~"),
  (@{term "plus :: int => _"}, "+"),
  (@{term "minus :: int => _"}, "-"),
  (@{term "times :: int => _"}, "*"),
  (@{term "op div :: int => _"}, "div"),
  (@{term "op mod :: int => _"}, "mod"),
  (@{term "op rem"}, "rem"),
  (@{term "uminus :: real => _"}, "~"),
  (@{term "plus :: real => _"}, "+"),
  (@{term "minus :: real => _"}, "-"),
  (@{term "times :: real => _"}, "*"),
  (@{term "op / :: real => _"}, "/"),
  (@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"),
  (@{term "op AND :: 'a::len0 word => _"}, "bvand"),
  (@{term "op OR :: 'a::len0 word => _"}, "bvor"),
  (@{term "op XOR :: 'a::len0 word => _"}, "bvxor"),
  (@{term "uminus :: 'a::len0 word => _"}, "bvneg"),
  (@{term "op + :: 'a::len0 word => _"}, "bvadd"),
  (@{term "op - :: 'a::len0 word => _"}, "bvsub"),
  (@{term "op * :: 'a::len0 word => _"}, "bvmul"),
  (@{term "op div :: 'a::len0 word => _"}, "bvudiv"),
  (@{term "op mod :: 'a::len0 word => _"}, "bvurem"),
  (@{term "op sdiv"}, "bvsdiv"),
  (@{term "op smod"}, "bvsmod"),
  (@{term "op srem"}, "bvsrem"),
  (@{term word_cat}, "concat"),
  (@{term bv_shl}, "bvshl"),
  (@{term bv_lshr}, "bvlshr"),
  (@{term bv_ashr}, "bvashr")]
  |> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract"))
  |> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend"))
  |> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend"))
  |> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left"))
  |> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right"))

val builtin_preds = T.builtin_make [
  (@{term True}, "true"),
  (@{term False}, "false"),
  (@{term Not}, "not"),
  (@{term "op &"}, "and"),
  (@{term "op |"}, "or"),
  (@{term "op -->"}, "implies"),
  (@{term "op iff"}, "iff"),
  (@{term If}, "if_then_else"),
  (@{term distinct}, "distinct"),
  (@{term "op ="}, "="),
  (@{term "op < :: int => _"}, "<"),
  (@{term "op <= :: int => _"}, "<="),
  (@{term "op < :: real => _"}, "<"),
  (@{term "op <= :: real => _"}, "<="),
  (@{term "op < :: 'a::len0 word => _"}, "bvult"),
  (@{term "op <= :: 'a::len0 word => _"}, "bvule"),
  (@{term word_sless}, "bvslt"),
  (@{term word_sle}, "bvsle")]

val builtins = {
  builtin_typ = builtin_typ,
  builtin_num = builtin_num,
  builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }

val interface = SMTLIB_Interface.gen_interface builtins []

end