Include file:
#include "mcrl2/smt/unfold_pattern_matching.h"
mcrl2::smt::always_false
mcrl2::smt::structured_sort_functions
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.
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.
Parameters:
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.
mcrl2::smt::
unfold_pattern_matching
(const data::data_specification &dataspec, native_translations &nt)¶