moved old setup for SMT out
authorblanchet
Thu Aug 28 00:40:37 2014 +0200 (2014-08-28)
changeset 58056fc6dd578d506
parent 58055 625bdd5c70b2
child 58057 883f3c4c928e
moved old setup for SMT out
src/HOL/Library/SMT.thy
src/HOL/Library/SMT/smt_word.ML
src/HOL/Word/Tools/smt_word.ML
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Library/SMT.thy	Thu Aug 28 00:40:37 2014 +0200
     1.2 +++ b/src/HOL/Library/SMT.thy	Thu Aug 28 00:40:37 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     1.5  
     1.6  theory SMT
     1.7 -imports "../Real"
     1.8 +imports "../Real" "../Word/Word"
     1.9  keywords "smt_status" :: diag
    1.10  begin
    1.11  
    1.12 @@ -422,6 +422,9 @@
    1.13  ML_file "SMT/smt_real.ML"
    1.14  setup SMT_Real.setup
    1.15  
    1.16 +ML_file "SMT/smt_word.ML"
    1.17 +setup SMT_Word.setup
    1.18 +
    1.19  hide_type (open) pattern
    1.20  hide_const fun_app term_true term_false z3div z3mod
    1.21  hide_const (open) trigger pat nopat weight
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/SMT/smt_word.ML	Thu Aug 28 00:40:37 2014 +0200
     2.3 @@ -0,0 +1,151 @@
     2.4 +(*  Title:      HOL/Library/SMT/smt_word.ML
     2.5 +    Author:     Sascha Boehme, TU Muenchen
     2.6 +
     2.7 +SMT setup for words.
     2.8 +*)
     2.9 +
    2.10 +signature SMT_WORD =
    2.11 +sig
    2.12 +  val setup: theory -> theory
    2.13 +end
    2.14 +
    2.15 +structure SMT_Word: SMT_WORD =
    2.16 +struct
    2.17 +
    2.18 +open Word_Lib
    2.19 +
    2.20 +(* SMT-LIB logic *)
    2.21 +
    2.22 +fun smtlib_logic ts =
    2.23 +  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
    2.24 +  then SOME "QF_AUFBV"
    2.25 +  else NONE
    2.26 +
    2.27 +
    2.28 +(* SMT-LIB builtins *)
    2.29 +
    2.30 +local
    2.31 +  val smtlibC = SMTLIB_Interface.smtlibC
    2.32 +
    2.33 +  val wordT = @{typ "'a::len word"}
    2.34 +
    2.35 +  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
    2.36 +  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
    2.37 +
    2.38 +  fun word_typ (Type (@{type_name word}, [T])) =
    2.39 +        Option.map (index1 "BitVec") (try dest_binT T)
    2.40 +    | word_typ _ = NONE
    2.41 +
    2.42 +  fun word_num (Type (@{type_name word}, [T])) i =
    2.43 +        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
    2.44 +    | word_num _ _ = NONE
    2.45 +
    2.46 +  fun if_fixed pred m n T ts =
    2.47 +    let val (Us, U) = Term.strip_type T
    2.48 +    in
    2.49 +      if pred (U, Us) then
    2.50 +        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
    2.51 +      else NONE
    2.52 +    end
    2.53 +
    2.54 +  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
    2.55 +  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
    2.56 +
    2.57 +  fun add_word_fun f (t, n) =
    2.58 +    let val (m, _) = Term.dest_Const t
    2.59 +    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
    2.60 +
    2.61 +  fun hd2 xs = hd (tl xs)
    2.62 +
    2.63 +  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
    2.64 +
    2.65 +  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
    2.66 +    | dest_nat t = raise TERM ("not a natural number", [t])
    2.67 +
    2.68 +  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
    2.69 +    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
    2.70 +
    2.71 +  fun shift m n T ts =
    2.72 +    let val U = Term.domain_type T
    2.73 +    in
    2.74 +      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
    2.75 +        (true, SOME i) =>
    2.76 +          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
    2.77 +      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
    2.78 +    end
    2.79 +
    2.80 +  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
    2.81 +
    2.82 +  fun extract m n T ts =
    2.83 +    let val U = Term.range_type (Term.range_type T)
    2.84 +    in
    2.85 +      (case (try (dest_nat o hd) ts, try dest_wordT U) of
    2.86 +        (SOME lb, SOME i) =>
    2.87 +          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
    2.88 +      | _ => NONE)
    2.89 +    end
    2.90 +
    2.91 +  fun mk_extend c ts = Term.list_comb (Const c, ts)
    2.92 +
    2.93 +  fun extend m n T ts =
    2.94 +    let val (U1, U2) = Term.dest_funT T
    2.95 +    in
    2.96 +      (case (try dest_wordT U1, try dest_wordT U2) of
    2.97 +        (SOME i, SOME j) =>
    2.98 +          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
    2.99 +          else NONE
   2.100 +      | _ => NONE)
   2.101 +    end
   2.102 +
   2.103 +  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
   2.104 +
   2.105 +  fun rotate m n T ts =
   2.106 +    let val U = Term.domain_type (Term.range_type T)
   2.107 +    in
   2.108 +      (case (can dest_wordT U, try (dest_nat o hd) ts) of
   2.109 +        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
   2.110 +      | _ => NONE)
   2.111 +    end
   2.112 +in
   2.113 +
   2.114 +val setup_builtins =
   2.115 +  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
   2.116 +  fold (add_word_fun if_fixed_all) [
   2.117 +    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
   2.118 +    (@{term "plus :: 'a::len word => _"}, "bvadd"),
   2.119 +    (@{term "minus :: 'a::len word => _"}, "bvsub"),
   2.120 +    (@{term "times :: 'a::len word => _"}, "bvmul"),
   2.121 +    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
   2.122 +    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
   2.123 +    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
   2.124 +    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
   2.125 +    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
   2.126 +  fold (add_word_fun shift) [
   2.127 +    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
   2.128 +    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
   2.129 +    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
   2.130 +  add_word_fun extract
   2.131 +    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
   2.132 +  fold (add_word_fun extend) [
   2.133 +    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
   2.134 +    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
   2.135 +  fold (add_word_fun rotate) [
   2.136 +    (@{term word_rotl}, "rotate_left"),
   2.137 +    (@{term word_rotr}, "rotate_right") ] #>
   2.138 +  fold (add_word_fun if_fixed_args) [
   2.139 +    (@{term "less :: 'a::len word => _"}, "bvult"),
   2.140 +    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
   2.141 +    (@{term word_sless}, "bvslt"),
   2.142 +    (@{term word_sle}, "bvsle") ]
   2.143 +
   2.144 +end
   2.145 +
   2.146 +
   2.147 +(* setup *)
   2.148 +
   2.149 +val setup = 
   2.150 +  Context.theory_map (
   2.151 +    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
   2.152 +    setup_builtins)
   2.153 +
   2.154 +end
     3.1 --- a/src/HOL/Word/Tools/smt_word.ML	Thu Aug 28 00:40:37 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,151 +0,0 @@
     3.4 -(*  Title:      HOL/Word/Tools/smt_word.ML
     3.5 -    Author:     Sascha Boehme, TU Muenchen
     3.6 -
     3.7 -SMT setup for words.
     3.8 -*)
     3.9 -
    3.10 -signature SMT_WORD =
    3.11 -sig
    3.12 -  val setup: theory -> theory
    3.13 -end
    3.14 -
    3.15 -structure SMT_Word: SMT_WORD =
    3.16 -struct
    3.17 -
    3.18 -open Word_Lib
    3.19 -
    3.20 -(* SMT-LIB logic *)
    3.21 -
    3.22 -fun smtlib_logic ts =
    3.23 -  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
    3.24 -  then SOME "QF_AUFBV"
    3.25 -  else NONE
    3.26 -
    3.27 -
    3.28 -(* SMT-LIB builtins *)
    3.29 -
    3.30 -local
    3.31 -  val smtlibC = SMTLIB_Interface.smtlibC
    3.32 -
    3.33 -  val wordT = @{typ "'a::len word"}
    3.34 -
    3.35 -  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
    3.36 -  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
    3.37 -
    3.38 -  fun word_typ (Type (@{type_name word}, [T])) =
    3.39 -        Option.map (index1 "BitVec") (try dest_binT T)
    3.40 -    | word_typ _ = NONE
    3.41 -
    3.42 -  fun word_num (Type (@{type_name word}, [T])) i =
    3.43 -        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
    3.44 -    | word_num _ _ = NONE
    3.45 -
    3.46 -  fun if_fixed pred m n T ts =
    3.47 -    let val (Us, U) = Term.strip_type T
    3.48 -    in
    3.49 -      if pred (U, Us) then
    3.50 -        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
    3.51 -      else NONE
    3.52 -    end
    3.53 -
    3.54 -  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
    3.55 -  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
    3.56 -
    3.57 -  fun add_word_fun f (t, n) =
    3.58 -    let val (m, _) = Term.dest_Const t
    3.59 -    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
    3.60 -
    3.61 -  fun hd2 xs = hd (tl xs)
    3.62 -
    3.63 -  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
    3.64 -
    3.65 -  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
    3.66 -    | dest_nat t = raise TERM ("not a natural number", [t])
    3.67 -
    3.68 -  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
    3.69 -    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
    3.70 -
    3.71 -  fun shift m n T ts =
    3.72 -    let val U = Term.domain_type T
    3.73 -    in
    3.74 -      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
    3.75 -        (true, SOME i) =>
    3.76 -          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
    3.77 -      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
    3.78 -    end
    3.79 -
    3.80 -  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
    3.81 -
    3.82 -  fun extract m n T ts =
    3.83 -    let val U = Term.range_type (Term.range_type T)
    3.84 -    in
    3.85 -      (case (try (dest_nat o hd) ts, try dest_wordT U) of
    3.86 -        (SOME lb, SOME i) =>
    3.87 -          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
    3.88 -      | _ => NONE)
    3.89 -    end
    3.90 -
    3.91 -  fun mk_extend c ts = Term.list_comb (Const c, ts)
    3.92 -
    3.93 -  fun extend m n T ts =
    3.94 -    let val (U1, U2) = Term.dest_funT T
    3.95 -    in
    3.96 -      (case (try dest_wordT U1, try dest_wordT U2) of
    3.97 -        (SOME i, SOME j) =>
    3.98 -          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
    3.99 -          else NONE
   3.100 -      | _ => NONE)
   3.101 -    end
   3.102 -
   3.103 -  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
   3.104 -
   3.105 -  fun rotate m n T ts =
   3.106 -    let val U = Term.domain_type (Term.range_type T)
   3.107 -    in
   3.108 -      (case (can dest_wordT U, try (dest_nat o hd) ts) of
   3.109 -        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
   3.110 -      | _ => NONE)
   3.111 -    end
   3.112 -in
   3.113 -
   3.114 -val setup_builtins =
   3.115 -  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
   3.116 -  fold (add_word_fun if_fixed_all) [
   3.117 -    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
   3.118 -    (@{term "plus :: 'a::len word => _"}, "bvadd"),
   3.119 -    (@{term "minus :: 'a::len word => _"}, "bvsub"),
   3.120 -    (@{term "times :: 'a::len word => _"}, "bvmul"),
   3.121 -    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
   3.122 -    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
   3.123 -    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
   3.124 -    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
   3.125 -    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
   3.126 -  fold (add_word_fun shift) [
   3.127 -    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
   3.128 -    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
   3.129 -    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
   3.130 -  add_word_fun extract
   3.131 -    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
   3.132 -  fold (add_word_fun extend) [
   3.133 -    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
   3.134 -    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
   3.135 -  fold (add_word_fun rotate) [
   3.136 -    (@{term word_rotl}, "rotate_left"),
   3.137 -    (@{term word_rotr}, "rotate_right") ] #>
   3.138 -  fold (add_word_fun if_fixed_args) [
   3.139 -    (@{term "less :: 'a::len word => _"}, "bvult"),
   3.140 -    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
   3.141 -    (@{term word_sless}, "bvslt"),
   3.142 -    (@{term word_sle}, "bvsle") ]
   3.143 -
   3.144 -end
   3.145 -
   3.146 -
   3.147 -(* setup *)
   3.148 -
   3.149 -val setup = 
   3.150 -  Context.theory_map (
   3.151 -    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
   3.152 -    setup_builtins)
   3.153 -
   3.154 -end
     4.1 --- a/src/HOL/Word/Word.thy	Thu Aug 28 00:40:37 2014 +0200
     4.2 +++ b/src/HOL/Word/Word.thy	Thu Aug 28 00:40:37 2014 +0200
     4.3 @@ -4753,8 +4753,6 @@
     4.4  declare bin_to_bl_def [simp]
     4.5  
     4.6  ML_file "Tools/word_lib.ML"
     4.7 -ML_file "Tools/smt_word.ML"
     4.8 -setup SMT_Word.setup
     4.9  ML_file "Tools/smt2_word.ML"
    4.10  
    4.11  hide_const (open) Word