author | wenzelm |
Tue, 28 Sep 2021 22:14:02 +0200 | |
changeset 74382 | 8d0294d877bd |
parent 69593 | 3dda49e08b9d |
child 74817 | 1fd8705503b4 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smt_real.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 |
SMT setup for reals. |
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 |
structure SMT_Real: sig end = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
|
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 |
(* SMT-LIB logic *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
fun smtlib_logic ts = |
69593 | 14 |
if exists (Term.exists_type (Term.exists_subtype (equal \<^typ>\<open>real\<close>))) ts |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
then SOME "AUFLIRA" |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
else NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
(* SMT-LIB and Z3 built-ins *) |
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 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
fun real_num _ i = SOME (string_of_int i ^ ".0") |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
|
58061 | 24 |
fun is_linear [t] = SMT_Util.is_number t |
25 |
| is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
| is_linear _ = false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
|
74382 | 28 |
fun mk_times ts = Term.list_comb (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, ts) |
56078
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 |
fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
32 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
val setup_builtins = |
58061 | 34 |
SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC |
69593 | 35 |
(\<^typ>\<open>real\<close>, K (SOME ("Real", [])), real_num) #> |
58061 | 36 |
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [ |
74382 | 37 |
(\<^Const>\<open>less \<^Type>\<open>real\<close>\<close>, "<"), |
38 |
(\<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>, "<="), |
|
39 |
(\<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>, "-"), |
|
40 |
(\<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, "+"), |
|
41 |
(\<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>, "-") ] #> |
|
58061 | 42 |
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC |
74382 | 43 |
(Term.dest_Const \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, times) #> |
58061 | 44 |
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C |
74382 | 45 |
(\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, "*") #> |
58061 | 46 |
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C |
74382 | 47 |
(\<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, "/") |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
51 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
52 |
(* Z3 constructors *) |
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 |
local |
69593 | 55 |
fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME \<^typ>\<open>real\<close> |
56 |
| z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME \<^typ>\<open>real\<close> |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
57 |
(*FIXME: delete*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
| z3_mk_builtin_typ _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
59 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
fun z3_mk_builtin_num _ i T = |
69593 | 61 |
if T = \<^typ>\<open>real\<close> then SOME (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> i) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
else NONE |
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 |
fun mk_nary _ cu [] = cu |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
| 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
|
66 |
|
74382 | 67 |
val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> |
68 |
val add = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close> |
|
69593 | 69 |
val real0 = Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 0 |
74382 | 70 |
val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close> |
71 |
val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> |
|
72 |
val mk_div = Thm.mk_binop \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close> |
|
73 |
val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close> |
|
74 |
val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close> |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
75 |
|
58061 | 76 |
fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
77 |
| z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts) |
|
78 |
| z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu) |
|
79 |
| z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu) |
|
80 |
| z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu) |
|
81 |
| z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu) |
|
82 |
| z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu) |
|
83 |
| z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct) |
|
84 |
| z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
| z3_mk_builtin_fun _ _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
86 |
in |
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 |
val z3_mk_builtins = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
89 |
mk_builtin_typ = z3_mk_builtin_typ, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
90 |
mk_builtin_num = z3_mk_builtin_num, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
91 |
mk_builtin_fun = (fn _ => fn sym => fn cts => |
59586 | 92 |
(case try (Thm.typ_of_cterm o hd) cts of |
69593 | 93 |
SOME \<^typ>\<open>real\<close> => z3_mk_builtin_fun sym cts |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
94 |
| _ => NONE)) } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
95 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
96 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
98 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
99 |
(* Z3 proof replay *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
100 |
|
61144 | 101 |
val real_linarith_proc = |
69593 | 102 |
Simplifier.make_simproc \<^context> "fast_real_arith" |
103 |
{lhss = [\<^term>\<open>(m::real) < n\<close>, \<^term>\<open>(m::real) \<le> n\<close>, \<^term>\<open>(m::real) = n\<close>], |
|
62913 | 104 |
proc = K Lin_Arith.simproc} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
106 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
(* setup *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
val _ = Theory.setup (Context.theory_map ( |
58061 | 110 |
SMTLIB_Interface.add_logic (10, smtlib_logic) #> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
111 |
setup_builtins #> |
58061 | 112 |
Z3_Interface.add_mk_builtins z3_mk_builtins #> |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
66551
diff
changeset
|
113 |
SMT_Replay.add_simproc real_linarith_proc)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
|
57229 | 115 |
end; |