12#ifndef MCRL2_DATA_DATA_SPECIFICATION_H
13#define MCRL2_DATA_DATA_SPECIFICATION_H
25data_expression
normalize_sorts(
const data_expression& x,
const data::sort_specification& sortspec);
27data::data_equation
normalize_sorts(
const data::data_equation& x,
const data::sort_specification& sortspec);
32class data_specification;
34std::string
pp(
const data::data_specification& x);
56 struct target_sort_to_function_map
59 std::map<sort_expression, std::vector<function_symbol> > _mapping;
61 target_sort_to_function_map()
68 template <
typename Container>
69 void group_functions_by_target_sort(std::map<
sort_expression, std::vector<function_symbol> >& c,
const Container& functions)
75 if(c.find(index_sort) == c.end() || std::find(c[index_sort].begin(), c[index_sort].end(), f) == c[index_sort].end())
79 std::vector<function_symbol>& relevant_rhs = c[index_sort];
80 const std::size_t f_arity=(
is_function_sort(s)?atermpp::down_cast<function_sort>(s).size():0);
81 std::vector<function_symbol>::iterator i=
82 std::find_if(relevant_rhs.begin(),
85 { const std::size_t g_arity=(is_function_sort(g.sort())?
86 atermpp::down_cast<function_sort>(g.sort()).size():0);
87 return f_arity<g_arity;
89 relevant_rhs.insert(i,f);
94 template <
typename FunctionContainer>
95 void reset(
const FunctionContainer& c)
100 group_functions_by_target_sort(_mapping, c);
110 std::map<sort_expression, std::vector<function_symbol> >&mapping()
216 template <
class Iterator >
219 for(Iterator i=begin; i!=end; ++i)
225 template <
class Iterator >
228 for(Iterator i=begin; i!=end; ++i)
234 template <
class Iterator >
237 for(Iterator i=begin; i!=end; ++i)
246 for(
const map_result_type f: c)
265 std::set < function_symbol >&
mappings,
267 const bool skip_equations)
const
294 std::set < function_symbol >&
mappings,
296 const bool skip_equations)
const
299 mappings.insert(f.begin(), f.end());
360 if (do_not_normalize)
566 std::set < function_symbol >&
mappings,
569 const bool skip_equations=
false)
const;
581 std::set < function_symbol >
mappings;
602 std::set < sort_expression >&
sorts,
604 std::set <function_symbol >&
mappings)
const;
656 return (normalised_sort1 == normalised_sort2);
717std::string
pp(
const data_specification& x);
805 const std::set<sort_expression>& r(data.
sorts());
806 const std::set<sort_expression>::const_iterator i = std::find_if(r.begin(), r.end(),
detail::sort_has_name(s));
823 if (eq.lhs() == d || eq.rhs() == d)
825 result.push_back(eq);
829 if (atermpp::down_cast<application>(eq.lhs()).head() == d)
831 result.push_back(eq);
836 if (atermpp::down_cast<application>(eq.rhs()).head() == d)
838 result.push_back(eq);
864 std::map < std::size_t,variable_list> vars_of_enumerated_type;
871 bool is_enumerated_type=
true;
876 is_enumerated_type=
false;
880 if (is_enumerated_type)
897 rest_vars=vars_of_finite_type + rest_vars;
898 for(std::map <std::size_t,variable_list>::const_reverse_iterator k=vars_of_enumerated_type.rbegin(); k!=vars_of_enumerated_type.rend(); ++k)
900 rest_vars = k->second + rest_vars;
910 std::set<core::identifier_string> result;
913 result.insert(f.name());
917 result.insert(f.name());
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
size_type size() const
Returns the size of the term_list.
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
void add_normalised_mappings(Iterator begin, Iterator end) const
bool is_constructor_sort(const sort_expression &s) const
Checks whether a sort is a constructor sort.
void add_normalised_cpp_implemented_functions(const implementation_map &c) const
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
void add_data_types_for_sorts() const
Puts the constructors, functions and equations in normalised form in de data type.
void add_mapping(const function_symbol &f)
Adds a mapping to this specification.
void add_equation(const data_equation &e)
Adds an equation to this specification.
void remove_constructor(const function_symbol &f)
Removes constructor from specification.
void remove_equation(const data_equation &e)
Removes equation from specification.
void translate_user_notation()
Translate user notation within the equations of the data specification.
bool equal_sorts(sort_expression const &s1, sort_expression const &s2) const
Checks whether two sort expressions represent the same sort.
void add_standard_mappings_and_equations(const sort_expression &sort, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
implementation_map m_cpp_implemented_functions
A map that for function symbols gives how it can be implemented.
data_equation_vector m_user_defined_equations
The equations of the specification.
const implementation_map & cpp_implemented_functions() const
Gets all equations in this specification including those that are system defined.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const std::set< data_equation > & equations() const
Gets all equations in this specification including those that are system defined.
void 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.
void add_normalised_constructor(const function_symbol &f) const
Adds a constructor to this specification, and marks it as system defined.
void add_normalised_constructors(Iterator begin, Iterator end) const
data_equation_vector & user_defined_equations()
void remove_mapping(const function_symbol &f)
Removes mapping from specification.
const function_symbol_vector & mappings(const sort_expression &s) const
Gets all mappings of a sort including those that are system defined.
target_sort_to_function_map m_grouped_normalised_constructors
Cache normalised constructors grouped by target sort.
void 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,...
function_symbol_vector m_normalised_mappings
Set containing system defined all mappings, including the system defined ones. The types in these map...
bool is_well_typed() const
Returns true if.
void normalise_data_specification_if_required() const
function_symbol_vector m_user_defined_constructors
A mapping of sort expressions to the constructors corresponding to that sort.
data_specification()
Default constructor. Generate a data specification that contains only booleans and positive numbers.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
std::set< data_equation > m_normalised_equations
Table containing all equations, including the system defined ones. The sorts in these equations are n...
void add_constructor(const function_symbol &f)
Adds a constructor to this specification.
void 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 add...
void add_normalised_mapping(const function_symbol &f) const
Adds a mapping to this specification, and marks it as system defined.
void 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 ...
data_specification(const atermpp::aterm &t)
Constructor from an aterm.
void add_normalised_equation(const data_equation &e) const
Adds an equation to this specification, and marks it as system defined.
bool is_certainly_finite(const sort_expression &s) const
Checks whether a sort is certainly finite.
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
function_symbol_vector m_user_defined_mappings
The mappings of the specification.
const function_symbol_vector & constructors(const sort_expression &s, const bool do_not_normalize=false) const
Gets all constructors of a sort including those that are system defined.
function_symbol_vector m_normalised_constructors
Set containing all constructors, including the system defined ones. The types in these constructors a...
void add_normalised_equations(Iterator begin, Iterator end) const
bool operator==(const data_specification &other) const
void data_is_not_necessarily_normalised_anymore() const
target_sort_to_function_map m_grouped_normalised_mappings
Cache normalised mappings grouped by target sort.
bool is_certainly_finite(const sort_expression_list &l) const
Checks whether all sorts are certainly finite in a sort_expression_list.
const function_symbol_vector & mappings() const
Gets all mappings in this specification including those that are system defined.
const sort_expression_list & domain() const
const sort_expression & sort() const
const sort_expression & target_sort() const
Returns the target sort of this expression.
const std::set< sort_expression > & context_sorts() const
Return the user defined context sorts of the current specification.
bool operator==(const sort_specification &other) const
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
const basic_sort_vector & user_defined_sorts() const
Gets all sorts defined by a user (excluding the system defined sorts).
bool m_normalised_data_is_up_to_date
The variable below indicates whether a surrounding data specification is up to data with respect to s...
void add_alias(const alias &a)
Adds an alias (new name for a sort) to this specification.
void add_sort(const basic_sort &s)
Adds a sort to this specification.
void add_context_sort(const sort_expression &s)
Adds the sort s to the context sorts.
void import_system_defined_sorts(const CONTAINER &sorts)
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
void import_system_defined_sort(const sort_expression &sort)
Adds the system defined sorts in a sequence. The second argument is used to check which sorts are add...
function_symbol_vector recogniser_functions(const sort_expression &s) const
function_symbol_vector constructor_functions(const sort_expression &s) const
data_equation_vector constructor_equations(const sort_expression &s) const
data_equation_vector recogniser_equations(const sort_expression &s) const
function_symbol_vector comparison_functions(const sort_expression &s) const
data_equation_vector comparison_equations(const sort_expression &s) const
function_symbol_vector projection_functions(const sort_expression &s) const
data_equation_vector projection_equations(const sort_expression &s) const
Add your file description here.
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
function_symbol find_mapping(data_specification const &data, std::string const &s)
Finds a mapping in a data specification.
data::data_equation translate_user_notation(const data::data_equation &x)
std::vector< alias > alias_vector
\brief vector of aliass
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
data_equation_vector standard_generate_equations_code(const sort_expression &s)
Give all standard system defined equations for sort s.
data_equation_vector find_equations(data_specification const &specification, const data_expression &d)
Gets all equations with a data expression as head on one of its sides.
std::string pp(const abstraction &x)
function_symbol find_constructor(data_specification const &data, std::string const &s)
Finds a constructor in a data specification.
sort_expression find_sort(data_specification const &data, std::string const &s)
Finds a sort in a data specification.
atermpp::term_list< data_equation > data_equation_list
\brief list of data_equations
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
atermpp::term_list< variable > variable_list
\brief list of variables
std::set< core::identifier_string > function_and_mapping_identifiers(const data_specification &dataspec)
Returns the names of functions and mappings that occur in a data specification.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
bool is_data_specification(const atermpp::aterm &x)
Test for a data specification expression.
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
variable_list order_variables_to_optimise_enumeration(const variable_list &l, const data_specification &data_spec)
Order the variables in a variable list such that enumeration over these variables becomes more effici...
data_specification operator+(data_specification spec1, const data_specification &spec2)
Merges two data specifications into one.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
std::ostream & operator<<(std::ostream &out, const abstraction &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
This file describes the a sort_specification,.
static const atermpp::function_symbol DataSpec