mcrl2::lps::confluence_checker

Include file:

#include "mcrl2/lps/confluence.h
class mcrl2::lps::confluence_checker

Protected types

type mcrl2::lps::confluence_checker::cache_result

Values:

  • yes

  • no

  • indeterminate

Protected attributes

std::map<std::pair<std::size_t, std::size_t>, bool> mcrl2::lps::confluence_checker::m_cache
data::variable_list mcrl2::lps::confluence_checker::m_process_parameters
data::rewriter mcrl2::lps::confluence_checker::m_rewr
data::mutable_indexed_substitution mcrl2::lps::confluence_checker::m_sigma
std::unique_ptr<smt::smt_solver> mcrl2::lps::confluence_checker::m_solver
std::vector<confluence_summand> mcrl2::lps::confluence_checker::m_summands

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
std::pair<bool, std::size_t> is_confluent(std::size_t j, ConfluenceCondition confluence_condition, bool check_disjointness) const
bool is_true(const data::data_expression &x) const
bool is_true_rewriter(data::data_expression x) const
bool is_true_smt(const data::data_expression &x) const

Public member functions

std::vector<std::size_t> compute_confluent_summands(const Specification &lpsspec, char confluence_type)
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
void run(Specification &lpsspec, char confluence_type, bool use_smt_solver = false)

Applies confluent reduction to an LPS.