10 end |
10 end |
11 |
11 |
12 structure SMT_Real: SMT_REAL = |
12 structure SMT_Real: SMT_REAL = |
13 struct |
13 struct |
14 |
14 |
|
15 structure B = SMT_Builtin |
|
16 |
15 |
17 |
16 (* SMT-LIB logic *) |
18 (* SMT-LIB logic *) |
17 |
19 |
18 fun smtlib_logic ts = |
20 fun smtlib_logic ts = |
19 if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts |
21 if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts |
20 then SOME "AUFLIRA" |
22 then SOME "AUFLIRA" |
21 else NONE |
23 else NONE |
22 |
24 |
23 |
25 |
24 |
26 (* SMT-LIB and Z3 built-ins *) |
25 (* SMT-LIB builtins *) |
|
26 |
27 |
27 local |
28 local |
28 fun smtlib_builtin_typ @{typ real} = SOME "Real" |
29 val smtlibC = SMTLIB_Interface.smtlibC |
29 | smtlib_builtin_typ _ = NONE |
|
30 |
30 |
31 fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0") |
31 fun real_num _ i = SOME (string_of_int i ^ ".0") |
32 | smtlib_builtin_num _ _ = NONE |
|
33 |
|
34 fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts) |
|
35 | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts) |
|
36 | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts) |
|
37 | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts) |
|
38 | smtlib_builtin_func _ _ = NONE |
|
39 |
|
40 fun smtlib_builtin_pred @{const_name less} = SOME "<" |
|
41 | smtlib_builtin_pred @{const_name less_eq} = SOME "<=" |
|
42 | smtlib_builtin_pred _ = NONE |
|
43 |
|
44 fun real_fun T y f x = |
|
45 (case try Term.domain_type T of |
|
46 SOME @{typ real} => f x |
|
47 | _ => y) |
|
48 in |
32 in |
49 |
33 |
50 val smtlib_builtins = { |
34 val setup_builtins = |
51 builtin_typ = smtlib_builtin_typ, |
35 B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #> |
52 builtin_num = smtlib_builtin_num, |
36 fold (B.add_builtin_fun' smtlibC) [ |
53 builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)), |
37 (@{const uminus (real)}, "~"), |
54 builtin_pred = (fn (n, T) => fn ts => |
38 (@{const plus (real)}, "+"), |
55 real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)), |
39 (@{const minus (real)}, "-"), |
56 is_builtin_pred = (fn n => fn T => |
40 (@{const times (real)}, "*"), |
57 real_fun T false (is_some o smtlib_builtin_pred) n) } |
41 (@{const less (real)}, "<"), |
|
42 (@{const less_eq (real)}, "<=") ] #> |
|
43 B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/") |
58 |
44 |
59 end |
45 end |
60 |
|
61 |
|
62 |
|
63 (* Z3 builtins *) |
|
64 |
|
65 local |
|
66 fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts) |
|
67 | z3_builtin_fun _ _ = NONE |
|
68 in |
|
69 |
|
70 val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts) |
|
71 |
|
72 end |
|
73 |
|
74 |
46 |
75 |
47 |
76 (* Z3 constructors *) |
48 (* Z3 constructors *) |
77 |
49 |
78 local |
50 local |
130 |
101 |
131 val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ |
102 val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ |
132 "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc) |
103 "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc) |
133 |
104 |
134 |
105 |
135 |
|
136 (* setup *) |
106 (* setup *) |
137 |
107 |
138 val setup = |
108 val setup = |
|
109 setup_builtins #> |
139 Context.theory_map ( |
110 Context.theory_map ( |
140 SMTLIB_Interface.add_logic smtlib_logic #> |
111 SMTLIB_Interface.add_logic (10, smtlib_logic) #> |
141 SMTLIB_Interface.add_builtins smtlib_builtins #> |
|
142 Z3_Interface.add_builtin_funs z3_builtins #> |
|
143 Z3_Interface.add_mk_builtins z3_mk_builtins #> |
112 Z3_Interface.add_mk_builtins z3_mk_builtins #> |
144 fold Z3_Proof_Reconstruction.add_z3_rule real_rules #> |
113 fold Z3_Proof_Reconstruction.add_z3_rule real_rules #> |
145 Z3_Proof_Tools.add_simproc real_linarith_proc) |
114 Z3_Proof_Tools.add_simproc real_linarith_proc) |
146 |
115 |
147 end |
116 end |