1(* Title: HOL/Tools/SMT/z3_real.ML 2 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