added to_mathematical_function_type

Author: Daniel Kroening

src/util/std_types.h

@@ -1752,4 +1752,31 @@ class mathematical_function_typet:public typet
   }
 };
 
+/*! \brief Cast a generic typet to a \ref mathematical_function_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * mathematical_function_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref mathematical_function_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const mathematical_function_typet &
+  to_mathematical_function_type(const typet &type)
+{
+  PRECONDITION(type.id()==ID_mathematical_function);
+  return static_cast<const mathematical_function_typet &>(type);
+}
+
+/*! \copydoc to_mathematical_function_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline mathematical_function_typet &
+  to_mathematical_function_type(typet &type)
+{
+  PRECONDITION(type.id()==ID_mathematical_function);
+  return static_cast<mathematical_function_typet &>(type);
+}
+
 #endif // CPROVER_UTIL_STD_TYPES_H