Namespace for system defined sort pos. More...

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

Functions
template<typename T > requires std::is_integral_v<T>
data_expression	pos (const T t)
	Constructs expression of type Bool from an integral type Type T is an unsigned integral type.

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

bool	is_positive_constant (const data_expression &n)
	Determines whether n is a positive constant.

std::string	positive_constant_as_string (const data_expression &n_in)
	Return the string representation of a positive number.

template<class NUMERIC_TYPE >
NUMERIC_TYPE	positive_constant_to_value (const data_expression &n)
	Returns the NUMERIC_TYPE representation of a positive number.

const core::identifier_string &	pos_name ()

const basic_sort &	pos ()
	Constructor for sort expression Pos.

bool	is_pos (const sort_expression &e)
	Recogniser for sort expression Pos.

const core::identifier_string &	c1_name ()
	Generate identifier @c1.

const function_symbol &	c1 ()
	Constructor for function symbol @c1.

bool	is_c1_function_symbol (const atermpp::aterm &e)
	Recogniser for function @c1.

const core::identifier_string &	cdub_name ()
	Generate identifier @cDub.

const function_symbol &	cdub ()
	Constructor for function symbol @cDub.

bool	is_cdub_function_symbol (const atermpp::aterm &e)
	Recogniser for function @cDub.

application	cdub (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @cDub.

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

bool	is_cdub_application (const atermpp::aterm &e)
	Recogniser for application of @cDub.

function_symbol_vector	pos_generate_constructors_code ()
	Give all system defined constructors for pos.

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

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

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

const function_symbol &	maximum ()
	Constructor for function symbol max.

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.

const function_symbol &	minimum ()
	Constructor for function symbol min.

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 &	succ_name ()
	Generate identifier succ.

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

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 &	pos_predecessor_name ()
	Generate identifier @pospred.

const function_symbol &	pos_predecessor ()
	Constructor for function symbol @pospred.

bool	is_pos_predecessor_function_symbol (const atermpp::aterm &e)
	Recogniser for function @pospred.

application	pos_predecessor (const data_expression &arg0)
	Application of function symbol @pospred.

void	make_pos_predecessor (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @pospred.

bool	is_pos_predecessor_application (const atermpp::aterm &e)
	Recogniser for application of @pospred.

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

const function_symbol &	plus ()
	Constructor for function symbol +.

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 &	add_with_carry_name ()
	Generate identifier @addc.

const function_symbol &	add_with_carry ()
	Constructor for function symbol @addc.

bool	is_add_with_carry_function_symbol (const atermpp::aterm &e)
	Recogniser for function @addc.

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

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

bool	is_add_with_carry_application (const atermpp::aterm &e)
	Recogniser for application of @addc.

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

const function_symbol &	times ()
	Constructor for function symbol *.

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 &	powerlog2_pos_name ()
	Generate identifier @powerlog2.

const function_symbol &	powerlog2_pos ()
	Constructor for function symbol @powerlog2.

bool	is_powerlog2_pos_function_symbol (const atermpp::aterm &e)
	Recogniser for function @powerlog2.

application	powerlog2_pos (const data_expression &arg0)
	Application of function symbol @powerlog2.

void	make_powerlog2_pos (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @powerlog2.

bool	is_powerlog2_pos_application (const atermpp::aterm &e)
	Recogniser for application of @powerlog2.

function_symbol_vector	pos_generate_functions_code ()
	Give all system defined mappings for pos.

function_symbol_vector	pos_generate_constructors_and_functions_code ()
	Give all system defined mappings and constructors for pos.

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

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

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	pos_generate_equations_code ()
	Give all system defined equations for pos.

const core::identifier_string &	succpos_name ()
	Generate identifier @succ_pos.

const function_symbol &	succpos ()
	Constructor for function symbol @succ_pos.

bool	is_succpos_function_symbol (const atermpp::aterm &e)
	Recogniser for function @succ_pos.

application	succpos (const data_expression &arg0)
	Application of function symbol @succ_pos.

void	make_succpos (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @succ_pos.

bool	is_succpos_application (const atermpp::aterm &e)
	Recogniser for application of @succ_pos.

const core::identifier_string &	most_significant_digit_name ()
	Generate identifier @most_significant_digit.

const function_symbol &	most_significant_digit ()
	Constructor for function symbol @most_significant_digit.

bool	is_most_significant_digit_function_symbol (const atermpp::aterm &e)
	Recogniser for function @most_significant_digit.

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

void	make_most_significant_digit (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @most_significant_digit.

bool	is_most_significant_digit_application (const atermpp::aterm &e)
	Recogniser for application of @most_significant_digit.

const core::identifier_string &	concat_digit_name ()
	Generate identifier @concat_digit.

const function_symbol &	concat_digit ()
	Constructor for function symbol @concat_digit.

bool	is_concat_digit_function_symbol (const atermpp::aterm &e)
	Recogniser for function @concat_digit.

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

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

bool	is_concat_digit_application (const atermpp::aterm &e)
	Recogniser for application of @concat_digit.

const core::identifier_string &	equals_one_name ()
	Generate identifier @equals_one.

const function_symbol &	equals_one ()
	Constructor for function symbol @equals_one.

bool	is_equals_one_function_symbol (const atermpp::aterm &e)
	Recogniser for function @equals_one.

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

void	make_equals_one (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @equals_one.

bool	is_equals_one_application (const atermpp::aterm &e)
	Recogniser for application of @equals_one.

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

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

const core::identifier_string &	auxiliary_plus_pos_name ()
	Generate identifier @plus_pos.

const function_symbol &	auxiliary_plus_pos ()
	Constructor for function symbol @plus_pos.

bool	is_auxiliary_plus_pos_function_symbol (const atermpp::aterm &e)
	Recogniser for function @plus_pos.

application	auxiliary_plus_pos (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @plus_pos.

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

bool	is_auxiliary_plus_pos_application (const atermpp::aterm &e)
	Recogniser for application of @plus_pos.

const core::identifier_string &	times_overflow_name ()
	Generate identifier @times_overflow.

const function_symbol &	times_overflow ()
	Constructor for function symbol @times_overflow.

bool	is_times_overflow_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_overflow.

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

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

bool	is_times_overflow_application (const atermpp::aterm &e)
	Recogniser for application of @times_overflow.

const core::identifier_string &	times_ordered_name ()
	Generate identifier @times_ordered.

const function_symbol &	times_ordered ()
	Constructor for function symbol @times_ordered.

bool	is_times_ordered_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_ordered.

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

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

bool	is_times_ordered_application (const atermpp::aterm &e)
	Recogniser for application of @times_ordered.

const core::identifier_string &	times_whr_mult_overflow_name ()
	Generate identifier @times_whr_mult_overflow.

const function_symbol &	times_whr_mult_overflow ()
	Constructor for function symbol @times_whr_mult_overflow.

bool	is_times_whr_mult_overflow_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_whr_mult_overflow.

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

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

bool	is_times_whr_mult_overflow_application (const atermpp::aterm &e)
	Recogniser for application of @times_whr_mult_overflow.

Detailed Description

Namespace for system defined sort pos.

Typedef Documentation

◆ implementation_map

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

Definition at line 180 of file pos1.h.

Function Documentation

◆ add_with_carry() [1/3]

const function_symbol & mcrl2::data::sort_pos::add_with_carry ( )

inline

Constructor for function symbol @addc.

Constructor for function symbol @add_with_carry.

Returns: Function symbol add_with_carry.

Definition at line 519 of file pos1.h.

◆ add_with_carry() [2/3]

application mcrl2::data::sort_pos::add_with_carry	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @add_with_carry.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

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

Definition at line 731 of file pos64.h.

◆ add_with_carry() [3/3]

application mcrl2::data::sort_pos::add_with_carry	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @addc.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

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

Definition at line 545 of file pos1.h.

◆ add_with_carry_name()

const core::identifier_string & mcrl2::data::sort_pos::add_with_carry_name ( )

inline

Generate identifier @addc.

Generate identifier @add_with_carry.

Returns: Identifier @addc.; Identifier @add_with_carry.

Definition at line 509 of file pos1.h.

◆ arg()

const data_expression & mcrl2::data::sort_pos::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 785 of file pos1.h.

◆ arg1()

const data_expression & mcrl2::data::sort_pos::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 797 of file pos1.h.

◆ arg2()

const data_expression & mcrl2::data::sort_pos::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 809 of file pos1.h.

◆ arg3()

const data_expression & mcrl2::data::sort_pos::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 821 of file pos1.h.

◆ auxiliary_plus_pos() [1/2]

const function_symbol & mcrl2::data::sort_pos::auxiliary_plus_pos ( )

inline

Constructor for function symbol @plus_pos.

Returns: Function symbol auxiliary_plus_pos.

Definition at line 770 of file pos64.h.

◆ auxiliary_plus_pos() [2/2]

application mcrl2::data::sort_pos::auxiliary_plus_pos	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @plus_pos.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

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

Definition at line 795 of file pos64.h.

◆ auxiliary_plus_pos_name()

const core::identifier_string & mcrl2::data::sort_pos::auxiliary_plus_pos_name ( )

inline

Generate identifier @plus_pos.

Returns: Identifier @plus_pos.

Definition at line 760 of file pos64.h.

◆ c1()

const function_symbol & mcrl2::data::sort_pos::c1 ( )

inline

Constructor for function symbol @c1.

Returns: Function symbol c1.

Definition at line 75 of file pos1.h.

◆ c1_name()

const core::identifier_string & mcrl2::data::sort_pos::c1_name ( )

inline

Generate identifier @c1.

Returns: Identifier @c1.

Definition at line 65 of file pos1.h.

◆ cdub() [1/2]

const function_symbol & mcrl2::data::sort_pos::cdub ( )

inline

Constructor for function symbol @cDub.

Returns: Function symbol cdub.

Definition at line 107 of file pos1.h.

◆ cdub() [2/2]

application mcrl2::data::sort_pos::cdub	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @cDub.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

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

Definition at line 132 of file pos1.h.

◆ cdub_name()

const core::identifier_string & mcrl2::data::sort_pos::cdub_name ( )

inline

Generate identifier @cDub.

Returns: Identifier @cDub.

Definition at line 97 of file pos1.h.

◆ concat_digit() [1/2]

const function_symbol & mcrl2::data::sort_pos::concat_digit ( )

inline

Constructor for function symbol @concat_digit.

Returns: Function symbol concat_digit.

Definition at line 264 of file pos64.h.

◆ concat_digit() [2/2]

application mcrl2::data::sort_pos::concat_digit	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @concat_digit.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

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

Definition at line 289 of file pos64.h.

◆ concat_digit_name()

const core::identifier_string & mcrl2::data::sort_pos::concat_digit_name ( )

inline

Generate identifier @concat_digit.

Returns: Identifier @concat_digit.

Definition at line 254 of file pos64.h.

◆ equals_one() [1/2]

const function_symbol & mcrl2::data::sort_pos::equals_one ( )

inline

Constructor for function symbol @equals_one.

Returns: Function symbol equals_one.

Definition at line 328 of file pos64.h.

◆ equals_one() [2/2]

application mcrl2::data::sort_pos::equals_one ( const data_expression & arg0 )

inline

Application of function symbol @equals_one.

Parameters

[in] arg0 A data expression.

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

Definition at line 352 of file pos64.h.

◆ equals_one_name()

const core::identifier_string & mcrl2::data::sort_pos::equals_one_name ( )

inline

Generate identifier @equals_one.

Returns: Identifier @equals_one.

Definition at line 318 of file pos64.h.

◆ is_add_with_carry_application()

bool mcrl2::data::sort_pos::is_add_with_carry_application ( const atermpp::aterm & e )

inline

Recogniser for application of @addc.

Recogniser for application of @add_with_carry.

Parameters

e	A data expression.

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

Definition at line 567 of file pos1.h.

◆ is_add_with_carry_function_symbol()

bool mcrl2::data::sort_pos::is_add_with_carry_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @addc.

Recogniser for function @add_with_carry.

Parameters

e	A data expression.

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

Parameters

e	A data expression.

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

Definition at line 529 of file pos1.h.

◆ is_auxiliary_plus_pos_application()

bool mcrl2::data::sort_pos::is_auxiliary_plus_pos_application ( const atermpp::aterm & e )

inline

Recogniser for application of @plus_pos.

Parameters

e	A data expression.

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

Definition at line 816 of file pos64.h.

◆ is_auxiliary_plus_pos_function_symbol()

bool mcrl2::data::sort_pos::is_auxiliary_plus_pos_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @plus_pos.

Parameters

e	A data expression.

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

Definition at line 780 of file pos64.h.

◆ is_c1_function_symbol()

bool mcrl2::data::sort_pos::is_c1_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @c1.

Parameters

e	A data expression.

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

Definition at line 85 of file pos1.h.

◆ is_cdub_application()

bool mcrl2::data::sort_pos::is_cdub_application ( const atermpp::aterm & e )

inline

Recogniser for application of @cDub.

Parameters

e	A data expression.

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

Definition at line 153 of file pos1.h.

◆ is_cdub_function_symbol()

bool mcrl2::data::sort_pos::is_cdub_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @cDub.

Parameters

e	A data expression.

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

Definition at line 117 of file pos1.h.

◆ is_concat_digit_application()

bool mcrl2::data::sort_pos::is_concat_digit_application ( const atermpp::aterm & e )

inline

Recogniser for application of @concat_digit.

Parameters

e	A data expression.

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

Definition at line 310 of file pos64.h.

◆ is_concat_digit_function_symbol()

bool mcrl2::data::sort_pos::is_concat_digit_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @concat_digit.

Parameters

e	A data expression.

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

Definition at line 274 of file pos64.h.

◆ is_equals_one_application()

bool mcrl2::data::sort_pos::is_equals_one_application ( const atermpp::aterm & e )

inline

Recogniser for application of @equals_one.

Parameters

e	A data expression.

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

Definition at line 372 of file pos64.h.

◆ is_equals_one_function_symbol()

bool mcrl2::data::sort_pos::is_equals_one_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @equals_one.

Parameters

e	A data expression.

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

Definition at line 338 of file pos64.h.

◆ is_maximum_application()

bool mcrl2::data::sort_pos::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 249 of file pos1.h.

◆ is_maximum_function_symbol()

bool mcrl2::data::sort_pos::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 213 of file pos1.h.

◆ is_minimum_application()

bool mcrl2::data::sort_pos::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 313 of file pos1.h.

◆ is_minimum_function_symbol()

bool mcrl2::data::sort_pos::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 277 of file pos1.h.

◆ is_most_significant_digit_application()

bool mcrl2::data::sort_pos::is_most_significant_digit_application ( const atermpp::aterm & e )

inline

Recogniser for application of @most_significant_digit.

Parameters

e	A data expression.

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

Definition at line 246 of file pos64.h.

◆ is_most_significant_digit_function_symbol()

bool mcrl2::data::sort_pos::is_most_significant_digit_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @most_significant_digit.

Parameters

e	A data expression.

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

Definition at line 212 of file pos64.h.

◆ is_plus_application()

bool mcrl2::data::sort_pos::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 501 of file pos1.h.

◆ is_plus_function_symbol()

bool mcrl2::data::sort_pos::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 465 of file pos1.h.

◆ is_pos()

bool mcrl2::data::sort_pos::is_pos ( const sort_expression & e )

inline

Recogniser for sort expression Pos.

Parameters

e	A sort expression

Returns: true iff e == pos()

Definition at line 52 of file pos1.h.

◆ is_pos_predecessor_application()

bool mcrl2::data::sort_pos::is_pos_predecessor_application ( const atermpp::aterm & e )

inline

Recogniser for application of @pospred.

Parameters

e	A data expression.

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

Definition at line 437 of file pos1.h.

◆ is_pos_predecessor_function_symbol()

bool mcrl2::data::sort_pos::is_pos_predecessor_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @pospred.

Parameters

e	A data expression.

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

Definition at line 403 of file pos1.h.

◆ is_positive_constant()

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

inline

Determines whether n is a positive constant.

Parameters

n	A data expression

Definition at line 359 of file standard_numbers_utility.h.

◆ is_powerlog2_pos_application()

bool mcrl2::data::sort_pos::is_powerlog2_pos_application ( const atermpp::aterm & e )

inline

Recogniser for application of @powerlog2.

Parameters

e	A data expression.

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

Definition at line 693 of file pos1.h.

◆ is_powerlog2_pos_function_symbol()

bool mcrl2::data::sort_pos::is_powerlog2_pos_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @powerlog2.

Parameters

e	A data expression.

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

Definition at line 659 of file pos1.h.

◆ is_succ_application()

bool mcrl2::data::sort_pos::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 375 of file pos1.h.

◆ is_succ_function_symbol()

bool mcrl2::data::sort_pos::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 341 of file pos1.h.

◆ is_succpos_application()

bool mcrl2::data::sort_pos::is_succpos_application ( const atermpp::aterm & e )

inline

Recogniser for application of @succ_pos.

Parameters

e	A data expression.

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

Definition at line 152 of file pos64.h.

◆ is_succpos_function_symbol()

bool mcrl2::data::sort_pos::is_succpos_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @succ_pos.

Parameters

e	A data expression.

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

Definition at line 118 of file pos64.h.

◆ is_times_application()

bool mcrl2::data::sort_pos::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 631 of file pos1.h.

◆ is_times_function_symbol()

bool mcrl2::data::sort_pos::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 595 of file pos1.h.

◆ is_times_ordered_application()

bool mcrl2::data::sort_pos::is_times_ordered_application ( const atermpp::aterm & e )

inline

Recogniser for application of @times_ordered.

Parameters

e	A data expression.

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

Definition at line 1010 of file pos64.h.

◆ is_times_ordered_function_symbol()

bool mcrl2::data::sort_pos::is_times_ordered_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @times_ordered.

Parameters

e	A data expression.

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

Definition at line 974 of file pos64.h.

◆ is_times_overflow_application()

bool mcrl2::data::sort_pos::is_times_overflow_application ( const atermpp::aterm & e )

inline

Recogniser for application of @times_overflow.

Parameters

e	A data expression.

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

Definition at line 946 of file pos64.h.

◆ is_times_overflow_function_symbol()

bool mcrl2::data::sort_pos::is_times_overflow_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @times_overflow.

Parameters

e	A data expression.

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

Definition at line 908 of file pos64.h.

◆ is_times_whr_mult_overflow_application()

bool mcrl2::data::sort_pos::is_times_whr_mult_overflow_application ( const atermpp::aterm & e )

inline

Recogniser for application of @times_whr_mult_overflow.

Parameters

e	A data expression.

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

Definition at line 1074 of file pos64.h.

◆ is_times_whr_mult_overflow_function_symbol()

bool mcrl2::data::sort_pos::is_times_whr_mult_overflow_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @times_whr_mult_overflow.

Parameters

e	A data expression.

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

Definition at line 1038 of file pos64.h.

◆ left()

const data_expression & mcrl2::data::sort_pos::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 761 of file pos1.h.

◆ make_add_with_carry() [1/2]

void mcrl2::data::sort_pos::make_add_with_carry	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @add_with_carry.

Parameters

[out]	result	The data expression where the @add_with_carry expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 742 of file pos64.h.

◆ make_add_with_carry() [2/2]

void mcrl2::data::sort_pos::make_add_with_carry	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Make an application of function symbol @addc.

Parameters

[out]	result	The data expression where the @addc expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Definition at line 557 of file pos1.h.

◆ make_auxiliary_plus_pos()

void mcrl2::data::sort_pos::make_auxiliary_plus_pos	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @plus_pos.

Parameters

[out]	result	The data expression where the @plus_pos expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 806 of file pos64.h.

◆ make_cdub()

void mcrl2::data::sort_pos::make_cdub	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @cDub.

Parameters

[out]	result	The data expression where the @cDub expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 143 of file pos1.h.

◆ make_concat_digit()

void mcrl2::data::sort_pos::make_concat_digit	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @concat_digit.

Parameters

[out]	result	The data expression where the @concat_digit expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 300 of file pos64.h.

◆ make_equals_one()

void mcrl2::data::sort_pos::make_equals_one	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @equals_one.

Parameters

[out]	result	The data expression where the @equals_one expression is put.
[in]	arg0	A data expression.

Definition at line 362 of file pos64.h.

◆ make_maximum()

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

inline

Make an application of function symbol max.

Parameters

[out]	result	The data expression where the max expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 239 of file pos1.h.

◆ make_minimum()

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

inline

Make an application of function symbol min.

Parameters

[out]	result	The data expression where the min expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 303 of file pos1.h.

◆ make_most_significant_digit()

void mcrl2::data::sort_pos::make_most_significant_digit	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @most_significant_digit.

Parameters

[out]	result	The data expression where the @most_significant_digit expression is put.
[in]	arg0	A data expression.

Definition at line 236 of file pos64.h.

◆ make_plus()

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

inline

Make an application of function symbol +.

Parameters

[out]	result	The data expression where the + expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 491 of file pos1.h.

◆ make_pos_predecessor()

void mcrl2::data::sort_pos::make_pos_predecessor	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @pospred.

Parameters

[out]	result	The data expression where the @pospred expression is put.
[in]	arg0	A data expression.

Definition at line 427 of file pos1.h.

◆ make_powerlog2_pos()

void mcrl2::data::sort_pos::make_powerlog2_pos	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @powerlog2.

Parameters

[out]	result	The data expression where the @powerlog2 expression is put.
[in]	arg0	A data expression.

Definition at line 683 of file pos1.h.

◆ make_succ()

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

inline

Make an application of function symbol succ.

Parameters

[out]	result	The data expression where the succ expression is put.
[in]	arg0	A data expression.

Definition at line 365 of file pos1.h.

◆ make_succpos()

void mcrl2::data::sort_pos::make_succpos	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @succ_pos.

Parameters

[out]	result	The data expression where the @succ_pos expression is put.
[in]	arg0	A data expression.

Definition at line 142 of file pos64.h.

◆ make_times()

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

inline

Make an application of function symbol *.

Parameters

[out]	result	The data expression where the * expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 621 of file pos1.h.

◆ make_times_ordered()

void mcrl2::data::sort_pos::make_times_ordered	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @times_ordered.

Parameters

[out]	result	The data expression where the @times_ordered expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 1000 of file pos64.h.

◆ make_times_overflow()

void mcrl2::data::sort_pos::make_times_overflow	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Make an application of function symbol @times_overflow.

Parameters

[out]	result	The data expression where the @times_overflow expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Definition at line 936 of file pos64.h.

◆ make_times_whr_mult_overflow()

void mcrl2::data::sort_pos::make_times_whr_mult_overflow	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @times_whr_mult_overflow.

Parameters

[out]	result	The data expression where the @times_whr_mult_overflow expression is put.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 1064 of file pos64.h.

◆ maximum() [1/2]

const function_symbol & mcrl2::data::sort_pos::maximum ( )

inline

Constructor for function symbol max.

Returns: Function symbol maximum.

Definition at line 203 of file pos1.h.

◆ maximum() [2/2]

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

inline

Application of function symbol max.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns: Application of max to a number of arguments.

Definition at line 228 of file pos1.h.

◆ maximum_name()

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

inline

Generate identifier max.

Returns: Identifier max.

Definition at line 193 of file pos1.h.

◆ minimum() [1/2]

const function_symbol & mcrl2::data::sort_pos::minimum ( )

inline

Constructor for function symbol min.

Returns: Function symbol minimum.

Definition at line 267 of file pos1.h.

◆ minimum() [2/2]

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

inline

Application of function symbol min.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns: Application of min to a number of arguments.

Definition at line 292 of file pos1.h.

◆ minimum_name()

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

inline

Generate identifier min.

Returns: Identifier min.

Definition at line 257 of file pos1.h.

◆ most_significant_digit() [1/2]

const function_symbol & mcrl2::data::sort_pos::most_significant_digit ( )

inline

Constructor for function symbol @most_significant_digit.

Returns: Function symbol most_significant_digit.

Definition at line 202 of file pos64.h.

◆ most_significant_digit() [2/2]

application mcrl2::data::sort_pos::most_significant_digit ( const data_expression & arg0 )

inline

Application of function symbol @most_significant_digit.

Parameters

[in] arg0 A data expression.

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

Definition at line 226 of file pos64.h.

◆ most_significant_digit_name()

const core::identifier_string & mcrl2::data::sort_pos::most_significant_digit_name ( )

inline

Generate identifier @most_significant_digit.

Returns: Identifier @most_significant_digit.

Definition at line 192 of file pos64.h.

◆ plus() [1/2]

const function_symbol & mcrl2::data::sort_pos::plus ( )

inline

Constructor for function symbol +.

Returns: Function symbol plus.

Definition at line 455 of file pos1.h.

◆ plus() [2/2]

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

inline

Application of function symbol +.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns: Application of + to a number of arguments.

Definition at line 480 of file pos1.h.

◆ plus_name()

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

inline

Generate identifier +.

Returns: Identifier +.

Definition at line 445 of file pos1.h.

◆ pos() [1/3]

const basic_sort & mcrl2::data::sort_pos::pos ( )

inline

Constructor for sort expression Pos.

Returns: Sort expression Pos.

Definition at line 42 of file pos1.h.

◆ pos() [2/3]

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

inline

Constructs expression of type Pos from a string.

Parameters

n A string

Definition at line 321 of file standard_numbers_utility.h.

◆ pos() [3/3]

template<typename T >
requires std::is_integral_v<T>

data_expression mcrl2::data::sort_pos::pos ( const T t )

inline

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

Definition at line 291 of file standard_numbers_utility.h.

◆ pos_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_pos::pos_cpp_implementable_constructors ( )

inline

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

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

Definition at line 184 of file pos1.h.

◆ pos_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_pos::pos_cpp_implementable_mappings ( )

inline

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

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

Definition at line 750 of file pos1.h.

◆ pos_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_and_functions_code ( )

inline

Give all system defined mappings and constructors for pos.

Returns: All system defined mappings for pos

Definition at line 717 of file pos1.h.

◆ pos_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_code ( )

inline

Give all system defined constructors for pos.

Returns: All system defined constructors for pos.

Definition at line 160 of file pos1.h.

◆ pos_generate_equations_code()

data_equation_vector mcrl2::data::sort_pos::pos_generate_equations_code ( )

inline

Give all system defined equations for pos.

Returns: All system defined equations for sort pos

Definition at line 830 of file pos1.h.

◆ pos_generate_functions_code()

function_symbol_vector mcrl2::data::sort_pos::pos_generate_functions_code ( )

inline

Give all system defined mappings for pos.

Returns: All system defined mappings for pos

Definition at line 700 of file pos1.h.

◆ pos_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_pos::pos_mCRL2_usable_constructors ( )

inline

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

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

Definition at line 171 of file pos1.h.

◆ pos_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_pos::pos_mCRL2_usable_mappings ( )

inline

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

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

Definition at line 730 of file pos1.h.

◆ pos_name()

const core::identifier_string & mcrl2::data::sort_pos::pos_name ( )

inline

Definition at line 33 of file pos1.h.

◆ pos_predecessor() [1/2]

const function_symbol & mcrl2::data::sort_pos::pos_predecessor ( )

inline

Constructor for function symbol @pospred.

Returns: Function symbol pos_predecessor.

Definition at line 393 of file pos1.h.

◆ pos_predecessor() [2/2]

application mcrl2::data::sort_pos::pos_predecessor ( const data_expression & arg0 )

inline

Application of function symbol @pospred.

Parameters

[in] arg0 A data expression.

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

Definition at line 417 of file pos1.h.

◆ pos_predecessor_name()

const core::identifier_string & mcrl2::data::sort_pos::pos_predecessor_name ( )

inline

Generate identifier @pospred.

Returns: Identifier @pospred.

Definition at line 383 of file pos1.h.

◆ positive_constant_as_string()

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

inline

Return the string representation of a positive number.

Parameters

n_in	A data expression

Precondition: is_positive_constant(n)

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

Definition at line 383 of file standard_numbers_utility.h.

◆ positive_constant_to_value()

template<class NUMERIC_TYPE >

NUMERIC_TYPE mcrl2::data::sort_pos::positive_constant_to_value ( const data_expression & n )

inline

Returns the NUMERIC_TYPE representation of a positive number.

Parameters

n_in	A data expression

Precondition: is_positive_constant(n)

Returns: Representation of n as sort NUMERIC_TYPE Transforms a positive constant n into number of sort NUMERIC_TYPE. Throws an exception when it does not fit. the decimal representation of n.

Definition at line 434 of file standard_numbers_utility.h.

◆ powerlog2_pos() [1/2]

const function_symbol & mcrl2::data::sort_pos::powerlog2_pos ( )

inline

Constructor for function symbol @powerlog2.

Returns: Function symbol powerlog2_pos.

Definition at line 649 of file pos1.h.

◆ powerlog2_pos() [2/2]

application mcrl2::data::sort_pos::powerlog2_pos ( const data_expression & arg0 )

inline

Application of function symbol @powerlog2.

Parameters

[in] arg0 A data expression.

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

Definition at line 673 of file pos1.h.

◆ powerlog2_pos_name()

const core::identifier_string & mcrl2::data::sort_pos::powerlog2_pos_name ( )

inline

Generate identifier @powerlog2.

Returns: Identifier @powerlog2.

Definition at line 639 of file pos1.h.

◆ right()

const data_expression & mcrl2::data::sort_pos::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 773 of file pos1.h.

◆ succ() [1/2]

const function_symbol & mcrl2::data::sort_pos::succ ( )

inline

Constructor for function symbol succ.

Returns: Function symbol succ.

Definition at line 331 of file pos1.h.

◆ succ() [2/2]

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

inline

Application of function symbol succ.

Parameters

[in] arg0 A data expression.

Returns: Application of succ to a number of arguments.

Definition at line 355 of file pos1.h.

◆ succ_name()

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

inline

Generate identifier succ.

Returns: Identifier succ.

Definition at line 321 of file pos1.h.

◆ succpos() [1/2]

const function_symbol & mcrl2::data::sort_pos::succpos ( )

inline

Constructor for function symbol @succ_pos.

Returns: Function symbol succpos.

Definition at line 108 of file pos64.h.

◆ succpos() [2/2]

application mcrl2::data::sort_pos::succpos ( const data_expression & arg0 )

inline

Application of function symbol @succ_pos.

Parameters

[in] arg0 A data expression.

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

Definition at line 132 of file pos64.h.

◆ succpos_name()

const core::identifier_string & mcrl2::data::sort_pos::succpos_name ( )

inline

Generate identifier @succ_pos.

Returns: Identifier @succ_pos.

Definition at line 98 of file pos64.h.

◆ times() [1/2]

const function_symbol & mcrl2::data::sort_pos::times ( )

inline

Constructor for function symbol *.

Returns: Function symbol times.

Definition at line 585 of file pos1.h.

◆ times() [2/2]

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

inline

Application of function symbol *.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns: Application of * to a number of arguments.

Definition at line 610 of file pos1.h.

◆ times_name()

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

inline

Generate identifier *.

Returns: Identifier *.

Definition at line 575 of file pos1.h.

◆ times_ordered() [1/2]

const function_symbol & mcrl2::data::sort_pos::times_ordered ( )

inline

Constructor for function symbol @times_ordered.

Returns: Function symbol times_ordered.

Definition at line 964 of file pos64.h.

◆ times_ordered() [2/2]

application mcrl2::data::sort_pos::times_ordered	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @times_ordered.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

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

Definition at line 989 of file pos64.h.

◆ times_ordered_name()

const core::identifier_string & mcrl2::data::sort_pos::times_ordered_name ( )

inline

Generate identifier @times_ordered.

Returns: Identifier @times_ordered.

Definition at line 954 of file pos64.h.

◆ times_overflow() [1/2]

const function_symbol & mcrl2::data::sort_pos::times_overflow ( )

inline

Constructor for function symbol @times_overflow.

Returns: Function symbol times_overflow.

Definition at line 898 of file pos64.h.

◆ times_overflow() [2/2]

application mcrl2::data::sort_pos::times_overflow	(	const data_expression &	arg0,
		const data_expression &	arg1,
		const data_expression &	arg2
	)

inline

Application of function symbol @times_overflow.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

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

Definition at line 924 of file pos64.h.

◆ times_overflow_name()

const core::identifier_string & mcrl2::data::sort_pos::times_overflow_name ( )

inline

Generate identifier @times_overflow.

Returns: Identifier @times_overflow.

Definition at line 888 of file pos64.h.

◆ times_whr_mult_overflow() [1/2]

const function_symbol & mcrl2::data::sort_pos::times_whr_mult_overflow ( )

inline

Constructor for function symbol @times_whr_mult_overflow.

Returns: Function symbol times_whr_mult_overflow.

Definition at line 1028 of file pos64.h.

◆ times_whr_mult_overflow() [2/2]

application mcrl2::data::sort_pos::times_whr_mult_overflow	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @times_whr_mult_overflow.

Parameters

[in]	arg0	A data expression.
[in]	arg1	A data expression.

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

Definition at line 1053 of file pos64.h.

◆ times_whr_mult_overflow_name()

const core::identifier_string & mcrl2::data::sort_pos::times_whr_mult_overflow_name ( )

inline

Generate identifier @times_whr_mult_overflow.

Returns: Identifier @times_whr_mult_overflow.

Definition at line 1018 of file pos64.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ add_with_carry() [1/3]

◆ add_with_carry() [2/3]

◆ add_with_carry() [3/3]

◆ add_with_carry_name()

◆ arg()

◆ arg1()

◆ arg2()

◆ arg3()

◆ auxiliary_plus_pos() [1/2]

◆ auxiliary_plus_pos() [2/2]

◆ auxiliary_plus_pos_name()

◆ c1()

◆ c1_name()

◆ cdub() [1/2]

◆ cdub() [2/2]

◆ cdub_name()

◆ concat_digit() [1/2]

◆ concat_digit() [2/2]

◆ concat_digit_name()

◆ equals_one() [1/2]

◆ equals_one() [2/2]

◆ equals_one_name()

◆ is_add_with_carry_application()

◆ is_add_with_carry_function_symbol()

◆ is_auxiliary_plus_pos_application()

◆ is_auxiliary_plus_pos_function_symbol()

◆ is_c1_function_symbol()

◆ is_cdub_application()

◆ is_cdub_function_symbol()

◆ is_concat_digit_application()

◆ is_concat_digit_function_symbol()

◆ is_equals_one_application()

◆ is_equals_one_function_symbol()

◆ is_maximum_application()

◆ is_maximum_function_symbol()

◆ is_minimum_application()

◆ is_minimum_function_symbol()

◆ is_most_significant_digit_application()

◆ is_most_significant_digit_function_symbol()

◆ is_plus_application()

◆ is_plus_function_symbol()

◆ is_pos()

◆ is_pos_predecessor_application()

◆ is_pos_predecessor_function_symbol()

◆ is_positive_constant()

◆ is_powerlog2_pos_application()

◆ is_powerlog2_pos_function_symbol()

◆ is_succ_application()

◆ is_succ_function_symbol()

◆ is_succpos_application()

◆ is_succpos_function_symbol()

◆ is_times_application()

◆ is_times_function_symbol()

◆ is_times_ordered_application()

◆ is_times_ordered_function_symbol()

◆ is_times_overflow_application()

◆ is_times_overflow_function_symbol()

◆ is_times_whr_mult_overflow_application()

◆ is_times_whr_mult_overflow_function_symbol()

◆ left()

◆ make_add_with_carry() [1/2]

◆ make_add_with_carry() [2/2]

◆ make_auxiliary_plus_pos()

◆ make_cdub()

◆ make_concat_digit()

◆ make_equals_one()

◆ make_maximum()

◆ make_minimum()

◆ make_most_significant_digit()

◆ make_plus()

◆ make_pos_predecessor()

◆ make_powerlog2_pos()

◆ make_succ()

◆ make_succpos()