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.