mcrl2/data/standard_numbers_utility.h

Include file:

#include "mcrl2/data/standard_numbers_utility.h"

Provides utilities for working with data expressions of standard sorts.

Functions

bool mcrl2::data::is_convertible(const sort_expression &s1, const sort_expression &s2)

Returns true if and only if s1 == s2, or if s1 is a less specific numeric type than s2.

Parameters:

  • s1 a sort expression
  • s2 a sort expression
data_expression mcrl2::data::number(const sort_expression &s, const std::string &n)

Construct numeric expression from a string representing a number in decimal notation.

Parameters:

  • s A sort expression
  • n A string

Pre: n is of the form [1]?[0...9]+

Functions

std::enable_if< std::is_integral< T >::value && std::is_unsigned< T >::value, data_expression >::type mcrl2::data::sort_int::int_(T t)

Constructs expression of type pos from an integral type.

std::enable_if< std::is_integral< T >::value && std::is_signed< T >::value, data_expression >::type mcrl2::data::sort_int::int_(T t)

Constructs expression of type pos from an integral type.

data_expression mcrl2::data::sort_int::int_(const std::string &n)

Constructs expression of type Int from a string.

Parameters:

  • n A string

Pre: n is of the form ([-]?[0...9][0...9]+)([0...9]+)

std::string mcrl2::data::sort_int::integer_constant_as_string(const data_expression &n)

Return the string representation of an integer number.

Parameters:

  • n A data expression

Pre: is_integer_constant(n)

Returns: String representation of n

bool mcrl2::data::sort_int::is_integer_constant(const data_expression &n)

Determines whether n is an integer constant.

Parameters:

  • n A data expression

Functions

bool mcrl2::data::sort_nat::is_natural_constant(const data_expression &n)

Determines whether n is a natural constant.

Parameters:

  • n A data expression
std::enable_if<std::is_integral<T>::value, data_expression>::type mcrl2::data::sort_nat::nat(T t)

Constructs expression of type pos from an integral type.

data_expression mcrl2::data::sort_nat::nat(const std::string &n)

Constructs expression of type Nat from a string.

Parameters:

  • n A string
std::string mcrl2::data::sort_nat::natural_constant_as_string(const data_expression &n)

Return the string representation of a natural number.

Parameters:

  • n A data expression

Pre: is_natural_constant(n)

Returns: String representation of n

Functions

bool mcrl2::data::sort_pos::is_positive_constant(const data_expression &n)

Determines whether n is a positive constant.

Parameters:

  • n A data expression
std::enable_if<std::is_integral<T>::value, data_expression>::type mcrl2::data::sort_pos::pos(const T t)

Constructs expression of type Bool from an integral type Type T is an unsigned integral type.

data_expression mcrl2::data::sort_pos::pos(const std::string &n)

Constructs expression of type Pos from a string.

Parameters:

  • n A string
std::string mcrl2::data::sort_pos::positive_constant_as_string(const data_expression &n_in)

Return the string representation of a positive number.

Parameters:

  • n_in A data expression

Pre: is_positive_constant(n)

Returns: String representation of n Transforms a positive constant n into a character array containing the decimal representation of n.

Functions

std::enable_if<std::is_integral<T>::value, data_expression>::type mcrl2::data::sort_real::real_(T t)

Constructs expression of type pos from an integral type.

Parameters:

  • t An expression of type T
std::enable_if<std::is_integral<T>::value, data_expression>::type mcrl2::data::sort_real::real_(T numerator, T denominator)

Constructs expression of type pos from an integral type.

Parameters:

  • numerator numerator
  • denominator denominator
data_expression mcrl2::data::sort_real::real_(const std::string &n)

Constructs expression of type Real from a string.

Parameters:

  • n A string

Pre: n is of the form (-[1...9][0...9]+)([0...9]+)