Include file:
#include "mcrl2/data/data_specification.h
mcrl2::data::
data_specification
¶data specification.
mcrl2::data::data_specification::
implementation_map
¶typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >
mcrl2::data::data_specification::
m_cpp_implemented_functions
¶A map that for function symbols gives how it can be implemented.
For each function symbol there is a function : application -> data_expression that when applied to a term in normal form with the function symbol as head symbol returns a function that can be applied to calculate this term. Furthermore, it provides the name of a function that when applied to the number of arguments that the function expects can be used to rewrite the term. This last string can be used for code generation.
mcrl2::data::data_specification::
m_grouped_normalised_constructors
¶Cache normalised constructors grouped by target sort.
mcrl2::data::data_specification::
m_grouped_normalised_mappings
¶Cache normalised mappings grouped by target sort.
mcrl2::data::data_specification::
m_normalised_constructors
¶Set containing all constructors, including the system defined ones. The types in these constructors are normalised.
mcrl2::data::data_specification::
m_normalised_equations
¶Table containing all equations, including the system defined ones. The sorts in these equations are normalised.
The normalised equations are a set as the number of equations can become large, in which case removing duplicates while inserting equations can be very time consuming.
mcrl2::data::data_specification::
m_normalised_mappings
¶Set containing system defined all mappings, including the system defined ones. The types in these mappings are normalised.
mcrl2::data::data_specification::
m_user_defined_constructors
¶A mapping of sort expressions to the constructors corresponding to that sort.
mcrl2::data::data_specification::
m_user_defined_equations
¶The equations of the specification.
mcrl2::data::data_specification::
m_user_defined_mappings
¶The mappings of the specification.
add_normalised_constructor
(const function_symbol &f) const¶Adds a constructor to this specification, and marks it as system defined.
Parameters:
Pre: f does not yet occur in this specification.
Post: is_system_defined(f) == true .. note:: this operation does not invalidate iterators of constructors_const_range
add_normalised_constructors
(Iterator begin, Iterator end) const¶add_normalised_cpp_implemented_functions
(const implementation_map &c) const¶add_normalised_equation
(const data_equation &e) const¶Adds an equation to this specification, and marks it as system defined.
Parameters:
Pre: e does not yet occur in this specification.
Post: is_system_defined(f) == true .. note:: this operation does not invalidate iterators of equations_const_range
add_normalised_equations
(Iterator begin, Iterator end) const¶add_normalised_mapping
(const function_symbol &f) const¶Adds a mapping to this specification, and marks it as system defined.
Parameters:
Pre: f does not yet occur in this specification.
Post: is_system_defined(f) == true .. note:: this operation does not invalidate iterators of mappings_const_range
add_normalised_mappings
(Iterator begin, Iterator end) const¶add_standard_mappings_and_equations
(const sort_expression &sort, std::set<function_symbol> &mappings, std::set<data_equation> &equations, const bool skip_equations) const¶data_is_not_necessarily_normalised_anymore
() const¶insert_mappings_constructors_for_structured_sort
(const structured_sort &sort, std::set<function_symbol> &constructors, std::set<function_symbol> &mappings, std::set<data_equation> &equations, const bool skip_equations) const¶Adds constructors, mappings and equations for a structured sort to this specification, and marks them as system defined.
Parameters:
add_constructor
(const function_symbol &f)¶Adds a constructor to this specification.
Parameters:
Pre: a mapping f does not yet occur in this specification. .. note:: this operation does not invalidate iterators of constructors_const_range
add_equation
(const data_equation &e)¶Adds an equation to this specification.
Parameters:
Pre: e does not yet occur in this specification. .. note:: this operation does not invalidate iterators of equations_const_range
add_mapping
(const function_symbol &f)¶Adds a mapping to this specification.
Parameters:
Pre: a constructor f does not yet occur in this specification. .. note:: this operation does not invalidate iterators of mappings_const_range
constructors
() const¶Gets all constructors including those that are system defined.
The time complexity is the same as for sorts().
Returns: All constructors in this specification, including those for structured sorts.
constructors
(const sort_expression &s, const bool do_not_normalize = false) const¶Gets all constructors of a sort including those that are system defined.
The time complexity is the same as for sorts().
Parameters:
Returns: The constructors for sort s in this specification.
cpp_implemented_functions
() const¶Gets all equations in this specification including those that are system defined.
The time complexity of this operation is the same as that for sort().
Returns: All equations in this specification, including those for structured sorts.
data_specification
()¶Default constructor. Generate a data specification that contains only booleans and positive numbers.
data_specification
(const atermpp::aterm_appl &t)¶Constructor from an aterm.
Parameters:
data_specification
(const basic_sort_vector &sorts, const alias_vector &aliases, const function_symbol_vector &constructors, const function_symbol_vector &user_defined_mappings, const data_equation_vector &user_defined_equations)¶Constructor from its members.
equal_sorts
(sort_expression const &s1, sort_expression const &s2) const¶Checks whether two sort expressions represent the same sort.
Parameters:
equations
() constGets all equations in this specification including those that are system defined.
The time complexity of this operation is the same as that for sort().
Returns: All equations in this specification, including those for structured sorts.
get_system_defined_sorts_constructors_and_mappings
(std::set<sort_expression> &sorts, std::set<function_symbol> &constructors, std::set<function_symbol> &mappings) const¶This function provides a sample of all system defined sorts, constructors and mappings that contains at least one specimen of each sort and function symbol. Because types can be parameterised not all function symbols for all types are provided.
The sorts, constructors and mappings for the following types are added: Bool, Pos, Int, Nat, Real, List(Pos), FSet(Pos), FBag(Pos), Set(Pos), Bag(Pos). How to deal with struct…
is_certainly_finite
(const sort_expression &s) const¶Checks whether a sort is certainly finite.
Parameters:
Returns: true if s can be determined to be finite, false otherwise.
is_constructor_sort
(const sort_expression &s) const¶Checks whether a sort is a constructor sort.
Parameters:
Returns: true if s is a constructor sort
is_well_typed
() constReturns true if.
Returns: True if the data specification is well typed.
mappings
() const¶Gets all mappings in this specification including those that are system defined.
The time complexity is the same as for sorts().
Returns: All mappings in this specification, including recognisers and projection functions from structured sorts.
mappings
(const sort_expression &s) const¶Gets all mappings of a sort including those that are system defined.
Parameters:
Returns: All mappings in this specification, for which s occurs as a right-hand side of the mapping’s sort.
operator==
(const data_specification &other) const¶remove_constructor
(const function_symbol &f)¶Removes constructor from specification.
Note that this does not remove equations containing the constructor.
Parameters:
Pre: f occurs in the specification as constructor.
Post: f does not occur as constructor. .. note:: this operation does not invalidate iterators of constructors_const_range, only if they point to the element that is removed
remove_equation
(const data_equation &e)¶Removes equation from specification.
Parameters:
Post: e is removed from this specification. .. note:: this operation does not invalidate iterators of equations_const_range, only if they point to the element that is removed
remove_mapping
(const function_symbol &f)¶Removes mapping from specification.
Note that this does not remove equations in which the mapping occurs.
Parameters:
Post: f does not occur as constructor. .. note:: this operation does not invalidate iterators of mappings_const_range, only if they point to the element that is removed
translate_user_notation
()¶Translate user notation within the equations of the data specification.
This function replaces explicit numbers, lists, sets and bags by their counterpart in the data types. This function is to be invoked after type checking.
user_defined_constructors
() const¶Gets the constructors defined by the user, excluding those that are system defined.
The time complexity for this operation is constant.
user_defined_equations
() const¶Gets all user defined equations.
The time complexity of this operation is constant.
Returns: All equations in this specification, including those for structured sorts.
user_defined_mappings
() const¶Gets all user defined mappings in this specification.
The time complexity is constant.
Returns: All mappings in this specification, including recognisers and projection functions from structured sorts.
add_data_types_for_sorts
() const¶Puts the constructors, functions and equations in normalised form in de data type.
See the function normalise_sorts on arbitrary objects for a more detailed description. All sorts in the constructors, mappings and equations are normalised.
find_associated_system_defined_data_types_for_a_sort
(const sort_expression &sort, std::set<function_symbol> &constructors, std::set<function_symbol> &mappings, std::set<data_equation> &equations, implementation_map &cpp_implemented_functions, const bool skip_equations = false) const¶Adds the system defined sorts to the sets with constructors, mappings, and equations for.
import_data_type_for_system_defined_sort
(const sort_expression &sort) const¶Adds the system defined sorts in a sequence. The second argument is used to check which sorts are added, to prevent useless repetitions of additions of sorts. The function normalise_sorts imports for the given sort_expression sort all sorts, constructors, mappings and equations that belong to this sort to the normalised sets in this data type. E.g. for the sort Nat of natural numbers, it is required that Pos (positive numbers) are defined.
normalise_data_specification_if_required
() const¶