Move mathematical types from std_types

Author: svorenova

src/util/c_types.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_C_TYPES_H
 #define CPROVER_UTIL_C_TYPES_H
 
+#include "mathematical_types.h"
 #include "std_types.h"
 
 bitvector_typet index_type();

src/util/simplify_expr_int.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
+#include "mathematical_types.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "rational.h"

src/util/std_expr.h

@@ -17,10 +17,10 @@ Author: Daniel Kroening, [email protected]
  * \date   Sun Jul 31 21:54:44 BST 2011
 */
 
+#include "expr_cast.h"
 #include "invariant.h"
+#include "mathematical_types.h"
 #include "std_types.h"
-#include "expr_cast.h"
-
 
 /*! \brief A transition system, consisting of
            state invariant, initial state predicate,

src/util/std_types.cpp

@@ -197,16 +197,6 @@ constant_exprt unsignedbv_typet::largest_expr() const
   return from_integer(largest(), *this);
 }
 
-/// Returns true if the type is a rational, real, integer, natural, complex,
-/// unsignedbv, signedbv, floatbv or fixedbv.
-bool is_number(const typet &type)
-{
-  const irep_idt &id = type.id();
-  return id == ID_rational || id == ID_real || id == ID_integer ||
-         id == ID_natural || id == ID_complex || id == ID_unsignedbv ||
-         id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv;
-}
-
 /// Identify whether a given type is constant itself or contains constant
 /// components.
 /// Examples include:

src/util/std_types.h

@@ -56,42 +56,6 @@ class void_typet:public empty_typet
 {
 };
 
-/// Unbounded, signed integers (mathematical integers, not bitvectors)
-class integer_typet:public typet
-{
-public:
-  integer_typet():typet(ID_integer)
-  {
-  }
-};
-
-/// Natural numbers including zero (mathematical integers, not bitvectors)
-class natural_typet:public typet
-{
-public:
-  natural_typet():typet(ID_natural)
-  {
-  }
-};
-
-/// Unbounded, signed rational numbers
-class rational_typet:public typet
-{
-public:
-  rational_typet():typet(ID_rational)
-  {
-  }
-};
-
-/// Unbounded, signed real numbers
-class real_typet:public typet
-{
-public:
-  real_typet():typet(ID_real)
-  {
-  }
-};
-
 /// A reference into the symbol table
 class symbol_typet:public typet
 {
@@ -1778,157 +1742,6 @@ inline vector_typet &to_vector_type(typet &type)
   return static_cast<vector_typet &>(type);
 }
 
-/// Complex numbers made of pair of given subtype
-class complex_typet:public type_with_subtypet
-{
-public:
-  complex_typet():type_with_subtypet(ID_complex)
-  {
-  }
-
-  explicit complex_typet(const typet &_subtype):
-    type_with_subtypet(ID_complex, _subtype)
-  {
-  }
-};
-
-/// Check whether a reference to a typet is a \ref complex_typet.
-/// \param type Source type.
-/// \return True if \param type is a \ref complex_typet.
-template <>
-inline bool can_cast_type<complex_typet>(const typet &type)
-{
-  return type.id() == ID_complex;
-}
-
-/// \brief Cast a typet to a \ref complex_typet
-///
-/// This is an unchecked conversion. \a type must be known to be \ref
-/// complex_typet. Will fail with a precondition violation if type
-/// doesn't match.
-///
-/// \param type Source type.
-/// \return Object of type \ref complex_typet.
-inline const complex_typet &to_complex_type(const typet &type)
-{
-  PRECONDITION(can_cast_type<complex_typet>(type));
-  return static_cast<const complex_typet &>(type);
-}
-
-/// \copydoc to_complex_type(const typet &)
-inline complex_typet &to_complex_type(typet &type)
-{
-  PRECONDITION(can_cast_type<complex_typet>(type));
-  return static_cast<complex_typet &>(type);
-}
-
-/// A type for mathematical functions (do not confuse with functions/methods
-/// in code)
-class mathematical_function_typet:public typet
-{
-public:
-  // the domain of the function is composed of zero, one, or
-  // many variables
-  class variablet:public irept
-  {
-  public:
-    // the identifier is optional
-    irep_idt get_identifier() const
-    {
-      return get(ID_identifier);
-    }
-
-    void set_identifier(const irep_idt &identifier)
-    {
-      return set(ID_identifier, identifier);
-    }
-
-    typet &type()
-    {
-      return static_cast<typet &>(add(ID_type));
-    }
-
-    const typet &type() const
-    {
-      return static_cast<const typet &>(find(ID_type));
-    }
-  };
-
-  using domaint=std::vector<variablet>;
-
-  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
-    : typet(ID_mathematical_function)
-  {
-    subtypes().resize(2);
-    domain() = _domain;
-    codomain() = _codomain;
-  }
-
-  domaint &domain()
-  {
-    return (domaint &)subtypes()[0].subtypes();
-  }
-
-  const domaint &domain() const
-  {
-    return (const domaint &)subtypes()[0].subtypes();
-  }
-
-  variablet &add_variable()
-  {
-    auto &d=domain();
-    d.push_back(variablet());
-    return d.back();
-  }
-
-  /// Return the codomain, i.e., the set of values that the function maps to
-  /// (the "target").
-  typet &codomain()
-  {
-    return subtypes()[1];
-  }
-
-  /// \copydoc codomain()
-  const typet &codomain() const
-  {
-    return subtypes()[1];
-  }
-};
-
-/// Check whether a reference to a typet is a \ref mathematical_function_typet.
-/// \param type Source type.
-/// \return True if \param type is a \ref mathematical_function_typet.
-template <>
-inline bool can_cast_type<mathematical_function_typet>(const typet &type)
-{
-  return type.id() == ID_mathematical_function;
-}
-
-/// \brief Cast a typet to a \ref mathematical_function_typet
-///
-/// This is an unchecked conversion. \a type must be known to be \ref
-/// mathematical_function_typet. Will fail with a precondition violation if type
-/// doesn't match.
-///
-/// \param type Source type.
-/// \return Object of type \ref mathematical_function_typet.
-inline const mathematical_function_typet &
-  to_mathematical_function_type(const typet &type)
-{
-  PRECONDITION(can_cast_type<mathematical_function_typet>(type));
-  return static_cast<const mathematical_function_typet &>(type);
-}
-
-/// \copydoc to_mathematical_function_type(const typet &)
-inline mathematical_function_typet &
-  to_mathematical_function_type(typet &type)
-{
-  PRECONDITION(can_cast_type<mathematical_function_typet>(type));
-  return static_cast<mathematical_function_typet &>(type);
-}
-
-bool is_number(const typet &type);
-
 bool is_constant_or_has_constant_components(
   const typet &type,
   const namespacet &ns);

src/util/type.h

@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 /// modeled with two subs named “subtype” (a single type) and “subtypes”
 /// (a vector of types). The class typet only adds specialized methods
 /// for accessing the subtype information to the interface of irept.
-/// For pre-defined types see `std_types.h`.
+/// For pre-defined types see `std_types.h` and `mathematical_types.h`.
 class typet:public irept
 {
 public: