src/HOL/Tools/SMT/smt_word.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40579 98ebd2300823
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
boehmes@36899
     1
(*  Title:      HOL/Tools/SMT/smt_word.ML
boehmes@36899
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36899
     3
boehmes@36899
     4
SMT setup for words.
boehmes@36899
     5
*)
boehmes@36899
     6
boehmes@36899
     7
signature SMT_WORD =
boehmes@36899
     8
sig
boehmes@36899
     9
  val setup: theory -> theory
boehmes@36899
    10
end
boehmes@36899
    11
boehmes@36899
    12
structure SMT_Word: SMT_WORD =
boehmes@36899
    13
struct
boehmes@36899
    14
boehmes@36899
    15
boehmes@36899
    16
(* utilities *)
boehmes@36899
    17
boehmes@36899
    18
fun dest_binT T =
boehmes@36899
    19
  (case T of
boehmes@36899
    20
    Type (@{type_name "Numeral_Type.num0"}, _) => 0
boehmes@36899
    21
  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
boehmes@36899
    22
  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
boehmes@36899
    23
  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
boehmes@36899
    24
  | _ => raise TYPE ("dest_binT", [T], []))
boehmes@36899
    25
boehmes@36899
    26
fun is_wordT (Type (@{type_name word}, _)) = true
boehmes@36899
    27
  | is_wordT _ = false
boehmes@36899
    28
boehmes@36899
    29
fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
boehmes@36899
    30
  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
boehmes@36899
    31
boehmes@36899
    32
boehmes@36899
    33
boehmes@36899
    34
(* SMT-LIB logic *)
boehmes@36899
    35
boehmes@36899
    36
fun smtlib_logic ts =
boehmes@36899
    37
  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
boehmes@36899
    38
  then SOME "QF_AUFBV"
boehmes@36899
    39
  else NONE
boehmes@36899
    40
boehmes@36899
    41
boehmes@36899
    42
boehmes@36899
    43
(* SMT-LIB builtins *)
boehmes@36899
    44
boehmes@36899
    45
local
boehmes@36899
    46
  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
boehmes@36899
    47
  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
boehmes@36899
    48
boehmes@36899
    49
  fun smtlib_builtin_typ (Type (@{type_name word}, [T])) =
boehmes@36899
    50
        Option.map (index1 "BitVec") (try dest_binT T)
boehmes@36899
    51
    | smtlib_builtin_typ _ = NONE
boehmes@36899
    52
boehmes@36899
    53
  fun smtlib_builtin_num (Type (@{type_name word}, [T])) i =
boehmes@36899
    54
        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
boehmes@36899
    55
    | smtlib_builtin_num _ _ = NONE
boehmes@36899
    56
boehmes@36899
    57
  fun if_fixed n T ts =
boehmes@36899
    58
    let val (Ts, T) = Term.strip_type T
boehmes@36899
    59
    in if forall (can dest_wordT) (T :: Ts) then SOME (n, ts) else NONE end
boehmes@36899
    60
boehmes@36899
    61
  fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
boehmes@36899
    62
    | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
boehmes@40579
    63
  fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
boehmes@36899
    64
    | dest_nat ts = raise TERM ("dest_nat", ts)
boehmes@36899
    65
  fun dest_nat_word_funT (T, ts) =
boehmes@36899
    66
    (dest_word_funT (Term.range_type T), dest_nat ts)
boehmes@36899
    67
boehmes@36899
    68
  fun shift n T ts =
boehmes@36899
    69
    let val U = Term.domain_type T
boehmes@36899
    70
    in
boehmes@36899
    71
      (case (can dest_wordT U, ts) of
boehmes@36899
    72
        (true, [t, u]) =>
boehmes@36899
    73
          (case try HOLogic.dest_number u of
boehmes@36899
    74
            SOME (_,i) => SOME (n, [t, HOLogic.mk_number U i])
boehmes@36899
    75
          | NONE => NONE)  (* FIXME: also support non-numerical shifts *)
boehmes@36899
    76
      | _ => NONE)
boehmes@36899
    77
    end
boehmes@36899
    78
boehmes@36899
    79
  fun extend n T ts =
boehmes@36899
    80
    (case try dest_word_funT T of
boehmes@36899
    81
      SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
boehmes@36899
    82
    | _ => NONE)
boehmes@36899
    83
boehmes@36899
    84
  fun rotate n T ts =
boehmes@36899
    85
    try dest_nat ts
boehmes@36899
    86
    |> Option.map (fn (i, ts') => (index1 n i, ts'))
boehmes@36899
    87
boehmes@36899
    88
  fun extract n T ts =
boehmes@36899
    89
    try dest_nat_word_funT (T, ts)
boehmes@36899
    90
    |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
boehmes@36899
    91
boehmes@36899
    92
  fun smtlib_builtin_func @{const_name uminus} = if_fixed "bvneg"
boehmes@36899
    93
    | smtlib_builtin_func @{const_name plus} = if_fixed "bvadd"
boehmes@36899
    94
    | smtlib_builtin_func @{const_name minus} = if_fixed "bvsub"
boehmes@36899
    95
    | smtlib_builtin_func @{const_name times} = if_fixed "bvmul"
boehmes@36899
    96
    | smtlib_builtin_func @{const_name bitNOT} = if_fixed "bvnot"
boehmes@36899
    97
    | smtlib_builtin_func @{const_name bitAND} = if_fixed "bvand"
boehmes@36899
    98
    | smtlib_builtin_func @{const_name bitOR} = if_fixed "bvor"
boehmes@36899
    99
    | smtlib_builtin_func @{const_name bitXOR} = if_fixed "bvxor"
boehmes@36899
   100
    | smtlib_builtin_func @{const_name word_cat} = if_fixed "concat"
boehmes@36899
   101
    | smtlib_builtin_func @{const_name shiftl} = shift "bvshl"
boehmes@36899
   102
    | smtlib_builtin_func @{const_name shiftr} = shift "bvlshr"
boehmes@36899
   103
    | smtlib_builtin_func @{const_name sshiftr} = shift "bvashr"
boehmes@36899
   104
    | smtlib_builtin_func @{const_name slice} = extract "extract"
boehmes@36899
   105
    | smtlib_builtin_func @{const_name ucast} = extend "zero_extend"
boehmes@36899
   106
    | smtlib_builtin_func @{const_name scast} = extend "sign_extend"
boehmes@36899
   107
    | smtlib_builtin_func @{const_name word_rotl} = rotate "rotate_left"
boehmes@36899
   108
    | smtlib_builtin_func @{const_name word_rotr} = rotate "rotate_right"
boehmes@36899
   109
    | smtlib_builtin_func _ = (fn _ => K NONE)
boehmes@36899
   110
        (* FIXME: support more builtin bitvector functions:
boehmes@36899
   111
             bvudiv/bvurem and bvsdiv/bvsmod/bvsrem *)
boehmes@36899
   112
boehmes@36899
   113
  fun smtlib_builtin_pred @{const_name less} = SOME "bvult"
boehmes@36899
   114
    | smtlib_builtin_pred @{const_name less_eq} = SOME "bvule"
boehmes@36899
   115
    | smtlib_builtin_pred @{const_name word_sless} = SOME "bvslt"
boehmes@36899
   116
    | smtlib_builtin_pred @{const_name word_sle} = SOME "bvsle"
boehmes@36899
   117
    | smtlib_builtin_pred _ = NONE
boehmes@36899
   118
boehmes@36899
   119
  fun smtlib_builtin_pred' (n, T) =
boehmes@36899
   120
    if can (dest_wordT o Term.domain_type) T then smtlib_builtin_pred n
boehmes@36899
   121
    else NONE
boehmes@36899
   122
in
boehmes@36899
   123
wenzelm@37165
   124
val smtlib_builtins : SMTLIB_Interface.builtins = {
boehmes@36899
   125
  builtin_typ = smtlib_builtin_typ,
boehmes@36899
   126
  builtin_num = smtlib_builtin_num,
boehmes@36899
   127
  builtin_func = (fn (n, T) => fn ts => smtlib_builtin_func n T ts),
boehmes@36899
   128
  builtin_pred = (fn c => fn ts =>
boehmes@36899
   129
    smtlib_builtin_pred' c |> Option.map (rpair ts)),
boehmes@36899
   130
  is_builtin_pred = curry (is_some o smtlib_builtin_pred') }
boehmes@36899
   131
boehmes@36899
   132
end
boehmes@36899
   133
boehmes@36899
   134
boehmes@36899
   135
boehmes@36899
   136
(* setup *)
boehmes@36899
   137
boehmes@36899
   138
val setup = 
boehmes@36899
   139
  Context.theory_map (
boehmes@36899
   140
    SMTLIB_Interface.add_logic smtlib_logic #>
boehmes@36899
   141
    SMTLIB_Interface.add_builtins smtlib_builtins)
boehmes@36899
   142
boehmes@36899
   143
end