author | wenzelm |
Fri, 01 Jan 2021 23:35:09 +0100 | |
changeset 73021 | f602a380e4f2 |
parent 72909 | f9424ceea3c3 |
child 74097 | 6d7be1227d02 |
permissions | -rw-r--r-- |
58061 | 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 | 7 |
signature SMT_WORD = |
8 |
sig |
|
9 |
val add_word_shift': term * string -> Context.generic -> Context.generic |
|
10 |
end |
|
11 |
||
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 | 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 | 29 |
val smtlibC = SMTLIB_Interface.smtlibC |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
|
69597 | 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 | 36 |
fun word_typ (Type (\<^type_name>\<open>word\<close>, [T])) = |
66551 | 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 | 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 | 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 | 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 | 68 |
fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t |
69 |
| mk_shift c ts = raise TERM ("bad arguments", Const c :: ts) |
|
70 |
||
71 |
fun shift m n T ts = |
|
72 |
let val U = Term.domain_type (Term.range_type T) |
|
73 |
in |
|
74 |
(case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of |
|
75 |
(true, SOME i) => |
|
76 |
SOME (n, 2, [hd (tl ts), HOLogic.mk_number U i], mk_shift (m, T)) |
|
77 |
| _ => NONE) (* FIXME: also support non-numerical shifts *) |
|
78 |
end |
|
79 |
||
72489 | 80 |
fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u)) |
81 |
| mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts) |
|
82 |
||
83 |
fun shift' m n T ts = |
|
84 |
let val U = Term.domain_type T |
|
85 |
in |
|
86 |
(case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of |
|
87 |
(true, SOME i) => |
|
88 |
SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T)) |
|
89 |
| _ => NONE) (* FIXME: also support non-numerical shifts *) |
|
90 |
end |
|
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 | 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 | 129 |
(\<^term>\<open>uminus :: 'a::len word \<Rightarrow> _\<close>, "bvneg"), |
130 |
(\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"), |
|
131 |
(\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"), |
|
132 |
(\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"), |
|
71826 | 133 |
(\<^term>\<open>NOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"), |
134 |
(\<^term>\<open>(AND) :: 'a::len word \<Rightarrow> _\<close>, "bvand"), |
|
135 |
(\<^term>\<open>(OR) :: 'a::len word \<Rightarrow> _\<close>, "bvor"), |
|
136 |
(\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"), |
|
69597 | 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 | 139 |
(\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"), |
140 |
(\<^term>\<open>drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvlshr"), |
|
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 | 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 | 145 |
(\<^term>\<open>ucast :: 'a::len word \<Rightarrow> _\<close>, "zero_extend"), |
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 | 148 |
(\<^term>\<open>word_rotl\<close>, "rotate_left"), |
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 | 151 |
(\<^term>\<open>less :: 'a::len word \<Rightarrow> _\<close>, "bvult"), |
152 |
(\<^term>\<open>less_eq :: 'a::len word \<Rightarrow> _\<close>, "bvule"), |
|
153 |
(\<^term>\<open>word_sless\<close>, "bvslt"), |
|
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 | 156 |
val add_word_shift' = add_word_fun shift' |
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 | 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 | 167 |
end; |