author | blanchet |
Sun, 27 Jul 2014 21:20:11 +0200 | |
changeset 57823 | d1e9022c0175 |
parent 57553 | 2a6c31ac1c9a |
permissions | -rw-r--r-- |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Word/Tools/smt2_word.ML |
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 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
7 |
structure SMT2_Word: sig end = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
open Word_Lib |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
|
57229 | 12 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
(* SMT-LIB logic *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
|
57823
d1e9022c0175
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
|
15 |
(* "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
|
16 |
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
|
17 |
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
|
18 |
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
|
19 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
21 |
(* SMT-LIB builtins *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
val smtlib2C = SMTLIB2_Interface.smtlib2C |
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 |
val wordT = @{typ "'a::len word"} |
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 |
fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
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
|
30 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
32 |
| word_typ _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
34 |
fun word_num (Type (@{type_name word}, [T])) k = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
Option.map (index1 ("bv" ^ string_of_int k)) (try dest_binT T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
| word_num _ _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
37 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
38 |
fun if_fixed pred m n T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
39 |
let val (Us, U) = Term.strip_type T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
40 |
in |
57823
d1e9022c0175
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
|
41 |
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
|
42 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
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
|
45 |
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
|
46 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
fun add_word_fun f (t, n) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
let val (m, _) = Term.dest_Const t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
in SMT2_Builtin.add_builtin_fun smtlib2C (Term.dest_Const t, K (f m n)) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
|
57823
d1e9022c0175
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
|
51 |
val mk_nat = HOLogic.mk_number @{typ nat} |
56078
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 mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
54 |
| mk_shift c ts = raise TERM ("bad arguments", Const c :: ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
55 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
56 |
fun shift m n T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
57 |
let val U = Term.domain_type T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
in |
57823
d1e9022c0175
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
|
59 |
(case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
(true, SOME i) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
| _ => NONE) (* FIXME: also support non-numerical shifts *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
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
|
66 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
67 |
fun extract m n T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
68 |
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
|
69 |
in |
57823
d1e9022c0175
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
|
70 |
(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
|
71 |
(SOME lb, SOME i) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
72 |
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
|
73 |
| _ => NONE) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
74 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
75 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
76 |
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
|
77 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
fun extend m n T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
79 |
let val (U1, U2) = Term.dest_funT T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
80 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
81 |
(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
|
82 |
(SOME i, SOME j) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
83 |
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
|
84 |
else NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
| _ => NONE) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
86 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
87 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
88 |
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
|
89 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
90 |
fun rotate m n T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
91 |
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
|
92 |
in |
57823
d1e9022c0175
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
|
93 |
(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
|
94 |
(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
|
95 |
| _ => NONE) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
96 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
98 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
99 |
val setup_builtins = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
100 |
SMT2_Builtin.add_builtin_typ smtlib2C (wordT, word_typ, word_num) #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
101 |
fold (add_word_fun if_fixed_all) [ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
102 |
(@{term "uminus :: 'a::len word => _"}, "bvneg"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
103 |
(@{term "plus :: 'a::len word => _"}, "bvadd"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
104 |
(@{term "minus :: 'a::len word => _"}, "bvsub"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
(@{term "times :: 'a::len word => _"}, "bvmul"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
106 |
(@{term "bitNOT :: 'a::len word => _"}, "bvnot"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
(@{term "bitAND :: 'a::len word => _"}, "bvand"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
(@{term "bitOR :: 'a::len word => _"}, "bvor"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
(@{term "bitXOR :: 'a::len word => _"}, "bvxor"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
(@{term "word_cat :: 'a::len word => _"}, "concat") ] #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
111 |
fold (add_word_fun shift) [ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
112 |
(@{term "shiftl :: 'a::len word => _ "}, "bvshl"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
113 |
(@{term "shiftr :: 'a::len word => _"}, "bvlshr"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
(@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
115 |
add_word_fun extract |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
(@{term "slice :: _ => 'a::len word => _"}, "extract") #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
fold (add_word_fun extend) [ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
(@{term "ucast :: 'a::len word => _"}, "zero_extend"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
119 |
(@{term "scast :: 'a::len word => _"}, "sign_extend") ] #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
fold (add_word_fun rotate) [ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
(@{term word_rotl}, "rotate_left"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
(@{term word_rotr}, "rotate_right") ] #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
fold (add_word_fun if_fixed_args) [ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
124 |
(@{term "less :: 'a::len word => _"}, "bvult"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
(@{term "less_eq :: 'a::len word => _"}, "bvule"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
(@{term word_sless}, "bvslt"), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
(@{term word_sle}, "bvsle") ] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
132 |
(* setup *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
val _ = Theory.setup (Context.theory_map ( |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
SMTLIB2_Interface.add_logic (20, smtlib_logic) #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
136 |
setup_builtins)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
|
57229 | 138 |
end; |