src/HOL/Tools/SMT/z3_real.ML
author blanchet
Thu Aug 28 00:40:38 2014 +0200 (2014-08-28)
changeset 58061 3d060f43accb
parent 57229 src/HOL/Tools/SMT2/z3_new_real.ML@489083abce44
child 60352 d46de31a50c4
permissions -rw-r--r--
renamed new SMT module from 'SMT2' to 'SMT'
     1 (*  Title:      HOL/Tools/SMT/z3_real.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Z3 setup for reals.
     5 *)
     6 
     7 structure Z3_Real: sig end =
     8 struct
     9 
    10 fun real_type_parser (SMTLIB.Sym "Real", []) = SOME @{typ Real.real}
    11   | real_type_parser _ = NONE
    12 
    13 fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
    14   | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
    15       SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2)
    16   | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
    17   | real_term_parser _ = NONE
    18 
    19 fun abstract abs t =
    20   (case t of
    21     (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 =>
    22       abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
    23   | (c as @{term "Real.real :: int => _"}) $ t =>
    24       abs t #>> (fn u => SOME (c $ u))
    25   | _ => pair NONE)
    26 
    27 val _ = Theory.setup (Context.theory_map (
    28   SMTLIB_Proof.add_type_parser real_type_parser #>
    29   SMTLIB_Proof.add_term_parser real_term_parser #>
    30   Z3_Replay_Methods.add_arith_abstracter abstract))
    31 
    32 end;