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/mathematical_types.cpp

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Pre-defined mathematical types
+
+Author: Daniel Kroening, [email protected]
+        Maria Svorenova, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Pre-defined 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,206 @@
+/*******************************************************************\
+
+Module: Pre-defined mathematical types
+
+Author: Daniel Kroening, [email protected]
+        Maria Svorenova, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Pre-defined 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)
+  {
+  }
+};
+
+/// 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);
+
+#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

@@ -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: