mcrl2/data/enumerator.h

Include file:

#include "mcrl2/data/enumerator.h"

The class enumerator.

Functions

data_expression_vector mcrl2::data::enumerate_expressions(const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr)

Returns a vector with all expressions of sort s.

Parameters:

  • s A sort expression.
  • dataspec The data specification defining the terms of sort s.
  • rewr A rewriter to be used to simplify terms and conditions.

It is assumed that the sort s has only a finite number of elements.

data_expression_vector mcrl2::data::enumerate_expressions(const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr, enumerator_identifier_generator &id_generator)

Returns a vector with all expressions of sort s.

Parameters:

  • s A sort expression.
  • dataspec The data specification defining the terms of sort s.
  • rewr A rewriter to be used to simplify terms and conditions.
  • id_generator An identifier generator used to generate new names for variables.

It is assumed that the sort s has only a finite number of elements.

static bool mcrl2::data::is_enumerable(const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort)
std::ostream &mcrl2::data::operator<<(std::ostream &out, const enumerator_list_element<Expression> &p)
std::ostream &mcrl2::data::operator<<(std::ostream &out, const enumerator_list_element_with_substitution<Expression> &p)

Functions

bool mcrl2::data::detail::compute_finite_function_sorts(const function_sort &sort, enumerator_identifier_generator &id_generator, const data::data_specification &dataspec, Rewriter datar, data_expression_vector &result, variable_list &function_parameter_list)

Computes the elements of a finite function sort, and puts them in result. If there are too many elements, false is returned.

bool mcrl2::data::detail::compute_finite_set_elements(const container_sort &sort, const data_specification &dataspec, Rewriter datar, MutableSubstitution &sigma, data_expression_vector &result, enumerator_identifier_generator &id_generator)

Computes the elements of a finite set sort, and puts them in result. If there are too many elements, false is returned.

bool mcrl2::data::detail::is_enumerable(const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort, std::list<sort_expression> &parents)
data_expression mcrl2::data::detail::make_if_expression_(std::size_t &function_index, const std::size_t argument_index, const std::vector<data_expression_vector> &data_domain_expressions, const data_expression_vector &codomain_expressions, const variable_vector &parameters)
data_expression mcrl2::data::detail::make_set_(std::size_t function_index, const sort_expression &element_sort, const data_expression_vector &set_elements)