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