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 "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);
}
 
bool is_number(const typet &type);
 
#endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H