mcrl2::data::sort_machine_word Namespace Reference

Namespace for system defined sort machine_word. More...

Namespaces
namespace	detail

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

Functions
void	zero_word_manual_implementation (data_expression &result)
	The machine number representing 0.
void	one_word_manual_implementation (data_expression &result)
	The machine number representing 1.
void	two_word_manual_implementation (data_expression &result)
	The machine number representing 2.
void	three_word_manual_implementation (data_expression &result)
	The machine number representing 3.
void	four_word_manual_implementation (data_expression &result)
	The machine number representing 4.
void	max_word_manual_implementation (data_expression &result)
	The largest representable machine number.
void	equals_zero_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is equal to 0.
void	not_equals_zero_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is not equal to 0.
void	equals_one_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is equal to 1.
void	equals_max_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is equal to the largest 64 bit number.
void	succ_word_manual_implementation (data_expression &result, const data_expression &e)
	The successor function on a machine numbers, that wraps around.
void	equal_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The equality function on two machine words.
void	not_equal_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The non equality function on two machine words.
void	less_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The less than function on two machine words.
void	less_equal_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The less than or equal function on two machine words.
void	greater_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The greater than function on two machine words.
void	greater_equal_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The greater than or equal function on two machine words.
void	add_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The result of adding two words modulo the maximal representable machine word plus 1.
void	add_with_carry_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The result of adding two words plus 1 modulo the maximal representable machine word plus 1.
void	add_overflow_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	An indication whether an overflow occurs when e1 and e2 are added.
void	add_with_carry_overflow_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	An indication whether an overflow occurs when e1 and e2 are added.
void	times_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The result of multiplying two words modulo the maximal representable machine word plus 1.
void	times_with_carry_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3)
	The result of multiplying two words and adding the third modulo the maximal representable machine word plus 1.
void	times_overflow_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The result of multiplying two words divided by the maximal representable machine word plus 1.
void	times_with_carry_overflow_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3)
	The result of multiplying two words and adding a third divided by the maximal representable machine word plus 1.
void	minus_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The result of subtracting two words modulo the maximal representable machine word plus 1.
void	monus_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The result of subtracting two words. If the result is negative 0 is returned.
void	div_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	Calculates the division of the first word by the second.
void	mod_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	Calculates e1 modulo e2.
void	sqrt_word_manual_implementation (data_expression &result, const data_expression &e)
	The square root of e, rounded down to a machine word.
void	div_doubleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3)
	Calculates (base*e1 + e2) div e3.
void	div_double_doubleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4)
	Calculates (base*e1 + e2) div (base*e3 + e4).
void	div_triple_doubleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5)
	Calculates (base*(base*e1 + e2)+e3) div (base*e4 + e5).
void	mod_double_doubleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4)
	Calculates (base*e1 + e2) mod (base*e3 + e4).
void	sqrt_doubleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The square root of base*e1+e2 rounded down.
void	mod_doubleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3)
	Calculates (base*e1 + e2) mod e3. The result fits in one word.
void	sqrt_tripleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3)
	Calculates the least significant word of the square root of base*(base*e1+e2)+e3.
void	sqrt_tripleword_overflow_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3)
	Calculates the most significant word of the square root of base*(base*e1+e2)+e3.
void	sqrt_quadrupleword_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4)
	Calculates the least significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.
void	sqrt_quadrupleword_overflow_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4)
	Calculates the most significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.
void	pred_word_manual_implementation (data_expression &result, const data_expression &e)
	The predecessor function on a machine numbers, that wraps around.
void	rightmost_bit_manual_implementation (data_expression &result, const data_expression &e)
	The right most bit of a machine number.
void	shift_right_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The machine word shifted one position to the right.
const core::identifier_string &	machine_word_name ()
const basic_sort &	machine_word ()
	Constructor for sort expression @word.
bool	is_machine_word (const sort_expression &e)
	Recogniser for sort expression @word.
const core::identifier_string &	zero_word_name ()
	Generate identifier @zero_word.
const function_symbol &	zero_word ()
	Constructor for function symbol @zero_word.
bool	is_zero_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @zero_word.
void	zero_word_application (data_expression &result, const data_expression &a)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	succ_word_name ()
	Generate identifier @succ_word.
const function_symbol &	succ_word ()
	Constructor for function symbol @succ_word.
bool	is_succ_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @succ_word.
application	succ_word (const data_expression &arg0)
	Application of function symbol @succ_word.
void	make_succ_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @succ_word.
bool	is_succ_word_application (const atermpp::aterm &e)
	Recogniser for application of @succ_word.
void	succ_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
function_symbol_vector	machine_word_generate_constructors_code ()
	Give all system defined constructors for machine_word.
function_symbol_vector	machine_word_mCRL2_usable_constructors ()
	Give all defined constructors which can be used in mCRL2 specs for machine_word.
implementation_map	machine_word_cpp_implementable_constructors ()
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for machine_word.
const core::identifier_string &	one_word_name ()
	Generate identifier @one_word.
const function_symbol &	one_word ()
	Constructor for function symbol @one_word.
bool	is_one_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @one_word.
void	one_word_application (data_expression &result, const data_expression &a)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	two_word_name ()
	Generate identifier @two_word.
const function_symbol &	two_word ()
	Constructor for function symbol @two_word.
bool	is_two_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @two_word.
void	two_word_application (data_expression &result, const data_expression &a)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	three_word_name ()
	Generate identifier @three_word.
const function_symbol &	three_word ()
	Constructor for function symbol @three_word.
bool	is_three_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @three_word.
void	three_word_application (data_expression &result, const data_expression &a)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	four_word_name ()
	Generate identifier @four_word.
const function_symbol &	four_word ()
	Constructor for function symbol @four_word.
bool	is_four_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @four_word.
void	four_word_application (data_expression &result, const data_expression &a)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	max_word_name ()
	Generate identifier @max_word.
const function_symbol &	max_word ()
	Constructor for function symbol @max_word.
bool	is_max_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @max_word.
void	max_word_application (data_expression &result, const data_expression &a)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	equals_zero_word_name ()
	Generate identifier @equals_zero_word.
const function_symbol &	equals_zero_word ()
	Constructor for function symbol @equals_zero_word.
bool	is_equals_zero_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @equals_zero_word.
application	equals_zero_word (const data_expression &arg0)
	Application of function symbol @equals_zero_word.
void	make_equals_zero_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @equals_zero_word.
bool	is_equals_zero_word_application (const atermpp::aterm &e)
	Recogniser for application of @equals_zero_word.
void	equals_zero_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	not_equals_zero_word_name ()
	Generate identifier @not_equals_zero_word.
const function_symbol &	not_equals_zero_word ()
	Constructor for function symbol @not_equals_zero_word.
bool	is_not_equals_zero_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @not_equals_zero_word.
application	not_equals_zero_word (const data_expression &arg0)
	Application of function symbol @not_equals_zero_word.
void	make_not_equals_zero_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @not_equals_zero_word.
bool	is_not_equals_zero_word_application (const atermpp::aterm &e)
	Recogniser for application of @not_equals_zero_word.
void	not_equals_zero_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	equals_one_word_name ()
	Generate identifier @equals_one_word.
const function_symbol &	equals_one_word ()
	Constructor for function symbol @equals_one_word.
bool	is_equals_one_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @equals_one_word.
application	equals_one_word (const data_expression &arg0)
	Application of function symbol @equals_one_word.
void	make_equals_one_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @equals_one_word.
bool	is_equals_one_word_application (const atermpp::aterm &e)
	Recogniser for application of @equals_one_word.
void	equals_one_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	equals_max_word_name ()
	Generate identifier @equals_max_word.
const function_symbol &	equals_max_word ()
	Constructor for function symbol @equals_max_word.
bool	is_equals_max_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @equals_max_word.
application	equals_max_word (const data_expression &arg0)
	Application of function symbol @equals_max_word.
void	make_equals_max_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @equals_max_word.
bool	is_equals_max_word_application (const atermpp::aterm &e)
	Recogniser for application of @equals_max_word.
void	equals_max_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	add_word_name ()
	Generate identifier @add_word.
const function_symbol &	add_word ()
	Constructor for function symbol @add_word.
bool	is_add_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @add_word.
application	add_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @add_word.
void	make_add_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @add_word.
bool	is_add_word_application (const atermpp::aterm &e)
	Recogniser for application of @add_word.
void	add_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	add_with_carry_word_name ()
	Generate identifier @add_with_carry_word.
const function_symbol &	add_with_carry_word ()
	Constructor for function symbol @add_with_carry_word.
bool	is_add_with_carry_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @add_with_carry_word.
application	add_with_carry_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @add_with_carry_word.
void	make_add_with_carry_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @add_with_carry_word.
bool	is_add_with_carry_word_application (const atermpp::aterm &e)
	Recogniser for application of @add_with_carry_word.
void	add_with_carry_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	add_overflow_word_name ()
	Generate identifier @add_overflow_word.
const function_symbol &	add_overflow_word ()
	Constructor for function symbol @add_overflow_word.
bool	is_add_overflow_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @add_overflow_word.
application	add_overflow_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @add_overflow_word.
void	make_add_overflow_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @add_overflow_word.
bool	is_add_overflow_word_application (const atermpp::aterm &e)
	Recogniser for application of @add_overflow_word.
void	add_overflow_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	add_with_carry_overflow_word_name ()
	Generate identifier @add_with_carry_overflow_word.
const function_symbol &	add_with_carry_overflow_word ()
	Constructor for function symbol @add_with_carry_overflow_word.
bool	is_add_with_carry_overflow_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @add_with_carry_overflow_word.
application	add_with_carry_overflow_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @add_with_carry_overflow_word.
void	make_add_with_carry_overflow_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @add_with_carry_overflow_word.
bool	is_add_with_carry_overflow_word_application (const atermpp::aterm &e)
	Recogniser for application of @add_with_carry_overflow_word.
void	add_with_carry_overflow_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	times_word_name ()
	Generate identifier @times_word.
const function_symbol &	times_word ()
	Constructor for function symbol @times_word.
bool	is_times_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_word.
application	times_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @times_word.
void	make_times_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @times_word.
bool	is_times_word_application (const atermpp::aterm &e)
	Recogniser for application of @times_word.
void	times_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	times_with_carry_word_name ()
	Generate identifier @times_with_carry_word.
const function_symbol &	times_with_carry_word ()
	Constructor for function symbol @times_with_carry_word.
bool	is_times_with_carry_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_with_carry_word.
application	times_with_carry_word (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @times_with_carry_word.
void	make_times_with_carry_word (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @times_with_carry_word.
bool	is_times_with_carry_word_application (const atermpp::aterm &e)
	Recogniser for application of @times_with_carry_word.
void	times_with_carry_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	times_overflow_word_name ()
	Generate identifier @times_overflow_word.
const function_symbol &	times_overflow_word ()
	Constructor for function symbol @times_overflow_word.
bool	is_times_overflow_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_overflow_word.
application	times_overflow_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @times_overflow_word.
void	make_times_overflow_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @times_overflow_word.
bool	is_times_overflow_word_application (const atermpp::aterm &e)
	Recogniser for application of @times_overflow_word.
void	times_overflow_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	times_with_carry_overflow_word_name ()
	Generate identifier @times_with_carry_overflow_word.
const function_symbol &	times_with_carry_overflow_word ()
	Constructor for function symbol @times_with_carry_overflow_word.
bool	is_times_with_carry_overflow_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @times_with_carry_overflow_word.
application	times_with_carry_overflow_word (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @times_with_carry_overflow_word.
void	make_times_with_carry_overflow_word (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @times_with_carry_overflow_word.
bool	is_times_with_carry_overflow_word_application (const atermpp::aterm &e)
	Recogniser for application of @times_with_carry_overflow_word.
void	times_with_carry_overflow_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	minus_word_name ()
	Generate identifier @minus_word.
const function_symbol &	minus_word ()
	Constructor for function symbol @minus_word.
bool	is_minus_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @minus_word.
application	minus_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @minus_word.
void	make_minus_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @minus_word.
bool	is_minus_word_application (const atermpp::aterm &e)
	Recogniser for application of @minus_word.
void	minus_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	monus_word_name ()
	Generate identifier @monus_word.
const function_symbol &	monus_word ()
	Constructor for function symbol @monus_word.
bool	is_monus_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @monus_word.
application	monus_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @monus_word.
void	make_monus_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @monus_word.
bool	is_monus_word_application (const atermpp::aterm &e)
	Recogniser for application of @monus_word.
void	monus_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	div_word_name ()
	Generate identifier @div_word.
const function_symbol &	div_word ()
	Constructor for function symbol @div_word.
bool	is_div_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @div_word.
application	div_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @div_word.
void	make_div_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @div_word.
bool	is_div_word_application (const atermpp::aterm &e)
	Recogniser for application of @div_word.
void	div_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	mod_word_name ()
	Generate identifier @mod_word.
const function_symbol &	mod_word ()
	Constructor for function symbol @mod_word.
bool	is_mod_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @mod_word.
application	mod_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @mod_word.
void	make_mod_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @mod_word.
bool	is_mod_word_application (const atermpp::aterm &e)
	Recogniser for application of @mod_word.
void	mod_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	sqrt_word_name ()
	Generate identifier @sqrt_word.
const function_symbol &	sqrt_word ()
	Constructor for function symbol @sqrt_word.
bool	is_sqrt_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @sqrt_word.
application	sqrt_word (const data_expression &arg0)
	Application of function symbol @sqrt_word.
void	make_sqrt_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @sqrt_word.
bool	is_sqrt_word_application (const atermpp::aterm &e)
	Recogniser for application of @sqrt_word.
void	sqrt_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	div_doubleword_name ()
	Generate identifier @div_doubleword.
const function_symbol &	div_doubleword ()
	Constructor for function symbol @div_doubleword.
bool	is_div_doubleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @div_doubleword.
application	div_doubleword (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @div_doubleword.
void	make_div_doubleword (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @div_doubleword.
bool	is_div_doubleword_application (const atermpp::aterm &e)
	Recogniser for application of @div_doubleword.
void	div_doubleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	div_double_doubleword_name ()
	Generate identifier @div_double_doubleword.
const function_symbol &	div_double_doubleword ()
	Constructor for function symbol @div_double_doubleword.
bool	is_div_double_doubleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @div_double_doubleword.
application	div_double_doubleword (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @div_double_doubleword.
void	make_div_double_doubleword (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Make an application of function symbol @div_double_doubleword.
bool	is_div_double_doubleword_application (const atermpp::aterm &e)
	Recogniser for application of @div_double_doubleword.
void	div_double_doubleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	div_triple_doubleword_name ()
	Generate identifier @div_triple_doubleword.
const function_symbol &	div_triple_doubleword ()
	Constructor for function symbol @div_triple_doubleword.
bool	is_div_triple_doubleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @div_triple_doubleword.
application	div_triple_doubleword (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
	Application of function symbol @div_triple_doubleword.
void	make_div_triple_doubleword (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)
	Make an application of function symbol @div_triple_doubleword.
bool	is_div_triple_doubleword_application (const atermpp::aterm &e)
	Recogniser for application of @div_triple_doubleword.
void	div_triple_doubleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	mod_doubleword_name ()
	Generate identifier @mod_doubleword.
const function_symbol &	mod_doubleword ()
	Constructor for function symbol @mod_doubleword.
bool	is_mod_doubleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @mod_doubleword.
application	mod_doubleword (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @mod_doubleword.
void	make_mod_doubleword (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @mod_doubleword.
bool	is_mod_doubleword_application (const atermpp::aterm &e)
	Recogniser for application of @mod_doubleword.
void	mod_doubleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	sqrt_doubleword_name ()
	Generate identifier @sqrt_doubleword.
const function_symbol &	sqrt_doubleword ()
	Constructor for function symbol @sqrt_doubleword.
bool	is_sqrt_doubleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @sqrt_doubleword.
application	sqrt_doubleword (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @sqrt_doubleword.
void	make_sqrt_doubleword (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @sqrt_doubleword.
bool	is_sqrt_doubleword_application (const atermpp::aterm &e)
	Recogniser for application of @sqrt_doubleword.
void	sqrt_doubleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	sqrt_tripleword_name ()
	Generate identifier @sqrt_tripleword.
const function_symbol &	sqrt_tripleword ()
	Constructor for function symbol @sqrt_tripleword.
bool	is_sqrt_tripleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @sqrt_tripleword.
application	sqrt_tripleword (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @sqrt_tripleword.
void	make_sqrt_tripleword (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @sqrt_tripleword.
bool	is_sqrt_tripleword_application (const atermpp::aterm &e)
	Recogniser for application of @sqrt_tripleword.
void	sqrt_tripleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	sqrt_tripleword_overflow_name ()
	Generate identifier @sqrt_tripleword_overflow.
const function_symbol &	sqrt_tripleword_overflow ()
	Constructor for function symbol @sqrt_tripleword_overflow.
bool	is_sqrt_tripleword_overflow_function_symbol (const atermpp::aterm &e)
	Recogniser for function @sqrt_tripleword_overflow.
application	sqrt_tripleword_overflow (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @sqrt_tripleword_overflow.
void	make_sqrt_tripleword_overflow (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @sqrt_tripleword_overflow.
bool	is_sqrt_tripleword_overflow_application (const atermpp::aterm &e)
	Recogniser for application of @sqrt_tripleword_overflow.
void	sqrt_tripleword_overflow_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	sqrt_quadrupleword_name ()
	Generate identifier @sqrt_quadrupleword.
const function_symbol &	sqrt_quadrupleword ()
	Constructor for function symbol @sqrt_quadrupleword.
bool	is_sqrt_quadrupleword_function_symbol (const atermpp::aterm &e)
	Recogniser for function @sqrt_quadrupleword.
application	sqrt_quadrupleword (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @sqrt_quadrupleword.
void	make_sqrt_quadrupleword (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Make an application of function symbol @sqrt_quadrupleword.
bool	is_sqrt_quadrupleword_application (const atermpp::aterm &e)
	Recogniser for application of @sqrt_quadrupleword.
void	sqrt_quadrupleword_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	sqrt_quadrupleword_overflow_name ()
	Generate identifier @sqrt_quadrupleword_overflow.
const function_symbol &	sqrt_quadrupleword_overflow ()
	Constructor for function symbol @sqrt_quadrupleword_overflow.
bool	is_sqrt_quadrupleword_overflow_function_symbol (const atermpp::aterm &e)
	Recogniser for function @sqrt_quadrupleword_overflow.
application	sqrt_quadrupleword_overflow (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @sqrt_quadrupleword_overflow.
void	make_sqrt_quadrupleword_overflow (data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Make an application of function symbol @sqrt_quadrupleword_overflow.
bool	is_sqrt_quadrupleword_overflow_application (const atermpp::aterm &e)
	Recogniser for application of @sqrt_quadrupleword_overflow.
void	sqrt_quadrupleword_overflow_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	pred_word_name ()
	Generate identifier @pred_word.
const function_symbol &	pred_word ()
	Constructor for function symbol @pred_word.
bool	is_pred_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @pred_word.
application	pred_word (const data_expression &arg0)
	Application of function symbol @pred_word.
void	make_pred_word (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @pred_word.
bool	is_pred_word_application (const atermpp::aterm &e)
	Recogniser for application of @pred_word.
void	pred_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	equal_word_name ()
	Generate identifier @equal.
const function_symbol &	equal_word ()
	Constructor for function symbol @equal.
bool	is_equal_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @equal.
application	equal_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @equal.
void	make_equal_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @equal.
bool	is_equal_word_application (const atermpp::aterm &e)
	Recogniser for application of @equal.
void	equal_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	not_equal_word_name ()
	Generate identifier @not_equal.
const function_symbol &	not_equal_word ()
	Constructor for function symbol @not_equal.
bool	is_not_equal_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @not_equal.
application	not_equal_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @not_equal.
void	make_not_equal_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @not_equal.
bool	is_not_equal_word_application (const atermpp::aterm &e)
	Recogniser for application of @not_equal.
void	not_equal_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	less_word_name ()
	Generate identifier @less.
const function_symbol &	less_word ()
	Constructor for function symbol @less.
bool	is_less_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @less.
application	less_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @less.
void	make_less_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @less.
bool	is_less_word_application (const atermpp::aterm &e)
	Recogniser for application of @less.
void	less_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	less_equal_word_name ()
	Generate identifier @less_equal.
const function_symbol &	less_equal_word ()
	Constructor for function symbol @less_equal.
bool	is_less_equal_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @less_equal.
application	less_equal_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @less_equal.
void	make_less_equal_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @less_equal.
bool	is_less_equal_word_application (const atermpp::aterm &e)
	Recogniser for application of @less_equal.
void	less_equal_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	greater_word_name ()
	Generate identifier @greater.
const function_symbol &	greater_word ()
	Constructor for function symbol @greater.
bool	is_greater_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @greater.
application	greater_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @greater.
void	make_greater_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @greater.
bool	is_greater_word_application (const atermpp::aterm &e)
	Recogniser for application of @greater.
void	greater_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	greater_equal_word_name ()
	Generate identifier @greater_equal.
const function_symbol &	greater_equal_word ()
	Constructor for function symbol @greater_equal.
bool	is_greater_equal_word_function_symbol (const atermpp::aterm &e)
	Recogniser for function @greater_equal.
application	greater_equal_word (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @greater_equal.
void	make_greater_equal_word (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @greater_equal.
bool	is_greater_equal_word_application (const atermpp::aterm &e)
	Recogniser for application of @greater_equal.
void	greater_equal_word_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	rightmost_bit_name ()
	Generate identifier @rightmost_bit.
const function_symbol &	rightmost_bit ()
	Constructor for function symbol @rightmost_bit.
bool	is_rightmost_bit_function_symbol (const atermpp::aterm &e)
	Recogniser for function @rightmost_bit.
application	rightmost_bit (const data_expression &arg0)
	Application of function symbol @rightmost_bit.
void	make_rightmost_bit (data_expression &result, const data_expression &arg0)
	Make an application of function symbol @rightmost_bit.
bool	is_rightmost_bit_application (const atermpp::aterm &e)
	Recogniser for application of @rightmost_bit.
void	rightmost_bit_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
const core::identifier_string &	shift_right_name ()
	Generate identifier @shift_right.
const function_symbol &	shift_right ()
	Constructor for function symbol @shift_right.
bool	is_shift_right_function_symbol (const atermpp::aterm &e)
	Recogniser for function @shift_right.
application	shift_right (const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @shift_right.
void	make_shift_right (data_expression &result, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @shift_right.
bool	is_shift_right_application (const atermpp::aterm &e)
	Recogniser for application of @shift_right.
void	shift_right_application (data_expression &result, const data_expression &a1)
	Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
function_symbol_vector	machine_word_generate_functions_code ()
	Give all system defined mappings for machine_word.
function_symbol_vector	machine_word_generate_constructors_and_functions_code ()
	Give all system defined mappings and constructors for machine_word.
function_symbol_vector	machine_word_mCRL2_usable_mappings ()
	Give all system defined mappings that can be used in mCRL2 specs for machine_word.
implementation_map	machine_word_cpp_implementable_mappings ()
	Give all system defined mappings that are to be implemented in C++ code for machine_word.
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.
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.
const data_expression &	arg4 (const data_expression &e)
	Function for projecting out argument. arg4 from an application.
const data_expression &	arg5 (const data_expression &e)
	Function for projecting out argument. arg5 from an application.
data_equation_vector	machine_word_generate_equations_code ()
	Give all system defined equations for machine_word.

Detailed Description

Namespace for system defined sort machine_word.

Typedef Documentation

implementation_map

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

Definition at line 216 of file machine_word.h.

Function Documentation

add_overflow_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::add_overflow_word ( )

inline

Constructor for function symbol @add_overflow_word.

Returns

Function symbol add_overflow_word.

Definition at line 974 of file machine_word.h.

add_overflow_word() [2/2]

application mcrl2::data::sort_machine_word::add_overflow_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @add_overflow_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @add_overflow_word to a number of arguments.

Definition at line 999 of file machine_word.h.

add_overflow_word_application()

void mcrl2::data::sort_machine_word::add_overflow_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1036 of file machine_word.h.

add_overflow_word_manual_implementation()

void mcrl2::data::sort_machine_word::add_overflow_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

An indication whether an overflow occurs when e1 and e2 are added.

The data expression of an application of the function symbol @add_overflow_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

If e1+e2 is larger than a machine word, then true, else false.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @add_overflow_word to a number of arguments.

Definition at line 452 of file machine_word.h.

add_overflow_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::add_overflow_word_name ( )

inline

Generate identifier @add_overflow_word.

Returns

Identifier @add_overflow_word.

Definition at line 964 of file machine_word.h.

add_with_carry_overflow_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::add_with_carry_overflow_word ( )

inline

Constructor for function symbol @add_with_carry_overflow_word.

Returns

Function symbol add_with_carry_overflow_word.

Definition at line 1058 of file machine_word.h.

add_with_carry_overflow_word() [2/2]

application mcrl2::data::sort_machine_word::add_with_carry_overflow_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @add_with_carry_overflow_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @add_with_carry_overflow_word to a number of arguments.

Definition at line 1083 of file machine_word.h.

add_with_carry_overflow_word_application()

void mcrl2::data::sort_machine_word::add_with_carry_overflow_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1120 of file machine_word.h.

add_with_carry_overflow_word_manual_implementation()

void mcrl2::data::sort_machine_word::add_with_carry_overflow_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

An indication whether an overflow occurs when e1 and e2 are added.

The data expression of an application of the function symbol @add_with_carry_overflow_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

If e1+e2+1 is larger than a machine word, then true, else false.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @add_with_carry_overflow_word to a number of arguments.

Definition at line 470 of file machine_word.h.

add_with_carry_overflow_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::add_with_carry_overflow_word_name ( )

inline

Generate identifier @add_with_carry_overflow_word.

Returns

Identifier @add_with_carry_overflow_word.

Definition at line 1048 of file machine_word.h.

add_with_carry_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::add_with_carry_word ( )

inline

Constructor for function symbol @add_with_carry_word.

Returns

Function symbol add_with_carry_word.

Definition at line 890 of file machine_word.h.

add_with_carry_word() [2/2]

application mcrl2::data::sort_machine_word::add_with_carry_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @add_with_carry_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @add_with_carry_word to a number of arguments.

Definition at line 915 of file machine_word.h.

add_with_carry_word_application()

void mcrl2::data::sort_machine_word::add_with_carry_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 952 of file machine_word.h.

add_with_carry_word_manual_implementation()

void mcrl2::data::sort_machine_word::add_with_carry_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The result of adding two words plus 1 modulo the maximal representable machine word plus 1.

The data expression of an application of the function symbol @add_with_carry_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1+e2+1 modulo the machine word.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @add_with_carry_word to a number of arguments.

Definition at line 439 of file machine_word.h.

add_with_carry_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::add_with_carry_word_name ( )

inline

Generate identifier @add_with_carry_word.

Returns

Identifier @add_with_carry_word.

Definition at line 880 of file machine_word.h.

add_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::add_word ( )

inline

Constructor for function symbol @add_word.

Returns

Function symbol add_word.

Definition at line 806 of file machine_word.h.

add_word() [2/2]

application mcrl2::data::sort_machine_word::add_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @add_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @add_word to a number of arguments.

Definition at line 831 of file machine_word.h.

add_word_application()

void mcrl2::data::sort_machine_word::add_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 868 of file machine_word.h.

add_word_manual_implementation()

void mcrl2::data::sort_machine_word::add_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The result of adding two words modulo the maximal representable machine word plus 1.

The data expression of an application of the function symbol @add_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1+e2 modulo the machine word.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @add_word to a number of arguments.

Definition at line 426 of file machine_word.h.

add_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::add_word_name ( )

inline

Generate identifier @add_word.

Returns

Identifier @add_word.

Definition at line 796 of file machine_word.h.

arg()

const data_expression & mcrl2::data::sort_machine_word::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 3600 of file machine_word.h.

arg1()

const data_expression & mcrl2::data::sort_machine_word::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 3636 of file machine_word.h.

arg2()

const data_expression & mcrl2::data::sort_machine_word::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 3648 of file machine_word.h.

arg3()

const data_expression & mcrl2::data::sort_machine_word::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 3660 of file machine_word.h.

arg4()

const data_expression & mcrl2::data::sort_machine_word::arg4 ( const data_expression &  e )

inline

Function for projecting out argument. arg4 from an application.

Parameters

e	A data expression.

Precondition

arg4 is defined for e.

Returns

The argument of e that corresponds to arg4.

Definition at line 3672 of file machine_word.h.

arg5()

const data_expression & mcrl2::data::sort_machine_word::arg5 ( const data_expression &  e )

inline

Function for projecting out argument. arg5 from an application.

Parameters

e	A data expression.

Precondition

arg5 is defined for e.

Returns

The argument of e that corresponds to arg5.

Definition at line 3684 of file machine_word.h.

div_double_doubleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::div_double_doubleword ( )

inline

Constructor for function symbol @div_double_doubleword.

Returns

Function symbol div_double_doubleword.

Definition at line 1988 of file machine_word.h.

div_double_doubleword() [2/2]

application mcrl2::data::sort_machine_word::div_double_doubleword ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Application of function symbol @div_double_doubleword.

Parameters

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

Returns

Application of @div_double_doubleword to a number of arguments.

Definition at line 2015 of file machine_word.h.

div_double_doubleword_application()

void mcrl2::data::sort_machine_word::div_double_doubleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2056 of file machine_word.h.

div_double_doubleword_manual_implementation()

void mcrl2::data::sort_machine_word::div_double_doubleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3, const data_expression &  e4  )

inline

Calculates (base*e1 + e2) div (base*e3 + e4).

The data expression of an application of the function symbol @div_double_doubleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.
e4	The fourth argument.

Returns

(base*e1 + e2) div (base*e3 + e4)

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @div_double_doubleword to a number of arguments.

Definition at line 621 of file machine_word.h.

div_double_doubleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::div_double_doubleword_name ( )

inline

Generate identifier @div_double_doubleword.

Returns

Identifier @div_double_doubleword.

Definition at line 1978 of file machine_word.h.

div_doubleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::div_doubleword ( )

inline

Constructor for function symbol @div_doubleword.

Returns

Function symbol div_doubleword.

Definition at line 1901 of file machine_word.h.

div_doubleword() [2/2]

application mcrl2::data::sort_machine_word::div_doubleword ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @div_doubleword.

Parameters

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

Returns

Application of @div_doubleword to a number of arguments.

Definition at line 1927 of file machine_word.h.

div_doubleword_application()

void mcrl2::data::sort_machine_word::div_doubleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1966 of file machine_word.h.

div_doubleword_manual_implementation()

void mcrl2::data::sort_machine_word::div_doubleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3  )

inline

Calculates (base*e1 + e2) div e3.

The data expression of an application of the function symbol @div_doubleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.

Returns

(base*e1 + e2) div e3

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @div_doubleword to a number of arguments.

Definition at line 605 of file machine_word.h.

div_doubleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::div_doubleword_name ( )

inline

Generate identifier @div_doubleword.

Returns

Identifier @div_doubleword.

Definition at line 1891 of file machine_word.h.

div_triple_doubleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::div_triple_doubleword ( )

inline

Constructor for function symbol @div_triple_doubleword.

Returns

Function symbol div_triple_doubleword.

Definition at line 2078 of file machine_word.h.

div_triple_doubleword() [2/2]

application mcrl2::data::sort_machine_word::div_triple_doubleword ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3, const data_expression &  arg4  )

inline

Application of function symbol @div_triple_doubleword.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns

Application of @div_triple_doubleword to a number of arguments.

Definition at line 2106 of file machine_word.h.

div_triple_doubleword_application()

void mcrl2::data::sort_machine_word::div_triple_doubleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2149 of file machine_word.h.

div_triple_doubleword_manual_implementation()

void mcrl2::data::sort_machine_word::div_triple_doubleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3, const data_expression &  e4, const data_expression &  e5  )

inline

Calculates (base*(base*e1 + e2)+e3) div (base*e4 + e5).

The data expression of an application of the function symbol @div_triple_doubleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.
e4	The fourth argument.
e5	The fifth argument.

Returns

(base*(base*e1 + e2)+e3) div (base*e4 + e5)

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Returns

The data expression corresponding to an application of @div_triple_doubleword to a number of arguments.

Definition at line 639 of file machine_word.h.

div_triple_doubleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::div_triple_doubleword_name ( )

inline

Generate identifier @div_triple_doubleword.

Returns

Identifier @div_triple_doubleword.

Definition at line 2068 of file machine_word.h.

div_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::div_word ( )

inline

Constructor for function symbol @div_word.

Returns

Function symbol div_word.

Definition at line 1652 of file machine_word.h.

div_word() [2/2]

application mcrl2::data::sort_machine_word::div_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @div_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @div_word to a number of arguments.

Definition at line 1677 of file machine_word.h.

div_word_application()

void mcrl2::data::sort_machine_word::div_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1714 of file machine_word.h.

div_word_manual_implementation()

void mcrl2::data::sort_machine_word::div_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

Calculates the division of the first word by the second.

The data expression of an application of the function symbol @div_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1/e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @div_word to a number of arguments.

Definition at line 568 of file machine_word.h.

div_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::div_word_name ( )

inline

Generate identifier @div_word.

Returns

Identifier @div_word.

Definition at line 1642 of file machine_word.h.

equal_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::equal_word ( )

inline

Constructor for function symbol @equal.

Returns

Function symbol equal_word.

Definition at line 2777 of file machine_word.h.

equal_word() [2/2]

application mcrl2::data::sort_machine_word::equal_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @equal.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @equal to a number of arguments.

Definition at line 2802 of file machine_word.h.

equal_word_application()

void mcrl2::data::sort_machine_word::equal_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2839 of file machine_word.h.

equal_word_manual_implementation()

void mcrl2::data::sort_machine_word::equal_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The equality function on two machine words.

The data expression of an application of the function symbol @equal.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1==e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @equal to a number of arguments.

Definition at line 350 of file machine_word.h.

equal_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::equal_word_name ( )

inline

Generate identifier @equal.

Returns

Identifier @equal.

Definition at line 2767 of file machine_word.h.

equals_max_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::equals_max_word ( )

inline

Constructor for function symbol @equals_max_word.

Returns

Function symbol equals_max_word.

Definition at line 725 of file machine_word.h.

equals_max_word() [2/2]

application mcrl2::data::sort_machine_word::equals_max_word ( const data_expression &  arg0 )

inline

Application of function symbol @equals_max_word.

Parameters

arg0	A data expression.

Returns

Application of @equals_max_word to a number of arguments.

Definition at line 749 of file machine_word.h.

equals_max_word_application()

void mcrl2::data::sort_machine_word::equals_max_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 784 of file machine_word.h.

equals_max_word_manual_implementation()

void mcrl2::data::sort_machine_word::equals_max_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

Checks whether the argument is equal to the largest 64 bit number.

The data expression of an application of the function symbol @equals_max_word.

Parameters

e
result	The data_expression into which the created object is stored.

Returns

True if e equals the largest 64 number, otherwise false.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @equals_max_word to a number of arguments.

Definition at line 323 of file machine_word.h.

equals_max_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::equals_max_word_name ( )

inline

Generate identifier @equals_max_word.

Returns

Identifier @equals_max_word.

Definition at line 715 of file machine_word.h.

equals_one_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::equals_one_word ( )

inline

Constructor for function symbol @equals_one_word.

Returns

Function symbol equals_one_word.

Definition at line 644 of file machine_word.h.

equals_one_word() [2/2]

application mcrl2::data::sort_machine_word::equals_one_word ( const data_expression &  arg0 )

inline

Application of function symbol @equals_one_word.

Parameters

arg0	A data expression.

Returns

Application of @equals_one_word to a number of arguments.

Definition at line 668 of file machine_word.h.

equals_one_word_application()

void mcrl2::data::sort_machine_word::equals_one_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 703 of file machine_word.h.

equals_one_word_manual_implementation()

void mcrl2::data::sort_machine_word::equals_one_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

Checks whether the argument is equal to 1.

The data expression of an application of the function symbol @equals_one_word.

Parameters

e
result	The data_expression into which the created object is stored.

Returns

True if e equals 0, otherwise false.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @equals_one_word to a number of arguments.

Definition at line 307 of file machine_word.h.

equals_one_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::equals_one_word_name ( )

inline

Generate identifier @equals_one_word.

Returns

Identifier @equals_one_word.

Definition at line 634 of file machine_word.h.

equals_zero_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::equals_zero_word ( )

inline

Constructor for function symbol @equals_zero_word.

Returns

Function symbol equals_zero_word.

Definition at line 482 of file machine_word.h.

equals_zero_word() [2/2]

application mcrl2::data::sort_machine_word::equals_zero_word ( const data_expression &  arg0 )

inline

Application of function symbol @equals_zero_word.

Parameters

arg0	A data expression.

Returns

Application of @equals_zero_word to a number of arguments.

Definition at line 506 of file machine_word.h.

equals_zero_word_application()

void mcrl2::data::sort_machine_word::equals_zero_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 541 of file machine_word.h.

equals_zero_word_manual_implementation()

void mcrl2::data::sort_machine_word::equals_zero_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

Checks whether the argument is equal to 0.

The data expression of an application of the function symbol @equals_zero_word.

Parameters

e
result	The data_expression into which the created object is stored.

Returns

True if e equals 0, otherwise false.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @equals_zero_word to a number of arguments.

Definition at line 275 of file machine_word.h.

equals_zero_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::equals_zero_word_name ( )

inline

Generate identifier @equals_zero_word.

Returns

Identifier @equals_zero_word.

Definition at line 472 of file machine_word.h.

four_word()

const function_symbol & mcrl2::data::sort_machine_word::four_word ( )

inline

Constructor for function symbol @four_word.

Returns

Function symbol four_word.

Definition at line 386 of file machine_word.h.

four_word_application()

void mcrl2::data::sort_machine_word::four_word_application ( data_expression &  result, const data_expression &  a  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 412 of file machine_word.h.

four_word_manual_implementation()

void mcrl2::data::sort_machine_word::four_word_manual_implementation ( data_expression &  result )

inline

The machine number representing 4.

The data expression of an application of the constant symbol @four_word.

Parameters

result

The data_expression into which the created object is stored.

Returns

The machine number 4.

This function is to be implemented manually. ///

Returns

The data expression corresponding to an application of @four_word to a number of arguments.

Definition at line 258 of file machine_word.h.

four_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::four_word_name ( )

inline

Generate identifier @four_word.

Returns

Identifier @four_word.

Definition at line 376 of file machine_word.h.

greater_equal_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::greater_equal_word ( )

inline

Constructor for function symbol @greater_equal.

Returns

Function symbol greater_equal_word.

Definition at line 3197 of file machine_word.h.

greater_equal_word() [2/2]

application mcrl2::data::sort_machine_word::greater_equal_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @greater_equal.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @greater_equal to a number of arguments.

Definition at line 3222 of file machine_word.h.

greater_equal_word_application()

void mcrl2::data::sort_machine_word::greater_equal_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 3259 of file machine_word.h.

greater_equal_word_manual_implementation()

void mcrl2::data::sort_machine_word::greater_equal_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The greater than or equal function on two machine words.

The data expression of an application of the function symbol @greater_equal.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1>=e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @greater_equal to a number of arguments.

Definition at line 414 of file machine_word.h.

greater_equal_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::greater_equal_word_name ( )

inline

Generate identifier @greater_equal.

Returns

Identifier @greater_equal.

Definition at line 3187 of file machine_word.h.

greater_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::greater_word ( )

inline

Constructor for function symbol @greater.

Returns

Function symbol greater_word.

Definition at line 3113 of file machine_word.h.

greater_word() [2/2]

application mcrl2::data::sort_machine_word::greater_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @greater.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @greater to a number of arguments.

Definition at line 3138 of file machine_word.h.

greater_word_application()

void mcrl2::data::sort_machine_word::greater_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 3175 of file machine_word.h.

greater_word_manual_implementation()

void mcrl2::data::sort_machine_word::greater_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The greater than function on two machine words.

The data expression of an application of the function symbol @greater.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1>e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @greater to a number of arguments.

Definition at line 402 of file machine_word.h.

greater_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::greater_word_name ( )

inline

Generate identifier @greater.

Returns

Identifier @greater.

Definition at line 3103 of file machine_word.h.

is_add_overflow_word_application()

bool mcrl2::data::sort_machine_word::is_add_overflow_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @add_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol add_overflow_word to a number of arguments.

Definition at line 1020 of file machine_word.h.

is_add_overflow_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_add_overflow_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @add_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @add_overflow_word.

Definition at line 984 of file machine_word.h.

is_add_with_carry_overflow_word_application()

bool mcrl2::data::sort_machine_word::is_add_with_carry_overflow_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @add_with_carry_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol add_with_carry_overflow_word to a number of arguments.

Definition at line 1104 of file machine_word.h.

is_add_with_carry_overflow_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_add_with_carry_overflow_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @add_with_carry_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @add_with_carry_overflow_word.

Definition at line 1068 of file machine_word.h.

is_add_with_carry_word_application()

bool mcrl2::data::sort_machine_word::is_add_with_carry_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @add_with_carry_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol add_with_carry_word to a number of arguments.

Definition at line 936 of file machine_word.h.

is_add_with_carry_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_add_with_carry_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @add_with_carry_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @add_with_carry_word.

Definition at line 900 of file machine_word.h.

is_add_word_application()

bool mcrl2::data::sort_machine_word::is_add_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @add_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol add_word to a number of arguments.

Definition at line 852 of file machine_word.h.

is_add_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_add_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @add_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @add_word.

Definition at line 816 of file machine_word.h.

is_div_double_doubleword_application()

bool mcrl2::data::sort_machine_word::is_div_double_doubleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @div_double_doubleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol div_double_doubleword to a number of arguments.

Definition at line 2038 of file machine_word.h.

is_div_double_doubleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_div_double_doubleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @div_double_doubleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @div_double_doubleword.

Definition at line 1998 of file machine_word.h.

is_div_doubleword_application()

bool mcrl2::data::sort_machine_word::is_div_doubleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @div_doubleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol div_doubleword to a number of arguments.

Definition at line 1949 of file machine_word.h.

is_div_doubleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_div_doubleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @div_doubleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @div_doubleword.

Definition at line 1911 of file machine_word.h.

is_div_triple_doubleword_application()

bool mcrl2::data::sort_machine_word::is_div_triple_doubleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @div_triple_doubleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol div_triple_doubleword to a number of arguments.

Definition at line 2130 of file machine_word.h.

is_div_triple_doubleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_div_triple_doubleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @div_triple_doubleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @div_triple_doubleword.

Definition at line 2088 of file machine_word.h.

is_div_word_application()

bool mcrl2::data::sort_machine_word::is_div_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @div_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol div_word to a number of arguments.

Definition at line 1698 of file machine_word.h.

is_div_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_div_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @div_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @div_word.

Definition at line 1662 of file machine_word.h.

is_equal_word_application()

bool mcrl2::data::sort_machine_word::is_equal_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @equal.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol equal_word to a number of arguments.

Definition at line 2823 of file machine_word.h.

is_equal_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_equal_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @equal.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @equal.

Definition at line 2787 of file machine_word.h.

is_equals_max_word_application()

bool mcrl2::data::sort_machine_word::is_equals_max_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @equals_max_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol equals_max_word to a number of arguments.

Definition at line 769 of file machine_word.h.

is_equals_max_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_equals_max_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @equals_max_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @equals_max_word.

Definition at line 735 of file machine_word.h.

is_equals_one_word_application()

bool mcrl2::data::sort_machine_word::is_equals_one_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @equals_one_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol equals_one_word to a number of arguments.

Definition at line 688 of file machine_word.h.

is_equals_one_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_equals_one_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @equals_one_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @equals_one_word.

Definition at line 654 of file machine_word.h.

is_equals_zero_word_application()

bool mcrl2::data::sort_machine_word::is_equals_zero_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @equals_zero_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol equals_zero_word to a number of arguments.

Definition at line 526 of file machine_word.h.

is_equals_zero_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_equals_zero_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @equals_zero_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @equals_zero_word.

Definition at line 492 of file machine_word.h.

is_four_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_four_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @four_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @four_word.

Definition at line 396 of file machine_word.h.

is_greater_equal_word_application()

bool mcrl2::data::sort_machine_word::is_greater_equal_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @greater_equal.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol greater_equal_word to a number of arguments.

Definition at line 3243 of file machine_word.h.

is_greater_equal_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_greater_equal_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @greater_equal.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @greater_equal.

Definition at line 3207 of file machine_word.h.

is_greater_word_application()

bool mcrl2::data::sort_machine_word::is_greater_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @greater.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol greater_word to a number of arguments.

Definition at line 3159 of file machine_word.h.

is_greater_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_greater_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @greater.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @greater.

Definition at line 3123 of file machine_word.h.

is_less_equal_word_application()

bool mcrl2::data::sort_machine_word::is_less_equal_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @less_equal.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol less_equal_word to a number of arguments.

Definition at line 3075 of file machine_word.h.

is_less_equal_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_less_equal_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @less_equal.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @less_equal.

Definition at line 3039 of file machine_word.h.

is_less_word_application()

bool mcrl2::data::sort_machine_word::is_less_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @less.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol less_word to a number of arguments.

Definition at line 2991 of file machine_word.h.

is_less_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_less_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @less.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @less.

Definition at line 2955 of file machine_word.h.

is_machine_word()

bool mcrl2::data::sort_machine_word::is_machine_word ( const sort_expression &  e )

inline

Recogniser for sort expression @word.

Parameters

e	A sort expression

Returns

true iff e == machine_word()

Definition at line 55 of file machine_word.h.

is_max_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_max_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @max_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @max_word.

Definition at line 444 of file machine_word.h.

is_minus_word_application()

bool mcrl2::data::sort_machine_word::is_minus_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @minus_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol minus_word to a number of arguments.

Definition at line 1530 of file machine_word.h.

is_minus_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_minus_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @minus_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @minus_word.

Definition at line 1494 of file machine_word.h.

is_mod_doubleword_application()

bool mcrl2::data::sort_machine_word::is_mod_doubleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @mod_doubleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol mod_doubleword to a number of arguments.

Definition at line 2219 of file machine_word.h.

is_mod_doubleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_mod_doubleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @mod_doubleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @mod_doubleword.

Definition at line 2181 of file machine_word.h.

is_mod_word_application()

bool mcrl2::data::sort_machine_word::is_mod_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @mod_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol mod_word to a number of arguments.

Definition at line 1782 of file machine_word.h.

is_mod_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_mod_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @mod_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @mod_word.

Definition at line 1746 of file machine_word.h.

is_monus_word_application()

bool mcrl2::data::sort_machine_word::is_monus_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @monus_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol monus_word to a number of arguments.

Definition at line 1614 of file machine_word.h.

is_monus_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_monus_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @monus_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @monus_word.

Definition at line 1578 of file machine_word.h.

is_not_equal_word_application()

bool mcrl2::data::sort_machine_word::is_not_equal_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @not_equal.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol not_equal_word to a number of arguments.

Definition at line 2907 of file machine_word.h.

is_not_equal_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_not_equal_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @not_equal.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @not_equal.

Definition at line 2871 of file machine_word.h.

is_not_equals_zero_word_application()

bool mcrl2::data::sort_machine_word::is_not_equals_zero_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @not_equals_zero_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol not_equals_zero_word to a number of arguments.

Definition at line 607 of file machine_word.h.

is_not_equals_zero_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_not_equals_zero_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @not_equals_zero_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @not_equals_zero_word.

Definition at line 573 of file machine_word.h.

is_one_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_one_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @one_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @one_word.

Definition at line 252 of file machine_word.h.

is_pred_word_application()

bool mcrl2::data::sort_machine_word::is_pred_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @pred_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol pred_word to a number of arguments.

Definition at line 2740 of file machine_word.h.

is_pred_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_pred_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @pred_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @pred_word.

Definition at line 2706 of file machine_word.h.

is_rightmost_bit_application()

bool mcrl2::data::sort_machine_word::is_rightmost_bit_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @rightmost_bit.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol rightmost_bit to a number of arguments.

Definition at line 3325 of file machine_word.h.

is_rightmost_bit_function_symbol()

bool mcrl2::data::sort_machine_word::is_rightmost_bit_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @rightmost_bit.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @rightmost_bit.

Definition at line 3291 of file machine_word.h.

is_shift_right_application()

bool mcrl2::data::sort_machine_word::is_shift_right_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @shift_right.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol shift_right to a number of arguments.

Definition at line 3408 of file machine_word.h.

is_shift_right_function_symbol()

bool mcrl2::data::sort_machine_word::is_shift_right_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @shift_right.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @shift_right.

Definition at line 3372 of file machine_word.h.

is_sqrt_doubleword_application()

bool mcrl2::data::sort_machine_word::is_sqrt_doubleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @sqrt_doubleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol sqrt_doubleword to a number of arguments.

Definition at line 2304 of file machine_word.h.

is_sqrt_doubleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_sqrt_doubleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @sqrt_doubleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @sqrt_doubleword.

Definition at line 2268 of file machine_word.h.

is_sqrt_quadrupleword_application()

bool mcrl2::data::sort_machine_word::is_sqrt_quadrupleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @sqrt_quadrupleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol sqrt_quadrupleword to a number of arguments.

Definition at line 2566 of file machine_word.h.

is_sqrt_quadrupleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_sqrt_quadrupleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @sqrt_quadrupleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @sqrt_quadrupleword.

Definition at line 2526 of file machine_word.h.

is_sqrt_quadrupleword_overflow_application()

bool mcrl2::data::sort_machine_word::is_sqrt_quadrupleword_overflow_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @sqrt_quadrupleword_overflow.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol sqrt_quadrupleword_overflow to a number of arguments.

Definition at line 2656 of file machine_word.h.

is_sqrt_quadrupleword_overflow_function_symbol()

bool mcrl2::data::sort_machine_word::is_sqrt_quadrupleword_overflow_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @sqrt_quadrupleword_overflow.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @sqrt_quadrupleword_overflow.

Definition at line 2616 of file machine_word.h.

is_sqrt_tripleword_application()

bool mcrl2::data::sort_machine_word::is_sqrt_tripleword_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @sqrt_tripleword.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol sqrt_tripleword to a number of arguments.

Definition at line 2390 of file machine_word.h.

is_sqrt_tripleword_function_symbol()

bool mcrl2::data::sort_machine_word::is_sqrt_tripleword_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @sqrt_tripleword.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @sqrt_tripleword.

Definition at line 2352 of file machine_word.h.

is_sqrt_tripleword_overflow_application()

bool mcrl2::data::sort_machine_word::is_sqrt_tripleword_overflow_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @sqrt_tripleword_overflow.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol sqrt_tripleword_overflow to a number of arguments.

Definition at line 2477 of file machine_word.h.

is_sqrt_tripleword_overflow_function_symbol()

bool mcrl2::data::sort_machine_word::is_sqrt_tripleword_overflow_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @sqrt_tripleword_overflow.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @sqrt_tripleword_overflow.

Definition at line 2439 of file machine_word.h.

is_sqrt_word_application()

bool mcrl2::data::sort_machine_word::is_sqrt_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @sqrt_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol sqrt_word to a number of arguments.

Definition at line 1864 of file machine_word.h.

is_sqrt_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_sqrt_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @sqrt_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @sqrt_word.

Definition at line 1830 of file machine_word.h.

is_succ_word_application()

bool mcrl2::data::sort_machine_word::is_succ_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @succ_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol succ_word to a number of arguments.

Definition at line 170 of file machine_word.h.

is_succ_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_succ_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @succ_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @succ_word.

Definition at line 136 of file machine_word.h.

is_three_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_three_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @three_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @three_word.

Definition at line 348 of file machine_word.h.

is_times_overflow_word_application()

bool mcrl2::data::sort_machine_word::is_times_overflow_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @times_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol times_overflow_word to a number of arguments.

Definition at line 1359 of file machine_word.h.

is_times_overflow_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_times_overflow_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @times_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @times_overflow_word.

Definition at line 1323 of file machine_word.h.

is_times_with_carry_overflow_word_application()

bool mcrl2::data::sort_machine_word::is_times_with_carry_overflow_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @times_with_carry_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol times_with_carry_overflow_word to a number of arguments.

Definition at line 1445 of file machine_word.h.

is_times_with_carry_overflow_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_times_with_carry_overflow_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @times_with_carry_overflow_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @times_with_carry_overflow_word.

Definition at line 1407 of file machine_word.h.

is_times_with_carry_word_application()

bool mcrl2::data::sort_machine_word::is_times_with_carry_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @times_with_carry_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol times_with_carry_word to a number of arguments.

Definition at line 1274 of file machine_word.h.

is_times_with_carry_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_times_with_carry_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @times_with_carry_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @times_with_carry_word.

Definition at line 1236 of file machine_word.h.

is_times_word_application()

bool mcrl2::data::sort_machine_word::is_times_word_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @times_word.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol times_word to a number of arguments.

Definition at line 1188 of file machine_word.h.

is_times_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_times_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @times_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @times_word.

Definition at line 1152 of file machine_word.h.

is_two_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_two_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @two_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @two_word.

Definition at line 300 of file machine_word.h.

is_zero_word_function_symbol()

bool mcrl2::data::sort_machine_word::is_zero_word_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @zero_word.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @zero_word.

Definition at line 88 of file machine_word.h.

left()

const data_expression & mcrl2::data::sort_machine_word::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 3612 of file machine_word.h.

less_equal_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::less_equal_word ( )

inline

Constructor for function symbol @less_equal.

Returns

Function symbol less_equal_word.

Definition at line 3029 of file machine_word.h.

less_equal_word() [2/2]

application mcrl2::data::sort_machine_word::less_equal_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @less_equal.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @less_equal to a number of arguments.

Definition at line 3054 of file machine_word.h.

less_equal_word_application()

void mcrl2::data::sort_machine_word::less_equal_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 3091 of file machine_word.h.

less_equal_word_manual_implementation()

void mcrl2::data::sort_machine_word::less_equal_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The less than or equal function on two machine words.

The data expression of an application of the function symbol @less_equal.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1<=e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @less_equal to a number of arguments.

Definition at line 390 of file machine_word.h.

less_equal_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::less_equal_word_name ( )

inline

Generate identifier @less_equal.

Returns

Identifier @less_equal.

Definition at line 3019 of file machine_word.h.

less_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::less_word ( )

inline

Constructor for function symbol @less.

Returns

Function symbol less_word.

Definition at line 2945 of file machine_word.h.

less_word() [2/2]

application mcrl2::data::sort_machine_word::less_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @less.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @less to a number of arguments.

Definition at line 2970 of file machine_word.h.

less_word_application()

void mcrl2::data::sort_machine_word::less_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 3007 of file machine_word.h.

less_word_manual_implementation()

void mcrl2::data::sort_machine_word::less_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The less than function on two machine words.

The data expression of an application of the function symbol @less.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1<e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @less to a number of arguments.

Definition at line 378 of file machine_word.h.

less_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::less_word_name ( )

inline

Generate identifier @less.

Returns

Identifier @less.

Definition at line 2935 of file machine_word.h.

machine_word()

const basic_sort & mcrl2::data::sort_machine_word::machine_word ( )

inline

Constructor for sort expression @word.

Returns

Sort expression @word.

Definition at line 45 of file machine_word.h.

machine_word_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_machine_word::machine_word_cpp_implementable_constructors ( )

inline

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

Returns

All system defined constructors that are to be implemented in C++ for machine_word.

Definition at line 220 of file machine_word.h.

machine_word_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_machine_word::machine_word_cpp_implementable_mappings ( )

inline

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

Returns

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

Definition at line 3549 of file machine_word.h.

machine_word_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_machine_word::machine_word_generate_constructors_and_functions_code ( )

inline

Give all system defined mappings and constructors for machine_word.

Returns

All system defined mappings for machine_word

Definition at line 3484 of file machine_word.h.

machine_word_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_machine_word::machine_word_generate_constructors_code ( )

inline

Give all system defined constructors for machine_word.

Returns

All system defined constructors for machine_word.

Definition at line 196 of file machine_word.h.

machine_word_generate_equations_code()

data_equation_vector mcrl2::data::sort_machine_word::machine_word_generate_equations_code ( )

inline

Give all system defined equations for machine_word.

Returns

All system defined equations for sort machine_word

Definition at line 3693 of file machine_word.h.

machine_word_generate_functions_code()

function_symbol_vector mcrl2::data::sort_machine_word::machine_word_generate_functions_code ( )

inline

Give all system defined mappings for machine_word.

Returns

All system defined mappings for machine_word

Definition at line 3435 of file machine_word.h.

machine_word_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_machine_word::machine_word_mCRL2_usable_constructors ( )

inline

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

Returns

All system defined constructors that can be used in an mCRL2 specification for machine_word.

Definition at line 207 of file machine_word.h.

machine_word_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_machine_word::machine_word_mCRL2_usable_mappings ( )

inline

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

Returns

All system defined mappings for that can be used in mCRL2 specificationis machine_word

Definition at line 3497 of file machine_word.h.

machine_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::machine_word_name ( )

inline

Definition at line 36 of file machine_word.h.

make_add_overflow_word()

void mcrl2::data::sort_machine_word::make_add_overflow_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @add_overflow_word.

Parameters

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

Definition at line 1010 of file machine_word.h.

make_add_with_carry_overflow_word()

void mcrl2::data::sort_machine_word::make_add_with_carry_overflow_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @add_with_carry_overflow_word.

Parameters

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

Definition at line 1094 of file machine_word.h.

make_add_with_carry_word()

void mcrl2::data::sort_machine_word::make_add_with_carry_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @add_with_carry_word.

Parameters

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

Definition at line 926 of file machine_word.h.

make_add_word()

void mcrl2::data::sort_machine_word::make_add_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @add_word.

Parameters

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

Definition at line 842 of file machine_word.h.

make_div_double_doubleword()

void mcrl2::data::sort_machine_word::make_div_double_doubleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Make an application of function symbol @div_double_doubleword.

Parameters

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

Definition at line 2028 of file machine_word.h.

make_div_doubleword()

void mcrl2::data::sort_machine_word::make_div_doubleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @div_doubleword.

Parameters

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

Definition at line 1939 of file machine_word.h.

make_div_triple_doubleword()

void mcrl2::data::sort_machine_word::make_div_triple_doubleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3, const data_expression &  arg4  )

inline

Make an application of function symbol @div_triple_doubleword.

Parameters

result	The data expression where the @div_triple_doubleword expression is put.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.
arg3	A data expression.
arg4	A data expression.

Definition at line 2120 of file machine_word.h.

make_div_word()

void mcrl2::data::sort_machine_word::make_div_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @div_word.

Parameters

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

Definition at line 1688 of file machine_word.h.

make_equal_word()

void mcrl2::data::sort_machine_word::make_equal_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @equal.

Parameters

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

Definition at line 2813 of file machine_word.h.

make_equals_max_word()

void mcrl2::data::sort_machine_word::make_equals_max_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @equals_max_word.

Parameters

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

Definition at line 759 of file machine_word.h.

make_equals_one_word()

void mcrl2::data::sort_machine_word::make_equals_one_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @equals_one_word.

Parameters

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

Definition at line 678 of file machine_word.h.

make_equals_zero_word()

void mcrl2::data::sort_machine_word::make_equals_zero_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @equals_zero_word.

Parameters

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

Definition at line 516 of file machine_word.h.

make_greater_equal_word()

void mcrl2::data::sort_machine_word::make_greater_equal_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @greater_equal.

Parameters

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

Definition at line 3233 of file machine_word.h.

make_greater_word()

void mcrl2::data::sort_machine_word::make_greater_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @greater.

Parameters

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

Definition at line 3149 of file machine_word.h.

make_less_equal_word()

void mcrl2::data::sort_machine_word::make_less_equal_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @less_equal.

Parameters

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

Definition at line 3065 of file machine_word.h.

make_less_word()

void mcrl2::data::sort_machine_word::make_less_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @less.

Parameters

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

Definition at line 2981 of file machine_word.h.

make_minus_word()

void mcrl2::data::sort_machine_word::make_minus_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @minus_word.

Parameters

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

Definition at line 1520 of file machine_word.h.

make_mod_doubleword()

void mcrl2::data::sort_machine_word::make_mod_doubleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @mod_doubleword.

Parameters

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

Definition at line 2209 of file machine_word.h.

make_mod_word()

void mcrl2::data::sort_machine_word::make_mod_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @mod_word.

Parameters

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

Definition at line 1772 of file machine_word.h.

make_monus_word()

void mcrl2::data::sort_machine_word::make_monus_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @monus_word.

Parameters

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

Definition at line 1604 of file machine_word.h.

make_not_equal_word()

void mcrl2::data::sort_machine_word::make_not_equal_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @not_equal.

Parameters

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

Definition at line 2897 of file machine_word.h.

make_not_equals_zero_word()

void mcrl2::data::sort_machine_word::make_not_equals_zero_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @not_equals_zero_word.

Parameters

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

Definition at line 597 of file machine_word.h.

make_pred_word()

void mcrl2::data::sort_machine_word::make_pred_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @pred_word.

Parameters

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

Definition at line 2730 of file machine_word.h.

make_rightmost_bit()

void mcrl2::data::sort_machine_word::make_rightmost_bit ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @rightmost_bit.

Parameters

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

Definition at line 3315 of file machine_word.h.

make_shift_right()

void mcrl2::data::sort_machine_word::make_shift_right ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @shift_right.

Parameters

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

Definition at line 3398 of file machine_word.h.

make_sqrt_doubleword()

void mcrl2::data::sort_machine_word::make_sqrt_doubleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @sqrt_doubleword.

Parameters

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

Definition at line 2294 of file machine_word.h.

make_sqrt_quadrupleword()

void mcrl2::data::sort_machine_word::make_sqrt_quadrupleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Make an application of function symbol @sqrt_quadrupleword.

Parameters

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

Definition at line 2556 of file machine_word.h.

make_sqrt_quadrupleword_overflow()

void mcrl2::data::sort_machine_word::make_sqrt_quadrupleword_overflow ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Make an application of function symbol @sqrt_quadrupleword_overflow.

Parameters

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

Definition at line 2646 of file machine_word.h.

make_sqrt_tripleword()

void mcrl2::data::sort_machine_word::make_sqrt_tripleword ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @sqrt_tripleword.

Parameters

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

Definition at line 2380 of file machine_word.h.

make_sqrt_tripleword_overflow()

void mcrl2::data::sort_machine_word::make_sqrt_tripleword_overflow ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @sqrt_tripleword_overflow.

Parameters

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

Definition at line 2467 of file machine_word.h.

make_sqrt_word()

void mcrl2::data::sort_machine_word::make_sqrt_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @sqrt_word.

Parameters

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

Definition at line 1854 of file machine_word.h.

make_succ_word()

void mcrl2::data::sort_machine_word::make_succ_word ( data_expression &  result, const data_expression &  arg0  )

inline

Make an application of function symbol @succ_word.

Parameters

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

Definition at line 160 of file machine_word.h.

make_times_overflow_word()

void mcrl2::data::sort_machine_word::make_times_overflow_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @times_overflow_word.

Parameters

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

Definition at line 1349 of file machine_word.h.

make_times_with_carry_overflow_word()

void mcrl2::data::sort_machine_word::make_times_with_carry_overflow_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @times_with_carry_overflow_word.

Parameters

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

Definition at line 1435 of file machine_word.h.

make_times_with_carry_word()

void mcrl2::data::sort_machine_word::make_times_with_carry_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @times_with_carry_word.

Parameters

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

Definition at line 1264 of file machine_word.h.

make_times_word()

void mcrl2::data::sort_machine_word::make_times_word ( data_expression &  result, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @times_word.

Parameters

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

Definition at line 1178 of file machine_word.h.

max_word()

const function_symbol & mcrl2::data::sort_machine_word::max_word ( )

inline

Constructor for function symbol @max_word.

Returns

Function symbol max_word.

Definition at line 434 of file machine_word.h.

max_word_application()

void mcrl2::data::sort_machine_word::max_word_application ( data_expression &  result, const data_expression &  a  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 460 of file machine_word.h.

max_word_manual_implementation()

void mcrl2::data::sort_machine_word::max_word_manual_implementation ( data_expression &  result )

inline

The largest representable machine number.

The data expression of an application of the constant symbol @max_word.

Parameters

result

The data_expression into which the created object is stored.

Returns

The largest number a machine word can hold.

This function is to be implemented manually. ///

Returns

The data expression corresponding to an application of @max_word to a number of arguments.

Definition at line 266 of file machine_word.h.

max_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::max_word_name ( )

inline

Generate identifier @max_word.

Returns

Identifier @max_word.

Definition at line 424 of file machine_word.h.

minus_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::minus_word ( )

inline

Constructor for function symbol @minus_word.

Returns

Function symbol minus_word.

Definition at line 1484 of file machine_word.h.

minus_word() [2/2]

application mcrl2::data::sort_machine_word::minus_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @minus_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @minus_word to a number of arguments.

Definition at line 1509 of file machine_word.h.

minus_word_application()

void mcrl2::data::sort_machine_word::minus_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1546 of file machine_word.h.

minus_word_manual_implementation()

void mcrl2::data::sort_machine_word::minus_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The result of subtracting two words modulo the maximal representable machine word plus 1.

The data expression of an application of the function symbol @minus_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1-e2 modulo the machine word.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @minus_word to a number of arguments.

Definition at line 542 of file machine_word.h.

minus_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::minus_word_name ( )

inline

Generate identifier @minus_word.

Returns

Identifier @minus_word.

Definition at line 1474 of file machine_word.h.

mod_double_doubleword_manual_implementation()

void mcrl2::data::sort_machine_word::mod_double_doubleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3, const data_expression &  e4  )

inline

Calculates (base*e1 + e2) mod (base*e3 + e4).

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.
e4	The fourth argument.

Returns

(base*e1 + e2) mod (base*e3 + e4)

Definition at line 663 of file machine_word.h.

mod_doubleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::mod_doubleword ( )

inline

Constructor for function symbol @mod_doubleword.

Returns

Function symbol mod_doubleword.

Definition at line 2171 of file machine_word.h.

mod_doubleword() [2/2]

application mcrl2::data::sort_machine_word::mod_doubleword ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @mod_doubleword.

Parameters

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

Returns

Application of @mod_doubleword to a number of arguments.

Definition at line 2197 of file machine_word.h.

mod_doubleword_application()

void mcrl2::data::sort_machine_word::mod_doubleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2236 of file machine_word.h.

mod_doubleword_manual_implementation()

void mcrl2::data::sort_machine_word::mod_doubleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3  )

inline

Calculates (base*e1 + e2) mod e3. The result fits in one word.

The data expression of an application of the function symbol @mod_doubleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.

Returns

(base*e1 + e2) mod e3

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @mod_doubleword to a number of arguments.

Definition at line 692 of file machine_word.h.

mod_doubleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::mod_doubleword_name ( )

inline

Generate identifier @mod_doubleword.

Returns

Identifier @mod_doubleword.

Definition at line 2161 of file machine_word.h.

mod_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::mod_word ( )

inline

Constructor for function symbol @mod_word.

Returns

Function symbol mod_word.

Definition at line 1736 of file machine_word.h.

mod_word() [2/2]

application mcrl2::data::sort_machine_word::mod_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @mod_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @mod_word to a number of arguments.

Definition at line 1761 of file machine_word.h.

mod_word_application()

void mcrl2::data::sort_machine_word::mod_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1798 of file machine_word.h.

mod_word_manual_implementation()

void mcrl2::data::sort_machine_word::mod_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

Calculates e1 modulo e2.

The data expression of an application of the function symbol @mod_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1 modulo e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @mod_word to a number of arguments.

Definition at line 581 of file machine_word.h.

mod_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::mod_word_name ( )

inline

Generate identifier @mod_word.

Returns

Identifier @mod_word.

Definition at line 1726 of file machine_word.h.

monus_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::monus_word ( )

inline

Constructor for function symbol @monus_word.

Returns

Function symbol monus_word.

Definition at line 1568 of file machine_word.h.

monus_word() [2/2]

application mcrl2::data::sort_machine_word::monus_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @monus_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @monus_word to a number of arguments.

Definition at line 1593 of file machine_word.h.

monus_word_application()

void mcrl2::data::sort_machine_word::monus_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1630 of file machine_word.h.

monus_word_manual_implementation()

void mcrl2::data::sort_machine_word::monus_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The result of subtracting two words. If the result is negative 0 is returned.

The data expression of an application of the function symbol @monus_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

max(0,e1-e2).

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @monus_word to a number of arguments.

Definition at line 555 of file machine_word.h.

monus_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::monus_word_name ( )

inline

Generate identifier @monus_word.

Returns

Identifier @monus_word.

Definition at line 1558 of file machine_word.h.

not_equal_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::not_equal_word ( )

inline

Constructor for function symbol @not_equal.

Returns

Function symbol not_equal_word.

Definition at line 2861 of file machine_word.h.

not_equal_word() [2/2]

application mcrl2::data::sort_machine_word::not_equal_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @not_equal.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @not_equal to a number of arguments.

Definition at line 2886 of file machine_word.h.

not_equal_word_application()

void mcrl2::data::sort_machine_word::not_equal_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2923 of file machine_word.h.

not_equal_word_manual_implementation()

void mcrl2::data::sort_machine_word::not_equal_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The non equality function on two machine words.

The data expression of an application of the function symbol @not_equal.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1!=e2.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @not_equal to a number of arguments.

Definition at line 364 of file machine_word.h.

not_equal_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::not_equal_word_name ( )

inline

Generate identifier @not_equal.

Returns

Identifier @not_equal.

Definition at line 2851 of file machine_word.h.

not_equals_zero_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::not_equals_zero_word ( )

inline

Constructor for function symbol @not_equals_zero_word.

Returns

Function symbol not_equals_zero_word.

Definition at line 563 of file machine_word.h.

not_equals_zero_word() [2/2]

application mcrl2::data::sort_machine_word::not_equals_zero_word ( const data_expression &  arg0 )

inline

Application of function symbol @not_equals_zero_word.

Parameters

arg0	A data expression.

Returns

Application of @not_equals_zero_word to a number of arguments.

Definition at line 587 of file machine_word.h.

not_equals_zero_word_application()

void mcrl2::data::sort_machine_word::not_equals_zero_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 622 of file machine_word.h.

not_equals_zero_word_manual_implementation()

void mcrl2::data::sort_machine_word::not_equals_zero_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

Checks whether the argument is not equal to 0.

The data expression of an application of the function symbol @not_equals_zero_word.

Parameters

e
result	The data_expression into which the created object is stored.

Returns

True if e equals 0, otherwise false.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @not_equals_zero_word to a number of arguments.

Definition at line 291 of file machine_word.h.

not_equals_zero_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::not_equals_zero_word_name ( )

inline

Generate identifier @not_equals_zero_word.

Returns

Identifier @not_equals_zero_word.

Definition at line 553 of file machine_word.h.

one_word()

const function_symbol & mcrl2::data::sort_machine_word::one_word ( )

inline

Constructor for function symbol @one_word.

Returns

Function symbol one_word.

Definition at line 242 of file machine_word.h.

one_word_application()

void mcrl2::data::sort_machine_word::one_word_application ( data_expression &  result, const data_expression &  a  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 268 of file machine_word.h.

one_word_manual_implementation()

void mcrl2::data::sort_machine_word::one_word_manual_implementation ( data_expression &  result )

inline

The machine number representing 1.

The data expression of an application of the constant symbol @one_word.

Parameters

result

The data_expression into which the created object is stored.

Returns

The machine number 1.

This function is to be implemented manually. ///

Returns

The data expression corresponding to an application of @one_word to a number of arguments.

Definition at line 234 of file machine_word.h.

one_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::one_word_name ( )

inline

Generate identifier @one_word.

Returns

Identifier @one_word.

Definition at line 232 of file machine_word.h.

pred_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::pred_word ( )

inline

Constructor for function symbol @pred_word.

Returns

Function symbol pred_word.

Definition at line 2696 of file machine_word.h.

pred_word() [2/2]

application mcrl2::data::sort_machine_word::pred_word ( const data_expression &  arg0 )

inline

Application of function symbol @pred_word.

Parameters

arg0	A data expression.

Returns

Application of @pred_word to a number of arguments.

Definition at line 2720 of file machine_word.h.

pred_word_application()

void mcrl2::data::sort_machine_word::pred_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2755 of file machine_word.h.

pred_word_manual_implementation()

void mcrl2::data::sort_machine_word::pred_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

The predecessor function on a machine numbers, that wraps around.

The data expression of an application of the function symbol @pred_word.

Parameters

result	The data_expression into which the created object is stored.
e

Returns

e-1, or maxword if e is zero.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @pred_word to a number of arguments.

Definition at line 779 of file machine_word.h.

pred_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::pred_word_name ( )

inline

Generate identifier @pred_word.

Returns

Identifier @pred_word.

Definition at line 2686 of file machine_word.h.

right()

const data_expression & mcrl2::data::sort_machine_word::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 3624 of file machine_word.h.

rightmost_bit() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::rightmost_bit ( )

inline

Constructor for function symbol @rightmost_bit.

Returns

Function symbol rightmost_bit.

Definition at line 3281 of file machine_word.h.

rightmost_bit() [2/2]

application mcrl2::data::sort_machine_word::rightmost_bit ( const data_expression &  arg0 )

inline

Application of function symbol @rightmost_bit.

Parameters

arg0	A data expression.

Returns

Application of @rightmost_bit to a number of arguments.

Definition at line 3305 of file machine_word.h.

rightmost_bit_application()

void mcrl2::data::sort_machine_word::rightmost_bit_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 3340 of file machine_word.h.

rightmost_bit_manual_implementation()

void mcrl2::data::sort_machine_word::rightmost_bit_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

The right most bit of a machine number.

The data expression of an application of the function symbol @rightmost_bit.

Parameters

result	The data_expression into which the created object is stored.
e

Returns

true if the rightmost bit is 1.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @rightmost_bit to a number of arguments.

Definition at line 788 of file machine_word.h.

rightmost_bit_name()

const core::identifier_string & mcrl2::data::sort_machine_word::rightmost_bit_name ( )

inline

Generate identifier @rightmost_bit.

Returns

Identifier @rightmost_bit.

Definition at line 3271 of file machine_word.h.

shift_right() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::shift_right ( )

inline

Constructor for function symbol @shift_right.

Returns

Function symbol shift_right.

Definition at line 3362 of file machine_word.h.

shift_right() [2/2]

application mcrl2::data::sort_machine_word::shift_right ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @shift_right.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @shift_right to a number of arguments.

Definition at line 3387 of file machine_word.h.

shift_right_application()

void mcrl2::data::sort_machine_word::shift_right_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 3424 of file machine_word.h.

shift_right_manual_implementation()

void mcrl2::data::sort_machine_word::shift_right_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The machine word shifted one position to the right.

The data expression of an application of the function symbol @shift_right.

Parameters

result	The data_expression into which the created object is stored.
e1	A boolean indicating what the left most bit must be.
e2	The value shifted to the right.

Returns

The machine number e2 divided by 2 prepended with a bit 1 if e1 is true.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @shift_right to a number of arguments.

Definition at line 798 of file machine_word.h.

shift_right_name()

const core::identifier_string & mcrl2::data::sort_machine_word::shift_right_name ( )

inline

Generate identifier @shift_right.

Returns

Identifier @shift_right.

Definition at line 3352 of file machine_word.h.

sqrt_doubleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::sqrt_doubleword ( )

inline

Constructor for function symbol @sqrt_doubleword.

Returns

Function symbol sqrt_doubleword.

Definition at line 2258 of file machine_word.h.

sqrt_doubleword() [2/2]

application mcrl2::data::sort_machine_word::sqrt_doubleword ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @sqrt_doubleword.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @sqrt_doubleword to a number of arguments.

Definition at line 2283 of file machine_word.h.

sqrt_doubleword_application()

void mcrl2::data::sort_machine_word::sqrt_doubleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2320 of file machine_word.h.

sqrt_doubleword_manual_implementation()

void mcrl2::data::sort_machine_word::sqrt_doubleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The square root of base*e1+e2 rounded down.

The data expression of an application of the function symbol @sqrt_doubleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

The square root of base*e1+e2 rounded down.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @sqrt_doubleword to a number of arguments.

Definition at line 678 of file machine_word.h.

sqrt_doubleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::sqrt_doubleword_name ( )

inline

Generate identifier @sqrt_doubleword.

Returns

Identifier @sqrt_doubleword.

Definition at line 2248 of file machine_word.h.

sqrt_quadrupleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::sqrt_quadrupleword ( )

inline

Constructor for function symbol @sqrt_quadrupleword.

Returns

Function symbol sqrt_quadrupleword.

Definition at line 2516 of file machine_word.h.

sqrt_quadrupleword() [2/2]

application mcrl2::data::sort_machine_word::sqrt_quadrupleword ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Application of function symbol @sqrt_quadrupleword.

Parameters

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

Returns

Application of @sqrt_quadrupleword to a number of arguments.

Definition at line 2543 of file machine_word.h.

sqrt_quadrupleword_application()

void mcrl2::data::sort_machine_word::sqrt_quadrupleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2584 of file machine_word.h.

sqrt_quadrupleword_manual_implementation()

void mcrl2::data::sort_machine_word::sqrt_quadrupleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3, const data_expression &  e4  )

inline

Calculates the least significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.

The data expression of an application of the function symbol @sqrt_quadrupleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.
e4	The fourth argument.

Returns

The least significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @sqrt_quadrupleword to a number of arguments.

Definition at line 738 of file machine_word.h.

sqrt_quadrupleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::sqrt_quadrupleword_name ( )

inline

Generate identifier @sqrt_quadrupleword.

Returns

Identifier @sqrt_quadrupleword.

Definition at line 2506 of file machine_word.h.

sqrt_quadrupleword_overflow() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::sqrt_quadrupleword_overflow ( )

inline

Constructor for function symbol @sqrt_quadrupleword_overflow.

Returns

Function symbol sqrt_quadrupleword_overflow.

Definition at line 2606 of file machine_word.h.

sqrt_quadrupleword_overflow() [2/2]

application mcrl2::data::sort_machine_word::sqrt_quadrupleword_overflow ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Application of function symbol @sqrt_quadrupleword_overflow.

Parameters

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

Returns

Application of @sqrt_quadrupleword_overflow to a number of arguments.

Definition at line 2633 of file machine_word.h.

sqrt_quadrupleword_overflow_application()

void mcrl2::data::sort_machine_word::sqrt_quadrupleword_overflow_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2674 of file machine_word.h.

sqrt_quadrupleword_overflow_manual_implementation()

void mcrl2::data::sort_machine_word::sqrt_quadrupleword_overflow_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3, const data_expression &  e4  )

inline

Calculates the most significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.

The data expression of an application of the function symbol @sqrt_quadrupleword_overflow.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.
e4	The fourth argument.

Returns

The most significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @sqrt_quadrupleword_overflow to a number of arguments.

Definition at line 760 of file machine_word.h.

sqrt_quadrupleword_overflow_name()

const core::identifier_string & mcrl2::data::sort_machine_word::sqrt_quadrupleword_overflow_name ( )

inline

Generate identifier @sqrt_quadrupleword_overflow.

Returns

Identifier @sqrt_quadrupleword_overflow.

Definition at line 2596 of file machine_word.h.

sqrt_tripleword() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::sqrt_tripleword ( )

inline

Constructor for function symbol @sqrt_tripleword.

Returns

Function symbol sqrt_tripleword.

Definition at line 2342 of file machine_word.h.

sqrt_tripleword() [2/2]

application mcrl2::data::sort_machine_word::sqrt_tripleword ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @sqrt_tripleword.

Parameters

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

Returns

Application of @sqrt_tripleword to a number of arguments.

Definition at line 2368 of file machine_word.h.

sqrt_tripleword_application()

void mcrl2::data::sort_machine_word::sqrt_tripleword_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2407 of file machine_word.h.

sqrt_tripleword_manual_implementation()

void mcrl2::data::sort_machine_word::sqrt_tripleword_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3  )

inline

Calculates the least significant word of the square root of base*(base*e1+e2)+e3.

The data expression of an application of the function symbol @sqrt_tripleword.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.

Returns

the least significant word of the square root of base*(base*e1+e2)+e3.

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @sqrt_tripleword to a number of arguments.

Definition at line 707 of file machine_word.h.

sqrt_tripleword_name()

const core::identifier_string & mcrl2::data::sort_machine_word::sqrt_tripleword_name ( )

inline

Generate identifier @sqrt_tripleword.

Returns

Identifier @sqrt_tripleword.

Definition at line 2332 of file machine_word.h.

sqrt_tripleword_overflow() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::sqrt_tripleword_overflow ( )

inline

Constructor for function symbol @sqrt_tripleword_overflow.

Returns

Function symbol sqrt_tripleword_overflow.

Definition at line 2429 of file machine_word.h.

sqrt_tripleword_overflow() [2/2]

application mcrl2::data::sort_machine_word::sqrt_tripleword_overflow ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @sqrt_tripleword_overflow.

Parameters

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

Returns

Application of @sqrt_tripleword_overflow to a number of arguments.

Definition at line 2455 of file machine_word.h.

sqrt_tripleword_overflow_application()

void mcrl2::data::sort_machine_word::sqrt_tripleword_overflow_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 2494 of file machine_word.h.

sqrt_tripleword_overflow_manual_implementation()

void mcrl2::data::sort_machine_word::sqrt_tripleword_overflow_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3  )

inline

Calculates the most significant word of the square root of base*(base*e1+e2)+e3.

The data expression of an application of the function symbol @sqrt_tripleword_overflow.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.
e3	The third argument.

Returns

the most significant word of the square root of base*(base*e1+e2)+e3.

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @sqrt_tripleword_overflow to a number of arguments.

Definition at line 722 of file machine_word.h.

sqrt_tripleword_overflow_name()

const core::identifier_string & mcrl2::data::sort_machine_word::sqrt_tripleword_overflow_name ( )

inline

Generate identifier @sqrt_tripleword_overflow.

Returns

Identifier @sqrt_tripleword_overflow.

Definition at line 2419 of file machine_word.h.

sqrt_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::sqrt_word ( )

inline

Constructor for function symbol @sqrt_word.

Returns

Function symbol sqrt_word.

Definition at line 1820 of file machine_word.h.

sqrt_word() [2/2]

application mcrl2::data::sort_machine_word::sqrt_word ( const data_expression &  arg0 )

inline

Application of function symbol @sqrt_word.

Parameters

arg0	A data expression.

Returns

Application of @sqrt_word to a number of arguments.

Definition at line 1844 of file machine_word.h.

sqrt_word_application()

void mcrl2::data::sort_machine_word::sqrt_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1879 of file machine_word.h.

sqrt_word_manual_implementation()

void mcrl2::data::sort_machine_word::sqrt_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

The square root of e, rounded down to a machine word.

The data expression of an application of the function symbol @sqrt_word.

Parameters

result	The data_expression into which the created object is stored.
e	The argument.

Returns

The square root of e rounded down.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @sqrt_word to a number of arguments.

Definition at line 593 of file machine_word.h.

sqrt_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::sqrt_word_name ( )

inline

Generate identifier @sqrt_word.

Returns

Identifier @sqrt_word.

Definition at line 1810 of file machine_word.h.

succ_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::succ_word ( )

inline

Constructor for function symbol @succ_word.

Returns

Function symbol succ_word.

Definition at line 126 of file machine_word.h.

succ_word() [2/2]

application mcrl2::data::sort_machine_word::succ_word ( const data_expression &  arg0 )

inline

Application of function symbol @succ_word.

Parameters

arg0	A data expression.

Returns

Application of @succ_word to a number of arguments.

Definition at line 150 of file machine_word.h.

succ_word_application()

void mcrl2::data::sort_machine_word::succ_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 185 of file machine_word.h.

succ_word_manual_implementation()

void mcrl2::data::sort_machine_word::succ_word_manual_implementation ( data_expression &  result, const data_expression &  e  )

inline

The successor function on a machine numbers, that wraps around.

The data expression of an application of the function symbol @succ_word.

Parameters

result	The data_expression into which the created object is stored.
e

Returns

e+1, or zero if n is the maximum number.

This function is to be implemented manually.

Parameters

arg0	A data expression.

Returns

The data expression corresponding to an application of @succ_word to a number of arguments.

Definition at line 339 of file machine_word.h.

succ_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::succ_word_name ( )

inline

Generate identifier @succ_word.

Returns

Identifier @succ_word.

Definition at line 116 of file machine_word.h.

three_word()

const function_symbol & mcrl2::data::sort_machine_word::three_word ( )

inline

Constructor for function symbol @three_word.

Returns

Function symbol three_word.

Definition at line 338 of file machine_word.h.

three_word_application()

void mcrl2::data::sort_machine_word::three_word_application ( data_expression &  result, const data_expression &  a  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 364 of file machine_word.h.

three_word_manual_implementation()

void mcrl2::data::sort_machine_word::three_word_manual_implementation ( data_expression &  result )

inline

The machine number representing 3.

The data expression of an application of the constant symbol @three_word.

Parameters

result

The data_expression into which the created object is stored.

Returns

The machine number 3.

This function is to be implemented manually. ///

Returns

The data expression corresponding to an application of @three_word to a number of arguments.

Definition at line 250 of file machine_word.h.

three_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::three_word_name ( )

inline

Generate identifier @three_word.

Returns

Identifier @three_word.

Definition at line 328 of file machine_word.h.

times_overflow_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::times_overflow_word ( )

inline

Constructor for function symbol @times_overflow_word.

Returns

Function symbol times_overflow_word.

Definition at line 1313 of file machine_word.h.

times_overflow_word() [2/2]

application mcrl2::data::sort_machine_word::times_overflow_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @times_overflow_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @times_overflow_word to a number of arguments.

Definition at line 1338 of file machine_word.h.

times_overflow_word_application()

void mcrl2::data::sort_machine_word::times_overflow_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1375 of file machine_word.h.

times_overflow_word_manual_implementation()

void mcrl2::data::sort_machine_word::times_overflow_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The result of multiplying two words divided by the maximal representable machine word plus 1.

The data expression of an application of the function symbol @times_overflow_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1*e2 div the maximal machine word+1.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @times_overflow_word to a number of arguments.

Definition at line 515 of file machine_word.h.

times_overflow_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::times_overflow_word_name ( )

inline

Generate identifier @times_overflow_word.

Returns

Identifier @times_overflow_word.

Definition at line 1303 of file machine_word.h.

times_with_carry_overflow_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::times_with_carry_overflow_word ( )

inline

Constructor for function symbol @times_with_carry_overflow_word.

Returns

Function symbol times_with_carry_overflow_word.

Definition at line 1397 of file machine_word.h.

times_with_carry_overflow_word() [2/2]

application mcrl2::data::sort_machine_word::times_with_carry_overflow_word ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @times_with_carry_overflow_word.

Parameters

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

Returns

Application of @times_with_carry_overflow_word to a number of arguments.

Definition at line 1423 of file machine_word.h.

times_with_carry_overflow_word_application()

void mcrl2::data::sort_machine_word::times_with_carry_overflow_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1462 of file machine_word.h.

times_with_carry_overflow_word_manual_implementation()

void mcrl2::data::sort_machine_word::times_with_carry_overflow_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3  )

inline

The result of multiplying two words and adding a third divided by the maximal representable machine word plus 1.

The data expression of an application of the function symbol @times_with_carry_overflow_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1*e2 div the maximal machine word+1.

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @times_with_carry_overflow_word to a number of arguments.

Definition at line 528 of file machine_word.h.

times_with_carry_overflow_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::times_with_carry_overflow_word_name ( )

inline

Generate identifier @times_with_carry_overflow_word.

Returns

Identifier @times_with_carry_overflow_word.

Definition at line 1387 of file machine_word.h.

times_with_carry_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::times_with_carry_word ( )

inline

Constructor for function symbol @times_with_carry_word.

Returns

Function symbol times_with_carry_word.

Definition at line 1226 of file machine_word.h.

times_with_carry_word() [2/2]

application mcrl2::data::sort_machine_word::times_with_carry_word ( const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @times_with_carry_word.

Parameters

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

Returns

Application of @times_with_carry_word to a number of arguments.

Definition at line 1252 of file machine_word.h.

times_with_carry_word_application()

void mcrl2::data::sort_machine_word::times_with_carry_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1291 of file machine_word.h.

times_with_carry_word_manual_implementation()

void mcrl2::data::sort_machine_word::times_with_carry_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2, const data_expression &  e3  )

inline

The result of multiplying two words and adding the third modulo the maximal representable machine word plus 1.

The data expression of an application of the function symbol @times_with_carry_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1*e2+e3 modulo the machine word.

This function is to be implemented manually.

Parameters

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

Returns

The data expression corresponding to an application of @times_with_carry_word to a number of arguments.

Definition at line 501 of file machine_word.h.

times_with_carry_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::times_with_carry_word_name ( )

inline

Generate identifier @times_with_carry_word.

Returns

Identifier @times_with_carry_word.

Definition at line 1216 of file machine_word.h.

times_word() [1/2]

const function_symbol & mcrl2::data::sort_machine_word::times_word ( )

inline

Constructor for function symbol @times_word.

Returns

Function symbol times_word.

Definition at line 1142 of file machine_word.h.

times_word() [2/2]

application mcrl2::data::sort_machine_word::times_word ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @times_word.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

Application of @times_word to a number of arguments.

Definition at line 1167 of file machine_word.h.

times_word_application()

void mcrl2::data::sort_machine_word::times_word_application ( data_expression &  result, const data_expression &  a1  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 1204 of file machine_word.h.

times_word_manual_implementation()

void mcrl2::data::sort_machine_word::times_word_manual_implementation ( data_expression &  result, const data_expression &  e1, const data_expression &  e2  )

inline

The result of multiplying two words modulo the maximal representable machine word plus 1.

The data expression of an application of the function symbol @times_word.

Parameters

result	The data_expression into which the created object is stored.
e1	The first argument.
e2	The second argument.

Returns

e1*e2 modulo the machine word.

This function is to be implemented manually.

Parameters

arg0	A data expression.
arg1	A data expression.

Returns

The data expression corresponding to an application of @times_word to a number of arguments.

Definition at line 488 of file machine_word.h.

times_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::times_word_name ( )

inline

Generate identifier @times_word.

Returns

Identifier @times_word.

Definition at line 1132 of file machine_word.h.

two_word()

const function_symbol & mcrl2::data::sort_machine_word::two_word ( )

inline

Constructor for function symbol @two_word.

Returns

Function symbol two_word.

Definition at line 290 of file machine_word.h.

two_word_application()

void mcrl2::data::sort_machine_word::two_word_application ( data_expression &  result, const data_expression &  a  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 316 of file machine_word.h.

two_word_manual_implementation()

void mcrl2::data::sort_machine_word::two_word_manual_implementation ( data_expression &  result )

inline

The machine number representing 2.

The data expression of an application of the constant symbol @two_word.

Parameters

result

The data_expression into which the created object is stored.

Returns

The machine number 2.

This function is to be implemented manually. ///

Returns

The data expression corresponding to an application of @two_word to a number of arguments.

Definition at line 242 of file machine_word.h.

two_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::two_word_name ( )

inline

Generate identifier @two_word.

Returns

Identifier @two_word.

Definition at line 280 of file machine_word.h.

zero_word()

const function_symbol & mcrl2::data::sort_machine_word::zero_word ( )

inline

Constructor for function symbol @zero_word.

Returns

Function symbol zero_word.

Definition at line 78 of file machine_word.h.

zero_word_application()

void mcrl2::data::sort_machine_word::zero_word_application ( data_expression &  result, const data_expression &  a  )

inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 104 of file machine_word.h.

zero_word_manual_implementation()

void mcrl2::data::sort_machine_word::zero_word_manual_implementation ( data_expression &  result )

inline

The machine number representing 0.

The data expression of an application of the constant symbol @zero_word.

Parameters

result

The data_expression into which the created object is stored.

Returns

The machine number 0.

This function is to be implemented manually. ///

Returns

The data expression corresponding to an application of @zero_word to a number of arguments.

Definition at line 226 of file machine_word.h.

zero_word_name()

const core::identifier_string & mcrl2::data::sort_machine_word::zero_word_name ( )

inline

Generate identifier @zero_word.

Returns

Identifier @zero_word.

Definition at line 68 of file machine_word.h.