machine_word.h File Reference

Go to the source code of this file.

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::data
	Namespace for all data library functionality.
namespace	mcrl2::data::sort_machine_word
	Namespace for system defined sort machine_word.
namespace	mcrl2::data::sort_machine_word::detail

Functions
const machine_number &	mcrl2::data::sort_machine_word::detail::zero_word ()
const machine_number &	mcrl2::data::sort_machine_word::detail::one_word ()
const machine_number &	mcrl2::data::sort_machine_word::detail::two_word ()
const machine_number &	mcrl2::data::sort_machine_word::detail::three_word ()
const machine_number &	mcrl2::data::sort_machine_word::detail::four_word ()
const machine_number &	mcrl2::data::sort_machine_word::detail::max_word ()
bool	mcrl2::data::sort_machine_word::detail::equals_zero_word (const std::size_t n)
bool	mcrl2::data::sort_machine_word::detail::equals_one_word (const std::size_t n)
bool	mcrl2::data::sort_machine_word::detail::equals_max_word (const std::size_t n)
std::size_t	mcrl2::data::sort_machine_word::detail::succ_word (const std::size_t n)
bool	mcrl2::data::sort_machine_word::detail::equal_word (const std::size_t n1, const std::size_t n2)
bool	mcrl2::data::sort_machine_word::detail::less_word (const std::size_t n1, const std::size_t n2)
bool	mcrl2::data::sort_machine_word::detail::less_equal_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::add_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::add_with_carry_word (const std::size_t n1, const std::size_t n2)
bool	mcrl2::data::sort_machine_word::detail::add_overflow_word (const std::size_t n1, const std::size_t n2)
bool	mcrl2::data::sort_machine_word::detail::add_with_carry_overflow_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::times_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::times_with_carry_word (const std::size_t n1, const std::size_t n2, const std::size_t n3)
std::size_t	mcrl2::data::sort_machine_word::detail::times_overflow_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::times_with_carry_overflow_word (const std::size_t n1, const std::size_t n2, std::size_t n3)
std::size_t	mcrl2::data::sort_machine_word::detail::minus_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::monus_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::div_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::mod_word (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::div_doubleword (const std::size_t n1, const std::size_t n2, const std::size_t n3)
std::size_t	mcrl2::data::sort_machine_word::detail::mod_doubleword (const std::size_t n1, const std::size_t n2, const std::size_t n3)
std::size_t	mcrl2::data::sort_machine_word::detail::div_double_doubleword (const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4)
std::size_t	mcrl2::data::sort_machine_word::detail::mod_double_doubleword (const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4)
std::size_t	mcrl2::data::sort_machine_word::detail::div_triple_doubleword (const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4, const std::size_t n5)
std::size_t	mcrl2::data::sort_machine_word::detail::sqrt_word (const std::size_t n)
std::size_t	mcrl2::data::sort_machine_word::detail::sqrt_doubleword (const std::size_t n1, const std::size_t n2)
std::size_t	mcrl2::data::sort_machine_word::detail::sqrt_tripleword (const std::size_t n1, const std::size_t n2, const std::size_t n3)
std::size_t	mcrl2::data::sort_machine_word::detail::sqrt_tripleword_overflow (const std::size_t n1, const std::size_t n2, const std::size_t n3)
std::size_t	mcrl2::data::sort_machine_word::detail::sqrt_quadrupleword (const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4)
std::size_t	mcrl2::data::sort_machine_word::detail::sqrt_quadrupleword_overflow (const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4)
std::size_t	mcrl2::data::sort_machine_word::detail::pred_word (const std::size_t n)
void	mcrl2::data::sort_machine_word::detail::rightmost_bit (data_expression &result, const std::size_t n)
std::size_t	mcrl2::data::sort_machine_word::detail::shift_right (const data_expression &e1, const std::size_t n)
void	mcrl2::data::sort_machine_word::zero_word_manual_implementation (data_expression &result)
	The machine number representing 0.
void	mcrl2::data::sort_machine_word::one_word_manual_implementation (data_expression &result)
	The machine number representing 1.
void	mcrl2::data::sort_machine_word::two_word_manual_implementation (data_expression &result)
	The machine number representing 2.
void	mcrl2::data::sort_machine_word::three_word_manual_implementation (data_expression &result)
	The machine number representing 3.
void	mcrl2::data::sort_machine_word::four_word_manual_implementation (data_expression &result)
	The machine number representing 4.
void	mcrl2::data::sort_machine_word::max_word_manual_implementation (data_expression &result)
	The largest representable machine number.
void	mcrl2::data::sort_machine_word::equals_zero_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is equal to 0.
void	mcrl2::data::sort_machine_word::not_equals_zero_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is not equal to 0.
void	mcrl2::data::sort_machine_word::equals_one_word_manual_implementation (data_expression &result, const data_expression &e)
	Checks whether the argument is equal to 1.
void	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::succ_word_manual_implementation (data_expression &result, const data_expression &e)
	The successor function on a machine numbers, that wraps around.
void	mcrl2::data::sort_machine_word::equal_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The equality function on two machine words.
void	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::less_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The less than function on two machine words.
void	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::greater_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The greater than function on two machine words.
void	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	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)
	The result of multiplying two words and adding the third modulo the maximal representable machine word plus 1.
void	mcrl2::data::sort_machine_word::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	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)
	The result of multiplying two words and adding a third divided by the maximal representable machine word plus 1.
void	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::mod_word_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	Calculates e1 modulo e2.
void	mcrl2::data::sort_machine_word::sqrt_word_manual_implementation (data_expression &result, const data_expression &e)
	The square root of e, rounded down to a machine word.
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)
	Calculates (base*e1 + e2) div e3.
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)
	Calculates (base*e1 + e2) div (base*e3 + e4).
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)
	Calculates (base*(base*e1 + e2)+e3) div (base*e4 + e5).
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)
	Calculates (base*e1 + e2) mod (base*e3 + e4).
void	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	mcrl2::data::sort_machine_word::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	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)
	Calculates the most significant word of the square root of base*(base*e1+e2)+e3.
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)
	Calculates the least significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.
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)
	Calculates the most significant word of the square root of base*(base*(base*e1+e2)+e3)+e4.
void	mcrl2::data::sort_machine_word::pred_word_manual_implementation (data_expression &result, const data_expression &e)
	The predecessor function on a machine numbers, that wraps around.
void	mcrl2::data::sort_machine_word::rightmost_bit_manual_implementation (data_expression &result, const data_expression &e)
	The right most bit of a machine number.
void	mcrl2::data::sort_machine_word::shift_right_manual_implementation (data_expression &result, const data_expression &e1, const data_expression &e2)
	The machine word shifted one position to the right.