# HG changeset patch
# User blanchet
# Date 1409179237 -7200
# Node ID fc6dd578d50621b55a14530730e9f4e436f1b020
# Parent  625bdd5c70b2da24b4b45894abb52b48272eb3a3
moved old setup for SMT out

diff -r 625bdd5c70b2 -r fc6dd578d506 src/HOL/Library/SMT.thy
--- a/src/HOL/Library/SMT.thy	Thu Aug 28 00:40:37 2014 +0200
+++ b/src/HOL/Library/SMT.thy	Thu Aug 28 00:40:37 2014 +0200
@@ -5,7 +5,7 @@
 header {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
 
 theory SMT
-imports "../Real"
+imports "../Real" "../Word/Word"
 keywords "smt_status" :: diag
 begin
 
@@ -422,6 +422,9 @@
 ML_file "SMT/smt_real.ML"
 setup SMT_Real.setup
 
+ML_file "SMT/smt_word.ML"
+setup SMT_Word.setup
+
 hide_type (open) pattern
 hide_const fun_app term_true term_false z3div z3mod
 hide_const (open) trigger pat nopat weight
diff -r 625bdd5c70b2 -r fc6dd578d506 src/HOL/Library/SMT/smt_word.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SMT/smt_word.ML	Thu Aug 28 00:40:37 2014 +0200
@@ -0,0 +1,151 @@
+(*  Title:      HOL/Library/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
+
+open Word_Lib
+
+(* 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
+  val smtlibC = SMTLIB_Interface.smtlibC
+
+  val wordT = @{typ "'a::len word"}
+
+  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
+  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
+
+  fun word_typ (Type (@{type_name word}, [T])) =
+        Option.map (index1 "BitVec") (try dest_binT T)
+    | word_typ _ = NONE
+
+  fun word_num (Type (@{type_name word}, [T])) i =
+        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
+    | word_num _ _ = NONE
+
+  fun if_fixed pred m n T ts =
+    let val (Us, U) = Term.strip_type T
+    in
+      if pred (U, Us) then
+        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
+      else NONE
+    end
+
+  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
+  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
+
+  fun add_word_fun f (t, n) =
+    let val (m, _) = Term.dest_Const t
+    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
+
+  fun hd2 xs = hd (tl xs)
+
+  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
+
+  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
+    | dest_nat t = raise TERM ("not a natural number", [t])
+
+  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
+    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
+
+  fun shift m n T ts =
+    let val U = Term.domain_type T
+    in
+      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
+        (true, SOME i) =>
+          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
+      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
+    end
+
+  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
+
+  fun extract m n T ts =
+    let val U = Term.range_type (Term.range_type T)
+    in
+      (case (try (dest_nat o hd) ts, try dest_wordT U) of
+        (SOME lb, SOME i) =>
+          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
+      | _ => NONE)
+    end
+
+  fun mk_extend c ts = Term.list_comb (Const c, ts)
+
+  fun extend m n T ts =
+    let val (U1, U2) = Term.dest_funT T
+    in
+      (case (try dest_wordT U1, try dest_wordT U2) of
+        (SOME i, SOME j) =>
+          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
+          else NONE
+      | _ => NONE)
+    end
+
+  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
+
+  fun rotate m n T ts =
+    let val U = Term.domain_type (Term.range_type T)
+    in
+      (case (can dest_wordT U, try (dest_nat o hd) ts) of
+        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
+      | _ => NONE)
+    end
+in
+
+val setup_builtins =
+  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
+  fold (add_word_fun if_fixed_all) [
+    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
+    (@{term "plus :: 'a::len word => _"}, "bvadd"),
+    (@{term "minus :: 'a::len word => _"}, "bvsub"),
+    (@{term "times :: 'a::len word => _"}, "bvmul"),
+    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
+    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
+    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
+    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
+    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
+  fold (add_word_fun shift) [
+    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
+    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
+    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
+  add_word_fun extract
+    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
+  fold (add_word_fun extend) [
+    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
+    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
+  fold (add_word_fun rotate) [
+    (@{term word_rotl}, "rotate_left"),
+    (@{term word_rotr}, "rotate_right") ] #>
+  fold (add_word_fun if_fixed_args) [
+    (@{term "less :: 'a::len word => _"}, "bvult"),
+    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
+    (@{term word_sless}, "bvslt"),
+    (@{term word_sle}, "bvsle") ]
+
+end
+
+
+(* setup *)
+
+val setup = 
+  Context.theory_map (
+    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
+    setup_builtins)
+
+end
diff -r 625bdd5c70b2 -r fc6dd578d506 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Thu Aug 28 00:40:37 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-(*  Title:      HOL/Word/Tools/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
-
-open Word_Lib
-
-(* 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
-  val smtlibC = SMTLIB_Interface.smtlibC
-
-  val wordT = @{typ "'a::len word"}
-
-  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
-  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
-
-  fun word_typ (Type (@{type_name word}, [T])) =
-        Option.map (index1 "BitVec") (try dest_binT T)
-    | word_typ _ = NONE
-
-  fun word_num (Type (@{type_name word}, [T])) i =
-        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
-    | word_num _ _ = NONE
-
-  fun if_fixed pred m n T ts =
-    let val (Us, U) = Term.strip_type T
-    in
-      if pred (U, Us) then
-        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
-      else NONE
-    end
-
-  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
-  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
-
-  fun add_word_fun f (t, n) =
-    let val (m, _) = Term.dest_Const t
-    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
-
-  fun hd2 xs = hd (tl xs)
-
-  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
-
-  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
-    | dest_nat t = raise TERM ("not a natural number", [t])
-
-  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
-    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
-
-  fun shift m n T ts =
-    let val U = Term.domain_type T
-    in
-      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
-        (true, SOME i) =>
-          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
-      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
-    end
-
-  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
-
-  fun extract m n T ts =
-    let val U = Term.range_type (Term.range_type T)
-    in
-      (case (try (dest_nat o hd) ts, try dest_wordT U) of
-        (SOME lb, SOME i) =>
-          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
-      | _ => NONE)
-    end
-
-  fun mk_extend c ts = Term.list_comb (Const c, ts)
-
-  fun extend m n T ts =
-    let val (U1, U2) = Term.dest_funT T
-    in
-      (case (try dest_wordT U1, try dest_wordT U2) of
-        (SOME i, SOME j) =>
-          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
-          else NONE
-      | _ => NONE)
-    end
-
-  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
-
-  fun rotate m n T ts =
-    let val U = Term.domain_type (Term.range_type T)
-    in
-      (case (can dest_wordT U, try (dest_nat o hd) ts) of
-        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
-      | _ => NONE)
-    end
-in
-
-val setup_builtins =
-  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
-  fold (add_word_fun if_fixed_all) [
-    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
-    (@{term "plus :: 'a::len word => _"}, "bvadd"),
-    (@{term "minus :: 'a::len word => _"}, "bvsub"),
-    (@{term "times :: 'a::len word => _"}, "bvmul"),
-    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
-    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
-    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
-    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
-    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
-  fold (add_word_fun shift) [
-    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
-    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
-    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
-  add_word_fun extract
-    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
-  fold (add_word_fun extend) [
-    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
-    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
-  fold (add_word_fun rotate) [
-    (@{term word_rotl}, "rotate_left"),
-    (@{term word_rotr}, "rotate_right") ] #>
-  fold (add_word_fun if_fixed_args) [
-    (@{term "less :: 'a::len word => _"}, "bvult"),
-    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
-    (@{term word_sless}, "bvslt"),
-    (@{term word_sle}, "bvsle") ]
-
-end
-
-
-(* setup *)
-
-val setup = 
-  Context.theory_map (
-    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
-    setup_builtins)
-
-end
diff -r 625bdd5c70b2 -r fc6dd578d506 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Aug 28 00:40:37 2014 +0200
+++ b/src/HOL/Word/Word.thy	Thu Aug 28 00:40:37 2014 +0200
@@ -4753,8 +4753,6 @@
 declare bin_to_bl_def [simp]
 
 ML_file "Tools/word_lib.ML"
-ML_file "Tools/smt_word.ML"
-setup SMT_Word.setup
 ML_file "Tools/smt2_word.ML"
 
 hide_const (open) Word