Namespace for system defined sort int_. 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 &	int_name ()

const basic_sort &	int_ ()
	Constructor for sort expression Int.

bool	is_int (const sort_expression &e)
	Recogniser for sort expression Int.

const core::identifier_string &	cint_name ()
	Generate identifier @cInt.

const function_symbol &	cint ()
	Constructor for function symbol @cInt.

bool	is_cint_function_symbol (const atermpp::aterm &e)
	Recogniser for function @cInt.

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

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

bool	is_cint_application (const atermpp::aterm &e)
	Recogniser for application of @cInt.

const core::identifier_string &	cneg_name ()
	Generate identifier @cNeg.

const function_symbol &	cneg ()
	Constructor for function symbol @cNeg.

bool	is_cneg_function_symbol (const atermpp::aterm &e)
	Recogniser for function @cNeg.

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

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

bool	is_cneg_application (const atermpp::aterm &e)
	Recogniser for application of @cNeg.

function_symbol_vector	int_generate_constructors_code ()
	Give all system defined constructors for int_.

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

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

const core::identifier_string &	nat2int_name ()
	Generate identifier Nat2Int.

const function_symbol &	nat2int ()
	Constructor for function symbol Nat2Int.

bool	is_nat2int_function_symbol (const atermpp::aterm &e)
	Recogniser for function Nat2Int.

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

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

bool	is_nat2int_application (const atermpp::aterm &e)
	Recogniser for application of Nat2Int.

const core::identifier_string &	int2nat_name ()
	Generate identifier Int2Nat.

const function_symbol &	int2nat ()
	Constructor for function symbol Int2Nat.

bool	is_int2nat_function_symbol (const atermpp::aterm &e)
	Recogniser for function Int2Nat.

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

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

bool	is_int2nat_application (const atermpp::aterm &e)
	Recogniser for application of Int2Nat.

const core::identifier_string &	pos2int_name ()
	Generate identifier Pos2Int.

const function_symbol &	pos2int ()
	Constructor for function symbol Pos2Int.

bool	is_pos2int_function_symbol (const atermpp::aterm &e)
	Recogniser for function Pos2Int.

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

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

bool	is_pos2int_application (const atermpp::aterm &e)
	Recogniser for application of Pos2Int.

const core::identifier_string &	int2pos_name ()
	Generate identifier Int2Pos.

const function_symbol &	int2pos ()
	Constructor for function symbol Int2Pos.

bool	is_int2pos_function_symbol (const atermpp::aterm &e)
	Recogniser for function Int2Pos.

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

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

bool	is_int2pos_application (const atermpp::aterm &e)
	Recogniser for application of Int2Pos.

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.

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

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 &	div_name ()
	Generate identifier div.

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

bool	is_div_function_symbol (const atermpp::aterm &e)
	Recogniser for function div.

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

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

bool	is_div_application (const atermpp::aterm &e)
	Recogniser for application of div.

const core::identifier_string &	mod_name ()
	Generate identifier mod.

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

bool	is_mod_function_symbol (const atermpp::aterm &e)
	Recogniser for function mod.

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

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

bool	is_mod_application (const atermpp::aterm &e)
	Recogniser for application of mod.

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.

function_symbol_vector	int_generate_functions_code ()
	Give all system defined mappings for int_.

function_symbol_vector	int_generate_constructors_and_functions_code ()
	Give all system defined mappings and constructors for int_.

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

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

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

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.

data_equation_vector	int_generate_equations_code ()
	Give all system defined equations for int_.

template<typename T >
std::enable_if< std::is_integral< T >::value &&std::is_unsigned< T >::value, data_expression >::type	int_ (T t)
	Constructs expression of type pos from an integral type.

template<typename T >
std::enable_if< std::is_integral< T >::value &&std::is_signed< T >::value, data_expression >::type	int_ (T t)
	Constructs expression of type pos from an integral type.

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

bool	is_integer_constant (const data_expression &n)
	Determines whether n is an integer constant.

std::string	integer_constant_as_string (const data_expression &n)
	Return the string representation of an integer number.

template<class NUMERIC_VALUE >
NUMERIC_VALUE	integer_constant_to_value (const data_expression &n)
	Return the NUMERIC_VALUE representation of an integer number.

Detailed Description

Namespace for system defined sort int_.

Typedef Documentation

◆ implementation_map

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

Definition at line 213 of file int1.h.

Function Documentation

◆ abs() [1/2]

const function_symbol & mcrl2::data::sort_int::abs ( )

inline

Constructor for function symbol abs.

Returns: Function symbol abs.

Definition at line 670 of file int1.h.

◆ abs() [2/2]

application mcrl2::data::sort_int::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 694 of file int1.h.

◆ abs_name()

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

inline

Generate identifier abs.

Returns: Identifier abs.

Definition at line 660 of file int1.h.

◆ arg()

const data_expression & mcrl2::data::sort_int::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 1492 of file int1.h.

◆ cint() [1/2]

const function_symbol & mcrl2::data::sort_int::cint ( )

inline

Constructor for function symbol @cInt.

Returns: Function symbol cint.

Definition at line 80 of file int1.h.

◆ cint() [2/2]

application mcrl2::data::sort_int::cint ( const data_expression & arg0 )

inline

Application of function symbol @cInt.

Parameters

arg0	A data expression.

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

Definition at line 104 of file int1.h.

◆ cint_name()

const core::identifier_string & mcrl2::data::sort_int::cint_name ( )

inline

Generate identifier @cInt.

Returns: Identifier @cInt.

Definition at line 70 of file int1.h.

◆ cneg() [1/2]

const function_symbol & mcrl2::data::sort_int::cneg ( )

inline

Constructor for function symbol @cNeg.

Returns: Function symbol cneg.

Definition at line 142 of file int1.h.

◆ cneg() [2/2]

application mcrl2::data::sort_int::cneg ( const data_expression & arg0 )

inline

Application of function symbol @cNeg.

Parameters

arg0	A data expression.

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

Definition at line 166 of file int1.h.

◆ cneg_name()

const core::identifier_string & mcrl2::data::sort_int::cneg_name ( )

inline

Generate identifier @cNeg.

Returns: Identifier @cNeg.

Definition at line 132 of file int1.h.

◆ div() [1/2]

application mcrl2::data::sort_int::div	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol div.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of div to a number of arguments.

Definition at line 1224 of file int1.h.

◆ div() [2/2]

function_symbol mcrl2::data::sort_int::div	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1184 of file int1.h.

◆ div_name()

const core::identifier_string & mcrl2::data::sort_int::div_name ( )

inline

Generate identifier div.

Returns: Identifier div.

Definition at line 1176 of file int1.h.

◆ exp() [1/2]

application mcrl2::data::sort_int::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 1369 of file int1.h.

◆ exp() [2/2]

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

inline

Definition at line 1325 of file int1.h.

◆ exp_name()

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

inline

Generate identifier exp.

Returns: Identifier exp.

Definition at line 1317 of file int1.h.

◆ int2nat() [1/2]

const function_symbol & mcrl2::data::sort_int::int2nat ( )

inline

Constructor for function symbol Int2Nat.

Returns: Function symbol int2nat.

Definition at line 298 of file int1.h.

◆ int2nat() [2/2]

application mcrl2::data::sort_int::int2nat ( const data_expression & arg0 )

inline

Application of function symbol Int2Nat.

Parameters

arg0	A data expression.

Returns: Application of Int2Nat to a number of arguments.

Definition at line 322 of file int1.h.

◆ int2nat_name()

const core::identifier_string & mcrl2::data::sort_int::int2nat_name ( )

inline

Generate identifier Int2Nat.

Returns: Identifier Int2Nat.

Definition at line 288 of file int1.h.

◆ int2pos() [1/2]

const function_symbol & mcrl2::data::sort_int::int2pos ( )

inline

Constructor for function symbol Int2Pos.

Returns: Function symbol int2pos.

Definition at line 422 of file int1.h.

◆ int2pos() [2/2]

application mcrl2::data::sort_int::int2pos ( const data_expression & arg0 )

inline

Application of function symbol Int2Pos.

Parameters

arg0	A data expression.

Returns: Application of Int2Pos to a number of arguments.

Definition at line 446 of file int1.h.

◆ int2pos_name()

const core::identifier_string & mcrl2::data::sort_int::int2pos_name ( )

inline

Generate identifier Int2Pos.

Returns: Identifier Int2Pos.

Definition at line 412 of file int1.h.

◆ int_() [1/4]

const basic_sort & mcrl2::data::sort_int::int_ ( )

inline

Constructor for sort expression Int.

Returns: Sort expression Int.

Definition at line 47 of file int1.h.

◆ int_() [2/4]

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

inline

Constructs expression of type Int from a string.

Parameters

n A string.

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

Definition at line 690 of file standard_numbers_utility.h.

◆ int_() [3/4]

template<typename T >

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

inline

Constructs expression of type pos from an integral type.

Definition at line 670 of file standard_numbers_utility.h.

◆ int_() [4/4]

template<typename T >

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

inline

Constructs expression of type pos from an integral type.

Definition at line 678 of file standard_numbers_utility.h.

◆ int_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_int::int_cpp_implementable_constructors ( )

inline

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

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

Definition at line 217 of file int1.h.

◆ int_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_int::int_cpp_implementable_mappings ( )

inline

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

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

Definition at line 1481 of file int1.h.

◆ int_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_int::int_generate_constructors_and_functions_code ( )

inline

Give all system defined mappings and constructors for int_.

Returns: All system defined mappings for int_

Definition at line 1431 of file int1.h.

◆ int_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_int::int_generate_constructors_code ( )

inline

Give all system defined constructors for int_.

Returns: All system defined constructors for int_.

Definition at line 193 of file int1.h.

◆ int_generate_equations_code()

data_equation_vector mcrl2::data::sort_int::int_generate_equations_code ( )

inline

Give all system defined equations for int_.

Returns: All system defined equations for sort int_

Definition at line 1525 of file int1.h.

◆ int_generate_functions_code()

function_symbol_vector mcrl2::data::sort_int::int_generate_functions_code ( )

inline

Give all system defined mappings for int_.

Returns: All system defined mappings for int_

Definition at line 1397 of file int1.h.

◆ int_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_int::int_mCRL2_usable_constructors ( )

inline

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

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

Definition at line 204 of file int1.h.

◆ int_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_int::int_mCRL2_usable_mappings ( )

inline

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

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

Definition at line 1444 of file int1.h.

◆ int_name()

const core::identifier_string & mcrl2::data::sort_int::int_name ( )

inline

Definition at line 38 of file int1.h.

◆ integer_constant_as_string()

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

inline

Return the string representation of an integer number.

Parameters

n	A data expression.

Precondition: is_integer_constant(n).

Returns: String representation of n.

Definition at line 714 of file standard_numbers_utility.h.

◆ integer_constant_to_value()

template<class NUMERIC_VALUE >

NUMERIC_VALUE mcrl2::data::sort_int::integer_constant_to_value ( const data_expression & n )

inline

Return the NUMERIC_VALUE representation of an integer number.

Parameters

n	A data expression.

Precondition: is_integer_constant(n).

Returns: NUMERIC_VALUE representation of n.

Definition at line 732 of file standard_numbers_utility.h.

◆ is_abs_application()

bool mcrl2::data::sort_int::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 714 of file int1.h.

◆ is_abs_function_symbol()

bool mcrl2::data::sort_int::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 680 of file int1.h.

◆ is_cint_application()

bool mcrl2::data::sort_int::is_cint_application ( const atermpp::aterm & e )

inline

Recogniser for application of @cInt.

Parameters

e	A data expression.

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

Definition at line 124 of file int1.h.

◆ is_cint_function_symbol()

bool mcrl2::data::sort_int::is_cint_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @cInt.

Parameters

e	A data expression.

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

Definition at line 90 of file int1.h.

◆ is_cneg_application()

bool mcrl2::data::sort_int::is_cneg_application ( const atermpp::aterm & e )

inline

Recogniser for application of @cNeg.

Parameters

e	A data expression.

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

Definition at line 186 of file int1.h.

◆ is_cneg_function_symbol()

bool mcrl2::data::sort_int::is_cneg_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @cNeg.

Parameters

e	A data expression.

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

Definition at line 152 of file int1.h.

◆ is_div_application()

bool mcrl2::data::sort_int::is_div_application ( const atermpp::aterm & e )

inline

Recogniser for application of div.

Parameters

e	A data expression.

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

Definition at line 1245 of file int1.h.

◆ is_div_function_symbol()

bool mcrl2::data::sort_int::is_div_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function div.

Parameters

e	A data expression.

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

Definition at line 1208 of file int1.h.

◆ is_exp_application()

bool mcrl2::data::sort_int::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 1390 of file int1.h.

◆ is_exp_function_symbol()

bool mcrl2::data::sort_int::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 1353 of file int1.h.

◆ is_int()

bool mcrl2::data::sort_int::is_int ( const sort_expression & e )

inline

Recogniser for sort expression Int.

Parameters

e	A sort expression

Returns: true iff e == int_()

Definition at line 57 of file int1.h.

◆ is_int2nat_application()

bool mcrl2::data::sort_int::is_int2nat_application ( const atermpp::aterm & e )

inline

Recogniser for application of Int2Nat.

Parameters

e	A data expression.

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

Definition at line 342 of file int1.h.

◆ is_int2nat_function_symbol()

bool mcrl2::data::sort_int::is_int2nat_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Int2Nat.

Parameters

e	A data expression.

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

Definition at line 308 of file int1.h.

◆ is_int2pos_application()

bool mcrl2::data::sort_int::is_int2pos_application ( const atermpp::aterm & e )

inline

Recogniser for application of Int2Pos.

Parameters

e	A data expression.

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

Definition at line 466 of file int1.h.

◆ is_int2pos_function_symbol()

bool mcrl2::data::sort_int::is_int2pos_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Int2Pos.

Parameters

e	A data expression.

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

Definition at line 432 of file int1.h.

◆ is_integer_constant()

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

inline

Determines whether n is an integer constant.

Parameters

n	A data expression.

Definition at line 701 of file standard_numbers_utility.h.

◆ is_maximum_application()

bool mcrl2::data::sort_int::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 571 of file int1.h.

◆ is_maximum_function_symbol()

bool mcrl2::data::sort_int::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 534 of file int1.h.

◆ is_minimum_application()

bool mcrl2::data::sort_int::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 652 of file int1.h.

◆ is_minimum_function_symbol()

bool mcrl2::data::sort_int::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 615 of file int1.h.

◆ is_minus_application()

bool mcrl2::data::sort_int::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 1087 of file int1.h.

◆ is_minus_function_symbol()

bool mcrl2::data::sort_int::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 1050 of file int1.h.

◆ is_mod_application()

bool mcrl2::data::sort_int::is_mod_application ( const atermpp::aterm & e )

inline

Recogniser for application of mod.

Parameters

e	A data expression.

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

Definition at line 1309 of file int1.h.

◆ is_mod_function_symbol()

bool mcrl2::data::sort_int::is_mod_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function mod.

Parameters

e	A data expression.

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

Definition at line 1272 of file int1.h.

◆ is_nat2int_application()

bool mcrl2::data::sort_int::is_nat2int_application ( const atermpp::aterm & e )

inline

Recogniser for application of Nat2Int.

Parameters

e	A data expression.

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

Definition at line 280 of file int1.h.

◆ is_nat2int_function_symbol()

bool mcrl2::data::sort_int::is_nat2int_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Nat2Int.

Parameters

e	A data expression.

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

Definition at line 246 of file int1.h.

◆ is_negate_application()

bool mcrl2::data::sort_int::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 776 of file int1.h.

◆ is_negate_function_symbol()

bool mcrl2::data::sort_int::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 741 of file int1.h.

◆ is_plus_application()

bool mcrl2::data::sort_int::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 1023 of file int1.h.

◆ is_plus_function_symbol()

bool mcrl2::data::sort_int::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 986 of file int1.h.

◆ is_pos2int_application()

bool mcrl2::data::sort_int::is_pos2int_application ( const atermpp::aterm & e )

inline

Recogniser for application of Pos2Int.

Parameters

e	A data expression.

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

Definition at line 404 of file int1.h.

◆ is_pos2int_function_symbol()

bool mcrl2::data::sort_int::is_pos2int_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Pos2Int.

Parameters

e	A data expression.

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

Definition at line 370 of file int1.h.

◆ is_pred_application()

bool mcrl2::data::sort_int::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 934 of file int1.h.

◆ is_pred_function_symbol()

bool mcrl2::data::sort_int::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 899 of file int1.h.

◆ is_succ_application()

bool mcrl2::data::sort_int::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 855 of file int1.h.

◆ is_succ_function_symbol()

bool mcrl2::data::sort_int::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 820 of file int1.h.

◆ is_times_application()

bool mcrl2::data::sort_int::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 1168 of file int1.h.

◆ is_times_function_symbol()

bool mcrl2::data::sort_int::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 1131 of file int1.h.

◆ left()

const data_expression & mcrl2::data::sort_int::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 1504 of file int1.h.

◆ make_abs()

void mcrl2::data::sort_int::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 704 of file int1.h.

◆ make_cint()

void mcrl2::data::sort_int::make_cint	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @cInt.

Parameters

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

Definition at line 114 of file int1.h.

◆ make_cneg()

void mcrl2::data::sort_int::make_cneg	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @cNeg.

Parameters

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

Definition at line 176 of file int1.h.

◆ make_div()

void mcrl2::data::sort_int::make_div	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol div.

Parameters

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

Definition at line 1235 of file int1.h.

◆ make_exp()

void mcrl2::data::sort_int::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 1380 of file int1.h.

◆ make_int2nat()

void mcrl2::data::sort_int::make_int2nat	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Int2Nat.

Parameters

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

Definition at line 332 of file int1.h.

◆ make_int2pos()

void mcrl2::data::sort_int::make_int2pos	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Int2Pos.

Parameters

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

Definition at line 456 of file int1.h.

◆ make_maximum()

void mcrl2::data::sort_int::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 561 of file int1.h.

◆ make_minimum()

void mcrl2::data::sort_int::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 642 of file int1.h.

◆ make_minus()

void mcrl2::data::sort_int::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 1077 of file int1.h.

◆ make_mod()

void mcrl2::data::sort_int::make_mod	(	data_expression &	result,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol mod.

Parameters

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

Definition at line 1299 of file int1.h.

◆ make_nat2int()

void mcrl2::data::sort_int::make_nat2int	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Nat2Int.

Parameters

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

Definition at line 270 of file int1.h.

◆ make_negate()

void mcrl2::data::sort_int::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 766 of file int1.h.

◆ make_plus()

void mcrl2::data::sort_int::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 1013 of file int1.h.

◆ make_pos2int()

void mcrl2::data::sort_int::make_pos2int	(	data_expression &	result,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Pos2Int.

Parameters

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

Definition at line 394 of file int1.h.

◆ make_pred()

void mcrl2::data::sort_int::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 924 of file int1.h.

◆ make_succ()

void mcrl2::data::sort_int::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 845 of file int1.h.

◆ make_times()

void mcrl2::data::sort_int::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 1158 of file int1.h.

◆ maximum() [1/2]

application mcrl2::data::sort_int::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 550 of file int1.h.

◆ maximum() [2/2]

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

inline

Definition at line 482 of file int1.h.

◆ maximum_name()

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

inline

Generate identifier max.

Returns: Identifier max.

Definition at line 474 of file int1.h.

◆ minimum() [1/2]

application mcrl2::data::sort_int::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 631 of file int1.h.

◆ minimum() [2/2]

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

inline

Definition at line 587 of file int1.h.

◆ minimum_name()

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

inline

Generate identifier min.

Returns: Identifier min.

Definition at line 579 of file int1.h.

◆ minus() [1/2]

application mcrl2::data::sort_int::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 1066 of file int1.h.

◆ minus() [2/2]

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

inline

Definition at line 1039 of file int1.h.

◆ minus_name()

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

inline

Generate identifier -.

Returns: Identifier -.

Definition at line 1031 of file int1.h.

◆ mod() [1/2]

application mcrl2::data::sort_int::mod	(	const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol mod.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns: Application of mod to a number of arguments.

Definition at line 1288 of file int1.h.

◆ mod() [2/2]

function_symbol mcrl2::data::sort_int::mod	(	const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 1261 of file int1.h.

◆ mod_name()

const core::identifier_string & mcrl2::data::sort_int::mod_name ( )

inline

Generate identifier mod.

Returns: Identifier mod.

Definition at line 1253 of file int1.h.

◆ nat2int() [1/2]

const function_symbol & mcrl2::data::sort_int::nat2int ( )

inline

Constructor for function symbol Nat2Int.

Returns: Function symbol nat2int.

Definition at line 236 of file int1.h.

◆ nat2int() [2/2]

application mcrl2::data::sort_int::nat2int ( const data_expression & arg0 )

inline

Application of function symbol Nat2Int.

Parameters

arg0	A data expression.

Returns: Application of Nat2Int to a number of arguments.

Definition at line 260 of file int1.h.

◆ nat2int_name()

const core::identifier_string & mcrl2::data::sort_int::nat2int_name ( )

inline

Generate identifier Nat2Int.

Returns: Identifier Nat2Int.

Definition at line 226 of file int1.h.

◆ negate() [1/2]

application mcrl2::data::sort_int::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 756 of file int1.h.

◆ negate() [2/2]

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

inline

Definition at line 730 of file int1.h.

◆ negate_name()

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

inline

Generate identifier -.

Returns: Identifier -.

Definition at line 722 of file int1.h.

◆ plus() [1/2]

application mcrl2::data::sort_int::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 1002 of file int1.h.

◆ plus() [2/2]

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

inline

Definition at line 950 of file int1.h.

◆ plus_name()

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

inline

Generate identifier +.

Returns: Identifier +.

Definition at line 942 of file int1.h.

◆ pos2int() [1/2]

const function_symbol & mcrl2::data::sort_int::pos2int ( )

inline

Constructor for function symbol Pos2Int.

Returns: Function symbol pos2int.

Definition at line 360 of file int1.h.

◆ pos2int() [2/2]

application mcrl2::data::sort_int::pos2int ( const data_expression & arg0 )

inline

Application of function symbol Pos2Int.

Parameters

arg0	A data expression.

Returns: Application of Pos2Int to a number of arguments.

Definition at line 384 of file int1.h.

◆ pos2int_name()

const core::identifier_string & mcrl2::data::sort_int::pos2int_name ( )

inline

Generate identifier Pos2Int.

Returns: Identifier Pos2Int.

Definition at line 350 of file int1.h.

◆ pred() [1/2]

application mcrl2::data::sort_int::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 914 of file int1.h.

◆ pred() [2/2]

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

inline

Definition at line 871 of file int1.h.

◆ pred_name()

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

inline

Generate identifier pred.

Returns: Identifier pred.

Definition at line 863 of file int1.h.

◆ right()

const data_expression & mcrl2::data::sort_int::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 1516 of file int1.h.

◆ succ() [1/2]

application mcrl2::data::sort_int::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 835 of file int1.h.

◆ succ() [2/2]

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

inline

Definition at line 792 of file int1.h.

◆ succ_name()

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

inline

Generate identifier succ.

Returns: Identifier succ.

Definition at line 784 of file int1.h.

◆ times() [1/2]

application mcrl2::data::sort_int::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 1147 of file int1.h.

◆ times() [2/2]

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

inline

Definition at line 1103 of file int1.h.

◆ times_name()

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

inline

Generate identifier *.

Returns: Identifier *.

Definition at line 1095 of file int1.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ abs() [1/2]

◆ abs() [2/2]

◆ abs_name()

◆ arg()

◆ cint() [1/2]

◆ cint() [2/2]

◆ cint_name()

◆ cneg() [1/2]

◆ cneg() [2/2]

◆ cneg_name()

◆ div() [1/2]

◆ div() [2/2]

◆ div_name()

◆ exp() [1/2]

◆ exp() [2/2]

◆ exp_name()

◆ int2nat() [1/2]

◆ int2nat() [2/2]

◆ int2nat_name()

◆ int2pos() [1/2]

◆ int2pos() [2/2]

◆ int2pos_name()

◆ int_() [1/4]

◆ int_() [2/4]

◆ int_() [3/4]

◆ int_() [4/4]

◆ int_cpp_implementable_constructors()

◆ int_cpp_implementable_mappings()

◆ int_generate_constructors_and_functions_code()

◆ int_generate_constructors_code()

◆ int_generate_equations_code()

◆ int_generate_functions_code()

◆ int_mCRL2_usable_constructors()

◆ int_mCRL2_usable_mappings()

◆ int_name()

◆ integer_constant_as_string()

◆ integer_constant_to_value()

◆ is_abs_application()

◆ is_abs_function_symbol()

◆ is_cint_application()

◆ is_cint_function_symbol()

◆ is_cneg_application()

◆ is_cneg_function_symbol()

◆ is_div_application()

◆ is_div_function_symbol()

◆ is_exp_application()

◆ is_exp_function_symbol()

◆ is_int()

◆ is_int2nat_application()

◆ is_int2nat_function_symbol()

◆ is_int2pos_application()

◆ is_int2pos_function_symbol()

◆ is_integer_constant()

◆ is_maximum_application()

◆ is_maximum_function_symbol()

◆ is_minimum_application()

◆ is_minimum_function_symbol()

◆ is_minus_application()

◆ is_minus_function_symbol()

◆ is_mod_application()

◆ is_mod_function_symbol()

◆ is_nat2int_application()

◆ is_nat2int_function_symbol()

◆ is_negate_application()

◆ is_negate_function_symbol()

◆ is_plus_application()

◆ is_plus_function_symbol()

◆ is_pos2int_application()

◆ is_pos2int_function_symbol()

◆ is_pred_application()

◆ is_pred_function_symbol()

◆ is_succ_application()

◆ is_succ_function_symbol()

◆ is_times_application()