Move mathematical types from std_types

Author: svorenova

src/util/Makefile

@@ -41,6 +41,7 @@ SRC = arith_tools.cpp \
       json_stream.cpp \
       lispexpr.cpp \
       lispirep.cpp \
+      mathematical_types.cpp \
       memory_info.cpp \
       merge_irep.cpp \
       message.cpp \

src/util/mathematical_types.cpp

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Mathematical types
+
+Author: Daniel Kroening, [email protected]
+        Maria Svorenova, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Mathematical types
+
+#include "mathematical_types.h"
+
+/// 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;
+}

src/util/mathematical_types.h

@@ -0,0 +1,162 @@
+/*******************************************************************\
+
+Module: Mathematical types
+
+Author: Daniel Kroening, [email protected]
+        Maria Svorenova, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Mathematical types
+
+#ifndef CPROVER_UTIL_MATHEMATICAL_TYPES_H
+#define CPROVER_UTIL_MATHEMATICAL_TYPES_H
+
+#include "expr_cast.h"
+#include "invariant.h"
+#include "type.h"
+
+/// 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 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);
+
+#endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H

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

@@ -13,10 +13,10 @@ Author: Daniel Kroening, [email protected]
 /// \file util/std_expr.h
 /// API to expression classes
 
+#include "expr_cast.h"
 #include "invariant.h"
+#include "mathematical_types.h"
 #include "std_types.h"
-#include "expr_cast.h"
-
 
 /// Transition system, consisting of state invariant, initial state predicate,
 /// and transition 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
 {
@@ -1822,113 +1786,6 @@ inline complex_typet &to_complex_type(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: