1261991Sdim(*  Title:      HOL/Tools/SMT/z3_real.ML
2261991Sdim    Author:     Sascha Boehme, TU Muenchen
3
4Z3 setup for reals.
5*)
6
7structure Z3_Real: sig end =
8struct
9
10fun real_type_parser (SMTLIB.Sym "Real", []) = SOME \<^typ>\<open>Real.real\<close>
11  | real_type_parser _ = NONE
12
13fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number \<^typ>\<open>Real.real\<close> i)
14  | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
15      SOME (\<^term>\<open>Rings.divide :: real => _\<close> $ t1 $ t2)
16  | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (\<^term>\<open>Int.of_int :: int => _\<close> $ t)
17  | real_term_parser _ = NONE
18
19fun abstract abs t =
20  (case t of
21    (c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
22      abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
23  | (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ t =>
24      abs t #>> (fn u => SOME (c $ u))
25  | _ => pair NONE)
26
27val _ = Theory.setup (Context.theory_map (
28  SMTLIB_Proof.add_type_parser real_type_parser #>
29  SMTLIB_Proof.add_term_parser real_term_parser #>
30  SMT_Replay_Methods.add_arith_abstracter abstract))
31
32end;
33