mcrl2/smt/unfold_pattern_matching.h

Include file:

#include "mcrl2/smt/unfold_pattern_matching.h"

Classes

• mcrl2::smt::rule

• mcrl2::smt::structured_sort_functions

Functions

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.

static data::data_expression mcrl2::smt::construct_condition_rhs(const std::vector<rule> &rules, const data::data_expression &representative)

static data::data_expression mcrl2::smt::construct_rhs(const structured_sort_functions &ssf, data::representative_generator &gen, const std::vector<rule> &rules, const data::sort_expression &sort)

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, const native_translations &nt)

bool mcrl2::smt::is_pattern_matching_rule(const structured_sort_functions &ssf, const data::data_equation &rewrite_rule)

data::data_expression mcrl2::smt::lazyif(const data::data_expression &cond, const data::data_expression &then, const data::data_expression &else_)

std::ostream &mcrl2::smt::operator<<(std::ostream &out, const rule &r)

data::data_equation mcrl2::smt::unfold_pattern_matching(const data::function_symbol &mapping, const data::data_equation_vector &rewrite_rules, const structured_sort_functions &ssf, data::representative_generator &gen, data::set_identifier_generator &id_gen)

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