Miscellaneous helper functions

Modules
	Graph Data Structures
	Hashing functions
	Random functions

Classes
struct	spot::bdd_less_than
	Comparison functor for BDDs. More...
struct	spot::bdd_less_than_stable
	Comparison functor for BDDs. More...
struct	spot::bdd_hash
	Hash functor for BDDs. More...
class	spot::bitset< N >
	A fixed-size bitset backed by N unsigned words. More...
class	spot::printable
	Abstract base class for objects that can be printed to a stream via a format string. More...
struct	spot::char_ptr_less_than
	Strict Weak Ordering for char*. More...
class	spot::minato_isop
	Generate an irredundant sum-of-products (ISOP) form of a BDD function. More...
class	spot::option_map
	Manage a map of options. More...
class	spot::satsolver_command
	Interface with a given sat solver. More...
struct	spot::stopwatch
	A simple stopwatch. More...
class	spot::temporary_file
	Temporary file name. More...
class	spot::trival
	A class implementing Kleene's three-valued logic. More...

Functions
template<typename T , typename U >
T	spot::down_cast (U *u) noexcept
template<typename T , typename U >
T	spot::down_cast (const std::shared_ptr< U > &u) noexcept
template<typename T , typename U >
T	spot::down_cast (U u)
template<typename Type , typename = std::enable_if_t<std::is_unsigned<Type>::value>>
constexpr unsigned	spot::clz (Type n) noexcept
	Count leading zeros of an unsigned integer.
void	spot::fixed_size_pool< Kind >::deallocate (void *ptr)
	Recycle size bytes of memory.
int	spot::memusage ()
	Total number of pages in use by the program.
void	spot::multiple_size_pool::deallocate (const void *ptr, size_t size)
	Recycle size bytes of memory.
template<typename values >
void	spot::permute_vector (std::vector< values > &data, const std::vector< unsigned > &indices)
	Reorder data in place according to the permutation indices.
const char *	spot::version ()
	Return Spot's version.
bool	spot::is_spin_ap (const char *str)
	Whether a word can be used as an atomic proposition for Spin 5.
std::ostream &	spot::escape_rfc4180 (std::ostream &os, const std::string &str)
	Double characters " in strings.
std::ostream &	spot::escape_latex (std::ostream &os, const std::string &str)
	Escape special LaTeX characters.
std::ostream &	spot::escape_html (std::ostream &os, const std::string &str)
	Escape special HTML characters.
std::ostream &	spot::escape_str (std::ostream &os, const std::string &str)
	Escape characters ", \, and \n in str.
std::string	spot::escape_str (const std::string &str)
	Escape characters ", \, and \n in str.
std::ostream &	spot::quote_shell_string (std::ostream &os, const char *str)
	Output str between simple quote or double quotes.
void	spot::int_array_array_compress2 (const int *array, size_t n, int *dest, size_t &dest_size)
	Compress an int array of size n into a int array.
void	spot::int_array_array_decompress2 (const int *array, size_t array_size, int *res, size_t size)
	Uncompress an int array of size array_size into a int array of size size.
void	spot::int_vector_vector_compress (const std::vector< int > &input, std::vector< unsigned int > &output)
	Compress an int vector into a vector of unsigned int.
void	spot::int_vector_vector_decompress (const std::vector< unsigned int > &array, std::vector< int > &output, size_t size)
	Uncompress a vector of unsigned int into a vector of size size.
const std::vector< unsigned int > *	spot::int_array_vector_compress (const int *array, size_t n)
	Compress an int array if size n into a vector of unsigned int.
void	spot::int_vector_array_decompress (const std::vector< unsigned int > *array, int *res, size_t size)
	Uncompress a vector of unsigned int into an int array of size size.
void	spot::int_array_array_compress (const int *array, size_t n, int *dest, size_t &dest_size)
	Compress an int array of size n into a int array.
void	spot::int_array_array_decompress (const int *array, size_t array_size, int *res, size_t size)
	Uncompress an int array of size array_size into a int array of size size.

Detailed Description

Function Documentation

clz()

template<typename Type , typename = std::enable_if_t<std::is_unsigned<Type>::value>>

constexpr unsigned spot::clz ( Type  n )

inlineconstexprnoexcept

#include <spot/misc/clz.hh>

Count leading zeros of an unsigned integer.

Referenced by spot::fixed_size_pool< Kind >::fixed_size_pool(), and spot::bitset< N >::highest().

deallocate() [1/2]

void spot::multiple_size_pool::deallocate ( const void *  ptr, size_t  size  )

inline

#include <spot/misc/mspool.hh>

Recycle size bytes of memory.

Despite the name, the memory is not really deallocated in the "delete" sense: it is still owned by the pool and will be reused by allocate as soon as possible. The memory is only freed when the pool is destroyed.

The size argument should be the same as the one passed to allocate().

References spot::multiple_size_pool::fixsize().

deallocate() [2/2]

template<pool_type Kind>

void spot::fixed_size_pool< Kind >::deallocate ( void *  ptr )

inline

#include <spot/misc/fixpool.hh>

Recycle size bytes of memory.

Despite the name, the memory is not really deallocated in the "delete" sense: it is still owned by the pool and will be reused by allocate as soon as possible. The memory is only freed when the pool is destroyed.

Referenced by spot::iterable_uf< State, StateHash, StateEqual >::make_claim(), and spot::iterable_uf_ec< State, StateHash, StateEqual >::make_claim().

down_cast() [1/3]

template<typename T , typename U >

T spot::down_cast ( const std::shared_ptr< U > &  u )

inlinenoexcept

#include <spot/misc/casts.hh>

Downcast shared pointer u to T.

down_cast() [2/3]

template<typename T , typename U >

T spot::down_cast ( U *  u )

inlinenoexcept

#include <spot/misc/casts.hh>

Downcast pointer u to T.

down_cast() [3/3]

template<typename T , typename U >

T spot::down_cast ( U  u )

inline

#include <spot/misc/casts.hh>

Downcast reference u to T.

escape_html()

std::ostream & spot::escape_html	(	std::ostream &	os,
		const std::string &	str
	)

#include <spot/misc/escape.hh>

Escape special HTML characters.

The following characters are rewritten: > < " &

escape_latex()

std::ostream & spot::escape_latex	(	std::ostream &	os,
		const std::string &	str
	)

#include <spot/misc/escape.hh>

Escape special LaTeX characters.

The following characters are rewritten: & % $ # _ { } ~ ^ \

escape_rfc4180()

std::ostream & spot::escape_rfc4180	(	std::ostream &	os,
		const std::string &	str
	)

#include <spot/misc/escape.hh>

Double characters " in strings.

In CSV files, as defined by RFC4180, double-quoted string that contain double-quotes should simply duplicate those quotes.

Note that since C++14,

os << std::quoted(str, '"', '"');

outputs the same result as

escape_rfc4180(os << '"', str) << '"';

escape_str() [1/2]

std::string spot::escape_str

(

const std::string &

str

)

#include <spot/misc/escape.hh>

Escape characters ", \, and \n in str.

escape_str() [2/2]

std::ostream & spot::escape_str	(	std::ostream &	os,
		const std::string &	str
	)

#include <spot/misc/escape.hh>

Escape characters ", \, and \n in str.

int_array_array_compress()

void spot::int_array_array_compress	(	const int *	array,
		size_t	n,
		int *	dest,
		size_t &	dest_size
	)

#include <spot/misc/intvcomp.hh>

Compress an int array of size n into a int array.

The destination array should be at least dest_size large. An assert will be triggered if dest_size is too small. On return, dest_size will be set to the actual number of int filled in dest

int_array_array_compress2()

void spot::int_array_array_compress2	(	const int *	array,
		size_t	n,
		int *	dest,
		size_t &	dest_size
	)

#include <spot/misc/intvcmp2.hh>

Compress an int array of size n into a int array.

The destination array should be at least dest_size large. An assert will be triggered if dest_size is too small. On return, dest_size will be set to the actual number of int filled in dest

int_array_array_decompress()

void spot::int_array_array_decompress	(	const int *	array,
		size_t	array_size,
		int *	res,
		size_t	size
	)

#include <spot/misc/intvcomp.hh>

Uncompress an int array of size array_size into a int array of size size.

size must be the exact expected size of uncompressed array.

int_array_array_decompress2()

void spot::int_array_array_decompress2	(	const int *	array,
		size_t	array_size,
		int *	res,
		size_t	size
	)

#include <spot/misc/intvcmp2.hh>

Uncompress an int array of size array_size into a int array of size size.

size must be the exact expected size of uncompressed array.

int_array_vector_compress()

const std::vector< unsigned int > * spot::int_array_vector_compress	(	const int *	array,
		size_t	n
	)

#include <spot/misc/intvcomp.hh>

Compress an int array if size n into a vector of unsigned int.

int_vector_array_decompress()

void spot::int_vector_array_decompress	(	const std::vector< unsigned int > *	array,
		int *	res,
		size_t	size
	)

#include <spot/misc/intvcomp.hh>

Uncompress a vector of unsigned int into an int array of size size.

size must be the exact expected size of uncompressed array.

int_vector_vector_compress()

void spot::int_vector_vector_compress	(	const std::vector< int > &	input,
		std::vector< unsigned int > &	output
	)

#include <spot/misc/intvcomp.hh>

Compress an int vector into a vector of unsigned int.

int_vector_vector_decompress()

void spot::int_vector_vector_decompress	(	const std::vector< unsigned int > &	array,
		std::vector< int > &	output,
		size_t	size
	)

#include <spot/misc/intvcomp.hh>

Uncompress a vector of unsigned int into a vector of size size.

size must be the exact expected size of uncompressed array.

is_spin_ap()

bool spot::is_spin_ap

(

const char *

str

)

#include <spot/misc/bareword.hh>

Whether a word can be used as an atomic proposition for Spin 5.

In Spin 5 (hence in ltl2ba and ltl3ba as well) atomic propositions should start with a lowercase letter, and can then consist solely of alphanumeric characters and underscores.

memusage()

int spot::memusage

(

)

#include <spot/misc/memusage.hh>

Total number of pages in use by the program.

Returns

The total number of pages in use by the program if known. -1 otherwise.

permute_vector()

template<typename values >

void spot::permute_vector	(	std::vector< values > &	data,
		const std::vector< unsigned > &	indices
	)

#include <spot/misc/permute.hh>

Reorder data in place according to the permutation indices.

Referenced by spot::digraph< State_Data, Edge_Data >::defrag_states().

quote_shell_string()

std::ostream & spot::quote_shell_string	(	std::ostream &	os,
		const char *	str
	)

#include <spot/misc/escape.hh>

Output str between simple quote or double quotes.

Simple quotes are preferred unless str contains some simple quotes. In that case we use double quotes and escape anything that needs to be escaped.

version()

const char * spot::version

(

)

#include <spot/misc/version.hh>

Return Spot's version.