Classes
struct	atomic_wrapper

class	bucket_list
	This essentially implements the std::forward_list, with the difference that it does not own the nodes in the list. It just keeps track of the list next pointers. More...

struct	command

class	free_list
	This essentially implements the std::forward_list, with the difference that it does not own the nodes in the list. It just keeps track of the list next pointers. Furthermore this assumes that the objects in the list will not be accessed, so it stores the next pointer within the Element. More...

struct	is_transparent

struct	is_transparent< X, void_t< typename X::is_transparent > >

struct	position_counter

struct	Sentinel

class	transform_tool

Typedefs
template<typename... >
using	void_t = void

Functions
template<typename Key , bool ThreadSafe = false, typename Hash = std::hash<Key>, typename Equals = std::equal_to<Key>, typename Allocator = std::allocator<Key>, typename KeyTable = atermpp::deque<Key >>
bool	contains (const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)

std::size_t	add_single_number (const std::size_t n1, const std::size_t n2, std::size_t &carry)

std::size_t	subtract_single_number (const std::size_t n1, const std::size_t n2, std::size_t &carry)

std::size_t	multiply_single_number (const std::size_t n1, const std::size_t n2, std::size_t &multiplication_carry)

std::size_t	divide_single_number (const std::size_t p, const std::size_t q, std::size_t &remainder)

std::size_t	greatest_common_divisor (std::size_t p, std::size_t q)

void	remove_common_divisor (std::size_t &p, std::size_t &q)

template<typename Allocator , typename ... Args>
auto	allocate (Allocator &allocator, const Args &... args) -> decltype(allocator.allocate_args(args...))
	A compile time check for allocate_args in the given allocator, calls allocate(1) otherwise.

template<typename Allocator , typename ... Args>
auto	allocate (Allocator &allocator, const Args &...) -> decltype(allocator.allocate(1))

template<typename Map >
Map::mapped_type	map_element (const Map &m, const typename Map::key_type &key)
	Returns the value corresponding to the given key in the map m. If the key is not present, an exception is thrown.

template<typename Map >
Map::mapped_type	mapped_value (const Map &m, const typename Map::key_type &key, const typename Map::mapped_type &undefined_value)

template<typename Container >
bool	contains (const Container &c, const typename Container::value_type &v)
	Returns the value corresponding to the given key in the set m. If the key is not present, an exception is thrown.

template<typename T >
bool	contains (const std::set< T > &c, const typename std::set< T >::value_type &v)

template<typename T >
bool	contains (const std::multiset< T > &c, const typename std::multiset< T >::value_type &v)

template<typename T >
bool	contains (const std::unordered_set< T > &c, const typename std::set< T >::value_type &v)

template<typename Key , typename T >
bool	has_key (const std::map< Key, T > &c, const Key &v)
	Returns the value corresponding to the given key in the set m. If the key is not present, an exception is thrown.

template<typename Key , typename T >
bool	has_key (const std::multimap< Key, T > &c, const Key &v)
	Returns the value corresponding to the given key in the set m. If the key is not present, an exception is thrown.

template<typename Container >
Container::value_type	pick_element (Container &v)

template<typename T , typename Container >
void	set_insert (std::set< T > &s, const Container &c)

template<typename T , typename Container >
void	set_remove (std::set< T > &s, const Container &c)

template<typename ContainerT , typename PredicateT >
void	remove_if (ContainerT &items, const PredicateT &predicate)

template<typename InputIterator1 , typename InputIterator2 >
bool	has_empty_intersection (InputIterator1 first1, InputIterator1 last1, InputIterator2 first2, InputIterator2 last2)
	Returns true if the sorted ranges [first1, ..., last1) and [first2, ..., last2) have an empty intersection.

template<typename SetContainer1 , typename SetContainer2 >
bool	has_empty_intersection (const SetContainer1 &s1, const SetContainer2 &s2)

template<typename T >
std::set< T >	set_union (const std::set< T > &x, const std::set< T > &y)
	Returns the union of two sets.

template<typename T >
std::set< T >	set_difference (const std::set< T > &x, const std::set< T > &y)
	Returns the difference of two sets.

template<typename T >
std::set< T >	set_intersection (const std::set< T > &x, const std::set< T > &y)
	Returns the intersection of two sets.

template<typename T >
bool	set_includes (const std::set< T > &x, const std::set< T > &y)
	Returns if y is included in x.

template<typename T >
std::vector< T >	as_vector (const std::set< T > &x)

template<typename T >
std::set< T >	as_set (const std::vector< T > &x)

static constexpr std::size_t	EMPTY (std::numeric_limits< std::size_t >::max())
	in the hashtable we use the following constant to indicate free positions.

static constexpr std::size_t	RESERVED (std::numeric_limits< std::size_t >::max() -1)

std::string	read_text (const std::string &filename)
	Reads text from the file filename, or from stdin if filename equals "-".

void	write_text (const std::string &filename, const std::string &text)
	Saves text to the file filename, or to stdout if filename equals "-".

template<class Iter , class T >
void	iota (Iter first, Iter last, T value)
	Generates the sequence value, value + 1, ... and writes it to the sequence [first, last)

template<typename T , typename OutputIterator , typename MatchFunction , typename AccessorFunction1 , typename AccessorFunction2 >
void	split (const T &t, OutputIterator i, MatchFunction match, AccessorFunction1 lhs, AccessorFunction2 rhs)
	Splits a binary tree T into a sequence, and writes the result to the output range given by an output iterator.

template<typename T , typename FwdIt , typename BinaryOperation >
T	join (FwdIt first, FwdIt last, BinaryOperation op, T empty_sequence_result)
	Given a sequence [t1, t2, ..., tn] of elements of type T, returns op(t1, op(t2, ...), tn)))).

template<typename T , typename RndIt , typename BinaryOperation >
T	join_balanced (RndIt first, RndIt last, BinaryOperation op)
	Given a non-empty sequence [t1, t2, ..., tn] of elements of type T, returns op(op(t1, op(t2, ...), tn)))). The height of the resulting expression tree is minimal.

std::pair< std::string, std::string >	separate_keyword_section (const std::string &text1, const std::string &keyword, const std::vector< std::string > &all_keywords, bool repeat_keyword=false)

std::vector< std::string >	split_text (const std::string &text, const std::string &keyword)

std::map< std::string, std::string >	split_text_using_keywords (const std::string &text, const std::vector< std::string > &keywords)

std::vector< std::string >	nonempty_lines (const std::string &text)

template<typename T >
T	identity (T t)

template<typename Parser , typename Operation1 , typename Operation2 , typename Compare >
bool	test_operation (const std::string &expr1, const std::string &expr2, Parser parse, Compare comp, Operation1 op1, const std::string &opname1, Operation2 op2, const std::string &opname2)
	Generic function that applies two operations to two objects, and compares the results.

template<typename Parser , typename Operation , typename Compare >
bool	test_operation (const std::string &expr1, const std::string &expr2, Parser parse, Compare comp, Operation op, const std::string &opname)
	Generic function that applies an operation to an object, and compares it with another object.

std::size_t	hash_combine (const std::size_t h1, const std::size_t h2)

std::size_t	hash_combine_cheap (const std::size_t seed, const std::size_t hash_number)
	Auxiliary function to combine seed with a hash number.

template<typename Iterator >
Iterator	parse_next_natural_number (Iterator first, Iterator last, std::size_t &result)

Variables
static constexpr bool	GlobalThreadSafe
	Enables thread safety for the whole toolset.

static constexpr Sentinel	EndIterator = {}
	A end of the iterator sentinel.

static const std::size_t	STEP = 1
	The position on which the next hash entry is searched.

static constexpr float	max_load_factor = 0.6f
	The load factor before the hash table is resized.

static constexpr std::size_t	PRIME_NUMBER = 999953

static constexpr std::size_t	minimal_hashtable_size = 16

static constexpr std::size_t	RESERVATION_FRACTION = 8

Typedef Documentation

◆ void_t

template<typename... >

using mcrl2::utilities::detail::void_t = typedef void

Definition at line 46 of file unordered_set.h.

Function Documentation

◆ add_single_number()

std::size_t mcrl2::utilities::detail::add_single_number	(	const std::size_t	n1,
		const std::size_t	n2,
		std::size_t &	carry
	)

inline

Definition at line 49 of file big_numbers.h.

◆ allocate() [1/2]

template<typename Allocator , typename ... Args>

auto mcrl2::utilities::detail::allocate	(	Allocator &	allocator,
		const Args &...	args
	)		-> decltype(allocator.allocate_args(args...))

inline

A compile time check for allocate_args in the given allocator, calls allocate(1) otherwise.

Definition at line 32 of file bucket_list.h.

◆ allocate() [2/2]

template<typename Allocator , typename ... Args>

auto mcrl2::utilities::detail::allocate	(	Allocator &	allocator,
		const Args &	...
	)		-> decltype(allocator.allocate(1))

inline

Definition at line 38 of file bucket_list.h.

◆ as_set()

template<typename T >

std::set< T > mcrl2::utilities::detail::as_set ( const std::vector< T > & x )

Definition at line 229 of file container_utility.h.

◆ as_vector()

template<typename T >

std::vector< T > mcrl2::utilities::detail::as_vector ( const std::set< T > & x )

Definition at line 223 of file container_utility.h.

◆ contains() [1/5]

template<typename Key , bool ThreadSafe = false, typename Hash = std::hash<Key>, typename Equals = std::equal_to<Key>, typename Allocator = std::allocator<Key>, typename KeyTable = atermpp::deque<Key >>

bool mcrl2::utilities::detail::contains	(	const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &	c,
		const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &	v,
		const std::size_t	thread_index = `0`
	)

Definition at line 86 of file indexed_set.h.

◆ contains() [2/5]

template<typename Container >

bool mcrl2::utilities::detail::contains	(	const Container &	c,
		const typename Container::value_type &	v
	)

Returns the value corresponding to the given key in the set m. If the key is not present, an exception is thrown.

Definition at line 57 of file container_utility.h.

◆ contains() [3/5]

template<typename T >

bool mcrl2::utilities::detail::contains	(	const std::multiset< T > &	c,
		const typename std::multiset< T >::value_type &	v
	)

Definition at line 71 of file container_utility.h.

◆ contains() [4/5]

template<typename T >

bool mcrl2::utilities::detail::contains	(	const std::set< T > &	c,
		const typename std::set< T >::value_type &	v
	)

Definition at line 64 of file container_utility.h.

◆ contains() [5/5]

template<typename T >

bool mcrl2::utilities::detail::contains	(	const std::unordered_set< T > &	c,
		const typename std::set< T >::value_type &	v
	)

Definition at line 78 of file container_utility.h.

◆ divide_single_number()

std::size_t mcrl2::utilities::detail::divide_single_number	(	const std::size_t	p,
		const std::size_t	q,
		std::size_t &	remainder
	)

inline

Definition at line 128 of file big_numbers.h.

◆ EMPTY()

static constexpr std::size_t mcrl2::utilities::detail::EMPTY ( std::numeric_limits< std::size_t > ::max() )

staticconstexpr

in the hashtable we use the following constant to indicate free positions.

◆ greatest_common_divisor()

std::size_t mcrl2::utilities::detail::greatest_common_divisor	(	std::size_t	p,
		std::size_t	q
	)

inline

Definition at line 154 of file big_numbers.h.

◆ has_empty_intersection() [1/2]

template<typename SetContainer1 , typename SetContainer2 >

bool mcrl2::utilities::detail::has_empty_intersection	(	const SetContainer1 &	s1,
		const SetContainer2 &	s2
	)

Definition at line 170 of file container_utility.h.

◆ has_empty_intersection() [2/2]

template<typename InputIterator1 , typename InputIterator2 >

bool mcrl2::utilities::detail::has_empty_intersection	(	InputIterator1	first1,
		InputIterator1	last1,
		InputIterator2	first2,
		InputIterator2	last2
	)

Returns true if the sorted ranges [first1, ..., last1) and [first2, ..., last2) have an empty intersection.

Definition at line 149 of file container_utility.h.

◆ has_key() [1/2]

template<typename Key , typename T >

bool mcrl2::utilities::detail::has_key	(	const std::map< Key, T > &	c,
		const Key &	v
	)

Returns the value corresponding to the given key in the set m. If the key is not present, an exception is thrown.

Definition at line 86 of file container_utility.h.

◆ has_key() [2/2]

template<typename Key , typename T >

bool mcrl2::utilities::detail::has_key	(	const std::multimap< Key, T > &	c,
		const Key &	v
	)

Returns the value corresponding to the given key in the set m. If the key is not present, an exception is thrown.

Definition at line 94 of file container_utility.h.

◆ hash_combine()

std::size_t mcrl2::utilities::detail::hash_combine	(	const std::size_t	h1,
		const std::size_t	h2
	)

inline

Definition at line 32 of file hash_utility.h.

◆ hash_combine_cheap()

std::size_t mcrl2::utilities::detail::hash_combine_cheap	(	const std::size_t	seed,
		const std::size_t	hash_number
	)

inline

Auxiliary function to combine seed with a hash number.

Definition at line 39 of file hash_utility.h.

◆ identity()

template<typename T >

T mcrl2::utilities::detail::identity ( T t )

Definition at line 29 of file test_operation.h.

◆ iota()

template<class Iter , class T >

void mcrl2::utilities::detail::iota	(	Iter	first,
		Iter	last,
		T	value
	)

Generates the sequence value, value + 1, ... and writes it to the sequence [first, last)

Parameters

first	Start of a sequence
last	End of a sequence
value	A value

Definition at line 29 of file iota.h.

◆ join()

template<typename T , typename FwdIt , typename BinaryOperation >

T mcrl2::utilities::detail::join	(	FwdIt	first,
		FwdIt	last,
		BinaryOperation	op,
		T	empty_sequence_result
	)

Given a sequence [t1, t2, ..., tn] of elements of type T, returns op(t1, op(t2, ...), tn)))).

Parameters

empty_sequence_result	The value that is returned when the sequence is empty.
first	[first, last) is the range of elements.
last
op	An operator

Returns: The joined sequence

Definition at line 55 of file join.h.

◆ join_balanced()

template<typename T , typename RndIt , typename BinaryOperation >

T mcrl2::utilities::detail::join_balanced	(	RndIt	first,
		RndIt	last,
		BinaryOperation	op
	)

Given a non-empty sequence [t1, t2, ..., tn] of elements of type T, returns op(op(t1, op(t2, ...), tn)))). The height of the resulting expression tree is minimal.

Parameters

first	[first, last) is the range of elements.
last
op	An operator

Returns: The joined sequence

Definition at line 76 of file join.h.

◆ map_element()

template<typename Map >

Map::mapped_type mcrl2::utilities::detail::map_element	(	const Map &	m,
		const typename Map::key_type &	key
	)

Returns the value corresponding to the given key in the map m. If the key is not present, an exception is thrown.

Definition at line 30 of file container_utility.h.

◆ mapped_value()

template<typename Map >

Map::mapped_type mcrl2::utilities::detail::mapped_value	(	const Map &	m,
		const typename Map::key_type &	key,
		const typename Map::mapped_type &	undefined_value
	)

Definition at line 44 of file container_utility.h.

◆ multiply_single_number()

std::size_t mcrl2::utilities::detail::multiply_single_number	(	const std::size_t	n1,
		const std::size_t	n2,
		std::size_t &	multiplication_carry
	)

inline

Definition at line 95 of file big_numbers.h.

◆ nonempty_lines()

std::vector< std::string > mcrl2::utilities::detail::nonempty_lines ( const std::string & text )

inline

Definition at line 59 of file split.h.

◆ parse_next_natural_number()

template<typename Iterator >

Iterator mcrl2::utilities::detail::parse_next_natural_number	(	Iterator	first,
		Iterator	last,
		std::size_t &	result
	)

Definition at line 32 of file parse_numbers.h.

◆ pick_element()

template<typename Container >

Container::value_type mcrl2::utilities::detail::pick_element ( Container & v )

Definition at line 101 of file container_utility.h.

◆ read_text()

std::string mcrl2::utilities::detail::read_text ( const std::string & filename )

inline

Reads text from the file filename, or from stdin if filename equals "-".

Definition at line 27 of file io.h.

◆ remove_common_divisor()

void mcrl2::utilities::detail::remove_common_divisor	(	std::size_t &	p,
		std::size_t &	q
	)

inline

Definition at line 173 of file big_numbers.h.

◆ remove_if()

template<typename ContainerT , typename PredicateT >

void mcrl2::utilities::detail::remove_if	(	ContainerT &	items,
		const PredicateT &	predicate
	)

Definition at line 132 of file container_utility.h.

◆ RESERVED()

static constexpr std::size_t mcrl2::utilities::detail::RESERVED ( std::numeric_limits< std::size_t >::max() - 1 )

staticconstexpr

◆ separate_keyword_section()

std::pair< std::string, std::string > mcrl2::utilities::detail::separate_keyword_section	(	const std::string &	text1,
		const std::string &	keyword,
		const std::vector< std::string > &	all_keywords,
		bool	repeat_keyword = `false`
	)

inline

Definition at line 29 of file separate_keyword_section.h.

◆ set_difference()

template<typename T >

std::set< T > mcrl2::utilities::detail::set_difference	(	const std::set< T > &	x,
		const std::set< T > &	y
	)

Returns the difference of two sets.

Parameters

x	A set
y	A set

Returns: The difference of two sets.

Definition at line 192 of file container_utility.h.

◆ set_includes()

template<typename T >

bool mcrl2::utilities::detail::set_includes	(	const std::set< T > &	x,
		const std::set< T > &	y
	)

Returns if y is included in x.

Parameters

x	A set
y	A set

Returns: The intersection of two sets.

Definition at line 216 of file container_utility.h.

◆ set_insert()

template<typename T , typename Container >

void mcrl2::utilities::detail::set_insert	(	std::set< T > &	s,
		const Container &	c
	)

Definition at line 111 of file container_utility.h.

◆ set_intersection()

template<typename T >

std::set< T > mcrl2::utilities::detail::set_intersection	(	const std::set< T > &	x,
		const std::set< T > &	y
	)

Returns the intersection of two sets.

Parameters

x	A set
y	A set

Returns: The intersection of two sets.

Definition at line 204 of file container_utility.h.

◆ set_remove()

template<typename T , typename Container >

void mcrl2::utilities::detail::set_remove	(	std::set< T > &	s,
		const Container &	c
	)

Definition at line 121 of file container_utility.h.

◆ set_union()

template<typename T >

std::set< T > mcrl2::utilities::detail::set_union	(	const std::set< T > &	x,
		const std::set< T > &	y
	)

Returns the union of two sets.

Parameters

x	A set
y	A set

Returns: The union of two sets.

Definition at line 180 of file container_utility.h.

◆ split()

template<typename T , typename OutputIterator , typename MatchFunction , typename AccessorFunction1 , typename AccessorFunction2 >

void mcrl2::utilities::detail::split	(	const T &	t,
		OutputIterator	i,
		MatchFunction	match,
		AccessorFunction1	lhs,
		AccessorFunction2	rhs
	)

Splits a binary tree T into a sequence, and writes the result to the output range given by an output iterator.

Parameters

t	The tree that has to be split.
i	The output iterator.
match	If this functions returns true in a node, the node will be split.
lhs	Function for getting the left subtree of a node.
rhs	Function for getting the right subtree of a node.

Definition at line 34 of file join.h.

◆ split_text()

std::vector< std::string > mcrl2::utilities::detail::split_text	(	const std::string &	text,
		const std::string &	keyword
	)

inline

Definition at line 26 of file split.h.

◆ split_text_using_keywords()

std::map< std::string, std::string > mcrl2::utilities::detail::split_text_using_keywords	(	const std::string &	text,
		const std::vector< std::string > &	keywords
	)

inline

Definition at line 43 of file split.h.

◆ subtract_single_number()

std::size_t mcrl2::utilities::detail::subtract_single_number	(	const std::size_t	n1,
		const std::size_t	n2,
		std::size_t &	carry
	)

inline

Definition at line 72 of file big_numbers.h.

◆ test_operation() [1/2]

template<typename Parser , typename Operation , typename Compare >

bool mcrl2::utilities::detail::test_operation	(	const std::string &	expr1,
		const std::string &	expr2,
		Parser	parse,
		Compare	comp,
		Operation	op,
		const std::string &	opname
	)

Generic function that applies an operation to an object, and compares it with another object.

Definition at line 76 of file test_operation.h.

◆ test_operation() [2/2]

template<typename Parser , typename Operation1 , typename Operation2 , typename Compare >

bool mcrl2::utilities::detail::test_operation	(	const std::string &	expr1,
		const std::string &	expr2,
		Parser	parse,
		Compare	comp,
		Operation1	op1,
		const std::string &	opname1,
		Operation2	op2,
		const std::string &	opname2
	)

Generic function that applies two operations to two objects, and compares the results.

Definition at line 36 of file test_operation.h.

◆ write_text()

void mcrl2::utilities::detail::write_text	(	const std::string &	filename,
		const std::string &	text
	)

inline

Saves text to the file filename, or to stdout if filename equals "-".

Definition at line 46 of file io.h.

Variable Documentation

◆ EndIterator

constexpr Sentinel mcrl2::utilities::detail::EndIterator = {}

staticconstexpr

A end of the iterator sentinel.

Definition at line 28 of file bucket_list.h.

◆ GlobalThreadSafe

constexpr bool mcrl2::utilities::detail::GlobalThreadSafe

staticconstexpr

Initial value:

=     
 
    false

Enables thread safety for the whole toolset.

Definition at line 17 of file configuration.h.

◆ max_load_factor

constexpr float mcrl2::utilities::detail::max_load_factor = 0.6f

staticconstexpr

The load factor before the hash table is resized.

Definition at line 34 of file indexed_set.h.

◆ minimal_hashtable_size

constexpr std::size_t mcrl2::utilities::detail::minimal_hashtable_size = 16

staticconstexpr

Definition at line 39 of file indexed_set.h.

◆ PRIME_NUMBER

constexpr std::size_t mcrl2::utilities::detail::PRIME_NUMBER = 999953

staticconstexpr

Definition at line 36 of file indexed_set.h.

◆ RESERVATION_FRACTION

constexpr std::size_t mcrl2::utilities::detail::RESERVATION_FRACTION = 8

staticconstexpr

Definition at line 43 of file indexed_set.h.

◆ STEP

const std::size_t mcrl2::utilities::detail::STEP = 1

static

The position on which the next hash entry is searched.

Definition at line 27 of file indexed_set.h.

Classes

Typedefs

Functions

Variables

Typedef Documentation

◆ void_t

Function Documentation

◆ add_single_number()

◆ allocate() [1/2]

◆ allocate() [2/2]

◆ as_set()

◆ as_vector()

◆ contains() [1/5]

◆ contains() [2/5]

◆ contains() [3/5]

◆ contains() [4/5]

◆ contains() [5/5]

◆ divide_single_number()

◆ EMPTY()

◆ greatest_common_divisor()

◆ has_empty_intersection() [1/2]

◆ has_empty_intersection() [2/2]

◆ has_key() [1/2]

◆ has_key() [2/2]

◆ hash_combine()

◆ hash_combine_cheap()

◆ identity()

◆ iota()

◆ join()

◆ join_balanced()

◆ map_element()

◆ mapped_value()

◆ multiply_single_number()

◆ nonempty_lines()

◆ parse_next_natural_number()

◆ pick_element()

◆ read_text()

◆ remove_common_divisor()

◆ remove_if()

◆ RESERVED()

◆ separate_keyword_section()

◆ set_difference()

◆ set_includes()

◆ set_insert()

◆ set_intersection()

◆ set_remove()

◆ set_union()

◆ split()

◆ split_text()

◆ split_text_using_keywords()

◆ subtract_single_number()

◆ test_operation() [1/2]

◆ test_operation() [2/2]

◆ write_text()

Variable Documentation

◆ EndIterator

◆ GlobalThreadSafe

◆ max_load_factor

◆ minimal_hashtable_size

◆ PRIME_NUMBER

◆ RESERVATION_FRACTION

◆ STEP