Namespace for system defined sort real_. More...

Typedefs
typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > >	implementation_map

Functions
const core::identifier_string &	real_name ()

const basic_sort &	real_ ()
	Constructor for sort expression Real.

bool	is_real (const sort_expression &e)
	Recogniser for sort expression Real.

function_symbol_vector	real_generate_constructors_code ()
	Give all system defined constructors for real_.

function_symbol_vector	real_mCRL2_usable_constructors ()
	Give all defined constructors which can be used in mCRL2 specs for real_.

implementation_map	real_cpp_implementable_constructors ()
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for real_.

const core::identifier_string &	creal_name ()
	Generate identifier @cReal.

const function_symbol &	creal ()
	Constructor for function symbol @cReal.

bool	is_creal_function_symbol (const atermpp::aterm &e)
	Recogniser for function @cReal.

application	creal (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @cReal.

void	make_creal (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @cReal.

bool	is_creal_application (const atermpp::aterm &e)
	Recogniser for application of @cReal.

const core::identifier_string &	pos2real_name ()
	Generate identifier Pos2Real.

const function_symbol &	pos2real ()
	Constructor for function symbol Pos2Real.

bool	is_pos2real_function_symbol (const atermpp::aterm &e)
	Recogniser for function Pos2Real.

application	pos2real (const data_expression &arg0)
	Application of function symbol Pos2Real.

void	make_pos2real (data_expression &result, const data_expression &arg0)
	Make an application of function symbol Pos2Real.

bool	is_pos2real_application (const atermpp::aterm &e)
	Recogniser for application of Pos2Real.

const core::identifier_string &	nat2real_name ()
	Generate identifier Nat2Real.

const function_symbol &	nat2real ()
	Constructor for function symbol Nat2Real.

bool	is_nat2real_function_symbol (const atermpp::aterm &e)
	Recogniser for function Nat2Real.

application	nat2real (const data_expression &arg0)
	Application of function symbol Nat2Real.

void	make_nat2real (data_expression &result, const data_expression &arg0)
	Make an application of function symbol Nat2Real.

bool	is_nat2real_application (const atermpp::aterm &e)
	Recogniser for application of Nat2Real.

const core::identifier_string &	int2real_name ()
	Generate identifier Int2Real.

const function_symbol &	int2real ()
	Constructor for function symbol Int2Real.

bool	is_int2real_function_symbol (const atermpp::aterm &e)
	Recogniser for function Int2Real.

application	int2real (const data_expression &arg0)
	Application of function symbol Int2Real.

void	make_int2real (data_expression &result, const data_expression &arg0)
	Make an application of function symbol Int2Real.

bool	is_int2real_application (const atermpp::aterm &e)
	Recogniser for application of Int2Real.

const core::identifier_string &	real2pos_name ()
	Generate identifier Real2Pos.

const function_symbol &	real2pos ()
	Constructor for function symbol Real2Pos.

bool	is_real2pos_function_symbol (const atermpp::aterm &e)
	Recogniser for function Real2Pos.

application	real2pos (const data_expression &arg0)
	Application of function symbol Real2Pos.

void	make_real2pos (data_expression &result, const data_expression &arg0)
	Make an application of function symbol Real2Pos.

bool	is_real2pos_application (const atermpp::aterm &e)
	Recogniser for application of Real2Pos.

const core::identifier_string &	real2nat_name ()
	Generate identifier Real2Nat.

const function_symbol &	real2nat ()
	Constructor for function symbol Real2Nat.

bool	is_real2nat_function_symbol (const atermpp::aterm &e)
	Recogniser for function Real2Nat.

application	real2nat (const data_expression &arg0)
	Application of function symbol Real2Nat.

void	make_real2nat (data_expression &result, const data_expression &arg0)
	Make an application of function symbol Real2Nat.

bool	is_real2nat_application (const atermpp::aterm &e)
	Recogniser for application of Real2Nat.

const core::identifier_string &	real2int_name ()
	Generate identifier Real2Int.

const function_symbol &	real2int ()
	Constructor for function symbol Real2Int.

bool	is_real2int_function_symbol (const atermpp::aterm &e)
	Recogniser for function Real2Int.

application	real2int (const data_expression &arg0)
	Application of function symbol Real2Int.

void	make_real2int (data_expression &result, const data_expression &arg0)
	Make an application of function symbol Real2Int.

bool	is_real2int_application (const atermpp::aterm &e)
	Recogniser for application of Real2Int.

const core::identifier_string &	maximum_name ()
	Generate identifier max.

function_symbol	maximum (const sort_expression &s0, const sort_expression &s1)

bool	is_maximum_function_symbol (const atermpp::aterm &e)
	Recogniser for function max.

application	maximum (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol max.

void	make_maximum (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol max.

bool	is_maximum_application (const atermpp::aterm &e)
	Recogniser for application of max.

const core::identifier_string &	minimum_name ()
	Generate identifier min.

function_symbol	minimum (const sort_expression &s0, const sort_expression &s1)

bool	is_minimum_function_symbol (const atermpp::aterm &e)
	Recogniser for function min.

application	minimum (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol min.

void	make_minimum (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol min.

bool	is_minimum_application (const atermpp::aterm &e)
	Recogniser for application of min.

const core::identifier_string &	abs_name ()
	Generate identifier abs.

function_symbol	abs (const sort_expression &s0)

bool	is_abs_function_symbol (const atermpp::aterm &e)
	Recogniser for function abs.

application	abs (const data_expression &arg0)
	Application of function symbol abs.

void	make_abs (data_expression &result, const data_expression &arg0)
	Make an application of function symbol abs.

bool	is_abs_application (const atermpp::aterm &e)
	Recogniser for application of abs.

const core::identifier_string &	negate_name ()
	Generate identifier -.

function_symbol	negate (const sort_expression &s0)

bool	is_negate_function_symbol (const atermpp::aterm &e)
	Recogniser for function -.

application	negate (const data_expression &arg0)
	Application of function symbol -.

void	make_negate (data_expression &result, const data_expression &arg0)
	Make an application of function symbol -.

bool	is_negate_application (const atermpp::aterm &e)
	Recogniser for application of -.

const core::identifier_string &	succ_name ()
	Generate identifier succ.

function_symbol	succ (const sort_expression &s0)

bool	is_succ_function_symbol (const atermpp::aterm &e)
	Recogniser for function succ.

application	succ (const data_expression &arg0)
	Application of function symbol succ.

void	make_succ (data_expression &result, const data_expression &arg0)
	Make an application of function symbol succ.

bool	is_succ_application (const atermpp::aterm &e)
	Recogniser for application of succ.

const core::identifier_string &	pred_name ()
	Generate identifier pred.

function_symbol	pred (const sort_expression &s0)

bool	is_pred_function_symbol (const atermpp::aterm &e)
	Recogniser for function pred.

application	pred (const data_expression &arg0)
	Application of function symbol pred.

void	make_pred (data_expression &result, const data_expression &arg0)
	Make an application of function symbol pred.

bool	is_pred_application (const atermpp::aterm &e)
	Recogniser for application of pred.

const core::identifier_string &	plus_name ()
	Generate identifier +.

function_symbol	plus (const sort_expression &s0, const sort_expression &s1)

bool	is_plus_function_symbol (const atermpp::aterm &e)
	Recogniser for function +.

application	plus (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol +.

void	make_plus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol +.

bool	is_plus_application (const atermpp::aterm &e)
	Recogniser for application of +.

const core::identifier_string &	minus_name ()
	Generate identifier -.

function_symbol	minus (const sort_expression &s0, const sort_expression &s1)

bool	is_minus_function_symbol (const atermpp::aterm &e)
	Recogniser for function -.

application	minus (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol -.

void	make_minus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol -.

bool	is_minus_application (const atermpp::aterm &e)
	Recogniser for application of -.

const core::identifier_string &	times_name ()
	Generate identifier *.

function_symbol	times (const sort_expression &s0, const sort_expression &s1)

bool	is_times_function_symbol (const atermpp::aterm &e)
	Recogniser for function *.

application	times (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol *.

void	make_times (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol *.

bool	is_times_application (const atermpp::aterm &e)
	Recogniser for application of *.

const core::identifier_string &	exp_name ()
	Generate identifier exp.

function_symbol	exp (const sort_expression &s0, const sort_expression &s1)

bool	is_exp_function_symbol (const atermpp::aterm &e)
	Recogniser for function exp.

application	exp (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol exp.

void	make_exp (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol exp.

bool	is_exp_application (const atermpp::aterm &e)
	Recogniser for application of exp.

const core::identifier_string &	divides_name ()
	Generate identifier /.

function_symbol	divides (const sort_expression &s0, const sort_expression &s1)

bool	is_divides_function_symbol (const atermpp::aterm &e)
	Recogniser for function /.

application	divides (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol /.

void	make_divides (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol /.

bool	is_divides_application (const atermpp::aterm &e)
	Recogniser for application of /.

const core::identifier_string &	floor_name ()
	Generate identifier floor.

const function_symbol &	floor ()
	Constructor for function symbol floor.

bool	is_floor_function_symbol (const atermpp::aterm &e)
	Recogniser for function floor.

application	floor (const data_expression &arg0)
	Application of function symbol floor.

void	make_floor (data_expression &result, const data_expression &arg0)
	Make an application of function symbol floor.

bool	is_floor_application (const atermpp::aterm &e)
	Recogniser for application of floor.

const core::identifier_string &	ceil_name ()
	Generate identifier ceil.

const function_symbol &	ceil ()
	Constructor for function symbol ceil.

bool	is_ceil_function_symbol (const atermpp::aterm &e)
	Recogniser for function ceil.

application	ceil (const data_expression &arg0)
	Application of function symbol ceil.

void	make_ceil (data_expression &result, const data_expression &arg0)
	Make an application of function symbol ceil.

bool	is_ceil_application (const atermpp::aterm &e)
	Recogniser for application of ceil.

const core::identifier_string &	round_name ()
	Generate identifier round.

const function_symbol &	round ()
	Constructor for function symbol round.

bool	is_round_function_symbol (const atermpp::aterm &e)
	Recogniser for function round.

application	round (const data_expression &arg0)
	Application of function symbol round.

void	make_round (data_expression &result, const data_expression &arg0)
	Make an application of function symbol round.

bool	is_round_application (const atermpp::aterm &e)
	Recogniser for application of round.

const core::identifier_string &	reduce_fraction_name ()
	Generate identifier @redfrac.

const function_symbol &	reduce_fraction ()
	Constructor for function symbol @redfrac.

bool	is_reduce_fraction_function_symbol (const atermpp::aterm &e)
	Recogniser for function @redfrac.

application	reduce_fraction (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @redfrac.

void	make_reduce_fraction (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @redfrac.

bool	is_reduce_fraction_application (const atermpp::aterm &e)
	Recogniser for application of @redfrac.

const core::identifier_string &	reduce_fraction_where_name ()
	Generate identifier @redfracwhr.

const function_symbol &	reduce_fraction_where ()
	Constructor for function symbol @redfracwhr.

bool	is_reduce_fraction_where_function_symbol (const atermpp::aterm &e)
	Recogniser for function @redfracwhr.

application	reduce_fraction_where (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @redfracwhr.

void	make_reduce_fraction_where (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @redfracwhr.

bool	is_reduce_fraction_where_application (const atermpp::aterm &e)
	Recogniser for application of @redfracwhr.

const core::identifier_string &	reduce_fraction_helper_name ()
	Generate identifier @redfrachlp.

const function_symbol &	reduce_fraction_helper ()
	Constructor for function symbol @redfrachlp.

bool	is_reduce_fraction_helper_function_symbol (const atermpp::aterm &e)
	Recogniser for function @redfrachlp.

application	reduce_fraction_helper (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @redfrachlp.

void	make_reduce_fraction_helper (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @redfrachlp.

bool	is_reduce_fraction_helper_application (const atermpp::aterm &e)
	Recogniser for application of @redfrachlp.

function_symbol_vector	real_generate_functions_code ()
	Give all system defined mappings for real_.

function_symbol_vector	real_generate_constructors_and_functions_code ()
	Give all system defined mappings and constructors for real_.

function_symbol_vector	real_mCRL2_usable_mappings ()
	Give all system defined mappings that can be used in mCRL2 specs for real_.

implementation_map	real_cpp_implementable_mappings ()
	Give all system defined mappings that are to be implemented in C++ code for real_.

const data_expression &	left (const data_expression &e)
	Function for projecting out argument. left from an application.

const data_expression &	right (const data_expression &e)
	Function for projecting out argument. right from an application.

const data_expression &	arg (const data_expression &e)
	Function for projecting out argument. arg from an application.

const data_expression &	arg1 (const data_expression &e)
	Function for projecting out argument. arg1 from an application.

const data_expression &	arg2 (const data_expression &e)
	Function for projecting out argument. arg2 from an application.

const data_expression &	arg3 (const data_expression &e)
	Function for projecting out argument. arg3 from an application.

data_equation_vector	real_generate_equations_code ()
	Give all system defined equations for real_.

data_expression &	real_zero ()

data_expression &	real_one ()

bool	is_zero (const atermpp::aterm &e)

bool	is_one (const atermpp::aterm &e)

bool	is_larger_zero (const atermpp::aterm &e)
	Functions that returns true if e is a closed real number larger than zero.

template<typename T >
std::enable_if< std::is_integral< T >::value, data_expression >::type	real_ (T t)
	Constructs expression of type Real from an integral type.

template<typename T >
std::enable_if< std::is_integral< T >::value, data_expression >::type	real_ (T numerator, T denominator)
	Constructs expression of type Real from an integral type.

data_expression	real_ (const std::string &numerator, const std::string &denominator)
	Constructs expression of type Real from two number strings.

data_expression	real_ (const std::string &n)
	Constructs expression of type Real from a string.

template<class NUMERIC_TYPE >
NUMERIC_TYPE	value (const data_expression &r, typename std::enable_if< std::is_floating_point< NUMERIC_TYPE >::value >::type *=nullptr)
	Yields the real value of a data expression.

Detailed Description

Namespace for system defined sort real_.

Typedef Documentation

◆ implementation_map

typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > mcrl2::data::sort_real::implementation_map

Definition at line 84 of file real1.h.

Function Documentation

◆ abs() [1/2]

application mcrl2::data::sort_real::abs ( const data_expression & arg0 )

inline

Application of function symbol abs.

Parameters

arg0	A data expression.

Returns: Application of abs to a number of arguments.

Definition at line 774 of file real1.h.

◆ abs() [2/2]

function_symbol mcrl2::data::sort_real::abs ( const sort_expression & s0 )

inline

Definition at line 735 of file real1.h.

◆ abs_name()

const core::identifier_string & mcrl2::data::sort_real::abs_name ( )

inline

Generate identifier abs.

Returns: Identifier abs.

Definition at line 727 of file real1.h.

◆ arg()

const data_expression & mcrl2::data::sort_real::arg ( const data_expression & e )

inline

Function for projecting out argument. arg from an application.

Parameters

e	A data expression.

Precondition: arg is defined for e.

Returns: The argument of e that corresponds to arg.

Definition at line 1965 of file real1.h.

◆ arg1()

const data_expression & mcrl2::data::sort_real::arg1 ( const data_expression & e )

inline

Function for projecting out argument. arg1 from an application.

Parameters

e	A data expression.

Precondition: arg1 is defined for e.

Returns: The argument of e that corresponds to arg1.

Definition at line 1977 of file real1.h.

◆ arg2()

const data_expression & mcrl2::data::sort_real::arg2 ( const data_expression & e )

inline

Function for projecting out argument. arg2 from an application.

Parameters

e	A data expression.

Precondition: arg2 is defined for e.

Returns: The argument of e that corresponds to arg2.

Definition at line 1989 of file real1.h.

◆ arg3()

const data_expression & mcrl2::data::sort_real::arg3 ( const data_expression & e )

inline

Function for projecting out argument. arg3 from an application.

Parameters

e	A data expression.

Precondition: arg3 is defined for e.

Returns: The argument of e that corresponds to arg3.

Definition at line 2001 of file real1.h.

◆ ceil() [1/2]

const function_symbol & mcrl2::data::sort_real::ceil ( )

inline

Constructor for function symbol ceil.

Returns: Function symbol ceil.

Definition at line 1535 of file real1.h.

◆ ceil() [2/2]

application mcrl2::data::sort_real::ceil ( const data_expression & arg0 )

inline

Application of function symbol ceil.

Parameters

arg0	A data expression.

Returns: Application of ceil to a number of arguments.

Definition at line 1559 of file real1.h.

◆ ceil_name()

const core::identifier_string & mcrl2::data::sort_real::ceil_name ( )

inline

Generate identifier ceil.

Returns: Identifier ceil.

Definition at line 1525 of file real1.h.

◆ creal() [1/2]

const function_symbol & mcrl2::data::sort_real::creal ( )

inline

Constructor for function symbol @cReal.

Returns: Function symbol creal.

Definition at line 107 of file real1.h.

◆ creal() [2/2]

application mcrl2::data::sort_real::creal	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @cReal.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of @cReal to a number of arguments.

Definition at line 132 of file real1.h.

◆ creal_name()

const core::identifier_string & mcrl2::data::sort_real::creal_name ( )

inline

Generate identifier @cReal.

Returns: Identifier @cReal.

Definition at line 97 of file real1.h.

◆ divides() [1/2]

application mcrl2::data::sort_real::divides	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol /.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of / to a number of arguments.

Definition at line 1434 of file real1.h.

◆ divides() [2/2]

function_symbol mcrl2::data::sort_real::divides	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1407 of file real1.h.

◆ divides_name()

const core::identifier_string & mcrl2::data::sort_real::divides_name ( )

inline

Generate identifier /.

Returns: Identifier /.

Definition at line 1399 of file real1.h.

◆ exp() [1/2]

application mcrl2::data::sort_real::exp	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol exp.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of exp to a number of arguments.

Definition at line 1370 of file real1.h.

◆ exp() [2/2]

function_symbol mcrl2::data::sort_real::exp	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1322 of file real1.h.

◆ exp_name()

const core::identifier_string & mcrl2::data::sort_real::exp_name ( )

inline

Generate identifier exp.

Returns: Identifier exp.

Definition at line 1314 of file real1.h.

◆ floor() [1/2]

const function_symbol & mcrl2::data::sort_real::floor ( )

inline

Constructor for function symbol floor.

Returns: Function symbol floor.

Definition at line 1473 of file real1.h.

◆ floor() [2/2]

application mcrl2::data::sort_real::floor ( const data_expression & arg0 )

inline

Application of function symbol floor.

Parameters

arg0	A data expression.

Returns: Application of floor to a number of arguments.

Definition at line 1497 of file real1.h.

◆ floor_name()

const core::identifier_string & mcrl2::data::sort_real::floor_name ( )

inline

Generate identifier floor.

Returns: Identifier floor.

Definition at line 1463 of file real1.h.

◆ int2real() [1/2]

const function_symbol & mcrl2::data::sort_real::int2real ( )

inline

Constructor for function symbol Int2Real.

Returns: Function symbol int2real.

Definition at line 295 of file real1.h.

◆ int2real() [2/2]

application mcrl2::data::sort_real::int2real ( const data_expression & arg0 )

inline

Application of function symbol Int2Real.

Parameters

arg0	A data expression.

Returns: Application of Int2Real to a number of arguments.

Definition at line 319 of file real1.h.

◆ int2real_name()

const core::identifier_string & mcrl2::data::sort_real::int2real_name ( )

inline

Generate identifier Int2Real.

Returns: Identifier Int2Real.

Definition at line 285 of file real1.h.

◆ is_abs_application()

bool mcrl2::data::sort_real::is_abs_application ( const atermpp::aterm & e )

inline

Recogniser for application of abs.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol abs to a number of arguments.

Definition at line 794 of file real1.h.

◆ is_abs_function_symbol()

bool mcrl2::data::sort_real::is_abs_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function abs.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching abs.

Definition at line 759 of file real1.h.

◆ is_ceil_application()

bool mcrl2::data::sort_real::is_ceil_application ( const atermpp::aterm & e )

inline

Recogniser for application of ceil.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol ceil to a number of arguments.

Definition at line 1579 of file real1.h.

◆ is_ceil_function_symbol()

bool mcrl2::data::sort_real::is_ceil_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function ceil.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching ceil.

Definition at line 1545 of file real1.h.

◆ is_creal_application()

bool mcrl2::data::sort_real::is_creal_application ( const atermpp::aterm & e )

inline

Recogniser for application of @cReal.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol creal to a number of arguments.

Definition at line 153 of file real1.h.

◆ is_creal_function_symbol()

bool mcrl2::data::sort_real::is_creal_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @cReal.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @cReal.

Definition at line 117 of file real1.h.

◆ is_divides_application()

bool mcrl2::data::sort_real::is_divides_application ( const atermpp::aterm & e )

inline

Recogniser for application of /.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol divides to a number of arguments.

Definition at line 1455 of file real1.h.

◆ is_divides_function_symbol()

bool mcrl2::data::sort_real::is_divides_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function /.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching /.

Definition at line 1418 of file real1.h.

◆ is_exp_application()

bool mcrl2::data::sort_real::is_exp_application ( const atermpp::aterm & e )

inline

Recogniser for application of exp.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol exp to a number of arguments.

Definition at line 1391 of file real1.h.

◆ is_exp_function_symbol()

bool mcrl2::data::sort_real::is_exp_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function exp.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching exp.

Definition at line 1354 of file real1.h.

◆ is_floor_application()

bool mcrl2::data::sort_real::is_floor_application ( const atermpp::aterm & e )

inline

Recogniser for application of floor.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol floor to a number of arguments.

Definition at line 1517 of file real1.h.

◆ is_floor_function_symbol()

bool mcrl2::data::sort_real::is_floor_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function floor.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching floor.

Definition at line 1483 of file real1.h.

◆ is_int2real_application()

bool mcrl2::data::sort_real::is_int2real_application ( const atermpp::aterm & e )

inline

Recogniser for application of Int2Real.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol int2real to a number of arguments.

Definition at line 339 of file real1.h.

◆ is_int2real_function_symbol()

bool mcrl2::data::sort_real::is_int2real_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Int2Real.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Int2Real.

Definition at line 305 of file real1.h.

◆ is_larger_zero()

bool mcrl2::data::sort_real::is_larger_zero ( const atermpp::aterm & e )

inline

Functions that returns true if e is a closed real number larger than zero.

Definition at line 48 of file real_utilities.h.

◆ is_maximum_application()

bool mcrl2::data::sort_real::is_maximum_application ( const atermpp::aterm & e )

inline

Recogniser for application of max.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol maximum to a number of arguments.

Definition at line 634 of file real1.h.

◆ is_maximum_function_symbol()

bool mcrl2::data::sort_real::is_maximum_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function max.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching max.

Definition at line 597 of file real1.h.

◆ is_minimum_application()

bool mcrl2::data::sort_real::is_minimum_application ( const atermpp::aterm & e )

inline

Recogniser for application of min.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol minimum to a number of arguments.

Definition at line 719 of file real1.h.

◆ is_minimum_function_symbol()

bool mcrl2::data::sort_real::is_minimum_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function min.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching min.

Definition at line 682 of file real1.h.

◆ is_minus_application()

bool mcrl2::data::sort_real::is_minus_application ( const atermpp::aterm & e )

inline

Recogniser for application of -.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol minus to a number of arguments.

Definition at line 1221 of file real1.h.

◆ is_minus_function_symbol()

bool mcrl2::data::sort_real::is_minus_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function -.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching -.

Definition at line 1184 of file real1.h.

◆ is_nat2real_application()

bool mcrl2::data::sort_real::is_nat2real_application ( const atermpp::aterm & e )

inline

Recogniser for application of Nat2Real.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol nat2real to a number of arguments.

Definition at line 277 of file real1.h.

◆ is_nat2real_function_symbol()

bool mcrl2::data::sort_real::is_nat2real_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Nat2Real.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Nat2Real.

Definition at line 243 of file real1.h.

◆ is_negate_application()

bool mcrl2::data::sort_real::is_negate_application ( const atermpp::aterm & e )

inline

Recogniser for application of -.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol negate to a number of arguments.

Definition at line 877 of file real1.h.

◆ is_negate_function_symbol()

bool mcrl2::data::sort_real::is_negate_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function -.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching -.

Definition at line 842 of file real1.h.

◆ is_one()

bool mcrl2::data::sort_real::is_one ( const atermpp::aterm & e )

inline

Definition at line 42 of file real_utilities.h.

◆ is_plus_application()

bool mcrl2::data::sort_real::is_plus_application ( const atermpp::aterm & e )

inline

Recogniser for application of +.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol plus to a number of arguments.

Definition at line 1136 of file real1.h.

◆ is_plus_function_symbol()

bool mcrl2::data::sort_real::is_plus_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function +.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching +.

Definition at line 1099 of file real1.h.

◆ is_pos2real_application()

bool mcrl2::data::sort_real::is_pos2real_application ( const atermpp::aterm & e )

inline

Recogniser for application of Pos2Real.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol pos2real to a number of arguments.

Definition at line 215 of file real1.h.

◆ is_pos2real_function_symbol()

bool mcrl2::data::sort_real::is_pos2real_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Pos2Real.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Pos2Real.

Definition at line 181 of file real1.h.

◆ is_pred_application()

bool mcrl2::data::sort_real::is_pred_application ( const atermpp::aterm & e )

inline

Recogniser for application of pred.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol pred to a number of arguments.

Definition at line 1043 of file real1.h.

◆ is_pred_function_symbol()

bool mcrl2::data::sort_real::is_pred_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function pred.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching pred.

Definition at line 1008 of file real1.h.

◆ is_real()

bool mcrl2::data::sort_real::is_real ( const sort_expression & e )

inline

Recogniser for sort expression Real.

Parameters

e	A sort expression

Returns: true iff e == real_()

Definition at line 58 of file real1.h.

◆ is_real2int_application()

bool mcrl2::data::sort_real::is_real2int_application ( const atermpp::aterm & e )

inline

Recogniser for application of Real2Int.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol real2int to a number of arguments.

Definition at line 525 of file real1.h.

◆ is_real2int_function_symbol()

bool mcrl2::data::sort_real::is_real2int_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Real2Int.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Real2Int.

Definition at line 491 of file real1.h.

◆ is_real2nat_application()

bool mcrl2::data::sort_real::is_real2nat_application ( const atermpp::aterm & e )

inline

Recogniser for application of Real2Nat.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol real2nat to a number of arguments.

Definition at line 463 of file real1.h.

◆ is_real2nat_function_symbol()

bool mcrl2::data::sort_real::is_real2nat_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Real2Nat.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Real2Nat.

Definition at line 429 of file real1.h.

◆ is_real2pos_application()

bool mcrl2::data::sort_real::is_real2pos_application ( const atermpp::aterm & e )

inline

Recogniser for application of Real2Pos.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol real2pos to a number of arguments.

Definition at line 401 of file real1.h.

◆ is_real2pos_function_symbol()

bool mcrl2::data::sort_real::is_real2pos_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Real2Pos.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Real2Pos.

Definition at line 367 of file real1.h.

◆ is_reduce_fraction_application()

bool mcrl2::data::sort_real::is_reduce_fraction_application ( const atermpp::aterm & e )

inline

Recogniser for application of @redfrac.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol reduce_fraction to a number of arguments.

Definition at line 1705 of file real1.h.

◆ is_reduce_fraction_function_symbol()

bool mcrl2::data::sort_real::is_reduce_fraction_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @redfrac.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @redfrac.

Definition at line 1669 of file real1.h.

◆ is_reduce_fraction_helper_application()

bool mcrl2::data::sort_real::is_reduce_fraction_helper_application ( const atermpp::aterm & e )

inline

Recogniser for application of @redfrachlp.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol reduce_fraction_helper to a number of arguments.

Definition at line 1835 of file real1.h.

◆ is_reduce_fraction_helper_function_symbol()

bool mcrl2::data::sort_real::is_reduce_fraction_helper_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @redfrachlp.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @redfrachlp.

Definition at line 1799 of file real1.h.

◆ is_reduce_fraction_where_application()

bool mcrl2::data::sort_real::is_reduce_fraction_where_application ( const atermpp::aterm & e )

inline

Recogniser for application of @redfracwhr.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol reduce_fraction_where to a number of arguments.

Definition at line 1771 of file real1.h.

◆ is_reduce_fraction_where_function_symbol()

bool mcrl2::data::sort_real::is_reduce_fraction_where_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @redfracwhr.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @redfracwhr.

Definition at line 1733 of file real1.h.

◆ is_round_application()

bool mcrl2::data::sort_real::is_round_application ( const atermpp::aterm & e )

inline

Recogniser for application of round.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol round to a number of arguments.

Definition at line 1641 of file real1.h.

◆ is_round_function_symbol()

bool mcrl2::data::sort_real::is_round_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function round.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching round.

Definition at line 1607 of file real1.h.

◆ is_succ_application()

bool mcrl2::data::sort_real::is_succ_application ( const atermpp::aterm & e )

inline

Recogniser for application of succ.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol succ to a number of arguments.

Definition at line 960 of file real1.h.

◆ is_succ_function_symbol()

bool mcrl2::data::sort_real::is_succ_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function succ.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching succ.

Definition at line 925 of file real1.h.

◆ is_times_application()

bool mcrl2::data::sort_real::is_times_application ( const atermpp::aterm & e )

inline

Recogniser for application of *.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol times to a number of arguments.

Definition at line 1306 of file real1.h.

◆ is_times_function_symbol()

bool mcrl2::data::sort_real::is_times_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function *.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching *.

Definition at line 1269 of file real1.h.

◆ is_zero()

bool mcrl2::data::sort_real::is_zero ( const atermpp::aterm & e )

inline

Definition at line 37 of file real_utilities.h.

◆ left()

const data_expression & mcrl2::data::sort_real::left ( const data_expression & e )

inline

Function for projecting out argument. left from an application.

Parameters

e	A data expression.

Precondition: left is defined for e.

Returns: The argument of e that corresponds to left.

Definition at line 1941 of file real1.h.

◆ make_abs()

void mcrl2::data::sort_real::make_abs	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol abs.

Parameters

result	The data expression where the abs expression is put.
arg0	A data expression.

Definition at line 784 of file real1.h.

◆ make_ceil()

void mcrl2::data::sort_real::make_ceil	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol ceil.

Parameters

result	The data expression where the ceil expression is put.
arg0	A data expression.

Definition at line 1569 of file real1.h.

◆ make_creal()

void mcrl2::data::sort_real::make_creal	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @cReal.

Parameters

result	The data expression where the @cReal expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 143 of file real1.h.

◆ make_divides()

void mcrl2::data::sort_real::make_divides	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol /.

Parameters

result	The data expression where the / expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1445 of file real1.h.

◆ make_exp()

void mcrl2::data::sort_real::make_exp	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol exp.

Parameters

result	The data expression where the exp expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1381 of file real1.h.

◆ make_floor()

void mcrl2::data::sort_real::make_floor	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol floor.

Parameters

result	The data expression where the floor expression is put.
arg0	A data expression.

Definition at line 1507 of file real1.h.

◆ make_int2real()

void mcrl2::data::sort_real::make_int2real	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Int2Real.

Parameters

result	The data expression where the Int2Real expression is put.
arg0	A data expression.

Definition at line 329 of file real1.h.

◆ make_maximum()

void mcrl2::data::sort_real::make_maximum	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol max.

Parameters

result	The data expression where the max expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 624 of file real1.h.

◆ make_minimum()

void mcrl2::data::sort_real::make_minimum	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol min.

Parameters

result	The data expression where the min expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 709 of file real1.h.

◆ make_minus()

void mcrl2::data::sort_real::make_minus	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol -.

Parameters

result	The data expression where the - expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1211 of file real1.h.

◆ make_nat2real()

void mcrl2::data::sort_real::make_nat2real	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Nat2Real.

Parameters

result	The data expression where the Nat2Real expression is put.
arg0	A data expression.

Definition at line 267 of file real1.h.

◆ make_negate()

void mcrl2::data::sort_real::make_negate	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol -.

Parameters

result	The data expression where the - expression is put.
arg0	A data expression.

Definition at line 867 of file real1.h.

◆ make_plus()

void mcrl2::data::sort_real::make_plus	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol +.

Parameters

result	The data expression where the + expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1126 of file real1.h.

◆ make_pos2real()

void mcrl2::data::sort_real::make_pos2real	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Pos2Real.

Parameters

result	The data expression where the Pos2Real expression is put.
arg0	A data expression.

Definition at line 205 of file real1.h.

◆ make_pred()

void mcrl2::data::sort_real::make_pred	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol pred.

Parameters

result	The data expression where the pred expression is put.
arg0	A data expression.

Definition at line 1033 of file real1.h.

◆ make_real2int()

void mcrl2::data::sort_real::make_real2int	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Real2Int.

Parameters

result	The data expression where the Real2Int expression is put.
arg0	A data expression.

Definition at line 515 of file real1.h.

◆ make_real2nat()

void mcrl2::data::sort_real::make_real2nat	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Real2Nat.

Parameters

result	The data expression where the Real2Nat expression is put.
arg0	A data expression.

Definition at line 453 of file real1.h.

◆ make_real2pos()

void mcrl2::data::sort_real::make_real2pos	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Real2Pos.

Parameters

result	The data expression where the Real2Pos expression is put.
arg0	A data expression.

Definition at line 391 of file real1.h.

◆ make_reduce_fraction()

void mcrl2::data::sort_real::make_reduce_fraction	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @redfrac.

Parameters

result	The data expression where the @redfrac expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1695 of file real1.h.

◆ make_reduce_fraction_helper()

void mcrl2::data::sort_real::make_reduce_fraction_helper	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @redfrachlp.

Parameters

result	The data expression where the @redfrachlp expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1825 of file real1.h.

◆ make_reduce_fraction_where()

void mcrl2::data::sort_real::make_reduce_fraction_where	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Make an application of function symbol @redfracwhr.

Parameters

result	The data expression where the @redfracwhr expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Definition at line 1761 of file real1.h.

◆ make_round()

void mcrl2::data::sort_real::make_round	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol round.

Parameters

result	The data expression where the round expression is put.
arg0	A data expression.

Definition at line 1631 of file real1.h.

◆ make_succ()

void mcrl2::data::sort_real::make_succ	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol succ.

Parameters

result	The data expression where the succ expression is put.
arg0	A data expression.

Definition at line 950 of file real1.h.

◆ make_times()

void mcrl2::data::sort_real::make_times	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol *.

Parameters

result	The data expression where the * expression is put.
arg0	A data expression.
arg1	A data expression.

Definition at line 1296 of file real1.h.

◆ maximum() [1/2]

application mcrl2::data::sort_real::maximum	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol max.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of max to a number of arguments.

Definition at line 613 of file real1.h.

◆ maximum() [2/2]

function_symbol mcrl2::data::sort_real::maximum	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 541 of file real1.h.

◆ maximum_name()

const core::identifier_string & mcrl2::data::sort_real::maximum_name ( )

inline

Generate identifier max.

Returns: Identifier max.

Definition at line 533 of file real1.h.

◆ minimum() [1/2]

application mcrl2::data::sort_real::minimum	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol min.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of min to a number of arguments.

Definition at line 698 of file real1.h.

◆ minimum() [2/2]

function_symbol mcrl2::data::sort_real::minimum	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 650 of file real1.h.

◆ minimum_name()

const core::identifier_string & mcrl2::data::sort_real::minimum_name ( )

inline

Generate identifier min.

Returns: Identifier min.

Definition at line 642 of file real1.h.

◆ minus() [1/2]

application mcrl2::data::sort_real::minus	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol -.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of - to a number of arguments.

Definition at line 1200 of file real1.h.

◆ minus() [2/2]

function_symbol mcrl2::data::sort_real::minus	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1152 of file real1.h.

◆ minus_name()

const core::identifier_string & mcrl2::data::sort_real::minus_name ( )

inline

Generate identifier -.

Returns: Identifier -.

Definition at line 1144 of file real1.h.

◆ nat2real() [1/2]

const function_symbol & mcrl2::data::sort_real::nat2real ( )

inline

Constructor for function symbol Nat2Real.

Returns: Function symbol nat2real.

Definition at line 233 of file real1.h.

◆ nat2real() [2/2]

application mcrl2::data::sort_real::nat2real ( const data_expression & arg0 )

inline

Application of function symbol Nat2Real.

Parameters

arg0	A data expression.

Returns: Application of Nat2Real to a number of arguments.

Definition at line 257 of file real1.h.

◆ nat2real_name()

const core::identifier_string & mcrl2::data::sort_real::nat2real_name ( )

inline

Generate identifier Nat2Real.

Returns: Identifier Nat2Real.

Definition at line 223 of file real1.h.

◆ negate() [1/2]

application mcrl2::data::sort_real::negate ( const data_expression & arg0 )

inline

Application of function symbol -.

Parameters

arg0	A data expression.

Returns: Application of - to a number of arguments.

Definition at line 857 of file real1.h.

◆ negate() [2/2]

function_symbol mcrl2::data::sort_real::negate ( const sort_expression & s0 )

inline

Definition at line 810 of file real1.h.

◆ negate_name()

const core::identifier_string & mcrl2::data::sort_real::negate_name ( )

inline

Generate identifier -.

Returns: Identifier -.

Definition at line 802 of file real1.h.

◆ plus() [1/2]

application mcrl2::data::sort_real::plus	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol +.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of + to a number of arguments.

Definition at line 1115 of file real1.h.

◆ plus() [2/2]

function_symbol mcrl2::data::sort_real::plus	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1059 of file real1.h.

◆ plus_name()

const core::identifier_string & mcrl2::data::sort_real::plus_name ( )

inline

Generate identifier +.

Returns: Identifier +.

Definition at line 1051 of file real1.h.

◆ pos2real() [1/2]

const function_symbol & mcrl2::data::sort_real::pos2real ( )

inline

Constructor for function symbol Pos2Real.

Returns: Function symbol pos2real.

Definition at line 171 of file real1.h.

◆ pos2real() [2/2]

application mcrl2::data::sort_real::pos2real ( const data_expression & arg0 )

inline

Application of function symbol Pos2Real.

Parameters

arg0	A data expression.

Returns: Application of Pos2Real to a number of arguments.

Definition at line 195 of file real1.h.

◆ pos2real_name()

const core::identifier_string & mcrl2::data::sort_real::pos2real_name ( )

inline

Generate identifier Pos2Real.

Returns: Identifier Pos2Real.

Definition at line 161 of file real1.h.

◆ pred() [1/2]

application mcrl2::data::sort_real::pred ( const data_expression & arg0 )

inline

Application of function symbol pred.

Parameters

arg0	A data expression.

Returns: Application of pred to a number of arguments.

Definition at line 1023 of file real1.h.

◆ pred() [2/2]

function_symbol mcrl2::data::sort_real::pred ( const sort_expression & s0 )

inline

Definition at line 976 of file real1.h.

◆ pred_name()

const core::identifier_string & mcrl2::data::sort_real::pred_name ( )

inline

Generate identifier pred.

Returns: Identifier pred.

Definition at line 968 of file real1.h.

◆ real2int() [1/2]

const function_symbol & mcrl2::data::sort_real::real2int ( )

inline

Constructor for function symbol Real2Int.

Returns: Function symbol real2int.

Definition at line 481 of file real1.h.

◆ real2int() [2/2]

application mcrl2::data::sort_real::real2int ( const data_expression & arg0 )

inline

Application of function symbol Real2Int.

Parameters

arg0	A data expression.

Returns: Application of Real2Int to a number of arguments.

Definition at line 505 of file real1.h.

◆ real2int_name()

const core::identifier_string & mcrl2::data::sort_real::real2int_name ( )

inline

Generate identifier Real2Int.

Returns: Identifier Real2Int.

Definition at line 471 of file real1.h.

◆ real2nat() [1/2]

const function_symbol & mcrl2::data::sort_real::real2nat ( )

inline

Constructor for function symbol Real2Nat.

Returns: Function symbol real2nat.

Definition at line 419 of file real1.h.

◆ real2nat() [2/2]

application mcrl2::data::sort_real::real2nat ( const data_expression & arg0 )

inline

Application of function symbol Real2Nat.

Parameters

arg0	A data expression.

Returns: Application of Real2Nat to a number of arguments.

Definition at line 443 of file real1.h.

◆ real2nat_name()

const core::identifier_string & mcrl2::data::sort_real::real2nat_name ( )

inline

Generate identifier Real2Nat.

Returns: Identifier Real2Nat.

Definition at line 409 of file real1.h.

◆ real2pos() [1/2]

const function_symbol & mcrl2::data::sort_real::real2pos ( )

inline

Constructor for function symbol Real2Pos.

Returns: Function symbol real2pos.

Definition at line 357 of file real1.h.

◆ real2pos() [2/2]

application mcrl2::data::sort_real::real2pos ( const data_expression & arg0 )

inline

Application of function symbol Real2Pos.

Parameters

arg0	A data expression.

Returns: Application of Real2Pos to a number of arguments.

Definition at line 381 of file real1.h.

◆ real2pos_name()

const core::identifier_string & mcrl2::data::sort_real::real2pos_name ( )

inline

Generate identifier Real2Pos.

Returns: Identifier Real2Pos.

Definition at line 347 of file real1.h.

◆ real_() [1/5]

const basic_sort & mcrl2::data::sort_real::real_ ( )

inline

Constructor for sort expression Real.

Returns: Sort expression Real.

Definition at line 48 of file real1.h.

◆ real_() [2/5]

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

inline

Constructs expression of type Real from a string.

Parameters

n A string

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

Definition at line 783 of file standard_numbers_utility.h.

◆ real_() [3/5]

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

inline

Constructs expression of type Real from two number strings.

Parameters

numerator	numerator.
denominator	denominator.

Returns: numerator / denominator.

Definition at line 775 of file standard_numbers_utility.h.

◆ real_() [4/5]

template<typename T >

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

inline

Constructs expression of type Real from an integral type.

Parameters

numerator	numerator.
denominator	denominator.

Definition at line 766 of file standard_numbers_utility.h.

◆ real_() [5/5]

template<typename T >

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

inline

Constructs expression of type Real from an integral type.

Parameters

t	An expression of type T.

Definition at line 752 of file standard_numbers_utility.h.

◆ real_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_real::real_cpp_implementable_constructors ( )

inline

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for real_.

Returns: All system defined constructors that are to be implemented in C++ for real_.

Definition at line 88 of file real1.h.

◆ real_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_real::real_cpp_implementable_mappings ( )

inline

Give all system defined mappings that are to be implemented in C++ code for real_.

Returns: A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for real_

Definition at line 1930 of file real1.h.

◆ real_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_real::real_generate_constructors_and_functions_code ( )

inline

Give all system defined mappings and constructors for real_.

Returns: All system defined mappings for real_

Definition at line 1878 of file real1.h.

◆ real_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_real::real_generate_constructors_code ( )

inline

Give all system defined constructors for real_.

Returns: All system defined constructors for real_.

Definition at line 70 of file real1.h.

◆ real_generate_equations_code()

data_equation_vector mcrl2::data::sort_real::real_generate_equations_code ( )

inline

Give all system defined equations for real_.

Returns: All system defined equations for sort real_

Definition at line 2010 of file real1.h.

◆ real_generate_functions_code()

function_symbol_vector mcrl2::data::sort_real::real_generate_functions_code ( )

inline

Give all system defined mappings for real_.

Returns: All system defined mappings for real_

Definition at line 1842 of file real1.h.

◆ real_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_real::real_mCRL2_usable_constructors ( )

inline

Give all defined constructors which can be used in mCRL2 specs for real_.

Returns: All system defined constructors that can be used in an mCRL2 specification for real_.

Definition at line 78 of file real1.h.

◆ real_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_real::real_mCRL2_usable_mappings ( )

inline

Give all system defined mappings that can be used in mCRL2 specs for real_.

Returns: All system defined mappings for that can be used in mCRL2 specificationis real_

Definition at line 1891 of file real1.h.

◆ real_name()

const core::identifier_string & mcrl2::data::sort_real::real_name ( )

inline

Definition at line 39 of file real1.h.

◆ real_one()

data_expression & mcrl2::data::sort_real::real_one ( )

inline

Definition at line 31 of file real_utilities.h.

◆ real_zero()

data_expression & mcrl2::data::sort_real::real_zero ( )

inline

Definition at line 25 of file real_utilities.h.

◆ reduce_fraction() [1/2]

const function_symbol & mcrl2::data::sort_real::reduce_fraction ( )

inline

Constructor for function symbol @redfrac.

Returns: Function symbol reduce_fraction.

Definition at line 1659 of file real1.h.

◆ reduce_fraction() [2/2]

application mcrl2::data::sort_real::reduce_fraction	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @redfrac.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of @redfrac to a number of arguments.

Definition at line 1684 of file real1.h.

◆ reduce_fraction_helper() [1/2]

const function_symbol & mcrl2::data::sort_real::reduce_fraction_helper ( )

inline

Constructor for function symbol @redfrachlp.

Returns: Function symbol reduce_fraction_helper.

Definition at line 1789 of file real1.h.

◆ reduce_fraction_helper() [2/2]

application mcrl2::data::sort_real::reduce_fraction_helper	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @redfrachlp.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of @redfrachlp to a number of arguments.

Definition at line 1814 of file real1.h.

◆ reduce_fraction_helper_name()

const core::identifier_string & mcrl2::data::sort_real::reduce_fraction_helper_name ( )

inline

Generate identifier @redfrachlp.

Returns: Identifier @redfrachlp.

Definition at line 1779 of file real1.h.

◆ reduce_fraction_name()

const core::identifier_string & mcrl2::data::sort_real::reduce_fraction_name ( )

inline

Generate identifier @redfrac.

Returns: Identifier @redfrac.

Definition at line 1649 of file real1.h.

◆ reduce_fraction_where() [1/2]

const function_symbol & mcrl2::data::sort_real::reduce_fraction_where ( )

inline

Constructor for function symbol @redfracwhr.

Returns: Function symbol reduce_fraction_where.

Definition at line 1723 of file real1.h.

◆ reduce_fraction_where() [2/2]

application mcrl2::data::sort_real::reduce_fraction_where	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @redfracwhr.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns: Application of @redfracwhr to a number of arguments.

Definition at line 1749 of file real1.h.

◆ reduce_fraction_where_name()

const core::identifier_string & mcrl2::data::sort_real::reduce_fraction_where_name ( )

inline

Generate identifier @redfracwhr.

Returns: Identifier @redfracwhr.

Definition at line 1713 of file real1.h.

◆ right()

const data_expression & mcrl2::data::sort_real::right ( const data_expression & e )

inline

Function for projecting out argument. right from an application.

Parameters

e	A data expression.

Precondition: right is defined for e.

Returns: The argument of e that corresponds to right.

Definition at line 1953 of file real1.h.

◆ round() [1/2]

const function_symbol & mcrl2::data::sort_real::round ( )

inline

Constructor for function symbol round.

Returns: Function symbol round.

Definition at line 1597 of file real1.h.

◆ round() [2/2]

application mcrl2::data::sort_real::round ( const data_expression & arg0 )

inline

Application of function symbol round.

Parameters

arg0	A data expression.

Returns: Application of round to a number of arguments.

Definition at line 1621 of file real1.h.

◆ round_name()

const core::identifier_string & mcrl2::data::sort_real::round_name ( )

inline

Generate identifier round.

Returns: Identifier round.

Definition at line 1587 of file real1.h.

◆ succ() [1/2]

application mcrl2::data::sort_real::succ ( const data_expression & arg0 )

inline

Application of function symbol succ.

Parameters

arg0	A data expression.

Returns: Application of succ to a number of arguments.

Definition at line 940 of file real1.h.

◆ succ() [2/2]

function_symbol mcrl2::data::sort_real::succ ( const sort_expression & s0 )

inline

Definition at line 893 of file real1.h.

◆ succ_name()

const core::identifier_string & mcrl2::data::sort_real::succ_name ( )

inline

Generate identifier succ.

Returns: Identifier succ.

Definition at line 885 of file real1.h.

◆ times() [1/2]

application mcrl2::data::sort_real::times	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol *.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of * to a number of arguments.

Definition at line 1285 of file real1.h.

◆ times() [2/2]

function_symbol mcrl2::data::sort_real::times	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1237 of file real1.h.

◆ times_name()

const core::identifier_string & mcrl2::data::sort_real::times_name ( )

inline

Generate identifier *.

Returns: Identifier *.

Definition at line 1229 of file real1.h.

◆ value()

template<class NUMERIC_TYPE >

NUMERIC_TYPE mcrl2::data::sort_real::value	(	const data_expression &	r,
		typename std::enable_if< std::is_floating_point< NUMERIC_TYPE >::value >::type *	= `nullptr`
	)

inline

Yields the real value of a data expression.

Parameters

r	A data expression of sort real in normal form.

Definition at line 795 of file standard_numbers_utility.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ abs() [1/2]

◆ abs() [2/2]

◆ abs_name()

◆ arg()

◆ arg1()

◆ arg2()

◆ arg3()

◆ ceil() [1/2]

◆ ceil() [2/2]

◆ ceil_name()

◆ creal() [1/2]

◆ creal() [2/2]

◆ creal_name()

◆ divides() [1/2]

◆ divides() [2/2]

◆ divides_name()

◆ exp() [1/2]

◆ exp() [2/2]

◆ exp_name()

◆ floor() [1/2]

◆ floor() [2/2]

◆ floor_name()

◆ int2real() [1/2]

◆ int2real() [2/2]

◆ int2real_name()

◆ is_abs_application()

◆ is_abs_function_symbol()

◆ is_ceil_application()

◆ is_ceil_function_symbol()

◆ is_creal_application()

◆ is_creal_function_symbol()

◆ is_divides_application()

◆ is_divides_function_symbol()

◆ is_exp_application()

◆ is_exp_function_symbol()

◆ is_floor_application()

◆ is_floor_function_symbol()

◆ is_int2real_application()

◆ is_int2real_function_symbol()

◆ is_larger_zero()

◆ is_maximum_application()

◆ is_maximum_function_symbol()

◆ is_minimum_application()

◆ is_minimum_function_symbol()

◆ is_minus_application()

◆ is_minus_function_symbol()

◆ is_nat2real_application()

◆ is_nat2real_function_symbol()

◆ is_negate_application()

◆ is_negate_function_symbol()

◆ is_one()

◆ is_plus_application()

◆ is_plus_function_symbol()

◆ is_pos2real_application()

◆ is_pos2real_function_symbol()

◆ is_pred_application()

◆ is_pred_function_symbol()

◆ is_real()

◆ is_real2int_application()

◆ is_real2int_function_symbol()

◆ is_real2nat_application()

◆ is_real2nat_function_symbol()

◆ is_real2pos_application()

◆ is_real2pos_function_symbol()

◆ is_reduce_fraction_application()

◆ is_reduce_fraction_function_symbol()

◆ is_reduce_fraction_helper_application()

◆ is_reduce_fraction_helper_function_symbol()

◆ is_reduce_fraction_where_application()

◆ is_reduce_fraction_where_function_symbol()

◆ is_round_application()

◆ is_round_function_symbol()

◆ is_succ_application()

◆ is_succ_function_symbol()