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...
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
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.
const char *	spot::version ()
	Return Spot's version.
bool	spot::is_bare_word (const char *str)
	Whether a word is bare.
std::string	spot::quote_unless_bare_word (const std::string &str)
	Double-quote words that are not bare.
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::formater::scan (const char *fmt, std::vector< bool > &has) const
	Scan the %-sequences occurring in fmt.
void	spot::formater::scan (const std::string &fmt, std::vector< bool > &has) const
	Scan the %-sequences occurring in fmt.
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

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().

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.

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 actually 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 actually 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_bare_word()

bool spot::is_bare_word

(

const char *

str

)

#include <spot/misc/bareword.hh>

Whether a word is bare.

Bare words should start with a letter, an underscore, or a dot, and consist solely of alphanumeric characters, underscores, and dots.

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.

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.

quote_unless_bare_word()

std::string spot::quote_unless_bare_word

(

const std::string &

str

)

#include <spot/misc/bareword.hh>

Double-quote words that are not bare.

See also

is_bare_word

scan() [1/2]

void spot::formater::scan	(	const char *	fmt,
		std::vector< bool > &	has
	)		const

#include <spot/misc/formater.hh>

Scan the %-sequences occurring in fmt.

Set has['c'] for each c in fmt. has must be 256 wide.

scan() [2/2]

void spot::formater::scan ( const std::string &  fmt, std::vector< bool > &  has  ) const

inline

#include <spot/misc/formater.hh>

Scan the %-sequences occurring in fmt.

Set has['c'] for each c in fmt. has must be 256 wide.

version()

const char * spot::version

(

)

#include <spot/misc/version.hh>

Return Spot's version.