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