36 if (constructors.empty())
45 const function_sort& f_sort=atermpp::down_cast<function_sort>(f.sort());
150 std::set<sort_expression> sorts_already_seen,
151 const bool toplevel)
const
155 if (sorts_already_seen.count(s)>0)
163 sorts_already_seen.insert(s);
165 sorts_already_seen.erase(s);
215 const std::multimap< sort_expression, sort_expression >& map1,
216 std::set < sort_expression > sorts_already_seen = std::set < sort_expression >())
218 assert(sorts_already_seen.find(e)==sorts_already_seen.end());
233 return function_sort(reverse(normalised_domain),normalised_codomain);
261 reverse(normalised_ssa),
262 constructor.recogniser()));
275 const std::multimap< sort_expression, sort_expression >::const_iterator i1=map1.find(result_sort);
279 sorts_already_seen.insert(result_sort);
319#ifdef MCRL2_ENABLE_MACHINENUMBERS
328#ifdef MCRL2_ENABLE_MACHINENUMBERS
334 const function_sort& fsort=atermpp::down_cast<function_sort>(sort);
403 std::set < sort_expression > sorts_already_seen;
410 mCRL2log(
log::debug) <<
"Encountered an alias loop in the alias for " << a.name() <<
". The normalised aliases are not constructed\n";
421 std::multimap< sort_expression, sort_expression > sort_aliases_to_be_investigated;
422 std::multimap< sort_expression, sort_expression > resulting_normalized_sort_aliases;
428 sort_aliases_to_be_investigated.insert(std::pair<sort_expression,sort_expression>(a.reference(),a.name()));
432 resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression>(a.name(),a.reference()));
437 for(; !sort_aliases_to_be_investigated.empty() ;)
439 const std::multimap< sort_expression, sort_expression >::iterator it=sort_aliases_to_be_investigated.begin();
442 sort_aliases_to_be_investigated.erase(it);
444 for(
const std::pair<const sort_expression, sort_expression >& p: resulting_normalized_sort_aliases)
460 if (e1!=left_hand_side)
464 if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
465 sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
466 [&rhs](
const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
467 == sort_aliases_to_be_investigated.upper_bound(normalised_lhs))
469 sort_aliases_to_be_investigated.insert(
470 std::pair<sort_expression,sort_expression > (normalised_lhs, e1));
487 if (e2!=left_hand_side)
491 if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
492 sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
493 [&rhs](
const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
494 == sort_aliases_to_be_investigated.upper_bound(normalised_lhs))
496 sort_aliases_to_be_investigated.insert(
497 std::pair<sort_expression,sort_expression > (normalised_lhs,e2));
506 if (normalised_lhs!=normalised_rhs)
508 resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression >(normalised_lhs,normalised_rhs));
515 for(
const std::pair<const sort_expression,sort_expression>& p: resulting_normalized_sort_aliases)
520 assert(p.first!=normalised_rhs);
528 std::set < function_symbol >& constructors,
529 std::set < function_symbol >& mappings,
530 std::set < data_equation >& equations,
532 const bool skip_equations)
const
540 mappings.insert(f.begin(), f.end());
615#ifdef MCRL2_ENABLE_MACHINENUMBERS
743 atermpp::down_cast<structured_sort>(sort),
750 std::set < sort_expression >& sorts,
751 std::set < function_symbol >& constructors,
752 std::set <function_symbol >& mappings)
const
757#ifdef MCRL2_ENABLE_MACHINENUMBERS
770 std::set < data_equation > dummy_equations;
775 assert(dummy_equations.size()==0);
783 std::clog <<
"data_specification::is_well_typed() failed: not all of the sorts appearing in the constructors "
791 std::clog <<
"data_specification::is_well_typed() failed: not all of the sorts appearing in the mappings "
806void data_specification::build_from_aterm(
const atermpp::aterm& term)
812 atermpp::down_cast<atermpp::term_list<atermpp::aterm> >(term[0][0]);
814 atermpp::down_cast<data::function_symbol_list>(term[1][0]);
816 atermpp::down_cast<data::function_symbol_list>(term[2][0]);
818 atermpp::down_cast<data::data_equation_list>(term[3][0]);
825 add_alias(atermpp::down_cast<data::alias>(t));
829 add_sort(atermpp::down_cast<basic_sort>(t));
834 for(
const function_symbol& f: term_constructors)
840 for(
const function_symbol& f: term_mappings)
846 for(
const data_equation& e: term_equations)
size_type size() const
Returns the size of the term_list.
const Term & front() const
Returns the first element of the list.
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
const container_type & container_name() const
const sort_expression & element_sort() const
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 add_standard_mappings_and_equations(const sort_expression &sort, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
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 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,...
bool is_well_typed() const
Returns true if.
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
void add_constructor(const function_symbol &f)
Adds a constructor to this specification.
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 ...
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.
const function_symbol_vector & mappings() const
Gets all mappings in this specification including those that are system defined.
bool is_finite(const container_sort &s)
bool is_finite(const basic_sort &s)
bool is_finite_aux(const sort_expression &s)
bool is_finite(const sort_expression &s)
std::set< sort_expression > m_visiting
bool is_finite(const alias &)
bool is_finite(const function_sort &s)
const data_specification & m_specification
finiteness_helper(const data_specification &specification)
bool is_finite(const structured_sort &s)
const sort_expression & codomain() const
const sort_expression_list & domain() const
const core::identifier_string & name() const
\brief Container type for sets
std::map< sort_expression, sort_expression > m_normalised_aliases
Table containing how sorts should be mapped to normalised sorts.
void add_system_defined_sort(const sort_expression &s)
Adds a sort to this specification, and marks it as system defined.
std::set< sort_expression > m_sorts_in_context
The sorts that occur are needed in this sort specification but are not explicitly defined as user def...
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
alias_vector m_user_defined_aliases
The basic sorts and structured sorts in the specification.
void add_predefined_basic_sorts()
void sorts_are_not_necessarily_normalised_anymore() const
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 reconstruct_m_normalised_aliases() const
void check_for_alias_loop(const sort_expression &s, std::set< sort_expression > sorts_already_seen, const bool toplevel=true) const
void import_system_defined_sorts(const CONTAINER &sorts)
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...
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
function_symbol_vector constructor_functions(const sort_expression &s) const
const structured_sort_constructor_list & constructors() const
Standard exception class for reporting runtime errors.
add your file description here.
add your file description here.
The class data_specification.
Add your file description here.
The standard sort function_update.
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
bool check_rule_DataSpec(const Term &t)
bool check_data_spec_sorts(const Container &container, const SortContainer &sorts)
Returns true if the domain sorts and range sort of the given functions are contained in sorts.
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
implementation_map bag_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for bag.
implementation_map bag_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
data_equation_vector bool_generate_equations_code()
Give all system defined equations for bool_.
const basic_sort & bool_()
Constructor for sort expression Bool.
implementation_map bool_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
function_symbol_vector bool_generate_constructors_code()
Give all system defined constructors for bool_.
implementation_map bool_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for bool_.
function_symbol_vector bool_generate_functions_code()
Give all system defined mappings for bool_.
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
implementation_map fbag_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
function_symbol_vector fbag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fbag.
implementation_map fbag_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for fbag.
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
function_symbol_vector fbag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fbag.
data_equation_vector fbag_generate_equations_code(const sort_expression &s)
Give all system defined equations for fbag.
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
function_symbol_vector fset_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fset.
implementation_map fset_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
function_symbol_vector fset_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fset.
implementation_map fset_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for fset.
data_equation_vector fset_generate_equations_code(const sort_expression &s)
Give all system defined equations for fset.
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
implementation_map int_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
const basic_sort & int_()
Constructor for sort expression Int.
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings for list.
implementation_map list_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for list.
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
implementation_map list_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
implementation_map machine_word_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for machine_word.
function_symbol_vector machine_word_generate_functions_code()
Give all system defined mappings for machine_word.
const basic_sort & machine_word()
Constructor for sort expression @word.
function_symbol_vector machine_word_generate_constructors_code()
Give all system defined constructors for machine_word.
implementation_map machine_word_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
data_equation_vector machine_word_generate_equations_code()
Give all system defined equations for machine_word.
data_equation_vector nat_generate_equations_code()
Give all system defined equations for nat.
const basic_sort & nat()
Constructor for sort expression Nat.
implementation_map nat_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
function_symbol_vector nat_generate_functions_code()
Give all system defined mappings for nat.
implementation_map nat_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for nat.
const basic_sort & natpair()
Constructor for sort expression @NatPair.
function_symbol_vector nat_generate_constructors_code()
Give all system defined constructors for nat.
implementation_map pos_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for pos.
function_symbol_vector pos_generate_functions_code()
Give all system defined mappings for pos.
implementation_map pos_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
data_equation_vector pos_generate_equations_code()
Give all system defined equations for pos.
const basic_sort & pos()
Constructor for sort expression Pos.
function_symbol_vector pos_generate_constructors_code()
Give all system defined constructors for pos.
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
const basic_sort & real_()
Constructor for sort expression Real.
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
implementation_map set_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for set_.
implementation_map set_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
static sort_expression find_normal_form(const sort_expression &e, const std::multimap< sort_expression, sort_expression > &map1, std::set< sort_expression > sorts_already_seen=std::set< sort_expression >())
std::vector< alias > alias_vector
\brief vector of aliass
implementation_map function_update_cpp_implementable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that are to be implemented in C++ code for function_update.
bool is_untyped_possible_sorts(const atermpp::aterm &x)
Returns true if the term t is an expression for multiple possible sorts.
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::string pp(const abstraction &x)
void replace_sort_expressions(T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
data_equation_vector function_update_generate_equations_code(const sort_expression &s, const sort_expression &t)
Give all system defined equations for function_update.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
implementation_map function_update_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
function_symbol_vector function_update_generate_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings for function_update.
bool is_alias(const atermpp::aterm &x)
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.
Substitution that maps a sort expression to a sort expression.