author | haftmann |
Sat, 19 Dec 2015 17:03:17 +0100 | |
changeset 61891 | 76189756ff65 |
parent 60352 | d46de31a50c4 |
child 63950 | cdc1e59aa513 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/z3_interface.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 |
Interface to Z3 based on a relaxed version of SMT-LIB. |
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 |
|
58061 | 7 |
signature Z3_INTERFACE = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
sig |
58061 | 9 |
val smtlib_z3C: SMT_Util.class |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
datatype sym = Sym of string * sym list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
type mk_builtins = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
mk_builtin_typ: sym -> typ option, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
mk_builtin_num: theory -> int -> typ -> cterm option, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
mk_builtin_fun: theory -> sym -> cterm list -> cterm option } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
val mk_builtin_typ: Proof.context -> sym -> typ option |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
val mk_builtin_num: Proof.context -> int -> typ -> cterm option |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option |
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 |
val is_builtin_theory_term: Proof.context -> term -> bool |
57229 | 22 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
|
58061 | 24 |
structure Z3_Interface: Z3_INTERFACE = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
|
58061 | 27 |
val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
28 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
(* interface *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
32 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
fun translate_config ctxt = |
58360 | 34 |
{logic = K "", fp_kinds = [BNF_Util.Least_FP], |
58061 | 35 |
serialize = #serialize (SMTLIB_Interface.translate_config ctxt)} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
|
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59632
diff
changeset
|
37 |
fun is_div_mod @{const divide (int)} = true |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
38 |
| is_div_mod @{const mod (int)} = true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
39 |
| is_div_mod _ = false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
40 |
|
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56101
diff
changeset
|
41 |
val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
42 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
fun add_div_mod _ (thms, extra_thms) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
if have_int_div_mod thms orelse have_int_div_mod extra_thms then |
56101 | 45 |
(thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
else (thms, extra_thms) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
val setup_builtins = |
58061 | 49 |
SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #> |
50 |
SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> |
|
51 |
SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
52 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
54 |
val _ = Theory.setup (Context.theory_map ( |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
55 |
setup_builtins #> |
58061 | 56 |
SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #> |
57 |
SMT_Translate.add_config (smtlib_z3C, translate_config))) |
|
56078
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 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
|
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 |
(* constructors *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
datatype sym = Sym of string * sym list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
|
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 |
(** additional constructors **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
68 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
69 |
type mk_builtins = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
70 |
mk_builtin_typ: sym -> typ option, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
71 |
mk_builtin_num: theory -> int -> typ -> cterm option, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
72 |
mk_builtin_fun: theory -> sym -> cterm list -> cterm option } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
73 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
74 |
fun chained _ [] = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
75 |
| chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
76 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
77 |
fun chained_mk_builtin_typ bs sym = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
79 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
80 |
fun chained_mk_builtin_num ctxt bs i T = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
81 |
let val thy = Proof_Context.theory_of ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
82 |
in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
83 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
84 |
fun chained_mk_builtin_fun ctxt bs s cts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
let val thy = Proof_Context.theory_of ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
86 |
in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs 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 fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) |
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 |
structure Mk_Builtins = Generic_Data |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
91 |
( |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
92 |
type T = (int * mk_builtins) list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
93 |
val empty = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
94 |
val extend = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
95 |
fun merge data = Ord_List.merge fst_int_ord data |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
96 |
) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
|
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56101
diff
changeset
|
98 |
fun add_mk_builtins mk = Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
99 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
100 |
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
101 |
|
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 |
(** basic and additional constructors **) |
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 mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool} |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
106 |
| mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
| mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
| mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
| mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
111 |
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
112 |
| mk_builtin_num ctxt i T = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
113 |
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
|
59632 | 115 |
val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False}) |
116 |
val mk_false = Thm.cterm_of @{context} @{const False} |
|
117 |
val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not}) |
|
118 |
val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies}) |
|
119 |
val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)}) |
|
120 |
val conj = Thm.cterm_of @{context} @{const HOL.conj} |
|
121 |
val disj = Thm.cterm_of @{context} @{const HOL.disj} |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
fun mk_nary _ cu [] = cu |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
124 |
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
|
58061 | 126 |
val eq = SMT_Util.mk_const_pat @{theory} @{const_name HOL.eq} SMT_Util.destT1 |
127 |
fun mk_eq ct cu = Thm.mk_binop (SMT_Util.instT' ct eq) ct cu |
|
56078
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 |
val if_term = |
58061 | 130 |
SMT_Util.mk_const_pat @{theory} @{const_name If} (SMT_Util.destT1 o SMT_Util.destT2) |
131 |
fun mk_if cc ct = Thm.mk_binop (Thm.apply (SMT_Util.instT' ct if_term) cc) ct |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
132 |
|
58061 | 133 |
val access = SMT_Util.mk_const_pat @{theory} @{const_name fun_app} SMT_Util.destT1 |
134 |
fun mk_access array = Thm.apply (SMT_Util.instT' array access) array |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
|
56090 | 136 |
val update = |
58061 | 137 |
SMT_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT_Util.destT1) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
fun mk_update array index value = |
59586 | 139 |
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array) |
58061 | 140 |
in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
141 |
|
59632 | 142 |
val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)}) |
143 |
val add = Thm.cterm_of @{context} @{const plus (int)} |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
val int0 = Numeral.mk_cnumber @{ctyp int} 0 |
59632 | 145 |
val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)}) |
146 |
val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)}) |
|
147 |
val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div}) |
|
148 |
val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod}) |
|
149 |
val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)}) |
|
150 |
val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)}) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
151 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
fun mk_builtin_fun ctxt sym cts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
153 |
(case (sym, cts) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
(Sym ("true", _), []) => SOME mk_true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
| (Sym ("false", _), []) => SOME mk_false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
156 |
| (Sym ("not", _), [ct]) => SOME (mk_not ct) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
| (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
| (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
159 |
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
160 |
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
161 |
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
162 |
| (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
163 |
| (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
164 |
| (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
165 |
| (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
166 |
| (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
167 |
| (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
168 |
| _ => |
59586 | 169 |
(case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
170 |
(Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
171 |
| (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
172 |
| (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
| (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
174 |
| (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
175 |
| (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
176 |
| (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
177 |
| (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
178 |
| (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
179 |
| (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
180 |
| _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
181 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
182 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
(* abstraction *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
184 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
185 |
fun is_builtin_theory_term ctxt t = |
58061 | 186 |
if SMT_Builtin.is_builtin_num ctxt t then true |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
187 |
else |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
188 |
(case Term.strip_comb t of |
58061 | 189 |
(Const c, ts) => SMT_Builtin.is_builtin_fun ctxt c ts |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
190 |
| _ => false) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
191 |
|
57229 | 192 |
end; |