src/HOL/Tools/SMT/smt_real.ML
changeset 41280 a7de9d36f4f2
parent 41072 9f9bc1bdacef
child 41281 679118e35378
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 00:13:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 17:55:56 2010 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4  structure SMT_Real: SMT_REAL =
     1.5  struct
     1.6  
     1.7 +structure U = SMT_Utils
     1.8  structure B = SMT_Builtin
     1.9  
    1.10  
    1.11 @@ -29,18 +30,31 @@
    1.12    val smtlibC = SMTLIB_Interface.smtlibC
    1.13  
    1.14    fun real_num _ i = SOME (string_of_int i ^ ".0")
    1.15 +
    1.16 +  fun is_linear [t] = U.is_number t
    1.17 +    | is_linear [t, u] = U.is_number t orelse U.is_number u
    1.18 +    | is_linear _ = false
    1.19 +
    1.20 +  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
    1.21 +    | times _ _ _  = NONE
    1.22 +
    1.23 +  fun divide _ T (ts as [_, t]) =
    1.24 +        if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE
    1.25 +    | divide _ _ _ = NONE
    1.26  in
    1.27  
    1.28  val setup_builtins =
    1.29    B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    1.30    fold (B.add_builtin_fun' smtlibC) [
    1.31 +    (@{const less (real)}, "<"),
    1.32 +    (@{const less_eq (real)}, "<="),
    1.33      (@{const uminus (real)}, "~"),
    1.34      (@{const plus (real)}, "+"),
    1.35 -    (@{const minus (real)}, "-"),
    1.36 -    (@{const times (real)}, "*"),
    1.37 -    (@{const less (real)}, "<"),
    1.38 -    (@{const less_eq (real)}, "<=") ] #>
    1.39 -  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    1.40 +    (@{const minus (real)}, "-") ] #>
    1.41 +  B.add_builtin_fun SMTLIB_Interface.smtlibC
    1.42 +    (Term.dest_Const @{const times (real)}, times) #>
    1.43 +  B.add_builtin_fun Z3_Interface.smtlib_z3C
    1.44 +    (Term.dest_Const @{const divide (real)}, divide)
    1.45  
    1.46  end
    1.47