src/HOL/Tools/SMT/smt_word.ML

tuned titles

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

SMT setup for words.
*)

signature SMT_WORD =
sig
  val setup: theory -> theory
end

structure SMT_Word: SMT_WORD =
struct


(* utilities *)

fun dest_binT T =
  (case T of
    Type (@{type_name "Numeral_Type.num0"}, _) => 0
  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
  | _ => raise TYPE ("dest_binT", [T], []))

fun is_wordT (Type (@{type_name word}, _)) = true
  | is_wordT _ = false

fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])



(* SMT-LIB logic *)

fun smtlib_logic ts =
  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
  then SOME "QF_AUFBV"
  else NONE



(* SMT-LIB builtins *)

local
  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"

  fun smtlib_builtin_typ (Type (@{type_name word}, [T])) =
        Option.map (index1 "BitVec") (try dest_binT T)
    | smtlib_builtin_typ _ = NONE

  fun smtlib_builtin_num (Type (@{type_name word}, [T])) i =
        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
    | smtlib_builtin_num _ _ = NONE

  fun if_fixed n T ts =
    let val (Ts, T) = Term.strip_type T
    in if forall (can dest_wordT) (T :: Ts) then SOME (n, ts) else NONE end

  fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
    | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
  fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
    | dest_nat ts = raise TERM ("dest_nat", ts)
  fun dest_nat_word_funT (T, ts) =
    (dest_word_funT (Term.range_type T), dest_nat ts)

  fun shift n T ts =
    let val U = Term.domain_type T
    in
      (case (can dest_wordT U, ts) of
        (true, [t, u]) =>
          (case try HOLogic.dest_number u of
            SOME (_,i) => SOME (n, [t, HOLogic.mk_number U i])
          | NONE => NONE)  (* FIXME: also support non-numerical shifts *)
      | _ => NONE)
    end

  fun extend n T ts =
    (case try dest_word_funT T of
      SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
    | _ => NONE)

  fun rotate n T ts =
    try dest_nat ts
    |> Option.map (fn (i, ts') => (index1 n i, ts'))

  fun extract n T ts =
    try dest_nat_word_funT (T, ts)
    |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))

  fun smtlib_builtin_func @{const_name uminus} = if_fixed "bvneg"
    | smtlib_builtin_func @{const_name plus} = if_fixed "bvadd"
    | smtlib_builtin_func @{const_name minus} = if_fixed "bvsub"
    | smtlib_builtin_func @{const_name times} = if_fixed "bvmul"
    | smtlib_builtin_func @{const_name bitNOT} = if_fixed "bvnot"
    | smtlib_builtin_func @{const_name bitAND} = if_fixed "bvand"
    | smtlib_builtin_func @{const_name bitOR} = if_fixed "bvor"
    | smtlib_builtin_func @{const_name bitXOR} = if_fixed "bvxor"
    | smtlib_builtin_func @{const_name word_cat} = if_fixed "concat"
    | smtlib_builtin_func @{const_name shiftl} = shift "bvshl"
    | smtlib_builtin_func @{const_name shiftr} = shift "bvlshr"
    | smtlib_builtin_func @{const_name sshiftr} = shift "bvashr"
    | smtlib_builtin_func @{const_name slice} = extract "extract"
    | smtlib_builtin_func @{const_name ucast} = extend "zero_extend"
    | smtlib_builtin_func @{const_name scast} = extend "sign_extend"
    | smtlib_builtin_func @{const_name word_rotl} = rotate "rotate_left"
    | smtlib_builtin_func @{const_name word_rotr} = rotate "rotate_right"
    | smtlib_builtin_func _ = (fn _ => K NONE)
        (* FIXME: support more builtin bitvector functions:
             bvudiv/bvurem and bvsdiv/bvsmod/bvsrem *)

  fun smtlib_builtin_pred @{const_name less} = SOME "bvult"
    | smtlib_builtin_pred @{const_name less_eq} = SOME "bvule"
    | smtlib_builtin_pred @{const_name word_sless} = SOME "bvslt"
    | smtlib_builtin_pred @{const_name word_sle} = SOME "bvsle"
    | smtlib_builtin_pred _ = NONE

  fun smtlib_builtin_pred' (n, T) =
    if can (dest_wordT o Term.domain_type) T then smtlib_builtin_pred n
    else NONE
in

val smtlib_builtins : SMTLIB_Interface.builtins = {
  builtin_typ = smtlib_builtin_typ,
  builtin_num = smtlib_builtin_num,
  builtin_func = (fn (n, T) => fn ts => smtlib_builtin_func n T ts),
  builtin_pred = (fn c => fn ts =>
    smtlib_builtin_pred' c |> Option.map (rpair ts)),
  is_builtin_pred = curry (is_some o smtlib_builtin_pred') }

end



(* setup *)

val setup = 
  Context.theory_map (
    SMTLIB_Interface.add_logic smtlib_logic #>
    SMTLIB_Interface.add_builtins smtlib_builtins)

end