Namespaces
namespace	detail

Classes
struct	always_false

class	child_process

struct	native_translations

class	smt_solver

class	stack_outstream

struct	structured_sort_functions
	Contains information on sorts that behave similar to a structured sort in a data specification. More...

class	translation_error

Typedefs
typedef std::function< void(data::data_expression, std::function< void(std::string)>, std::function< void(data::data_expression)>)>	native_translation_t

Enumerations
enum	answer { UNSAT = 0 , UNKNOWN = 1 , SAT = 2 }

Functions
std::ostream &	operator<< (std::ostream &out, const answer &a)

native_translations	initialise_native_translation (const data::data_specification &dataspec)

template<typename T , typename OutputStream >
void	translate_data_expression (const T &x, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)

template<typename T , typename OutputStream >
void	translate_assertion (const T &x, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)

template<typename Container , typename OutputStream >
void	translate_variable_declaration (const Container &vars, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)

template<typename T , typename OutputStream >
void	translate_sort_expression (const T &x, OutputStream &o, const native_translations &nt, const std::map< data::structured_sort, std::string > &snm=detail::empty_name_map())

template<typename OutputStream >
void	translate_data_specification (const data::data_specification &dataspec, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)

template<typename Skip = always_false<data::function_symbol>>
std::pair< structured_sort_functions, std::map< data::function_symbol, data::data_equation_vector > >	find_structured_sort_functions (const data::data_specification &dataspec, Skip skip=Skip())
	Find sorts that behave like a structured sort and the associated rewrite rules.

std::set< data::function_symbol >	complete_recognisers_projections (const data::data_specification &dataspec, native_translations &nt, structured_sort_functions &ssf)
	Complete the containers with recognisers and projections in ssf.

void	unfold_pattern_matching (const data::data_specification &dataspec, native_translations &nt)

std::string	translate_identifier (const std::string &id)

std::string	translate_identifier (const core::identifier_string &id)

std::string	translate_symbol (const data::function_symbol &f, const native_translations &nt)

std::string	make_projection_name (const data::function_symbol &cons, std::size_t i, const native_translations &nt)

data::function_symbol	make_projection_func (const data::function_symbol &cons, const data::sort_expression &arg_sort, std::size_t i, const native_translations &nt)

std::string	make_recogniser_name (const data::function_symbol &cons, const native_translations &nt)

data::function_symbol	make_recogniser_func (const data::function_symbol &cons, const native_translations &nt)

template<class T >
std::vector< T >	topological_sort (std::map< T, std::set< T > > dependencies)

Typedef Documentation

◆ native_translation_t

typedef std::function<void(data::data_expression, std::function<void(std::string)>, std::function<void(data::data_expression)>)> mcrl2::smt::native_translation_t

Definition at line 19 of file native_translation.h.

Enumeration Type Documentation

◆ answer

enum mcrl2::smt::answer

Enumerator
UNSAT
UNKNOWN
SAT

Definition at line 21 of file answer.h.

Function Documentation

◆ complete_recognisers_projections()

std::set< data::function_symbol > mcrl2::smt::complete_recognisers_projections	(	const data::data_specification &	dataspec,
		native_translations &	nt,
		structured_sort_functions &	ssf
	)

Complete the containers with recognisers and projections in ssf.

Also sets native translations and build a set of all recognisers and projections in dataspec.

Definition at line 260 of file unfold_pattern_matching.h.

◆ find_structured_sort_functions()

template<typename Skip = always_false<data::function_symbol>>

std::pair< structured_sort_functions, std::map< data::function_symbol, data::data_equation_vector > > mcrl2::smt::find_structured_sort_functions	(	const data::data_specification &	dataspec,
		Skip	skip = `Skip()`
	)

Find sorts that behave like a structured sort and the associated rewrite rules.

Template Parameters

Skip	Unary Boolean function type.

Parameters

dataspec	The data specification to consider
skip	If skip(f) is true then function symbol f will not be considered

Returns: A pair containing: (1) recogniser and projection function symbols for each structured sort and (2) a map that gives a list of equations for each function symbol.

Definition at line 90 of file unfold_pattern_matching.h.

◆ initialise_native_translation()

native_translations mcrl2::smt::initialise_native_translation ( const data::data_specification & dataspec )

Definition at line 125 of file solver.cpp.

◆ make_projection_func()

data::function_symbol mcrl2::smt::make_projection_func	(	const data::function_symbol &	cons,
		const data::sort_expression &	arg_sort,
		std::size_t	i,
		const native_translations &	nt
	)

inline

Definition at line 66 of file utilities.h.

◆ make_projection_name()

std::string mcrl2::smt::make_projection_name	(	const data::function_symbol &	cons,
		std::size_t	i,
		const native_translations &	nt
	)

inline

Definition at line 50 of file utilities.h.

◆ make_recogniser_func()

data::function_symbol mcrl2::smt::make_recogniser_func	(	const data::function_symbol &	cons,
		const native_translations &	nt
	)

inline

Definition at line 85 of file utilities.h.

◆ make_recogniser_name()

std::string mcrl2::smt::make_recogniser_name	(	const data::function_symbol &	cons,
		const native_translations &	nt
	)

inline

Definition at line 73 of file utilities.h.

◆ operator<<()

std::ostream & mcrl2::smt::operator<<	(	std::ostream &	out,
		const answer &	a
	)

inline

Definition at line 29 of file answer.h.

◆ topological_sort()

template<class T >

std::vector< T > mcrl2::smt::topological_sort ( std::map< T, std::set< T > > dependencies )

Definition at line 92 of file utilities.h.

◆ translate_assertion()

template<typename T , typename OutputStream >

void mcrl2::smt::translate_assertion	(	const T &	x,
		OutputStream &	o,
		std::unordered_map< data::data_expression, std::string > &	c,
		const native_translations &	nt
	)

Definition at line 176 of file translate_expression.h.

◆ translate_data_expression()

template<typename T , typename OutputStream >

void mcrl2::smt::translate_data_expression	(	const T &	x,
		OutputStream &	o,
		std::unordered_map< data::data_expression, std::string > &	c,
		const native_translations &	nt
	)

Definition at line 170 of file translate_expression.h.

◆ translate_data_specification()

template<typename OutputStream >

void mcrl2::smt::translate_data_specification	(	const data::data_specification &	dataspec,
		OutputStream &	o,
		std::unordered_map< data::data_expression, std::string > &	c,
		const native_translations &	nt
	)

Definition at line 305 of file translate_specification.h.

◆ translate_identifier() [1/2]

std::string mcrl2::smt::translate_identifier ( const core::identifier_string & id )

inline

Definition at line 37 of file utilities.h.

◆ translate_identifier() [2/2]

std::string mcrl2::smt::translate_identifier ( const std::string & id )

inline

Definition at line 23 of file utilities.h.

◆ translate_sort_expression()

template<typename T , typename OutputStream >

void mcrl2::smt::translate_sort_expression	(	const T &	x,
		OutputStream &	o,
		const native_translations &	nt,
		const std::map< data::structured_sort, std::string > &	snm = `detail::empty_name_map()`
	)

Definition at line 96 of file translate_sort.h.

◆ translate_symbol()

std::string mcrl2::smt::translate_symbol	(	const data::function_symbol &	f,
		const native_translations &	nt
	)

inline

Definition at line 43 of file utilities.h.

◆ translate_variable_declaration()

template<typename Container , typename OutputStream >

void mcrl2::smt::translate_variable_declaration	(	const Container &	vars,
		OutputStream &	o,
		std::unordered_map< data::data_expression, std::string > &	c,
		const native_translations &	nt
	)

Definition at line 184 of file translate_expression.h.

◆ unfold_pattern_matching()

void mcrl2::smt::unfold_pattern_matching	(	const data::data_specification &	dataspec,
		native_translations &	nt
	)

inline

Definition at line 303 of file unfold_pattern_matching.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ native_translation_t

Enumeration Type Documentation

◆ answer

Function Documentation

◆ complete_recognisers_projections()

◆ find_structured_sort_functions()

◆ initialise_native_translation()

◆ make_projection_func()

◆ make_projection_name()

◆ make_recogniser_func()

◆ make_recogniser_name()

◆ operator<<()

◆ topological_sort()

◆ translate_assertion()

◆ translate_data_expression()

◆ translate_data_specification()

◆ translate_identifier() [1/2]

◆ translate_identifier() [2/2]

◆ translate_sort_expression()

◆ translate_symbol()

◆ translate_variable_declaration()

◆ unfold_pattern_matching()