Include file:

#include "mcrl2/smt/unfold_pattern_matching.h"


  • mcrl2::smt::always_false
  • mcrl2::smt::structured_sort_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.

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, Skip skip = Skip())

Find sorts that behave like a structured sort and the associated rewrite rules.

templateparam * Skip Unary Boolean function type.


  • dataspec The data specification to consider
  • skip If skip(f) is true then function symbol f will not be considered

Returns: A pair containing: (1) recogniser and projection function symbols for each structured sort and (2) a map that gives a list of equations for each function symbol.

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