#include <confluence.h>

Public Member Functions
std::pair< bool, std::size_t >	is_commutative_confluent (std::size_t j, data::set_identifier_generator &generator) const

std::pair< bool, std::size_t >	is_square_confluent (std::size_t j) const

std::pair< bool, std::size_t >	is_triangular_confluent (std::size_t j) const

std::pair< bool, std::size_t >	is_trivial_confluent (std::size_t j) const

template<typename Specification >
std::vector< std::size_t >	compute_confluent_summands (const Specification &lpsspec, char confluence_type)

template<typename Specification >
void	run (Specification &lpsspec, char confluence_type, bool use_smt_solver=false)
	Applies confluent reduction to an LPS.

Protected Types
enum	cache_result { yes , no , indeterminate }

Protected Member Functions
cache_result	cache_lookup (std::size_t i, std::size_t j) const

void	cache_store (std::size_t i, std::size_t j, bool confluent) const

bool	is_true_rewriter (data::data_expression x) const

bool	is_true_smt (const data::data_expression &x) const

bool	is_true (const data::data_expression &x) const

template<typename ConfluenceCondition >
std::pair< bool, std::size_t >	is_confluent (std::size_t j, ConfluenceCondition confluence_condition, bool check_disjointness) const

Protected Attributes
std::vector< confluence_summand >	m_summands

data::variable_list	m_process_parameters

data::rewriter	m_rewr

data::mutable_indexed_substitution	m_sigma

std::unique_ptr< smt::smt_solver >	m_solver

std::map< std::pair< std::size_t, std::size_t >, bool >	m_cache

Detailed Description

Definition at line 404 of file confluence.h.

Member Enumeration Documentation

◆ cache_result

enum mcrl2::lps::confluence_checker::cache_result

protected

Enumerator
yes
no
indeterminate

Definition at line 416 of file confluence.h.

Member Function Documentation

◆ cache_lookup()

cache_result mcrl2::lps::confluence_checker::cache_lookup	(	std::size_t	i,
		std::size_t	j
	)		const

inlineprotected

Definition at line 421 of file confluence.h.

◆ cache_store()

void mcrl2::lps::confluence_checker::cache_store	(	std::size_t	i,
		std::size_t	j,
		bool	confluent
	)		const

inlineprotected

Definition at line 432 of file confluence.h.

◆ compute_confluent_summands()

template<typename Specification >

std::vector< std::size_t > mcrl2::lps::confluence_checker::compute_confluent_summands	(	const Specification &	lpsspec,
		char	confluence_type
	)

inline

Definition at line 549 of file confluence.h.

◆ is_commutative_confluent()

std::pair< bool, std::size_t > mcrl2::lps::confluence_checker::is_commutative_confluent	(	std::size_t	j,
		data::set_identifier_generator &	generator
	)		const

inline

Definition at line 524 of file confluence.h.

◆ is_confluent()

template<typename ConfluenceCondition >

std::pair< bool, std::size_t > mcrl2::lps::confluence_checker::is_confluent	(	std::size_t	j,
		ConfluenceCondition	confluence_condition,
		bool	check_disjointness
	)		const

inlineprotected

Definition at line 479 of file confluence.h.

◆ is_square_confluent()

std::pair< bool, std::size_t > mcrl2::lps::confluence_checker::is_square_confluent ( std::size_t j ) const

inline

Definition at line 530 of file confluence.h.

◆ is_triangular_confluent()

std::pair< bool, std::size_t > mcrl2::lps::confluence_checker::is_triangular_confluent ( std::size_t j ) const

inline

Definition at line 536 of file confluence.h.

◆ is_trivial_confluent()

std::pair< bool, std::size_t > mcrl2::lps::confluence_checker::is_trivial_confluent ( std::size_t j ) const

inline

Definition at line 542 of file confluence.h.

◆ is_true()

bool mcrl2::lps::confluence_checker::is_true ( const data::data_expression & x ) const

inlineprotected

Definition at line 471 of file confluence.h.

◆ is_true_rewriter()

bool mcrl2::lps::confluence_checker::is_true_rewriter ( data::data_expression x ) const

inlineprotected

Definition at line 438 of file confluence.h.

◆ is_true_smt()

bool mcrl2::lps::confluence_checker::is_true_smt ( const data::data_expression & x ) const

inlineprotected

Definition at line 447 of file confluence.h.

◆ run()

template<typename Specification >

void mcrl2::lps::confluence_checker::run	(	Specification &	lpsspec,
		char	confluence_type,
		bool	use_smt_solver = `false`
	)

inline

Applies confluent reduction to an LPS.

Definition at line 606 of file confluence.h.

Member Data Documentation

◆ m_cache

std::map<std::pair<std::size_t, std::size_t>, bool> mcrl2::lps::confluence_checker::m_cache

mutableprotected

Definition at line 414 of file confluence.h.

◆ m_process_parameters

data::variable_list mcrl2::lps::confluence_checker::m_process_parameters

protected

Definition at line 408 of file confluence.h.

◆ m_rewr

data::rewriter mcrl2::lps::confluence_checker::m_rewr

protected

Definition at line 409 of file confluence.h.

◆ m_sigma

data::mutable_indexed_substitution mcrl2::lps::confluence_checker::m_sigma

mutableprotected

Definition at line 410 of file confluence.h.

◆ m_solver

std::unique_ptr<smt::smt_solver> mcrl2::lps::confluence_checker::m_solver

protected

Definition at line 411 of file confluence.h.

◆ m_summands

std::vector<confluence_summand> mcrl2::lps::confluence_checker::m_summands

protected

Definition at line 407 of file confluence.h.

The documentation for this class was generated from the following file:

lps/include/mcrl2/lps/confluence.h

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ cache_result

Member Function Documentation

◆ cache_lookup()

◆ cache_store()

◆ compute_confluent_summands()

◆ is_commutative_confluent()

◆ is_confluent()

◆ is_square_confluent()

◆ is_triangular_confluent()

◆ is_trivial_confluent()

◆ is_true()

◆ is_true_rewriter()

◆ is_true_smt()

◆ run()

Member Data Documentation

◆ m_cache

◆ m_process_parameters

◆ m_rewr

◆ m_sigma

◆ m_solver

◆ m_summands