src/HOL/Library/Tools/smt_word.ML
author wenzelm
Fri, 01 Jan 2021 23:35:09 +0100
changeset 73021 f602a380e4f2
parent 72909 f9424ceea3c3
child 74097 6d7be1227d02
permissions -rw-r--r--
tuned signature -- prefer Isabelle/ML structure Integer (despite minor confusion due to canonical argument order of "pow");
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57696
diff changeset
     1
(*  Title:      HOL/Word/Tools/smt_word.ML
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     4
SMT setup for words.
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     5
*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     6
72508
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
     7
signature SMT_WORD =
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
     8
sig
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
     9
  val add_word_shift': term * string -> Context.generic -> Context.generic
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
    10
end
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
    11
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
    12
structure SMT_Word : SMT_WORD =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    13
struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    14
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    15
open Word_Lib
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    16
57229
blanchet
parents: 56078
diff changeset
    17
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    18
(* SMT-LIB logic *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    19
57696
fb71c6f100f8 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57553
diff changeset
    20
(* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers.
57553
2a6c31ac1c9a don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
blanchet
parents: 57229
diff changeset
    21
   Better set the logic to "" and make at least Z3 happy. *)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    22
fun smtlib_logic ts =
57553
2a6c31ac1c9a don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
blanchet
parents: 57229
diff changeset
    23
  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    24
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    25
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    26
(* SMT-LIB builtins *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    27
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    28
local
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57696
diff changeset
    29
  val smtlibC = SMTLIB_Interface.smtlibC
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    30
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
    31
  val wordT = \<^typ>\<open>'a::len word\<close>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    32
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    33
  fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    34
  fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    35
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
    36
  fun word_typ (Type (\<^type_name>\<open>word\<close>, [T])) =
66551
4df6b0ae900d towards support for HO SMT-LIB
blanchet
parents: 65336
diff changeset
    37
      Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    38
    | word_typ _ = NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    39
72909
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    40
  (*CVC4 does not support "_bvk T" when k does not fit in the BV of size T, so remove the bits that
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    41
   will be ignored according to the SMT-LIB*)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
    42
  fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
72909
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    43
        let
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    44
          val size = try dest_binT T
73021
f602a380e4f2 tuned signature -- prefer Isabelle/ML structure Integer (despite minor confusion due to canonical argument order of "pow");
wenzelm
parents: 72909
diff changeset
    45
          fun max_int size = Integer.pow size 2
72909
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    46
        in
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    47
          (case size of
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    48
            NONE => NONE
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    49
          | SOME size => SOME (index1 ("bv" ^ string_of_int (Int.rem(k, max_int size))) size))
f9424ceea3c3 don't generate not-fully-defined bit-vector constants in SMT problems
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72515
diff changeset
    50
        end
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    51
    | word_num _ _ = NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    52
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    53
  fun if_fixed pred m n T ts =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    54
    let val (Us, U) = Term.strip_type T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    55
    in
57696
fb71c6f100f8 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57553
diff changeset
    56
      if pred (U, Us) then SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) else NONE
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    57
    end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    58
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    59
  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    60
  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    61
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    62
  fun add_word_fun f (t, n) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    63
    let val (m, _) = Term.dest_Const t
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57696
diff changeset
    64
    in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    65
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
    66
  val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    67
72514
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    68
  fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    69
    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    70
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    71
  fun shift m n T ts =
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    72
    let val U = Term.domain_type (Term.range_type T)
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    73
    in
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    74
      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    75
        (true, SOME i) =>
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    76
          SOME (n, 2, [hd (tl ts), HOLogic.mk_number U i], mk_shift (m, T))
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    77
      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    78
    end
d8661799afb2 removed dependency
haftmann
parents: 72508
diff changeset
    79
72489
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    80
  fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    81
    | mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts)
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    82
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    83
  fun shift' m n T ts =
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    84
    let val U = Term.domain_type T
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    85
    in
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    86
      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    87
        (true, SOME i) =>
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    88
          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T))
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    89
      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    90
    end
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
    91
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    92
  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    93
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    94
  fun extract m n T ts =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    95
    let val U = Term.range_type (Term.range_type T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    96
    in
57696
fb71c6f100f8 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57553
diff changeset
    97
      (case (try (snd o HOLogic.dest_number o hd) ts, try dest_wordT U) of
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    98
        (SOME lb, SOME i) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    99
          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   100
      | _ => NONE)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   101
    end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   102
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   103
  fun mk_extend c ts = Term.list_comb (Const c, ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   104
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   105
  fun extend m n T ts =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   106
    let val (U1, U2) = Term.dest_funT T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   107
    in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   108
      (case (try dest_wordT U1, try dest_wordT U2) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   109
        (SOME i, SOME j) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   110
          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   111
          else NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   112
      | _ => NONE)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   113
    end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   114
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   115
  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   116
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   117
  fun rotate m n T ts =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   118
    let val U = Term.domain_type (Term.range_type T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   119
    in
57696
fb71c6f100f8 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents: 57553
diff changeset
   120
      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   121
        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   122
      | _ => NONE)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   123
    end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   124
in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   125
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   126
val setup_builtins =
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57696
diff changeset
   127
  SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   128
  fold (add_word_fun if_fixed_all) [
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   129
    (\<^term>\<open>uminus :: 'a::len word \<Rightarrow> _\<close>, "bvneg"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   130
    (\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   131
    (\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   132
    (\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"),
71826
f424e164d752 modernized notation for bit operations
haftmann
parents: 69597
diff changeset
   133
    (\<^term>\<open>NOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
f424e164d752 modernized notation for bit operations
haftmann
parents: 69597
diff changeset
   134
    (\<^term>\<open>(AND) :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
f424e164d752 modernized notation for bit operations
haftmann
parents: 69597
diff changeset
   135
    (\<^term>\<open>(OR) :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
f424e164d752 modernized notation for bit operations
haftmann
parents: 69597
diff changeset
   136
    (\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   137
    (\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   138
  fold (add_word_fun shift) [
72489
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
   139
    (\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
   140
    (\<^term>\<open>drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
a1366ce41368 early and more complete setup of tools
haftmann
parents: 71826
diff changeset
   141
    (\<^term>\<open>signed_drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   142
  add_word_fun extract
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   143
    (\<^term>\<open>slice :: _ \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "extract") #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   144
  fold (add_word_fun extend) [
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   145
    (\<^term>\<open>ucast :: 'a::len word \<Rightarrow> _\<close>, "zero_extend"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   146
    (\<^term>\<open>scast :: 'a::len word \<Rightarrow> _\<close>, "sign_extend") ] #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   147
  fold (add_word_fun rotate) [
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   148
    (\<^term>\<open>word_rotl\<close>, "rotate_left"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   149
    (\<^term>\<open>word_rotr\<close>, "rotate_right") ] #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   150
  fold (add_word_fun if_fixed_args) [
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   151
    (\<^term>\<open>less :: 'a::len word \<Rightarrow> _\<close>, "bvult"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   152
    (\<^term>\<open>less_eq :: 'a::len word \<Rightarrow> _\<close>, "bvule"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   153
    (\<^term>\<open>word_sless\<close>, "bvslt"),
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66551
diff changeset
   154
    (\<^term>\<open>word_sle\<close>, "bvsle") ]
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   155
72508
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
   156
val add_word_shift' = add_word_fun shift'
c89d8e8bd8c7 factored out theory Traditional_Syntax
haftmann
parents: 72489
diff changeset
   157
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   158
end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   159
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   160
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   161
(* setup *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   162
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   163
val _ = Theory.setup (Context.theory_map (
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57696
diff changeset
   164
  SMTLIB_Interface.add_logic (20, smtlib_logic) #>
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   165
  setup_builtins))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   166
57229
blanchet
parents: 56078
diff changeset
   167
end;