|
1 (* Title: HOL/Library/SMT/smt_real.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 SMT setup for reals. |
|
5 *) |
|
6 |
|
7 signature SMT_REAL = |
|
8 sig |
|
9 val setup: theory -> theory |
|
10 end |
|
11 |
|
12 structure SMT_Real: SMT_REAL = |
|
13 struct |
|
14 |
|
15 |
|
16 (* SMT-LIB logic *) |
|
17 |
|
18 fun smtlib_logic ts = |
|
19 if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts |
|
20 then SOME "AUFLIRA" |
|
21 else NONE |
|
22 |
|
23 |
|
24 (* SMT-LIB and Z3 built-ins *) |
|
25 |
|
26 local |
|
27 fun real_num _ i = SOME (string_of_int i ^ ".0") |
|
28 |
|
29 fun is_linear [t] = SMT_Utils.is_number t |
|
30 | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u |
|
31 | is_linear _ = false |
|
32 |
|
33 fun mk_times ts = Term.list_comb (@{const times (real)}, ts) |
|
34 |
|
35 fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
|
36 | times _ _ _ = NONE |
|
37 in |
|
38 |
|
39 val setup_builtins = |
|
40 SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC |
|
41 (@{typ real}, K (SOME "Real"), real_num) #> |
|
42 fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [ |
|
43 (@{const less (real)}, "<"), |
|
44 (@{const less_eq (real)}, "<="), |
|
45 (@{const uminus (real)}, "~"), |
|
46 (@{const plus (real)}, "+"), |
|
47 (@{const minus (real)}, "-") ] #> |
|
48 SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC |
|
49 (Term.dest_Const @{const times (real)}, times) #> |
|
50 SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C |
|
51 (@{const times (real)}, "*") #> |
|
52 SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C |
|
53 (@{const divide (real)}, "/") |
|
54 |
|
55 end |
|
56 |
|
57 |
|
58 (* Z3 constructors *) |
|
59 |
|
60 local |
|
61 fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME @{typ real} |
|
62 | z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME @{typ real} |
|
63 (*FIXME: delete*) |
|
64 | z3_mk_builtin_typ _ = NONE |
|
65 |
|
66 fun z3_mk_builtin_num _ i T = |
|
67 if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) |
|
68 else NONE |
|
69 |
|
70 fun mk_nary _ cu [] = cu |
|
71 | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
|
72 |
|
73 val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) |
|
74 val add = Thm.cterm_of @{theory} @{const plus (real)} |
|
75 val real0 = Numeral.mk_cnumber @{ctyp real} 0 |
|
76 val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
|
77 val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
|
78 val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
|
79 val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |
|
80 val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) |
|
81 |
|
82 fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
|
83 | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = |
|
84 SOME (mk_nary add real0 cts) |
|
85 | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = |
|
86 SOME (mk_sub ct cu) |
|
87 | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = |
|
88 SOME (mk_mul ct cu) |
|
89 | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = |
|
90 SOME (mk_div ct cu) |
|
91 | z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] = |
|
92 SOME (mk_lt ct cu) |
|
93 | z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] = |
|
94 SOME (mk_le ct cu) |
|
95 | z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] = |
|
96 SOME (mk_lt cu ct) |
|
97 | z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] = |
|
98 SOME (mk_le cu ct) |
|
99 | z3_mk_builtin_fun _ _ = NONE |
|
100 in |
|
101 |
|
102 val z3_mk_builtins = { |
|
103 mk_builtin_typ = z3_mk_builtin_typ, |
|
104 mk_builtin_num = z3_mk_builtin_num, |
|
105 mk_builtin_fun = (fn _ => fn sym => fn cts => |
|
106 (case try (#T o Thm.rep_cterm o hd) cts of |
|
107 SOME @{typ real} => z3_mk_builtin_fun sym cts |
|
108 | _ => NONE)) } |
|
109 |
|
110 end |
|
111 |
|
112 |
|
113 (* Z3 proof reconstruction *) |
|
114 |
|
115 val real_rules = @{lemma |
|
116 "0 + (x::real) = x" |
|
117 "x + 0 = x" |
|
118 "0 * x = 0" |
|
119 "1 * x = x" |
|
120 "x + y = y + x" |
|
121 by auto} |
|
122 |
|
123 val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ |
|
124 "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc |
|
125 |
|
126 |
|
127 (* setup *) |
|
128 |
|
129 val setup = |
|
130 Context.theory_map ( |
|
131 SMTLIB_Interface.add_logic (10, smtlib_logic) #> |
|
132 setup_builtins #> |
|
133 Z3_Interface.add_mk_builtins z3_mk_builtins #> |
|
134 fold Z3_Proof_Reconstruction.add_z3_rule real_rules #> |
|
135 Z3_Proof_Tools.add_simproc real_linarith_proc) |
|
136 |
|
137 end |