src/HOL/Tools/SMT/smtlib_interface.ML
changeset 41280 a7de9d36f4f2
parent 41127 2ea84c8535c6
child 41281 679118e35378
     1.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 00:13:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 17:55:56 2010 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4  structure SMTLIB_Interface: SMTLIB_INTERFACE =
     1.5  struct
     1.6  
     1.7 +structure U = SMT_Utils
     1.8  structure B = SMT_Builtin
     1.9  structure N = SMT_Normalize
    1.10  structure T = SMT_Translate
    1.11 @@ -28,6 +29,12 @@
    1.12  local
    1.13    fun int_num _ i = SOME (string_of_int i)
    1.14  
    1.15 +  fun is_linear [t] = U.is_number t
    1.16 +    | is_linear [t, u] = U.is_number t orelse U.is_number u
    1.17 +    | is_linear _ = false
    1.18 +
    1.19 +  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
    1.20 +
    1.21    fun distinct _ (Type (_, [Type (_, [T]), _])) [t] =
    1.22          (case try HOLogic.dest_list t of
    1.23            SOME (ts as _ :: _) =>
    1.24 @@ -56,8 +63,8 @@
    1.25      (@{const less_eq (int)}, "<="),
    1.26      (@{const uminus (int)}, "~"),
    1.27      (@{const plus (int)}, "+"),
    1.28 -    (@{const minus (int)}, "-"),
    1.29 -    (@{const times (int)}, "*") ] #>
    1.30 +    (@{const minus (int)}, "-") ] #>
    1.31 +  B.add_builtin_fun smtlibC (Term.dest_Const @{const times (int)}, times) #>
    1.32    B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
    1.33  
    1.34  end