mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::confluence_checker Class Reference

#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_summandm_summands
 
data::variable_list m_process_parameters
 
data::rewriter m_rewr
 
data::mutable_indexed_substitution m_sigma
 
std::unique_ptr< smt::smt_solverm_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

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: