Include file:
#include "mcrl2/data/data_specification.h
mcrl2::data::
data_specification
¶data specification.
m_grouped_normalised_constructors
¶Cache normalised constructors grouped by target sort.
m_grouped_normalised_mappings
¶Cache normalised mappings grouped by target sort.
m_normalised_constructors
¶Set containing all constructors, including the system defined ones. The types in these constructors are normalised.
m_normalised_equations
¶Table containing all equations, including the system defined ones. The sorts in these equations are normalised.
m_normalised_mappings
¶Set containing system defined all mappings, including the system defined ones. The types in these mappings are normalised.
m_user_defined_constructors
¶A mapping of sort expressions to the constructors corresponding to that sort.
m_user_defined_equations
¶The equations of the 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_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¶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.
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:
declare_data_specification_to_be_type_checked
()¶Indicates that the data specification is type checked.
This builds up internal data structures and allows access to the data specification using all the utility functions.
equal_sorts
(sort_expression const &s1, sort_expression const &s2) const¶Checks whether two sort expressions represent the same sort.
Parameters:
equations
() 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.
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
() const¶Returns true if.
Returns: True if the data specification is well typed.
load
(std::istream &stream, bool binary = true, const std::string &source = "")¶Reads a data specification from a stream.
Parameters:
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)¶
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
save
(std::ostream &stream, bool binary = true) const¶Writes the data specification to a stream.
Parameters:
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, 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¶