src/HOL/Word/Tools/smt_word.ML
author boehmes
Wed Dec 08 08:33:02 2010 +0100 (2010-12-08)
changeset 41072 9f9bc1bdacef
parent 41061 492f8fd35fc0
child 41127 2ea84c8535c6
permissions -rw-r--r--
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
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@41061
    15
structure B = SMT_Builtin
boehmes@41061
    16
boehmes@41060
    17
boehmes@41060
    18
(* utilities *)
boehmes@41060
    19
boehmes@41060
    20
fun dest_binT T =
boehmes@41060
    21
  (case T of
boehmes@41060
    22
    Type (@{type_name "Numeral_Type.num0"}, _) => 0
boehmes@41060
    23
  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
boehmes@41060
    24
  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
boehmes@41060
    25
  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
boehmes@41060
    26
  | _ => raise TYPE ("dest_binT", [T], []))
boehmes@41060
    27
boehmes@41060
    28
fun is_wordT (Type (@{type_name word}, _)) = true
boehmes@41060
    29
  | is_wordT _ = false
boehmes@41060
    30
boehmes@41060
    31
fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
boehmes@41060
    32
  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
boehmes@41060
    33
boehmes@41060
    34
boehmes@41060
    35
(* SMT-LIB logic *)
boehmes@41060
    36
boehmes@41060
    37
fun smtlib_logic ts =
boehmes@41060
    38
  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
boehmes@41060
    39
  then SOME "QF_AUFBV"
boehmes@41060
    40
  else NONE
boehmes@41060
    41
boehmes@41060
    42
boehmes@41060
    43
(* SMT-LIB builtins *)
boehmes@41060
    44
boehmes@41060
    45
local
boehmes@41061
    46
  val smtlibC = SMTLIB_Interface.smtlibC
boehmes@41061
    47
boehmes@41061
    48
  val wordT = @{typ "'a::len word"}
boehmes@41061
    49
boehmes@41060
    50
  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
boehmes@41060
    51
  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
boehmes@41060
    52
boehmes@41061
    53
  fun word_typ (Type (@{type_name word}, [T])) =
boehmes@41060
    54
        Option.map (index1 "BitVec") (try dest_binT T)
boehmes@41061
    55
    | word_typ _ = NONE
boehmes@41060
    56
boehmes@41061
    57
  fun word_num (Type (@{type_name word}, [T])) i =
boehmes@41060
    58
        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
boehmes@41061
    59
    | word_num _ _ = NONE
boehmes@41060
    60
boehmes@41060
    61
  fun if_fixed n T ts =
boehmes@41060
    62
    let val (Ts, T) = Term.strip_type T
boehmes@41060
    63
    in if forall (can dest_wordT) (T :: Ts) then SOME (n, ts) else NONE end
boehmes@41060
    64
boehmes@41061
    65
  fun if_fixed' n T ts =
boehmes@41061
    66
    if forall (can dest_wordT) (Term.binder_types T) then SOME (n, ts)
boehmes@41061
    67
    else NONE
boehmes@41061
    68
boehmes@41061
    69
  fun add_word_fun f (t, n) =
boehmes@41061
    70
    B.add_builtin_fun smtlibC (Term.dest_Const t, K (f n))
boehmes@41061
    71
boehmes@41061
    72
  fun add_word_fun' f (t, n) = add_word_fun f (t, n)
boehmes@41061
    73
boehmes@41060
    74
  fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
boehmes@41060
    75
    | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
boehmes@41060
    76
  fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
boehmes@41060
    77
    | dest_nat ts = raise TERM ("dest_nat", ts)
boehmes@41060
    78
  fun dest_nat_word_funT (T, ts) =
boehmes@41060
    79
    (dest_word_funT (Term.range_type T), dest_nat ts)
boehmes@41060
    80
boehmes@41060
    81
  fun shift n T ts =
boehmes@41060
    82
    let val U = Term.domain_type T
boehmes@41060
    83
    in
boehmes@41060
    84
      (case (can dest_wordT U, ts) of
boehmes@41060
    85
        (true, [t, u]) =>
boehmes@41060
    86
          (case try HOLogic.dest_number u of
boehmes@41060
    87
            SOME (_,i) => SOME (n, [t, HOLogic.mk_number U i])
boehmes@41060
    88
          | NONE => NONE)  (* FIXME: also support non-numerical shifts *)
boehmes@41060
    89
      | _ => NONE)
boehmes@41060
    90
    end
boehmes@41060
    91
boehmes@41061
    92
  fun extract n T ts =
boehmes@41061
    93
    try dest_nat_word_funT (T, ts)
boehmes@41061
    94
    |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
boehmes@41061
    95
boehmes@41060
    96
  fun extend n T ts =
boehmes@41060
    97
    (case try dest_word_funT T of
boehmes@41060
    98
      SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
boehmes@41060
    99
    | _ => NONE)
boehmes@41060
   100
boehmes@41060
   101
  fun rotate n T ts =
boehmes@41060
   102
    try dest_nat ts
boehmes@41060
   103
    |> Option.map (fn (i, ts') => (index1 n i, ts'))
boehmes@41060
   104
in
boehmes@41060
   105
boehmes@41061
   106
val setup_builtins =
boehmes@41061
   107
  B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
boehmes@41061
   108
  fold (add_word_fun' if_fixed) [
boehmes@41061
   109
    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
boehmes@41061
   110
    (@{term "plus :: 'a::len word => _"}, "bvadd"),
boehmes@41061
   111
    (@{term "minus :: 'a::len word => _"}, "bvsub"),
boehmes@41061
   112
    (@{term "times :: 'a::len word => _"}, "bvmul"),
boehmes@41061
   113
    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
boehmes@41061
   114
    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
boehmes@41061
   115
    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
boehmes@41061
   116
    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
boehmes@41061
   117
    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
boehmes@41061
   118
  fold (add_word_fun shift) [
boehmes@41061
   119
    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
boehmes@41061
   120
    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
boehmes@41061
   121
    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
boehmes@41061
   122
  add_word_fun extract
boehmes@41061
   123
    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
boehmes@41061
   124
  fold (add_word_fun extend) [
boehmes@41061
   125
    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
boehmes@41061
   126
    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
boehmes@41061
   127
  fold (add_word_fun rotate) [
boehmes@41061
   128
    (@{term word_rotl}, "rotate_left"),
boehmes@41061
   129
    (@{term word_rotr}, "rotate_right") ] #>
boehmes@41061
   130
  fold (add_word_fun' if_fixed') [
boehmes@41061
   131
    (@{term "less :: 'a::len word => _"}, "bvult"),
boehmes@41061
   132
    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
boehmes@41061
   133
    (@{term word_sless}, "bvslt"),
boehmes@41061
   134
    (@{term word_sle}, "bvsle") ]
boehmes@41060
   135
boehmes@41060
   136
end
boehmes@41060
   137
boehmes@41060
   138
boehmes@41060
   139
(* setup *)
boehmes@41060
   140
boehmes@41060
   141
val setup = 
boehmes@41072
   142
  Context.theory_map (
boehmes@41072
   143
    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
boehmes@41072
   144
    setup_builtins)
boehmes@41060
   145
boehmes@41060
   146
end