|
40277
|
1 |
(* Title: HOL/Tools/SMT/smt_builtin.ML
|
|
|
2 |
Author: Sascha Boehme, TU Muenchen
|
|
|
3 |
|
|
|
4 |
Crafted collection of SMT built-in symbols.
|
|
|
5 |
|
|
|
6 |
FIXME: This list is currently not automatically kept synchronized with the
|
|
|
7 |
remaining implementation.
|
|
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
signature SMT_BUILTIN =
|
|
|
11 |
sig
|
|
|
12 |
val is_partially_builtin: Proof.context -> string * typ -> bool
|
|
|
13 |
val is_builtin: Proof.context -> string * typ -> bool
|
|
|
14 |
end
|
|
|
15 |
|
|
|
16 |
structure SMT_Builtin: SMT_BUILTIN =
|
|
|
17 |
struct
|
|
|
18 |
|
|
|
19 |
fun is_arithT (Type (@{type_name fun}, [T, _])) =
|
|
|
20 |
(case T of
|
|
|
21 |
@{typ int} => true
|
|
|
22 |
| @{typ nat} => true
|
|
|
23 |
| Type ("RealDef.real", []) => true
|
|
|
24 |
| _ => false)
|
|
|
25 |
| is_arithT _ = false
|
|
|
26 |
|
|
|
27 |
val builtins = Symtab.make [
|
|
|
28 |
|
|
|
29 |
(* Pure constants *)
|
|
|
30 |
(@{const_name all}, K true),
|
|
|
31 |
(@{const_name "=="}, K true),
|
|
|
32 |
(@{const_name "==>"}, K true),
|
|
|
33 |
(@{const_name Trueprop}, K true),
|
|
|
34 |
|
|
|
35 |
(* logical constants *)
|
|
|
36 |
(@{const_name All}, K true),
|
|
|
37 |
(@{const_name Ex}, K true),
|
|
|
38 |
(@{const_name Ball}, K true),
|
|
|
39 |
(@{const_name Bex}, K true),
|
|
|
40 |
(@{const_name Ex1}, K true),
|
|
|
41 |
(@{const_name True}, K true),
|
|
|
42 |
(@{const_name False}, K true),
|
|
|
43 |
(@{const_name Not}, K true),
|
|
|
44 |
(@{const_name HOL.conj}, K true),
|
|
|
45 |
(@{const_name HOL.disj}, K true),
|
|
|
46 |
(@{const_name HOL.implies}, K true),
|
|
|
47 |
|
|
|
48 |
(* term abbreviations *)
|
|
|
49 |
(@{const_name If}, K true),
|
|
|
50 |
(@{const_name bool.bool_case}, K true),
|
|
|
51 |
(@{const_name Let}, K true),
|
|
|
52 |
(@{const_name SMT.distinct}, K true),
|
|
|
53 |
|
|
|
54 |
(* technicalities *)
|
|
|
55 |
(@{const_name SMT.pat}, K true),
|
|
|
56 |
(@{const_name SMT.nopat}, K true),
|
|
|
57 |
(@{const_name SMT.trigger}, K true),
|
|
40664
|
58 |
(@{const_name SMT.weight}, K true),
|
|
40277
|
59 |
(@{const_name SMT.fun_app}, K true),
|
|
|
60 |
(@{const_name SMT.z3div}, K true),
|
|
|
61 |
(@{const_name SMT.z3mod}, K true),
|
|
|
62 |
|
|
|
63 |
(* equality *)
|
|
|
64 |
(@{const_name HOL.eq}, K true),
|
|
|
65 |
|
|
|
66 |
(* numerals *)
|
|
|
67 |
(@{const_name zero_class.zero}, K true),
|
|
|
68 |
(@{const_name one_class.one}, K true),
|
|
|
69 |
(@{const_name Int.Pls}, K true),
|
|
|
70 |
(@{const_name Int.Min}, K true),
|
|
|
71 |
(@{const_name Int.Bit0}, K true),
|
|
|
72 |
(@{const_name Int.Bit1}, K true),
|
|
|
73 |
(@{const_name number_of}, K true),
|
|
|
74 |
|
|
|
75 |
(* arithmetic *)
|
|
|
76 |
(@{const_name nat}, K true),
|
|
|
77 |
(@{const_name of_nat}, K true),
|
|
|
78 |
(@{const_name Suc}, K true),
|
|
|
79 |
(@{const_name plus}, is_arithT),
|
|
|
80 |
(@{const_name uminus}, is_arithT),
|
|
|
81 |
(@{const_name minus}, is_arithT),
|
|
|
82 |
(@{const_name abs}, is_arithT),
|
|
|
83 |
(@{const_name min}, is_arithT),
|
|
|
84 |
(@{const_name max}, is_arithT),
|
|
|
85 |
(@{const_name less}, is_arithT),
|
|
|
86 |
(@{const_name less_eq}, is_arithT),
|
|
|
87 |
|
|
|
88 |
(* pairs *)
|
|
|
89 |
(@{const_name fst}, K true),
|
|
|
90 |
(@{const_name snd}, K true),
|
|
|
91 |
(@{const_name Pair}, K true)
|
|
|
92 |
|
|
|
93 |
]
|
|
|
94 |
|
|
|
95 |
val all_builtins =
|
|
|
96 |
builtins
|
|
|
97 |
|> Symtab.update (@{const_name times}, is_arithT)
|
|
|
98 |
|> Symtab.update (@{const_name div_class.div}, is_arithT)
|
|
|
99 |
|> Symtab.update (@{const_name div_class.mod}, is_arithT)
|
|
|
100 |
|> Symtab.update ("Rings.inverse_class.divide", is_arithT)
|
|
|
101 |
|
|
|
102 |
fun lookup_builtin bs (name, T) =
|
|
|
103 |
(case Symtab.lookup bs name of
|
|
|
104 |
SOME proper_type => proper_type T
|
|
|
105 |
| NONE => false)
|
|
|
106 |
|
|
|
107 |
fun is_partially_builtin _ = lookup_builtin builtins
|
|
|
108 |
|
|
|
109 |
fun is_builtin _ = lookup_builtin all_builtins
|
|
|
110 |
|
|
|
111 |
end
|