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