mathematical_types.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Mathematical types
 
Author: Daniel Kroening, kroening@kroening.com
        Maria Svorenova, maria.svorenova@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_MATHEMATICAL_TYPES_H
#define CPROVER_UTIL_MATHEMATICAL_TYPES_H
 
#include "expr_cast.h" // IWYU pragma: keep
#include "invariant.h"
#include "mp_arith.h"
#include "type.h"
 
class constant_exprt;
 
class integer_typet : public typet
{
public:
  integer_typet() : typet(ID_integer)
  {
  }
 
  constant_exprt zero_expr() const;
  constant_exprt one_expr() const;
};
 
class natural_typet : public typet
{
public:
  natural_typet() : typet(ID_natural)
  {
  }
 
  constant_exprt zero_expr() const;
  constant_exprt one_expr() const;
};
 
class rational_typet : public typet
{
public:
  rational_typet() : typet(ID_rational)
  {
  }
 
  constant_exprt zero_expr() const;
  constant_exprt one_expr() const;
};
 
class real_typet : public typet
{
public:
  real_typet() : typet(ID_real)
  {
  }
 
  constant_exprt zero_expr() const;
  constant_exprt one_expr() const;
};
 
class mathematical_function_typet : public type_with_subtypest
{
public:
  // the domain of the function is composed of zero, one, or
  // many variables, given by their type
  using domaint = std::vector<typet>;
 
  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
    : type_with_subtypest(
        ID_mathematical_function,
        {type_with_subtypest(irep_idt(), _domain), _codomain})
  {
  }
 
  domaint &domain()
  {
    return (domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
  }
 
  const domaint &domain() const
  {
    return (const domaint &)to_type_with_subtypes(subtypes()[0]).subtypes();
  }
 
  void add_variable(const typet &_type)
  {
    domain().push_back(_type);
  }
 
  typet &codomain()
  {
    return subtypes()[1];
  }
 
  const typet &codomain() const
  {
    return subtypes()[1];
  }
};
 
template <>
inline bool can_cast_type<mathematical_function_typet>(const typet &type)
{
  return type.id() == ID_mathematical_function;
}
 
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);
}
 
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);
}
 
class integer_range_typet : public typet
{
public:
  integer_range_typet(const mp_integer &_from, const mp_integer &_to)
    : typet(ID_range)
  {
    from(_from);
    to(_to);
  }
 
  mp_integer from() const;
 
  mp_integer to() const;
 
  bool includes(const mp_integer &) const;
 
  constant_exprt zero_expr() const;
 
  constant_exprt one_expr() const;
 
  mp_integer size() const;
 
  bool empty() const;
 
  void from(const mp_integer &);
  void to(const mp_integer &);
};
 
template <>
inline bool can_cast_type<integer_range_typet>(const typet &type)
{
  return type.id() == ID_range;
}
 
inline const integer_range_typet &to_integer_range_type(const typet &type)
{
  PRECONDITION(can_cast_type<integer_range_typet>(type));
  return static_cast<const integer_range_typet &>(type);
}
 
inline integer_range_typet &to_integer_range_type(typet &type)
{
  PRECONDITION(can_cast_type<integer_range_typet>(type));
  return static_cast<integer_range_typet &>(type);
}
 
bool is_number(const typet &type);
 
#endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H