--- a/src/HOL/IsaMakefile Tue Dec 07 14:53:12 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Dec 07 14:53:44 2010 +0100
@@ -1254,7 +1254,7 @@
Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \
Word/Bool_List_Representation.thy Word/Bit_Operations.thy \
Word/Word.thy Word/document/root.tex \
- Word/document/root.bib Tools/SMT/smt_word.ML
+ Word/document/root.bib Word/Tools/smt_word.ML
@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
--- a/src/HOL/Tools/SMT/smt_word.ML Tue Dec 07 14:53:12 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-(* 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 (@{const 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Tools/smt_word.ML Tue Dec 07 14:53:44 2010 +0100
@@ -0,0 +1,143 @@
+(* 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 (@{const 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
--- a/src/HOL/Word/Word.thy Tue Dec 07 14:53:12 2010 +0100
+++ b/src/HOL/Word/Word.thy Tue Dec 07 14:53:44 2010 +0100
@@ -6,7 +6,7 @@
theory Word
imports Type_Length Misc_Typedef Boolean_Algebra Bool_List_Representation
-uses ("~~/src/HOL/Tools/SMT/smt_word.ML")
+uses ("~~/src/HOL/Word/Tools/smt_word.ML")
begin
text {* see @{text "Examples/WordExamples.thy"} for examples *}
@@ -4748,8 +4748,8 @@
declare of_bl_True [simp]
-use "~~/src/HOL/Tools/SMT/smt_word.ML"
+use "~~/src/HOL/Word/Tools/smt_word.ML"
setup {* SMT_Word.setup *}
-end
\ No newline at end of file
+end