mCRL2
Loading...
Searching...
No Matches
is_untyped.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/data/detail/is_untyped.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_DATA_DETAIL_IS_UNTYPED_H
13#define MCRL2_DATA_DETAIL_IS_UNTYPED_H
14
15#include "mcrl2/data/traverser.h"
16
17namespace mcrl2 {
18
19namespace data {
20
21namespace detail {
22
24{
26 using super::enter;
27 using super::leave;
28 using super::apply;
29
30 bool result;
31
33 : result(false)
34 {}
35
37 {
38 result = true;
39 }
40
42 {
43 result = true;
44 }
45
46 void apply(const data::untyped_sort& )
47 {
48 result = true;
49 }
50
52 {
53 result = true;
54 }
55
57 {
58 result = true;
59 }
60
62 {
63 result = true;
64 }
65
67 {
68 result = true;
69 }
70};
71
72inline
74{
76 f.apply(x);
77 return f.result;
78}
79
80} // namespace detail
81
82} // namespace data
83
84} // namespace mcrl2
85
86#endif // MCRL2_DATA_DETAIL_IS_UNTYPED_H
An integer term stores a single std::size_t value. It carries no arguments.
Definition aterm_int.h:26
aterm_int(std::size_t value)
Constructs an integer term from a value.
Definition aterm_int.h:34
aterm_string & operator=(aterm_string &&t) noexcept=default
aterm_string(const std::string &s)
Constructor that allows construction from a string.
aterm_string & operator=(const aterm_string &t) noexcept=default
const aterm & operator[](const size_type i) const
Returns the i-th argument.
Definition aterm.h:187
aterm & operator=(const aterm &other) noexcept=default
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
bool empty() const
Returns true if the term has no arguments.
Definition aterm.h:158
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
term_appl_iterator< aterm > const_iterator
Const iterator used to iterate through an term_appl.
Definition aterm.h:45
bool operator!=(const function_symbol &f) const
Inequality test.
bool operator==(const function_symbol &f) const
Equality test.
A list of aterm objects.
Definition aterm_list.h:24
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
bool type_is_appl() const noexcept
Dynamic check whether the term is an aterm.
Definition aterm_core.h:55
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
Definition aterm_core.h:92
bool type_is_int() const noexcept
Dynamic check whether the term is an aterm_int.
Definition aterm_core.h:63
Traverser that defines functions for maintaining bound variables.
Definition add_binding.h:26
TraverserOrBuilder< Derived > super
Definition add_binding.h:28
std::multiset< variable_type >::size_type bind_count(const variable_type &v)
Returns the bind count of the variable v.
Definition add_binding.h:80
void decrease_bind_count(const Container &variables, typename atermpp::enable_if_container< Container, variable_type >::type *=nullptr)
Remove a sequence of variables from the multiset of bound variables.
Definition add_binding.h:58
void increase_bind_count(const Container &variables, typename atermpp::enable_if_container< Container, variable_type >::type *=nullptr)
Add a sequence of variables to the multiset of bound variables.
Definition add_binding.h:42
bool is_bound(variable_type const &v) const
Returns true if the variable v is bound.
Definition add_binding.h:68
const std::multiset< variable_type > & bound_variables() const
Returns the bound variables.
Definition add_binding.h:74
std::multiset< variable_type > m_bound_variables
Definition add_binding.h:32
void decrease_bind_count(const variable_type &var)
Remove a variable from the multiset of bound variables.
Definition add_binding.h:51
void increase_bind_count(const variable_type &var)
Add a variable to the multiset of bound variables.
Definition add_binding.h:35
Builder< apply_builder_arg1< Builder, Arg1 > > super
Definition builder.h:125
apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:133
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:157
Builder< apply_builder_arg2< Builder, Arg1, Arg2 > > super
Definition builder.h:149
Builder< apply_builder< Builder > > super
Definition builder.h:104
singleton_expression & operator=(singleton_expression &&)=delete
singleton_expression & operator=(const singleton_expression &)=delete
singleton_expression(singleton_expression &&)=delete
singleton_expression(const singleton_expression &)=delete
parse_node_exception(const std::string &message)
Definition parse.h:49
parse_node_exception(const parse_node &node, const std::string &message)
Definition parse.h:54
static std::string get_error_message(const parse_node &node, const std::string &user_message)
Definition parse.h:37
parse_node_unexpected_exception(const parser &p, const parse_node &node)
Definition parse.h:78
static std::string get_error_message(const parser &p, const parse_node &node)
Definition parse.h:62
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
Definition builder.h:225
Builder< update_apply_builder_arg1< Builder, Function, Arg1 > > super
Definition builder.h:208
void apply(T &result, const argument_type &x)
Definition builder.h:220
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
abstraction(const atermpp::aterm &term)
Constructor.
Definition abstraction.h:35
abstraction(const binder_type &binding_operator, const variable_list &variables, const data_expression &body)
Constructor.
Definition abstraction.h:42
abstraction(const abstraction &) noexcept=default
Move semantics.
abstraction(const binder_type &binding_operator, const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Constructor.
Definition abstraction.h:48
abstraction & operator=(abstraction &&) noexcept=default
const data_expression & body() const
Definition abstraction.h:68
abstraction(abstraction &&) noexcept=default
abstraction()
Default constructor.
Definition abstraction.h:29
const binder_type & binding_operator() const
Definition abstraction.h:58
abstraction & operator=(const abstraction &) noexcept=default
\brief A sort alias
Definition alias.h:26
alias()
\brief Default constructor X3.
Definition alias.h:29
alias(const alias &) noexcept=default
Move semantics.
alias & operator=(const alias &) noexcept=default
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:42
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
Definition alias.h:35
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
Definition alias.h:52
const sort_expression & reference() const
Definition alias.h:57
\brief Assignment expression
Definition assignment.h:27
assignment_expression(assignment_expression &&) noexcept=default
assignment_expression()
\brief Default constructor X3.
Definition assignment.h:30
assignment_expression & operator=(const assignment_expression &) noexcept=default
assignment_expression(const assignment_expression &) noexcept=default
Move semantics.
assignment_expression & operator=(assignment_expression &&) noexcept=default
assignment_expression(const atermpp::aterm &term)
Definition assignment.h:36
\brief Assignment of a data expression to a variable
Definition assignment.h:91
assignment(const variable &lhs, const data_expression &rhs)
\brief Constructor Z14.
Definition assignment.h:107
const data_expression & rhs() const
Definition assignment.h:122
assignment(const atermpp::aterm &term)
Definition assignment.h:100
assignment(assignment &&) noexcept=default
assignment & operator=(assignment &&) noexcept=default
const variable & lhs() const
Definition assignment.h:117
assignment & operator=(const assignment &) noexcept=default
assignment(const assignment &) noexcept=default
Move semantics.
assignment()
\brief Default constructor X3.
Definition assignment.h:94
const data_expression & operator()(const variable &x) const
Applies the assignment to a variable.
Definition assignment.h:130
\brief Binder for bag comprehension
bag_comprehension_binder(const atermpp::aterm &term)
bag_comprehension_binder & operator=(const bag_comprehension_binder &) noexcept=default
bag_comprehension_binder(const bag_comprehension_binder &) noexcept=default
Move semantics.
bag_comprehension_binder()
\brief Default constructor X3.
bag_comprehension_binder(bag_comprehension_binder &&) noexcept=default
bag_comprehension_binder & operator=(bag_comprehension_binder &&) noexcept=default
universal quantification.
bag_comprehension(const bag_comprehension &) noexcept=default
Move semantics.
bag_comprehension & operator=(bag_comprehension &&) noexcept=default
bag_comprehension & operator=(const bag_comprehension &) noexcept=default
bag_comprehension(bag_comprehension &&) noexcept=default
bag_comprehension(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
\brief Container type for bags
bag_container(const bag_container &) noexcept=default
Move semantics.
bag_container(bag_container &&) noexcept=default
bag_container & operator=(bag_container &&) noexcept=default
bag_container()
\brief Default constructor X3.
bag_container(const atermpp::aterm &term)
bag_container & operator=(const bag_container &) noexcept=default
\brief A basic sort
Definition basic_sort.h:26
basic_sort(const basic_sort &) noexcept=default
Move semantics.
basic_sort()
\brief Default constructor X3.
Definition basic_sort.h:29
basic_sort & operator=(const basic_sort &) noexcept=default
const core::identifier_string & name() const
Definition basic_sort.h:57
basic_sort(basic_sort &&) noexcept=default
basic_sort(const core::identifier_string &name)
\brief Constructor Z14.
Definition basic_sort.h:42
basic_sort(const std::string &name)
\brief Constructor Z2.
Definition basic_sort.h:47
basic_sort & operator=(basic_sort &&) noexcept=default
basic_sort(const atermpp::aterm &term)
Definition basic_sort.h:35
binder_type()
\brief Default constructor X3.
Definition binder_type.h:30
binder_type(binder_type &&) noexcept=default
binder_type & operator=(const binder_type &) noexcept=default
binder_type & operator=(binder_type &&) noexcept=default
binder_type(const binder_type &) noexcept=default
Move semantics.
binder_type(const atermpp::aterm &term)
Definition binder_type.h:36
\brief A container sort
container_sort()
\brief Default constructor X3.
container_sort & operator=(container_sort &&) noexcept=default
container_sort(const container_sort &) noexcept=default
Move semantics.
container_sort(const container_type &container_name, const sort_expression &element_sort)
\brief Constructor Z14.
container_sort(container_sort &&) noexcept=default
container_sort & operator=(const container_sort &) noexcept=default
const container_type & container_name() const
const sort_expression & element_sort() const
container_sort(const atermpp::aterm &term)
\brief Container type
container_type(container_type &&) noexcept=default
container_type(const atermpp::aterm &term)
container_type & operator=(const container_type &) noexcept=default
container_type & operator=(container_type &&) noexcept=default
container_type(const container_type &) noexcept=default
Move semantics.
container_type()
\brief Default constructor X3.
\brief A data equation
data_equation(const atermpp::aterm &term)
data_equation()
\brief Default constructor X3.
const data_expression & lhs() const
const data_expression & condition() const
data_equation & operator=(data_equation &&) noexcept=default
data_equation(const Container &variables, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Constructor.
const data_expression & rhs() const
data_equation(data_equation &&) noexcept=default
data_equation(const Container &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
\brief Constructor Z1.
data_equation(const variable_list &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs)
\brief Constructor Z12.
const variable_list & variables() const
data_equation & operator=(const data_equation &) noexcept=default
data_equation(const data_expression &lhs, const data_expression &rhs)
Constructor.
data_equation(const data_equation &) noexcept=default
Move semantics.
data_expression & operator=(const data_expression &) noexcept=default
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const
Apply a data expression to four data expressions.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3) const
Apply a data expression to three data expressions.
data_expression(const atermpp::aterm &term)
data_expression()
\brief Default constructor X3.
application operator()(const data_expression &e1, const data_expression &e2) const
Apply a data expression to two data expressions.
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const_iterator end() const
application operator()(const data_expression &e) const
Apply a data expression to a data expression.
data_expression(const data_expression &) noexcept=default
Move semantics.
data_expression(data_expression &&) noexcept=default
const_iterator begin() const
bool is_default_data_expression() const
A function to efficiently determine whether a data expression is made by the default constructor.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const
Apply a data expression to five data expressions.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const
Apply a data expression to six data expressions.
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.
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.
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.
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.
bool IsNotInferredL(sort_expression_list TypeList) const
bool TypeMatchL(const sort_expression_list &TypeList, const sort_expression_list &PosTypeList, sort_expression_list &result) const
bool UnFBag(sort_expression PosType, sort_expression &result) const
std::map< core::identifier_string, sort_expression_list > system_functions
Definition typecheck.h:32
bool MatchIf(const function_sort &type, sort_expression &result) const
sort_expression TraverseVarConsTypeD(const detail::variable_context &DeclaredVars, data_expression &DataTerm, const sort_expression &PosType, const bool strictly_ambiguous=true, const bool warn_upcasting=false, const bool print_cast_error=true) const
bool MatchFalseFunction(const function_sort &type, sort_expression &result) const
bool MatchListOpCons(const function_sort &type, sort_expression &result) const
std::map< core::identifier_string, sort_expression_list > system_constants
Definition typecheck.h:31
bool UnifyMinType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const
bool MatchListOpEltAt(const function_sort &type, sort_expression &result) const
const data_specification operator()() const
Yields a type checked data specification, provided typechecking was successful. If not successful an ...
bool EqTypesA(const sort_expression &Type1, const sort_expression &Type2) const
std::map< core::identifier_string, sort_expression_list > user_functions
Definition typecheck.h:34
sort_expression UpCastNumericType(sort_expression NeededType, sort_expression Type, data_expression &Par, const detail::variable_context &DeclaredVars, const bool strictly_ambiguous, bool warn_upcasting=false, const bool print_cast_error=false) const
bool UnifyElementSort(sort_expression &Arg1, sort_expression &Arg2, sort_expression &result) const
void operator()(data_equation_vector &eqns)
Yields a type checked equation list, and sets the types in the equations right. If not successful an ...
bool MatchListSetBagOpIn(const function_sort &type, sort_expression &result) const
bool match_fbag_cinsert(const function_sort &type, sort_expression &result) const
bool MatchSqrt(const function_sort &type, sort_expression &result) const
bool MatchBagOpBag2Set(const function_sort &type, sort_expression &result) const
void read_constructors_and_mappings(const function_symbol_vector &constructors, const function_symbol_vector &mappings, const function_symbol_vector &normalized_constructors)
bool MatchEqNeqComparison(const function_sort &type, sort_expression &result) const
void operator()(const variable &v, const detail::variable_context &context) const
Type checks a variable. Throws an mcrl2::runtime_error exception if the variable is not well typed.
bool InTypesL(const sort_expression_list &Type, atermpp::term_list< sort_expression_list > Types) const
sort_expression UnwindType(const sort_expression &Type) const
bool strict_type_check(const data_expression &d) const
Definition typecheck.cpp:84
bool MatchBagConstructor(const function_sort &type, sort_expression &result) const
bool MatchBagOpBagCount(const function_sort &type, sort_expression &result) const
assignment_list typecheck_assignment_list(const assignment_list &assignments, const detail::variable_context &variable_context)
Definition typecheck.h:97
sort_expression ExpandNumTypesUp(sort_expression Type) const
sort_expression ExpandNumTypesDown(sort_expression Type) const
sort_expression_list ExpandNumTypesUpL(const sort_expression_list &type_list) const
void add_constant(const data::function_symbol &f, const std::string &msg)
bool MatchSetBagOpUnionDiffIntersect(const core::identifier_string &data_term_name, const function_sort &type, sort_expression &result) const
bool MatchListOpSnoc(const function_sort &type, sort_expression &result) const
bool UnFSet(sort_expression PosType, sort_expression &result) const
bool MatchListOpConcat(const function_sort &type, sort_expression &result) const
void add_system_function(const data::function_symbol &f)
void ErrorMsgCannotCast(sort_expression CandidateType, data_expression_list Arguments, sort_expression_list ArgumentTypes, std::string previous_reason) const
void TransformVarConsTypeData(data_specification &data_spec)
void add_system_constants_and_functions(const std::vector< data::function_symbol > &v)
bool IsTypeAllowedA(const sort_expression &Type, const sort_expression &PosType) const
data_expression typecheck_data_expression(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:75
assignment typecheck_assignment(const assignment &x, const detail::variable_context &variable_context)
Definition typecheck.h:90
bool MatchSetOpSetCompl(const function_sort &type, sort_expression &result) const
void initialise_system_defined_functions(void)
bool InTypesA(const sort_expression &Type, sort_expression_list Types) const
bool MaximumType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const
std::map< core::identifier_string, sort_expression > user_constants
Definition typecheck.h:33
data_type_checker(const data_specification &data_spec)
make a data type checker. Throws a mcrl2::runtime_error exception if the data_specification is not we...
bool UnList(sort_expression PosType, sort_expression &result) const
bool MatchFuncUpdate(const function_sort &type, sort_expression &result) const
void add_system_constant(const data::function_symbol &f)
bool MatchSetOpSet2Bag(const function_sort &type, sort_expression &result) const
std::pair< bool, sort_expression_list > AdjustNotInferredList(const sort_expression_list &PosTypeList, const atermpp::term_list< sort_expression_list > &TypeListList) const
bool EqTypesL(sort_expression_list Type1, sort_expression_list Type2) const
sort_expression determine_allowed_type(const data_expression &d, const sort_expression &proposed_type) const
data_expression upcast_numeric_type(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:261
void add_function(const data::function_symbol &f, const std::string &msg, bool allow_double_decls=false)
sort_expression_list GetNotInferredList(const atermpp::term_list< sort_expression_list > &TypeListList) const
void operator()(const variable_list &l, const detail::variable_context &context) const
Type checks a variable list. Throws an mcrl2::runtime_error exception if the variables are not well t...
void read_sort(const sort_expression &SortExpr)
const data_specification & typechecked_data_specification() const
Definition typecheck.h:120
bool MatchListOpHead(const function_sort &type, sort_expression &result) const
bool match_fset_insert(const function_sort &type, sort_expression &result) const
sort_expression TraverseVarConsTypeDN(const detail::variable_context &DeclaredVars, data_expression &DataTerm, sort_expression PosType, const bool strictly_ambiguous=true, const std::size_t nFactPars=std::string::npos, const bool warn_upcasting=false, const bool print_cast_error=true) const
sort_expression_list InsertType(const sort_expression_list &TypeList, const sort_expression &Type) const
bool UnArrowProd(const sort_expression_list &ArgTypes, sort_expression PosType, sort_expression &result) const
bool TypeMatchA(const sort_expression &Type_in, const sort_expression &PosType_in, sort_expression &result) const
data_expression operator()(const data_expression &data_expr, const detail::variable_context &context) const
Type check a data expression. Throws a mcrl2::runtime_error exception if the expression is not well t...
bool IsTypeAllowedL(const sort_expression_list &TypeList, const sort_expression_list &PosTypeList) const
bool MatchSetConstructor(const function_sort &type, sort_expression &result) const
data_specification type_checked_data_spec
Definition typecheck.h:35
bool MatchListOpTail(const function_sort &type, sort_expression &result) const
variable UnwindType(const variable &v) const
atermpp::term_list< T > UnwindType(const atermpp::term_list< T > &l)
Definition typecheck.h:173
void typecheck_variable(const data_type_checker &typechecker, const variable &v) const
Definition typecheck.cpp:25
void add_context_variables(const VariableContainer &variables)
void add_context_variables(const VariableContainer &variables, const data_type_checker &typechecker)
std::map< core::identifier_string, sort_expression > m_variables
const std::map< core::identifier_string, sort_expression > & context() const
variable_context(const std::map< core::identifier_string, sort_expression > &variables)
\brief Binder for existential quantification
exists_binder(const exists_binder &) noexcept=default
Move semantics.
exists_binder & operator=(exists_binder &&) noexcept=default
exists_binder(exists_binder &&) noexcept=default
exists_binder & operator=(const exists_binder &) noexcept=default
exists_binder()
\brief Default constructor X3.
exists_binder(const atermpp::aterm &term)
existential quantification.
Definition exists.h:26
exists(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition exists.h:47
exists & operator=(exists &&) noexcept=default
exists(const aterm &d)
Definition exists.h:34
exists(exists &&) noexcept=default
exists & operator=(const exists &) noexcept=default
exists(const exists &) noexcept=default
Move semantics.
\brief Container type for finite bags
fbag_container & operator=(const fbag_container &) noexcept=default
fbag_container()
\brief Default constructor X3.
fbag_container(const fbag_container &) noexcept=default
Move semantics.
fbag_container & operator=(fbag_container &&) noexcept=default
fbag_container(const atermpp::aterm &term)
fbag_container(fbag_container &&) noexcept=default
\brief Binder for universal quantification
forall_binder(const forall_binder &) noexcept=default
Move semantics.
forall_binder & operator=(forall_binder &&) noexcept=default
forall_binder(const atermpp::aterm &term)
forall_binder()
\brief Default constructor X3.
forall_binder(forall_binder &&) noexcept=default
forall_binder & operator=(const forall_binder &) noexcept=default
universal quantification.
Definition forall.h:26
forall(forall &&) noexcept=default
forall(const aterm &d)
Definition forall.h:34
forall & operator=(const forall &) noexcept=default
forall(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition forall.h:47
forall & operator=(forall &&) noexcept=default
forall(const forall &) noexcept=default
Move semantics.
\brief Container type for finite sets
fset_container(fset_container &&) noexcept=default
fset_container(const fset_container &) noexcept=default
Move semantics.
fset_container(const atermpp::aterm &term)
fset_container()
\brief Default constructor X3.
fset_container & operator=(fset_container &&) noexcept=default
fset_container & operator=(const fset_container &) noexcept=default
\brief A function sort
const sort_expression & codomain() const
function_sort()
\brief Default constructor X3.
function_sort(const sort_expression_list &domain, const sort_expression &codomain)
\brief Constructor Z14.
function_sort & operator=(const function_sort &) noexcept=default
function_sort(const atermpp::aterm &term)
function_sort(const Container &domain, const sort_expression &codomain, typename atermpp::enable_if_container< Container, sort_expression >::type *=nullptr)
\brief Constructor Z2.
function_sort & operator=(function_sort &&) noexcept=default
function_sort(function_sort &&) noexcept=default
function_sort(const function_sort &) noexcept=default
Move semantics.
const sort_expression_list & domain() const
\brief A function symbol
function_symbol(const core::identifier_string &name, const sort_expression &sort)
Constructor.
function_symbol(const function_symbol &) noexcept=default
Move semantics.
function_symbol & operator=(function_symbol &&) noexcept=default
function_symbol()
Default constructor.
function_symbol(function_symbol &&) noexcept=default
function_symbol(const atermpp::aterm &term)
Constructor.
const core::identifier_string & name() const
const sort_expression & sort() const
function_symbol & operator=(const function_symbol &) noexcept=default
function_symbol(const std::string &name, const sort_expression &sort)
Constructor.
Abstract base class for identifier generators. Identifier generators generate fresh names that do not...
virtual core::identifier_string operator()(const std::string &hint, bool add_to_context=true)
Returns a fresh identifier, with the given hint as prefix. The returned identifier is added to the co...
virtual ~identifier_generator()=default
Destructor.
virtual void add_identifier(const core::identifier_string &s)=0
Adds the identifier s to the context.
virtual bool has_identifier(const core::identifier_string &s) const =0
Returns true if the identifier s appears in the context.
identifier_generator()=default
Constructor.
void remove_identifiers(const std::set< core::identifier_string > &ids)
Remove a set of identifiers from the context.
virtual void remove_identifier(const core::identifier_string &s)=0
Removes the identifier s from the context.
virtual void clear_context()=0
Clears the context.
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
\brief Binder for lambda abstraction
lambda_binder & operator=(lambda_binder &&) noexcept=default
lambda_binder(const atermpp::aterm &term)
lambda_binder()
\brief Default constructor X3.
lambda_binder(lambda_binder &&) noexcept=default
lambda_binder & operator=(const lambda_binder &) noexcept=default
lambda_binder(const lambda_binder &) noexcept=default
Move semantics.
function symbol.
Definition lambda.h:27
lambda(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition lambda.h:61
lambda(const variable &variable, const data_expression &body)
Definition lambda.h:49
lambda & operator=(const lambda &) noexcept=default
lambda(const aterm &d)
Definition lambda.h:37
lambda()
Constructor.
Definition lambda.h:30
lambda(const lambda &) noexcept=default
Move semantics.
lambda(lambda &&) noexcept=default
lambda & operator=(lambda &&) noexcept=default
\brief Container type for lists
list_container(list_container &&) noexcept=default
list_container()
\brief Default constructor X3.
list_container & operator=(list_container &&) noexcept=default
list_container & operator=(const list_container &) noexcept=default
list_container(const list_container &) noexcept=default
Move semantics.
list_container(const atermpp::aterm &term)
\brief A machine number
machine_number()
\brief Default constructor X2.
machine_number & operator=(machine_number &&) noexcept=default
machine_number & operator=(const machine_number &) noexcept=default
std::size_t value() const
machine_number(const machine_number &) noexcept=default
Move semantics.
machine_number(std::size_t value)
\brief Constructor Z13.
machine_number(machine_number &&) noexcept=default
machine_number(const atermpp::aterm &term)
Identifier generator that stores the identifiers of the context in a multiset. If an identifier occur...
bool has_identifier(const core::identifier_string &s) const override
Returns true if the identifier s appears in the context.
void remove_identifier(const core::identifier_string &s) override
Removes one occurrence of the identifier s from the context.
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
void clear_context() override
Clears the context.
const std::multiset< core::identifier_string > & context() const
Returns the context.
std::multiset< core::identifier_string > m_identifiers
The context of the identifier generator.
multiset_identifier_generator()=default
Constructor.
\brief Binder for set comprehension
set_comprehension_binder(const atermpp::aterm &term)
set_comprehension_binder & operator=(set_comprehension_binder &&) noexcept=default
set_comprehension_binder & operator=(const set_comprehension_binder &) noexcept=default
set_comprehension_binder()
\brief Default constructor X3.
set_comprehension_binder(set_comprehension_binder &&) noexcept=default
set_comprehension_binder(const set_comprehension_binder &) noexcept=default
Move semantics.
universal quantification.
set_comprehension & operator=(set_comprehension &&) noexcept=default
set_comprehension(set_comprehension &&) noexcept=default
set_comprehension(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
set_comprehension & operator=(const set_comprehension &) noexcept=default
set_comprehension(const set_comprehension &) noexcept=default
Move semantics.
\brief Container type for sets
set_container()
\brief Default constructor X3.
set_container(const set_container &) noexcept=default
Move semantics.
set_container(set_container &&) noexcept=default
set_container & operator=(set_container &&) noexcept=default
set_container & operator=(const set_container &) noexcept=default
set_container(const atermpp::aterm &term)
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
const std::set< core::identifier_string > & context() const
Returns the context.
void remove_identifier(const core::identifier_string &s) override
Removes one occurrence of the identifier s from the context.
set_identifier_generator()=default
Constructor.
void clear_context() override
Clears the context.
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
std::set< core::identifier_string > m_identifiers
The context of the identifier generator.
bool has_identifier(const core::identifier_string &s) const override
Returns true if the identifier s appears in the context.
\brief A sort expression
sort_expression & operator=(const sort_expression &) noexcept=default
sort_expression(const sort_expression &) noexcept=default
Move semantics.
sort_expression & operator=(sort_expression &&) noexcept=default
const sort_expression & target_sort() const
Returns the target sort of this expression.
sort_expression(sort_expression &&) noexcept=default
sort_expression()
\brief Default constructor X3.
sort_expression(const atermpp::aterm &term)
std::map< sort_expression, sort_expression > m_normalised_aliases
Table containing how sorts should be mapped to normalised sorts.
const std::set< sort_expression > & context_sorts() const
Return the user defined context sorts of the current specification.
void remove_sort(const sort_expression &s)
Removes sort from the user defined sorts in the specification. Note that this does not remove aliases...
void add_system_defined_sort(const sort_expression &s)
Adds a sort to this specification, and marks it as system defined.
basic_sort_vector m_user_defined_sorts
The basic sorts and structured sorts in the specification.
bool operator==(const sort_specification &other) const
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::map< sort_expression, sort_expression > & sort_alias_map() const
Gets a normalisation mapping that maps each sort to its unique normalised sort.
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
void add_context_sorts(const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
Adds the sorts in c to the context sorts.
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...
alias_vector m_user_defined_aliases
The basic sorts and structured sorts in the specification.
sort_specification()
Default constructor.
void sorts_are_not_necessarily_normalised_anymore() const
void data_is_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.
sort_specification(const basic_sort_vector &sorts, const alias_vector &aliases)
std::set< sort_expression > m_normalised_sorts
Set containing all the sorts, including the system defined ones.
void remove_alias(const alias &a)
Removes a user defined //alias from specification.
void add_context_sort(const sort_expression &s)
Adds the sort s to the context sorts.
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)
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
bool m_normalised_sorts_are_up_to_date
This boolean indicates whether the variables m_normalised_constructors, m_mappings,...
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...
void check_for_sort_alias_loop_through_function_sort(const basic_sort &end_search, const sort_expression &start_search, std::set< basic_sort > &visited, const bool observed_a_sort_constructor, const std::map< basic_sort, sort_expression > &alias_map)
sort_specification m_sort_specification
const sort_specification & get_sort_specification() const
void check_sort_list_is_declared(const sort_expression_list &SortExprList) const
sort_type_checker(const sort_specification &sort_spec, bool must_check_aliases=true)
constructs a sort expression checker.
void operator()(const sort_expression &x) const
Type check a sort expression. Throws an exception if the expression is not well typed.
void check_basic_sort_is_declared(const basic_sort &x) const
void check_for_empty_constructor_domains(const function_symbol_vector &constructors)
void check_alias_circularity(const data::basic_sort &lhs, const data::sort_expression &rhs, std::set< basic_sort > sort_already_seen, const std::map< basic_sort, sort_expression > &alias_map)
void check_sort_is_declared(const sort_expression &x) const
\brief An argument of a constructor of a structured sort
structured_sort_constructor_argument(const sort_expression &sort)
Constructor.
structured_sort_constructor_argument(const std::string &name, const sort_expression &sort)
\brief Constructor Z1.
structured_sort_constructor_argument(const core::identifier_string &name, const sort_expression &sort)
\brief Constructor Z12.
structured_sort_constructor_argument(structured_sort_constructor_argument &&) noexcept=default
structured_sort_constructor_argument(const char(&name)[S], const sort_expression &sort)
structured_sort_constructor_argument & operator=(const structured_sort_constructor_argument &) noexcept=default
structured_sort_constructor_argument(const structured_sort_constructor_argument &) noexcept=default
Move semantics.
structured_sort_constructor_argument & operator=(structured_sort_constructor_argument &&) noexcept=default
\brief A constructor for a structured sort
function_symbol constructor_function(const sort_expression &s) const
Returns the constructor function for this constructor, assuming it is internally represented with sor...
const core::identifier_string & name() const
structured_sort_constructor & operator=(structured_sort_constructor &&) noexcept=default
structured_sort_constructor(const char(&name)[S], const Container &arguments, const char(&recogniser)[S0], typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
structured_sort_constructor & operator=(const structured_sort_constructor &) noexcept=default
structured_sort_constructor(const structured_sort_constructor &) noexcept=default
Move semantics.
structured_sort_constructor(const core::identifier_string &name, const structured_sort_constructor_argument_list &arguments, core::identifier_string &recogniser)
\brief Constructor Z12.
structured_sort_constructor(const core::identifier_string &name, const core::identifier_string &recogniser)
Constructor.
function_symbol_vector projection_functions(const sort_expression &s) const
Returns the projection functions for this constructor.
structured_sort_constructor(structured_sort_constructor &&) noexcept=default
const core::identifier_string & recogniser() const
function_symbol recogniser_function(const sort_expression &s) const
Returns the function corresponding to the recogniser of this constructor, such that it is usable in t...
const structured_sort_constructor_argument_list & arguments() const
structured_sort_constructor()
\brief Default constructor X3.
void argument_sorts(OutIter out) const
Returns the sorts of the arguments in an output iterator.
structured_sort_constructor(const core::identifier_string &name)
Constructor.
data_equation_vector recogniser_equations() const
Generate equations for the recognisers of this sort, assuming that this sort is referred to with s.
function_symbol smaller_arguments_function(const sort_expression &s) const
structured_sort & operator=(const structured_sort &) noexcept=default
function_symbol_vector recogniser_functions(const sort_expression &s) const
function_symbol to_pos_function(const sort_expression &s) const
structured_sort(const structured_sort &) noexcept=default
Move semantics.
function_symbol_vector constructor_functions(const sort_expression &s) const
data_equation_vector comparison_equations() const
Returns the equations for the functions used to implement comparison operators on this sort....
data_equation_vector constructor_equations(const sort_expression &s) const
data_equation_vector recogniser_equations(const sort_expression &s) const
static bool has_recogniser(structured_sort_constructor const &s)
data_equation_vector projection_equations() const
Generate equations for the projection functions of this sort.
function_symbol equal_arguments_function(const sort_expression &s) const
structured_sort(const Container &constructors, typename atermpp::enable_if_container< Container, structured_sort_constructor >::type *=nullptr)
\brief Constructor Z2.
const structured_sort_constructor_list & constructors() const
function_symbol_vector constructor_functions() const
Returns the constructor functions of this sort, such that the result can be used by the rewriter.
function_symbol_vector projection_functions() const
Returns the projection functions of this sort, such that the result can be used by the rewriter.
function_symbol_vector comparison_functions(const sort_expression &s) const
function_symbol_vector comparison_functions() const
Returns the additional functions of this sort, used to implement its comparison operators.
data_equation_vector comparison_equations(const sort_expression &s) const
structured_sort(const structured_sort_constructor_list &constructors)
\brief Constructor Z14.
function_symbol_vector recogniser_functions() const
Returns the recogniser functions of this sort, such that the result can be used by the rewriter.
function_symbol_vector projection_functions(const sort_expression &s) const
structured_sort()
\brief Default constructor X3.
structured_sort(structured_sort &&) noexcept=default
data_equation_vector projection_equations(const sort_expression &s) const
structured_sort(const atermpp::aterm &term)
structured_sort & operator=(structured_sort &&) noexcept=default
data_equation_vector constructor_equations() const
Returns the equations for ==, < and <= for this sort, such that the result can be used by the rewrite...
function_symbol smaller_equal_arguments_function(const sort_expression &s) const
untyped_data_parameter(const core::identifier_string &name, const data_expression_list &arguments)
\brief Constructor Z12.
const core::identifier_string & name() const
untyped_data_parameter(const std::string &name, const data_expression_list &arguments)
\brief Constructor Z1.
const data_expression_list & arguments() const
untyped_data_parameter(const untyped_data_parameter &) noexcept=default
Move semantics.
untyped_data_parameter & operator=(untyped_data_parameter &&) noexcept=default
untyped_data_parameter & operator=(const untyped_data_parameter &) noexcept=default
untyped_data_parameter(const atermpp::aterm &term)
untyped_data_parameter(untyped_data_parameter &&) noexcept=default
untyped_data_parameter()
\brief Default constructor X3.
\brief Assignment of a data expression to a string
Definition assignment.h:182
const core::identifier_string & lhs() const
Definition assignment.h:213
untyped_identifier_assignment(const atermpp::aterm &term)
Definition assignment.h:191
untyped_identifier_assignment()
\brief Default constructor X3.
Definition assignment.h:185
const data_expression & rhs() const
Definition assignment.h:218
untyped_identifier_assignment & operator=(untyped_identifier_assignment &&) noexcept=default
untyped_identifier_assignment & operator=(const untyped_identifier_assignment &) noexcept=default
untyped_identifier_assignment(const core::identifier_string &lhs, const data_expression &rhs)
\brief Constructor Z14.
Definition assignment.h:198
untyped_identifier_assignment(untyped_identifier_assignment &&) noexcept=default
untyped_identifier_assignment(const untyped_identifier_assignment &) noexcept=default
Move semantics.
data_expression operator()(const untyped_identifier &x) const
Applies the assignment to a variable.
Definition assignment.h:226
\brief An untyped identifier
untyped_identifier(const atermpp::aterm &term)
untyped_identifier(const untyped_identifier &) noexcept=default
Move semantics.
untyped_identifier(const std::string &name)
\brief Constructor Z2.
untyped_identifier & operator=(untyped_identifier &&) noexcept=default
const core::identifier_string & name() const
untyped_identifier(untyped_identifier &&) noexcept=default
untyped_identifier & operator=(const untyped_identifier &) noexcept=default
untyped_identifier()
\brief Default constructor X3.
untyped_identifier(const core::identifier_string &name)
\brief Constructor Z14.
untyped_possible_sorts(const Container &sorts, typename atermpp::enable_if_container< Container, sort_expression >::type *=nullptr)
\brief Constructor Z2.
untyped_possible_sorts & operator=(const untyped_possible_sorts &) noexcept=default
untyped_possible_sorts(const untyped_possible_sorts &) noexcept=default
Move semantics.
untyped_possible_sorts & operator=(untyped_possible_sorts &&) noexcept=default
untyped_possible_sorts(const sort_expression_list &sorts)
\brief Constructor Z14.
untyped_possible_sorts(const atermpp::aterm &term)
untyped_possible_sorts(untyped_possible_sorts &&) noexcept=default
untyped_possible_sorts()
\brief Default constructor X3.
const sort_expression_list & sorts() const
\brief Binder for untyped set or bag comprehension
Definition binder_type.h:77
untyped_set_or_bag_comprehension_binder(untyped_set_or_bag_comprehension_binder &&) noexcept=default
untyped_set_or_bag_comprehension_binder(const atermpp::aterm &term)
Definition binder_type.h:86
untyped_set_or_bag_comprehension_binder()
\brief Default constructor X3.
Definition binder_type.h:80
untyped_set_or_bag_comprehension_binder(const untyped_set_or_bag_comprehension_binder &) noexcept=default
Move semantics.
untyped_set_or_bag_comprehension_binder & operator=(const untyped_set_or_bag_comprehension_binder &) noexcept=default
untyped_set_or_bag_comprehension_binder & operator=(untyped_set_or_bag_comprehension_binder &&) noexcept=default
untyped_set_or_bag_comprehension & operator=(untyped_set_or_bag_comprehension &&) noexcept=default
untyped_set_or_bag_comprehension(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
untyped_set_or_bag_comprehension(const untyped_set_or_bag_comprehension &) noexcept=default
Move semantics.
untyped_set_or_bag_comprehension(untyped_set_or_bag_comprehension &&) noexcept=default
untyped_set_or_bag_comprehension & operator=(const untyped_set_or_bag_comprehension &) noexcept=default
untyped_sort_variable & operator=(const untyped_sort_variable &) noexcept=default
untyped_sort_variable(const untyped_sort_variable &) noexcept=default
Move semantics.
untyped_sort_variable(const atermpp::aterm &term)
untyped_sort_variable & operator=(untyped_sort_variable &&) noexcept=default
untyped_sort_variable(untyped_sort_variable &&) noexcept=default
untyped_sort_variable(std::size_t value)
Constructor.
untyped_sort_variable(const atermpp::aterm_int &value)
\brief Constructor Z14.
untyped_sort_variable()
\brief Default constructor X3.
const atermpp::aterm_int & value() const
\brief Unknown sort expression
untyped_sort & operator=(const untyped_sort &) noexcept=default
untyped_sort(const atermpp::aterm &term)
untyped_sort(const untyped_sort &) noexcept=default
Move semantics.
untyped_sort & operator=(untyped_sort &&) noexcept=default
untyped_sort(untyped_sort &&) noexcept=default
untyped_sort()
\brief Default constructor X3.
\brief A data variable
Definition variable.h:28
variable(const variable &) noexcept=default
Move semantics.
variable(const std::string &name, const sort_expression &sort)
Constructor.
Definition variable.h:69
variable(variable &&) noexcept=default
variable()
Default constructor.
Definition variable.h:49
const core::identifier_string & name() const
Definition variable.h:38
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
Definition variable.h:43
variable & operator=(const variable &) noexcept=default
variable(const core::identifier_string &name, const sort_expression &sort)
Constructor.
Definition variable.h:62
variable(const atermpp::aterm &term)
Constructor.
Definition variable.h:55
\brief A where expression
where_clause & operator=(where_clause &&) noexcept=default
const assignment_list & assignments() const
where_clause(const where_clause &) noexcept=default
Move semantics.
where_clause(const atermpp::aterm &term)
const data_expression & body() const
const assignment_expression_list & declarations() const
where_clause & operator=(const where_clause &) noexcept=default
where_clause()
\brief Default constructor X3.
where_clause(const data_expression &body, const Container &declarations, typename atermpp::enable_if_container< Container, assignment_expression >::type *=nullptr)
\brief Constructor Z2.
where_clause(where_clause &&) noexcept=default
where_clause(const data_expression &body, const assignment_expression_list &declarations)
\brief Constructor Z14.
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
Standard exception class for reporting runtime errors.
Definition exception.h:27
runtime_error(const std::string &message)
Constructor.
Definition exception.h:31
Identifier generator that generates names consisting of a prefix followed by a number....
number_postfix_generator(std::string hint="FRESH_VAR")
Constructor.
std::string operator()(std::string hint, bool add_to_context=true) const
Generates a fresh identifier that doesn't appear in the context.
void add_identifiers(Iter first, Iter last)
Adds the strings in the range [first, last) to the context.
number_postfix_generator(Iter first, Iter last, std::string hint="FRESH_VAR")
Constructor.
void clear()
Clear the context of the generator.
std::map< std::string, std::size_t > m_index
A map that maintains the highest index for each prefix.
void add_identifier(const std::string &id)
Adds the strings in the range [first, last) to the context.
const std::string & hint() const
Returns the default hint.
std::string & hint()
Returns the default hint.
std::string operator()() const
Generates a fresh identifier that doesn't appear in the context.
D_ParserTables parser_tables_fsm
D_ParserTables parser_tables_dot
D_ParserTables parser_tables_mcrl2
Definition dparser.cpp:20
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
The main namespace for the aterm++ library.
Definition algorithm.h:21
term_list< aterm > aterm_list
A term_list with elements of type aterm.
Definition aterm_list.h:497
const aterm_string & empty_string()
Returns the empty aterm_string.
std::string pp(const atermpp::aterm &t)
Transform an aterm to an ascii string.
Definition aterm.h:440
bool check_term_PREqnSpec(const Term &t)
bool check_term_MapSpec(const Term &t)
bool check_term_PBESTrue(const Term &t)
bool check_term_Seq(const Term &t)
bool check_term_DataVarIdInit(const Term &t)
bool check_rule_DataVarIdInit(const Term &t)
bool check_term_Action(const Term &t)
bool check_term_PRESOr(const Term &t)
bool check_term_SortId(const Term &t)
bool check_term_Sum(const Term &t)
bool check_term_Whr(const Term &t)
bool check_term_ActAt(const Term &t)
bool check_rule_WhrDecl(const Term &t)
bool check_term_StateInfimum(const Term &t)
bool check_term_CommExpr(const Term &t)
bool check_rule_ActSpec(const Term &t)
bool check_term_UntypedSortUnknown(const Term &t)
bool check_term_ActFalse(const Term &t)
bool check_term_ActId(const Term &t)
bool check_term_RegTrans(const Term &t)
bool check_rule_Distribution(const Term &t)
bool check_term_LinearProcessSummand(const Term &t)
bool check_rule_Number(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedSortsPossible()
const atermpp::function_symbol & function_symbol_DataEqn()
const atermpp::function_symbol & function_symbol_DataVarId()
bool check_term_StateFalse(const Term &t)
bool check_term_argument(const Term &t, CheckFunction f)
const atermpp::function_symbol & function_symbol_StructCons()
bool check_term_UntypedSortVariable(const Term &t)
bool check_rule_ActFrm(const Term &t)
bool check_term_MultAct(const Term &t)
bool check_term_Tau(const Term &t)
bool check_rule_ActId(const Term &t)
bool check_term_UntypedProcessAssignment(const Term &t)
bool check_term_StateDelayTimed(const Term &t)
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
Definition dparser.cpp:463
bool check_term_Delta(const Term &t)
bool check_rule_PBEqn(const Term &t)
bool check_rule_Action(const Term &t)
const atermpp::function_symbol & function_symbol_SortRef()
bool check_term_PRESTrue(const Term &t)
bool check_rule_ActionRenameSpec(const Term &t)
bool check_rule_FixPoint(const Term &t)
bool check_list_argument(const Term &t, CheckFunction f, unsigned int minimum_size)
bool check_rule_DataEqn(const Term &t)
bool check_rule_LinProcSpec(const Term &t)
bool check_term_PRES(const Term &t)
bool check_rule_SortDecl(const Term &t)
bool check_rule_RenameExpr(const Term &t)
bool check_term_ActImp(const Term &t)
bool check_term_Allow(const Term &t)
bool check_term_Choice(const Term &t)
bool check_term_LinProcSpec(const Term &t)
bool check_rule_SortId(const Term &t)
bool check_term_PBESNot(const Term &t)
bool check_term_Sync(const Term &t)
const atermpp::function_symbol & function_symbol_StructProj()
bool check_rule_String(const Term &t)
bool check_term_ActMultAct(const Term &t)
bool check_term_PRESCondEq(const Term &t)
bool check_term_RegTransOrNil(const Term &t)
bool check_term_GlobVarSpec(const Term &t)
bool check_term_StateSupremum(const Term &t)
bool check_term_Mu(const Term &t)
bool check_rule_BindingOperator(const Term &t)
bool check_rule_CommExpr(const Term &t)
bool check_term_UntypedIdentifierAssignment(const Term &t)
bool check_term_RegNil(const Term &t)
bool check_term_DataEqn(const Term &t)
bool check_term_UntypedIdentifier(const Term &t)
bool check_term_StateMust(const Term &t)
bool check_rule_StructProj(const Term &t)
bool check_rule_ConsSpec(const Term &t)
bool check_term_ProcEqnSpec(const Term &t)
bool check_term_LMerge(const Term &t)
bool check_term_ConsSpec(const Term &t)
bool check_rule_SortConsType(const Term &t)
bool check_term_SortSet(const Term &t)
bool check_rule_SortSpec(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedIdentifierAssignment()
const atermpp::function_symbol & function_symbol_Binder()
bool check_rule_PRES(const Term &t)
bool check_term_Binder(const Term &t)
bool check_term_SortArrow(const Term &t)
bool check_rule_DataExpr(const Term &t)
bool check_term_StateSum(const Term &t)
bool check_term_DataVarId(const Term &t)
bool check_term_UntypedDataParameter(const Term &t)
bool check_term_PRESConstantMultiply(const Term &t)
bool check_term_PBESForall(const Term &t)
bool check_rule_DataEqnSpec(const Term &t)
bool check_term_ActTrue(const Term &t)
bool check_rule_MultActOrDelta(const Term &t)
bool check_rule_LinearProcess(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedSortVariable()
D_ParseNode * ambiguity_fn(struct D_Parser *, int n, struct D_ParseNode **v)
Function for resolving parser ambiguities.
Definition dparser.cpp:332
bool check_term_ProcessInit(const Term &t)
bool check_term_BagComp(const Term &t)
bool check_rule_ProcVarId(const Term &t)
bool check_term_SortFBag(const Term &t)
bool check_rule_PRExpr(const Term &t)
bool check_term_StateYaled(const Term &t)
const atermpp::function_symbol & function_symbol_SortArrow()
bool check_term_MultActName(const Term &t)
bool check_term_Nu(const Term &t)
bool check_term_PBESExists(const Term &t)
bool check_term_BInit(const Term &t)
bool check_term_ProcessAssignment(const Term &t)
bool check_term_Lambda(const Term &t)
bool check_term_StateMay(const Term &t)
bool check_term_PRESAnd(const Term &t)
bool check_term_StateVar(const Term &t)
bool check_term_SortRef(const Term &t)
bool check_term_PRESEqInf(const Term &t)
bool check_rule_StateFrm(const Term &t)
bool check_term_ProcSpec(const Term &t)
bool check_term_SortBag(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedDataParameter()
bool check_term_ProcEqn(const Term &t)
bool check_rule_MultActName(const Term &t)
bool check_term_StatePlus(const Term &t)
bool check_term_TimedMultAct(const Term &t)
bool check_term_PRESInfimum(const Term &t)
bool check_term_Rename(const Term &t)
bool check_rule_MapSpec(const Term &t)
bool check_rule_ProcEqnSpec(const Term &t)
bool check_rule_ProcEqn(const Term &t)
bool check_rule_PREqn(const Term &t)
bool check_term_StateYaledTimed(const Term &t)
bool check_term_StateImp(const Term &t)
bool check_term_StateConstantMultiply(const Term &t)
bool check_rule_DataVarId(const Term &t)
bool check_rule_UntypedIdentifierAssignment(const Term &t)
bool check_term_SortCons(const Term &t)
bool check_term_PRESSupremum(const Term &t)
bool check_term_PropVarInst(const Term &t)
bool check_term_UntypedRegFrm(const Term &t)
bool check_rule_PBES(const Term &t)
bool check_term_IfThen(const Term &t)
bool check_term_ActForall(const Term &t)
bool check_term_StateTrue(const Term &t)
bool check_term_SortSpec(const Term &t)
bool check_term_StateOr(const Term &t)
bool check_term_Forall(const Term &t)
bool check_term_UntypedSetBagComp(const Term &t)
bool check_term_LinearProcess(const Term &t)
bool check_term_PBInit(const Term &t)
bool check_rule_ProcExpr(const Term &t)
bool check_term_Comm(const Term &t)
bool check_term_StateAnd(const Term &t)
bool check_term_PBESOr(const Term &t)
const atermpp::function_symbol & function_symbol_SortId()
bool check_term_StateMinus(const Term &t)
bool check_term_RenameExpr(const Term &t)
bool check_term_ActExists(const Term &t)
bool check_term_LinearProcessInit(const Term &t)
bool check_rule_SortExpr(const Term &t)
bool check_term_PREqn(const Term &t)
bool check_term_UntypedMultiAction(const Term &t)
bool check_term_PBES(const Term &t)
bool check_rule_GlobVarSpec(const Term &t)
bool check_rule_ActionRenameRuleRHS(const Term &t)
bool check_term_ActAnd(const Term &t)
bool check_rule_DataSpec(const Term &t)
bool check_term_AtTime(const Term &t)
bool check_term_ActSpec(const Term &t)
bool check_term_StateMu(const Term &t)
bool check_rule_LinearProcessSummand(const Term &t)
bool check_rule_StringOrEmpty(const Term &t)
bool check_term_StateNu(const Term &t)
bool check_term_PBEqn(const Term &t)
const atermpp::function_symbol & function_symbol_Whr()
bool check_term_PRESSum(const Term &t)
bool check_term_ActionRenameSpec(const Term &t)
bool check_term_StateDelay(const Term &t)
bool check_rule_PBEqnSpec(const Term &t)
bool check_term_SortStruct(const Term &t)
bool check_rule_RegFrm(const Term &t)
bool check_rule_ActionRenameRules(const Term &t)
bool check_term_StochasticOperator(const Term &t)
bool check_rule_ProcSpec(const Term &t)
bool check_term_PBESImp(const Term &t)
bool gsIsDataAppl(const atermpp::aterm &Term)
bool check_rule_PropVarDecl(const Term &t)
bool check_term_StateForall(const Term &t)
bool check_term_PRInit(const Term &t)
bool check_term_DataEqnSpec(const Term &t)
bool check_term_StructCons(const Term &t)
const atermpp::function_symbol & function_symbol_SortStruct()
bool check_rule_ParamIdOrAction(const Term &t)
bool check_term_ProcVarId(const Term &t)
bool check_term_PRESConstantMultiplyAlt(const Term &t)
bool check_term_DataSpec(const Term &t)
bool check_term_Process(const Term &t)
bool gsIsDataAppl_no_check(const atermpp::aterm &Term)
bool check_term_ActionRenameRule(const Term &t)
bool check_rule_ActionRenameRule(const Term &t)
bool check_rule_PBExpr(const Term &t)
bool check_term_StateNot(const Term &t)
bool check_term_PRESFalse(const Term &t)
bool check_rule_UntypedMultiAction(const Term &t)
bool check_term_OpId(const Term &t)
bool check_term_Distribution(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedIdentifier()
bool check_term_ActNot(const Term &t)
bool check_term_PRESEqNInf(const Term &t)
bool check_term_UntypedSortsPossible(const Term &t)
bool check_rule_UntypedDataParameter(const Term &t)
bool check_term_Hide(const Term &t)
bool check_rule_PREqnSpec(const Term &t)
bool check_rule_TimedMultAct(const Term &t)
bool check_term_Merge(const Term &t)
bool check_rule_PropVarInst(const Term &t)
bool check_term_Exists(const Term &t)
void foreach_parse_node(const parse_node &x, Function f)
Calls the function f on each node in the parse tree with x as root.
bool check_term_SetComp(const Term &t)
bool check_term_ActOr(const Term &t)
bool check_term_StructProj(const Term &t)
bool check_term_PRESMinus(const Term &t)
bool check_rule_MultAct(const Term &t)
bool check_term_SortList(const Term &t)
bool check_term_PBEqnSpec(const Term &t)
bool check_rule_LinearProcessInit(const Term &t)
bool check_rule_PBInit(const Term &t)
bool check_term_IfThenElse(const Term &t)
bool check_term_PBESAnd(const Term &t)
bool check_rule_ProcInit(const Term &t)
bool check_term_PBESFalse(const Term &t)
bool check_rule_StructCons(const Term &t)
bool check_term_PRESPlus(const Term &t)
bool check_rule_OpId(const Term &t)
bool check_term_PropVarDecl(const Term &t)
bool check_term_SortFSet(const Term &t)
bool check_term_PRESCondSm(const Term &t)
bool check_term_Block(const Term &t)
const atermpp::function_symbol & function_symbol_SortCons()
const atermpp::function_symbol & function_symbol_OpId()
bool check_term_StateExists(const Term &t)
bool check_term_ActionRenameRules(const Term &t)
bool check_term_StateConstantMultiplyAlt(const Term &t)
bool check_term_DataAppl(const Term &t)
bool check_term_RegSeq(const Term &t)
bool check_term_PRESImp(const Term &t)
const atermpp::function_symbol & function_symbol_DataVarIdInit()
bool check_term_RegAlt(const Term &t)
bool check_rule_PRInit(const Term &t)
void warn_left_merge_merge(const parse_node &)
Prints a warning for each occurrence of 'x ||_ y || z' in the parse tree.
std::string pp(const core::identifier_string &x)
Definition core.cpp:26
apply_builder< Builder > make_apply_builder()
Definition builder.h:116
identifier_string empty_identifier_string()
Provides the empty identifier string.
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
Definition builder.h:233
void print_aterm(const T &)
Definition parse.h:250
void print_aterm(const atermpp::aterm &x)
Definition parse.h:256
atermpp::term_list< identifier_string > identifier_string_list
\brief list of identifier_strings
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
apply_builder_arg1< Builder, Arg1 > make_apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:140
void msg(const std::string &)
Definition builder.h:29
identifier_string parse_identifier(const std::string &text)
Parse an identifier.
Definition parse.h:263
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
Definition builder.h:199
bool is_user_identifier(std::string const &s)
Definition parse.h:274
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:164
bool is_greater(const application &x)
Definition print.h:229
bool is_minus(const application &x)
Definition print.h:111
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:224
bool is_equal_to(const application &x)
Definition print.h:205
bool is_snoc_list(data_expression x)
Definition print.h:291
bool is_in(const application &x)
Definition print.h:241
bool head_matches_undefined_symbol(const data_expression &x, const core::identifier_string &s)
Definition print.h:72
bool is_bag_intersection(const application &x)
Definition print.h:269
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:235
bool is_set_difference(const application &x)
Definition print.h:175
bool is_not_equal_to(const application &x)
Definition print.h:211
bool is_numeric_cast(const data_expression &x)
Definition print.h:45
void check_duplicate_variable_names(const data::variable_list &x, const std::string &msg)
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:246
bool is_divides(const application &x)
Definition print.h:153
bool is_set_union(const application &x)
Definition print.h:169
variable_list parse_variables(const std::string &text)
Definition data.cpp:213
bool is_bag_difference(const application &x)
Definition print.h:187
bool is_less_equal(const application &x)
Definition print.h:223
bool is_set_intersection(const application &x)
Definition print.h:263
sort_of_expression< variable > sort_of_variable
Function object that returns the sort of a data variable.
bool is_plus(const application &x)
Definition print.h:97
bool is_or(const application &x)
Definition print.h:199
bool is_greater_equal(const application &x)
Definition print.h:235
bool is_untyped(const data_expression &x)
Definition is_untyped.h:73
bool is_one(const data_expression &x)
Definition print.h:30
bool is_element_at(const application &x)
Definition print.h:257
bool is_bag_join(const application &x)
Definition print.h:181
bool is_concat(const application &x)
Definition print.h:275
bool is_and(const application &x)
Definition print.h:193
bool look_through_numeric_casts(const data_expression &x, std::function< bool(const data_expression &)> f)
Definition print.h:61
bool is_snoc(const application &x)
Definition print.h:307
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:203
bool is_implies(const application &x)
Definition print.h:163
bool is_cons_list(data_expression x)
Definition print.h:281
bool is_mod(const application &x)
Definition print.h:122
bool is_divmod(const application &x)
Definition print.h:143
bool is_div(const application &x)
Definition print.h:132
bool is_times(const application &x)
Definition print.h:247
bool is_cons(const application &x)
Definition print.h:301
bool is_less(const application &x)
Definition print.h:217
A collection of utilities for lazy expression construction.
data_expression implies(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p implies q.
data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns and applied to the sequence of data expressions [first, last)
data_expression not_(data_expression const &p)
Returns an expression equivalent to not p.
data_expression equal_to(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p == q.
data_expression not_equal_to(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p == q.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
data_expression or_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p and q.
data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns or applied to the sequence of data expressions [first, last)
data_expression if_(const data_expression &cond, const data_expression &then, const data_expression &else_)
Returns an expression equivalent to if(cond,then,else_)
Namespace for system defined sort bag.
Definition bag1.h:38
function_symbol fbag2fset(const sort_expression &s)
Constructor for function symbol @fbag2fset.
Definition bag1.h:1475
bool is_bag2set_application(const atermpp::aterm &e)
Recogniser for application of Bag2Set.
Definition bag1.h:751
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition bag1.h:559
void make_bool2nat_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Bool2Nat_.
Definition bag1.h:1243
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition bag1.h:668
const core::identifier_string & fbag2fset_name()
Generate identifier @fbag2fset.
Definition bag1.h:1465
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bag1.h:1636
bool is_min_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @min_.
Definition bag1.h:1029
function_symbol bag_fbag(const sort_expression &s)
Constructor for function symbol @bagfbag.
Definition bag1.h:176
bool is_min_function_application(const atermpp::aterm &e)
Recogniser for application of @min_.
Definition bag1.h:1065
function_symbol monus_function(const sort_expression &s)
Constructor for function symbol @monus_.
Definition bag1.h:1083
const core::identifier_string & fbag_intersect_name()
Generate identifier @fbag_inter.
Definition bag1.h:1329
void make_bag2set(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Bag2Set.
Definition bag1.h:741
bool is_fbag_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_diff.
Definition bag1.h:1417
bool is_fbag_join_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_join.
Definition bag1.h:1281
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol count.
Definition bag1.h:336
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
Definition bag1.h:1529
application zero_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @zero_.
Definition bag1.h:855
const core::identifier_string & bool2nat_function_name()
Generate identifier @Bool2Nat_.
Definition bag1.h:1199
void make_one_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @one_.
Definition bag1.h:927
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition bag1.h:1684
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition bag1.h:689
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:612
const core::identifier_string & set2bag_name()
Generate identifier Set2Bag.
Definition bag1.h:759
bool is_bag_fbag_application(const atermpp::aterm &e)
Recogniser for application of @bagfbag.
Definition bag1.h:220
application fbag2fset(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fbag2fset.
Definition bag1.h:1500
function_symbol_vector bag_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for bag.
Definition bag1.h:1562
void make_add_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @add_.
Definition bag1.h:991
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag1.h:1706
bool is_fbag_difference_application(const atermpp::aterm &e)
Recogniser for application of @fbag_diff.
Definition bag1.h:1457
bool is_bag_fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagfbag.
Definition bag1.h:186
const core::identifier_string & zero_function_name()
Generate identifier @zero_.
Definition bag1.h:821
const core::identifier_string & add_function_name()
Generate identifier @add_.
Definition bag1.h:945
application bag2set(const sort_expression &s, const data_expression &arg0)
Application of function symbol Bag2Set.
Definition bag1.h:731
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition bag1.h:389
function_symbol_vector bag_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for bag.
Definition bag1.h:143
bool is_fbag2fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag2fset.
Definition bag1.h:1485
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition bag1.h:495
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:707
bool is_monus_function_application(const atermpp::aterm &e)
Recogniser for application of @monus_.
Definition bag1.h:1129
const core::identifier_string & nat2bool_function_name()
Generate identifier @Nat2Bool_.
Definition bag1.h:1137
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:511
bool is_zero_function_application(const atermpp::aterm &e)
Recogniser for application of @zero_.
Definition bag1.h:875
const core::identifier_string & fbag_difference_name()
Generate identifier @fbag_diff.
Definition bag1.h:1397
void make_monus_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus_.
Definition bag1.h:1119
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.
Definition bag1.h:1612
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition bag1.h:309
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:298
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...
Definition bag1.h:156
function_symbol add_function(const sort_expression &s)
Constructor for function symbol @add_.
Definition bag1.h:955
bool is_nat2bool_function_application(const atermpp::aterm &e)
Recogniser for application of @Nat2Bool_.
Definition bag1.h:1191
function_symbol fbag_intersect(const sort_expression &s)
Constructor for function symbol @fbag_inter.
Definition bag1.h:1339
void make_fbag_intersect(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_inter.
Definition bag1.h:1379
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition bag1.h:458
void make_nat2bool_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Nat2Bool_.
Definition bag1.h:1181
application bag_fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagfbag.
Definition bag1.h:200
bool is_fbag_intersect_application(const atermpp::aterm &e)
Recogniser for application of @fbag_inter.
Definition bag1.h:1389
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition bag1.h:410
function_symbol fbag_difference(const sort_expression &s)
Constructor for function symbol @fbag_diff.
Definition bag1.h:1407
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition bag1.h:373
application bool2nat_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Bool2Nat_.
Definition bag1.h:1233
bool is_bag_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagcomp.
Definition bag1.h:248
void make_min_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @min_.
Definition bag1.h:1055
data_expression bag_enumeration(const sort_expression &s, data_expression_list const &range)
Application of function symbol bag_enumeration.
const core::identifier_string & min_function_name()
Generate identifier @min_.
Definition bag1.h:1009
bool is_set2bag_function_symbol(const atermpp::aterm &e)
Recogniser for function Set2Bag.
Definition bag1.h:779
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition bag1.h:474
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bag1.h:1624
function_symbol_vector bag_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for bag.
Definition bag1.h:1576
bool is_nat2bool_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Nat2Bool_.
Definition bag1.h:1157
application one_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @one_.
Definition bag1.h:917
const core::identifier_string & monus_function_name()
Generate identifier @monus_.
Definition bag1.h:1073
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition bag1.h:1696
bool is_add_function_application(const atermpp::aterm &e)
Recogniser for application of @add_.
Definition bag1.h:1001
void make_fbag2fset(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fbag2fset.
Definition bag1.h:1511
void make_fbag_join(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_join.
Definition bag1.h:1311
function_symbol min_function(const sort_expression &s)
Constructor for function symbol @min_.
Definition bag1.h:1019
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:769
const core::identifier_string & bag_fbag_name()
Generate identifier @bagfbag.
Definition bag1.h:166
const core::identifier_string & bag2set_name()
Generate identifier Bag2Set.
Definition bag1.h:697
const core::identifier_string & intersection_name()
Generate identifier *.
Definition bag1.h:503
application nat2bool_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Nat2Bool_.
Definition bag1.h:1171
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition bag1.h:400
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @bag.
Definition bag1.h:103
application fbag_intersect(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_inter.
Definition bag1.h:1366
function_symbol bag_comprehension(const sort_expression &s)
Constructor for function symbol @bagcomp.
Definition bag1.h:238
bool is_bag2set_function_symbol(const atermpp::aterm &e)
Recogniser for function Bag2Set.
Definition bag1.h:717
bool is_bool2nat_function_application(const atermpp::aterm &e)
Recogniser for application of @Bool2Nat_.
Definition bag1.h:1253
const core::identifier_string & fbag_join_name()
Generate identifier @fbag_join.
Definition bag1.h:1261
bool is_bag_enumeration_application(const atermpp::aterm &e)
Recogniser for application of bag_enumeration.
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition bag1.h:586
function_symbol fbag_join(const sort_expression &s)
Constructor for function symbol @fbag_join.
Definition bag1.h:1271
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @bag.
Definition bag1.h:124
core::identifier_string const & bag_enumeration_name()
Generate identifier bag_enumeration.
bool is_zero_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @zero_.
Definition bag1.h:841
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:78
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition bag1.h:1672
const core::identifier_string & constructor_name()
Generate identifier @bag.
Definition bag1.h:68
bool is_bag_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @bagcomp.
Definition bag1.h:282
bool is_set2bag_application(const atermpp::aterm &e)
Recogniser for application of Set2Bag.
Definition bag1.h:813
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:362
void make_zero_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @zero_.
Definition bag1.h:865
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition bag1.h:1660
void make_bag_fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagfbag.
Definition bag1.h:210
function_symbol bag_enumeration(const sort_expression &s)
Constructor for function symbol bag_enumeration.
function_symbol bool2nat_function(const sort_expression &s)
Constructor for function symbol @Bool2Nat_.
Definition bag1.h:1209
void make_set2bag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Set2Bag.
Definition bag1.h:803
const core::identifier_string & union_name()
Generate identifier +.
Definition bag1.h:418
bool is_fbag_intersect_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_inter.
Definition bag1.h:1349
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:426
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition bag1.h:596
void make_bag_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagcomp.
Definition bag1.h:272
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bag1.h:1648
data_expression bag_enumeration(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=0)
Application of function symbol bag_enumeration.
void make_fbag_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_diff.
Definition bag1.h:1447
const core::identifier_string & count_name()
Generate identifier count.
Definition bag1.h:290
void make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition bag1.h:485
function_symbol nat2bool_function(const sort_expression &s)
Constructor for function symbol @Nat2Bool_.
Definition bag1.h:1147
bool is_one_function_application(const atermpp::aterm &e)
Recogniser for application of @one_.
Definition bag1.h:937
application fbag_difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_diff.
Definition bag1.h:1434
bool is_bag_enumeration_function_symbol(const atermpp::aterm &e)
Recogniser for function bag_enumeration.
application add_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @add_.
Definition bag1.h:980
const core::identifier_string & difference_name()
Generate identifier -.
Definition bag1.h:604
application set2bag(const sort_expression &s, const data_expression &arg0)
Application of function symbol Set2Bag.
Definition bag1.h:793
bool is_bool2nat_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Bool2Nat_.
Definition bag1.h:1219
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag1.h:55
application monus_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus_.
Definition bag1.h:1108
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:44
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition bag1.h:652
bool is_fbag2fset_application(const atermpp::aterm &e)
Recogniser for application of @fbag2fset.
Definition bag1.h:1521
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition bag1.h:151
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition bag1.h:575
const core::identifier_string & in_name()
Generate identifier in.
Definition bag1.h:354
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @bag.
Definition bag1.h:88
const core::identifier_string & bag_comprehension_name()
Generate identifier @bagcomp.
Definition bag1.h:228
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition bag1.h:346
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition bag1.h:679
application fbag_join(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_join.
Definition bag1.h:1298
const core::identifier_string & one_function_name()
Generate identifier @one_.
Definition bag1.h:883
bool is_add_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @add_.
Definition bag1.h:965
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @bag.
Definition bag1.h:114
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:831
bool is_one_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_.
Definition bag1.h:903
application bag_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagcomp.
Definition bag1.h:262
function_symbol one_function(const sort_expression &s)
Constructor for function symbol @one_.
Definition bag1.h:893
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition bag1.h:325
application min_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @min_.
Definition bag1.h:1044
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag1.h:132
bool is_fbag_join_application(const atermpp::aterm &e)
Recogniser for application of @fbag_join.
Definition bag1.h:1321
bool is_monus_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus_.
Definition bag1.h:1093
Namespace for system defined sort bool_.
Definition bool.h:32
data_equation_vector bool_generate_equations_code()
Give all system defined equations for bool_.
Definition bool.h:502
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:119
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bool.h:469
function_symbol_vector bool_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for bool_.
Definition bool.h:442
function_symbol_vector bool_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for bool_.
Definition bool.h:141
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const core::identifier_string & implies_name()
Generate identifier =>.
Definition bool.h:353
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const core::identifier_string & or_name()
Generate identifier ||.
Definition bool.h:289
implementation_map bool_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition bool.h:154
const function_symbol & implies()
Constructor for function symbol =>.
Definition bool.h:363
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:493
bool is_not_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition bool.h:183
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:409
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:197
bool is_boolean_constant(data_expression const &b)
Determines whether b is a Boolean constant.
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
application and_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol &&.
Definition bool.h:260
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition bool.h:150
function_symbol_vector bool_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for bool_.
Definition bool.h:429
const core::identifier_string & not_name()
Generate identifier !.
Definition bool.h:163
application implies(const data_expression &arg0, const data_expression &arg1)
Application of function symbol =>.
Definition bool.h:388
function_symbol_vector bool_generate_constructors_code()
Give all system defined constructors for bool_.
Definition bool.h:130
implementation_map bool_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for bool_.
Definition bool.h:458
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:324
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const core::identifier_string & bool_name()
Definition bool.h:35
bool is_and_function_symbol(const atermpp::aterm &e)
Recogniser for function &&.
Definition bool.h:245
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
data_expression bool_(bool b)
Constructs expression of type Bool from an integral type.
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:299
bool is_or_function_symbol(const atermpp::aterm &e)
Recogniser for function ||.
Definition bool.h:309
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:87
const core::identifier_string & false_name()
Generate identifier false.
Definition bool.h:99
const core::identifier_string & true_name()
Generate identifier true.
Definition bool.h:67
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
function_symbol_vector bool_generate_functions_code()
Give all system defined mappings for bool_.
Definition bool.h:416
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
void make_not_(data_expression &result, const data_expression &arg0)
Make an application of function symbol !.
Definition bool.h:207
void make_and_(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol &&.
Definition bool.h:271
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_implies_function_symbol(const atermpp::aterm &e)
Recogniser for function =>.
Definition bool.h:373
void make_or_(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ||.
Definition bool.h:335
void make_implies(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol =>.
Definition bool.h:399
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:481
const core::identifier_string & and_name()
Generate identifier &&.
Definition bool.h:225
Namespace for system defined sort fbag.
Definition fbag1.h:37
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {:}.
Definition fbag1.h:87
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol count.
Definition fbag1.h:379
const core::identifier_string & count_all_name()
Generate identifier #.
Definition fbag1.h:715
function_symbol_vector fbag_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for fbag.
Definition fbag1.h:796
const core::identifier_string & fset2fbag_name()
Generate identifier @fset2fbag.
Definition fbag1.h:461
application fset2fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @fset2fbag.
Definition fbag1.h:495
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition fbag1.h:558
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition fbag1.h:417
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition fbag1.h:671
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition fbag1.h:622
const core::identifier_string & count_name()
Generate identifier count.
Definition fbag1.h:333
const core::identifier_string & cinsert_name()
Generate identifier @fbag_cinsert.
Definition fbag1.h:267
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fbag1.h:579
function_symbol intersection(const sort_expression &s)
Constructor for function symbol *.
Definition fbag1.h:597
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fbag1.h:868
function_symbol union_(const sort_expression &s)
Constructor for function symbol +.
Definition fbag1.h:533
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fbag1.h:904
bool is_cinsert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_cinsert.
Definition fbag1.h:287
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fbag_cons.
Definition fbag1.h:211
bool is_insert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_insert.
Definition fbag1.h:119
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fbag1.h:643
function_symbol count_all(const sort_expression &s)
Constructor for function symbol #.
Definition fbag1.h:725
application fbag(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
Constructs a finite bag expression from a range of expressions Type Sequence must be a model of the F...
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition fbag1.h:633
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_cons.
Definition fbag1.h:221
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition fbag1.h:432
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fbag_insert.
Definition fbag1.h:109
application fbag(const sort_expression &s, const data_expression_list &range)
Constructs a finite bag expression from a list of expressions.
application insert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_insert.
Definition fbag1.h:135
void make_fset2fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @fset2fbag.
Definition fbag1.h:505
void make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fbag_cons.
Definition fbag1.h:249
const core::identifier_string & cons_name()
Generate identifier @fbag_cons.
Definition fbag1.h:201
application cinsert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_cinsert.
Definition fbag1.h:303
bool is_fset2fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset2fbag.
Definition fbag1.h:481
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fbag1.h:453
const core::identifier_string & empty_name()
Generate identifier {:}.
Definition fbag1.h:67
const core::identifier_string & difference_name()
Generate identifier -.
Definition fbag1.h:651
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fbag1.h:707
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition fbag1.h:389
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cons.
Definition fbag1.h:259
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition fbag1.h:443
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fbag1.h:880
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fbag1.h:856
void make_count_all(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition fbag1.h:759
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition fbag1.h:353
application count_all(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition fbag1.h:749
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition fbag1.h:607
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_cons.
Definition fbag1.h:237
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...
Definition fbag1.h:191
const core::identifier_string & intersection_name()
Generate identifier *.
Definition fbag1.h:587
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fbag1.h:892
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition fbag1.h:407
function_symbol_vector fbag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fbag.
Definition fbag1.h:165
bool is_count_all_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fbag1.h:769
function_symbol count(const sort_expression &s)
Constructor for function symbol count.
Definition fbag1.h:343
void make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition fbag1.h:569
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.
Definition fbag1.h:832
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
Definition fbag1.h:54
void make_cinsert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fbag_cinsert.
Definition fbag1.h:315
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition fbag1.h:686
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:77
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition fbag1.h:697
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:277
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cinsert.
Definition fbag1.h:325
void make_insert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fbag_insert.
Definition fbag1.h:147
bool is_fset2fbag_application(const atermpp::aterm &e)
Recogniser for application of @fset2fbag.
Definition fbag1.h:515
bool is_count_all_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition fbag1.h:735
function_symbol_vector fbag_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for fbag.
Definition fbag1.h:810
function_symbol fset2fbag(const sort_expression &s)
Constructor for function symbol @fset2fbag.
Definition fbag1.h:471
const core::identifier_string & union_name()
Generate identifier +.
Definition fbag1.h:523
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition fbag1.h:368
function_symbol difference(const sort_expression &s)
Constructor for function symbol -.
Definition fbag1.h:661
function_symbol_vector fbag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fbag.
Definition fbag1.h:777
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_insert.
Definition fbag1.h:157
const core::identifier_string & insert_name()
Generate identifier @fbag_insert.
Definition fbag1.h:99
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition fbag1.h:186
data_equation_vector fbag_generate_equations_code(const sort_expression &s)
Give all system defined equations for fbag.
Definition fbag1.h:914
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition fbag1.h:543
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fbag1.h:844
function_symbol_vector fbag_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for fbag.
Definition fbag1.h:177
const core::identifier_string & in_name()
Generate identifier in.
Definition fbag1.h:397
Namespace for system defined sort fset.
Definition fset1.h:35
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:107
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
Definition fset1.h:52
function_symbol_vector fset_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for fset.
Definition fset1.h:676
void make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition fset1.h:501
application count(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition fset1.h:617
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {}.
Definition fset1.h:85
application insert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fset_insert.
Definition fset1.h:132
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fset1.h:383
bool is_cinsert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_cinsert.
Definition fset1.h:281
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition fset1.h:603
function_symbol_vector fset_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for fset.
Definition fset1.h:662
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fset_cinsert.
Definition fset1.h:271
function_symbol_vector fset_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for fset.
Definition fset1.h:173
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_cons.
Definition fset1.h:217
function_symbol_vector fset_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fset.
Definition fset1.h:161
const core::identifier_string & empty_name()
Generate identifier {}.
Definition fset1.h:65
application fset(const sort_expression &s, const data_expression_list &range)
Constructs a finite set expression from a list of expressions.
const core::identifier_string & intersection_name()
Generate identifier *.
Definition fset1.h:519
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition fset1.h:362
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...
Definition fset1.h:187
bool is_insert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_insert.
Definition fset1.h:117
function_symbol_vector fset_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fset.
Definition fset1.h:645
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fset_cons.
Definition fset1.h:232
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition fset1.h:411
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fset_cons.
Definition fset1.h:207
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition fset1.h:565
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.
Definition fset1.h:696
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
const core::identifier_string & difference_name()
Generate identifier -.
Definition fset1.h:391
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition fset1.h:475
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition fset1.h:437
function_symbol intersection(const sort_expression &s)
Constructor for function symbol *.
Definition fset1.h:529
void make_cinsert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @fset_cinsert.
Definition fset1.h:309
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fset1.h:720
function_symbol difference(const sort_expression &s)
Constructor for function symbol -.
Definition fset1.h:401
void make_insert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fset_insert.
Definition fset1.h:143
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition fset1.h:182
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition fset1.h:539
const core::identifier_string & cinsert_name()
Generate identifier @fset_cinsert.
Definition fset1.h:261
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition fset1.h:347
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition fset1.h:627
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fset1.h:708
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition fset1.h:337
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fset1.h:447
const core::identifier_string & count_name()
Generate identifier #.
Definition fset1.h:583
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fset1.h:744
data_equation_vector fset_generate_equations_code(const sort_expression &s)
Give all system defined equations for fset.
Definition fset1.h:778
const core::identifier_string & union_name()
Generate identifier +.
Definition fset1.h:455
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fset1.h:732
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition fset1.h:373
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fset1.h:756
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fset1.h:637
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition fset1.h:593
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fset_cons.
Definition fset1.h:253
application cinsert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fset_cinsert.
Definition fset1.h:297
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fset1.h:575
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition fset1.h:426
application fset(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
Constructs a finite set expression from a range of expressions.
const core::identifier_string & insert_name()
Generate identifier @fset_insert.
Definition fset1.h:97
void make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fset_cons.
Definition fset1.h:243
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition fset1.h:490
const core::identifier_string & cons_name()
Generate identifier @fset_cons.
Definition fset1.h:197
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fset1.h:768
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition fset1.h:554
function_symbol union_(const sort_expression &s)
Constructor for function symbol +.
Definition fset1.h:465
const core::identifier_string & in_name()
Generate identifier in.
Definition fset1.h:327
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fset_cinsert.
Definition fset1.h:319
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fset1.h:511
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fset_insert.
Definition fset1.h:153
Namespace for system defined sort int_.
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition int1.h:652
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition int1.h:1516
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition int1.h:642
const core::identifier_string & cint_name()
Generate identifier @cInt.
Definition int1.h:70
application cint(const data_expression &arg0)
Application of function symbol @cInt.
Definition int1.h:104
application abs(const data_expression &arg0)
Application of function symbol abs.
Definition int1.h:694
application nat2int(const data_expression &arg0)
Application of function symbol Nat2Int.
Definition int1.h:260
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition int1.h:835
application cneg(const data_expression &arg0)
Application of function symbol @cNeg.
Definition int1.h:166
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:1050
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition int1.h:571
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition int1.h:820
const core::identifier_string & abs_name()
Generate identifier abs.
Definition int1.h:660
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition int1.h:615
bool is_int2pos_application(const atermpp::aterm &e)
Recogniser for application of Int2Pos.
Definition int1.h:466
const core::identifier_string & pred_name()
Generate identifier pred.
Definition int1.h:863
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition int1.h:1353
bool is_int2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Pos.
Definition int1.h:432
const function_symbol & pos2int()
Constructor for function symbol Pos2Int.
Definition int1.h:360
const core::identifier_string & nat2int_name()
Generate identifier Nat2Int.
Definition int1.h:226
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition int1.h:1492
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition int1.h:1077
application negate(const data_expression &arg0)
Application of function symbol -.
Definition int1.h:756
bool is_cneg_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNeg.
Definition int1.h:152
std::enable_if< std::is_integral< T >::value &&std::is_unsigned< T >::value, data_expression >::type int_(T t)
Constructs expression of type pos from an integral type.
const core::identifier_string & int2pos_name()
Generate identifier Int2Pos.
Definition int1.h:412
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:482
void make_cneg(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNeg.
Definition int1.h:176
application int2nat(const data_expression &arg0)
Application of function symbol Int2Nat.
Definition int1.h:322
function_symbol pred(const sort_expression &s0)
Definition int1.h:871
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition int1.h:1002
const core::identifier_string & cneg_name()
Generate identifier @cNeg.
Definition int1.h:132
const core::identifier_string & exp_name()
Generate identifier exp.
Definition int1.h:1317
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition int1.h:1380
const core::identifier_string & minimum_name()
Generate identifier min.
Definition int1.h:579
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition int1.h:1309
const core::identifier_string & int_name()
Definition int1.h:38
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition int1.h:1272
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition int1.h:550
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition int1.h:1147
function_symbol_vector int_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for int_.
Definition int1.h:1444
const core::identifier_string & pos2int_name()
Generate identifier Pos2Int.
Definition int1.h:350
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:298
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:57
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1039
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition int1.h:934
const function_symbol & nat2int()
Constructor for function symbol Nat2Int.
Definition int1.h:236
application div(const data_expression &arg0, const data_expression &arg1)
Application of function symbol div.
Definition int1.h:1224
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition int1.h:1168
const core::identifier_string & maximum_name()
Generate identifier max.
Definition int1.h:474
bool is_int2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Nat.
Definition int1.h:308
bool is_cneg_application(const atermpp::aterm &e)
Recogniser for application of @cNeg.
Definition int1.h:186
const core::identifier_string & succ_name()
Generate identifier succ.
Definition int1.h:784
const function_symbol & cneg()
Constructor for function symbol @cNeg.
Definition int1.h:142
void make_pos2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Int.
Definition int1.h:394
const function_symbol & abs()
Constructor for function symbol abs.
Definition int1.h:670
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1325
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:124
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition int1.h:1131
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition int1.h:1023
const core::identifier_string & mod_name()
Generate identifier mod.
Definition int1.h:1253
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition int1.h:1013
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
Definition int1.h:1525
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition int1.h:1066
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:950
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition int1.h:631
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:422
bool is_integer_constant(const data_expression &n)
Determines whether n is an integer constant.
const core::identifier_string & plus_name()
Generate identifier +.
Definition int1.h:942
function_symbol_vector int_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for int_.
Definition int1.h:1431
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition int1.h:1235
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:776
function_symbol negate(const sort_expression &s0)
Definition int1.h:730
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition int1.h:1245
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition int1.h:1299
bool is_pos2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Int.
Definition int1.h:370
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
Definition int1.h:193
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition int1.h:714
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition int1.h:561
function_symbol_vector int_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for int_.
Definition int1.h:204
application int2pos(const data_expression &arg0)
Application of function symbol Int2Pos.
Definition int1.h:446
function_symbol succ(const sort_expression &s0)
Definition int1.h:792
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition int1.h:766
const core::identifier_string & negate_name()
Generate identifier -.
Definition int1.h:722
bool is_cint_function_symbol(const atermpp::aterm &e)
Recogniser for function @cInt.
Definition int1.h:90
std::string integer_constant_as_string(const data_expression &n)
Return the string representation of an integer number.
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition int1.h:704
std::enable_if< std::is_integral< T >::value &&std::is_signed< T >::value, data_expression >::type int_(T t)
Constructs expression of type pos from an integral type.
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
Definition int1.h:1397
implementation_map int_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition int1.h:217
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition int1.h:1390
application mod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol mod.
Definition int1.h:1288
void make_nat2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Int.
Definition int1.h:270
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:80
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
Definition int1.h:1481
application pos2int(const data_expression &arg0)
Application of function symbol Pos2Int.
Definition int1.h:384
bool is_nat2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Int.
Definition int1.h:246
bool is_int2nat_application(const atermpp::aterm &e)
Recogniser for application of Int2Nat.
Definition int1.h:342
const core::identifier_string & minus_name()
Generate identifier -.
Definition int1.h:1031
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1261
const core::identifier_string & int2nat_name()
Generate identifier Int2Nat.
Definition int1.h:288
const core::identifier_string & div_name()
Generate identifier div.
Definition int1.h:1176
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition int1.h:534
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition int1.h:1369
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition int1.h:1208
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition int1.h:914
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:741
void make_int2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Pos.
Definition int1.h:456
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1103
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition int1.h:986
bool is_nat2int_application(const atermpp::aterm &e)
Recogniser for application of Nat2Int.
Definition int1.h:280
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:1087
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition int1.h:1158
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:587
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition int1.h:899
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1184
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition int1.h:845
bool is_pos2int_application(const atermpp::aterm &e)
Recogniser for application of Pos2Int.
Definition int1.h:404
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition int1.h:924
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition int1.h:213
void make_cint(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cInt.
Definition int1.h:114
void make_int2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Nat.
Definition int1.h:332
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition int1.h:680
const core::identifier_string & times_name()
Generate identifier *.
Definition int1.h:1095
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition int1.h:1504
NUMERIC_VALUE integer_constant_to_value(const data_expression &n)
Return the NUMERIC_VALUE representation of an integer number.
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition int1.h:855
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:47
Namespace for system defined sort list.
Definition list1.h:36
const core::identifier_string & rtail_name()
Generate identifier rtail.
Definition list1.h:702
const core::identifier_string & snoc_name()
Generate identifier <|.
Definition list1.h:324
bool is_rhead_function_symbol(const atermpp::aterm &e)
Recogniser for function rhead.
Definition list1.h:660
bool is_rhead_application(const atermpp::aterm &e)
Recogniser for application of rhead.
Definition list1.h:694
bool is_snoc_function_symbol(const atermpp::aterm &e)
Recogniser for function <|.
Definition list1.h:344
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition list1.h:282
function_symbol_vector list_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for list.
Definition list1.h:174
const core::identifier_string & tail_name()
Generate identifier tail.
Definition list1.h:578
application head(const sort_expression &s, const data_expression &arg0)
Application of function symbol head.
Definition list1.h:550
bool is_tail_application(const atermpp::aterm &e)
Recogniser for application of tail.
Definition list1.h:632
bool is_element_at_function_symbol(const atermpp::aterm &e)
Recogniser for function ..
Definition list1.h:472
void make_snoc(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol <|.
Definition list1.h:370
bool is_list_enumeration_application(const atermpp::aterm &e)
Recogniser for application of list_enumeration.
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition list1.h:218
const core::identifier_string & rhead_name()
Generate identifier rhead.
Definition list1.h:640
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings for list.
Definition list1.h:764
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.
Definition list1.h:819
const core::identifier_string & in_name()
Generate identifier in.
Definition list1.h:198
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition list1.h:208
bool is_rtail_function_symbol(const atermpp::aterm &e)
Recogniser for function rtail.
Definition list1.h:722
bool is_concat_application(const atermpp::aterm &e)
Recogniser for application of ++.
Definition list1.h:444
const core::identifier_string & head_name()
Generate identifier head.
Definition list1.h:516
application concat(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol ++.
Definition list1.h:423
const core::identifier_string & cons_name()
Generate identifier |>.
Definition list1.h:98
const core::identifier_string & concat_name()
Generate identifier ++.
Definition list1.h:388
function_symbol rtail(const sort_expression &s)
Constructor for function symbol rtail.
Definition list1.h:712
const core::identifier_string & count_name()
Generate identifier #.
Definition list1.h:262
void make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol |>.
Definition list1.h:144
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
Definition list1.h:865
void make_rhead(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rhead.
Definition list1.h:684
bool is_tail_function_symbol(const atermpp::aterm &e)
Recogniser for function tail.
Definition list1.h:598
application rhead(const sort_expression &s, const data_expression &arg0)
Application of function symbol rhead.
Definition list1.h:674
function_symbol_vector list_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for list.
Definition list1.h:797
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition list1.h:254
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...
Definition list1.h:188
function_symbol_vector list_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for list.
Definition list1.h:783
application rtail(const sort_expression &s, const data_expression &arg0)
Application of function symbol rtail.
Definition list1.h:736
bool is_rtail_application(const atermpp::aterm &e)
Recogniser for application of rtail.
Definition list1.h:756
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
Definition list1.h:76
application tail(const sort_expression &s, const data_expression &arg0)
Application of function symbol tail.
Definition list1.h:612
function_symbol element_at(const sort_expression &s)
Constructor for function symbol ..
Definition list1.h:462
const core::identifier_string & empty_name()
Generate identifier [].
Definition list1.h:66
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
Definition list1.h:162
void make_concat(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ++.
Definition list1.h:434
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol |>.
Definition list1.h:133
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition list1.h:244
const core::identifier_string & element_at_name()
Generate identifier ..
Definition list1.h:452
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:526
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of |>.
Definition list1.h:154
bool is_snoc_application(const atermpp::aterm &e)
Recogniser for application of <|.
Definition list1.h:380
function_symbol list_enumeration(const sort_expression &s)
Constructor for function symbol list_enumeration.
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition list1.h:183
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list1.h:42
function_symbol snoc(const sort_expression &s)
Constructor for function symbol <|.
Definition list1.h:334
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition list1.h:272
bool is_element_at_application(const atermpp::aterm &e)
Recogniser for application of ..
Definition list1.h:508
core::identifier_string const & list_enumeration_name()
Generate identifier list_enumeration.
application list(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
Constructs a list expression from a range of expressions.
data_expression list_enumeration(const sort_expression &s, data_expression_list const &range)
Application of function symbol list_enumeration.
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition list1.h:831
void make_head(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol head.
Definition list1.h:560
function_symbol rhead(const sort_expression &s)
Constructor for function symbol rhead.
Definition list1.h:650
void make_element_at(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ..
Definition list1.h:498
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition list1.h:316
void make_rtail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rtail.
Definition list1.h:746
bool is_head_application(const atermpp::aterm &e)
Recogniser for application of head.
Definition list1.h:570
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition list1.h:306
function_symbol tail(const sort_expression &s)
Constructor for function symbol tail.
Definition list1.h:588
data_expression list_enumeration(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
Application of function symbol list_enumeration.
void make_tail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol tail.
Definition list1.h:622
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
Definition list1.h:108
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function |>.
Definition list1.h:118
bool is_concat_function_symbol(const atermpp::aterm &e)
Recogniser for function ++.
Definition list1.h:408
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition list1.h:855
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition list1.h:843
bool is_head_function_symbol(const atermpp::aterm &e)
Recogniser for function head.
Definition list1.h:536
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function [].
Definition list1.h:86
function_symbol concat(const sort_expression &s)
Constructor for function symbol ++.
Definition list1.h:398
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
Definition list1.h:53
application count(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition list1.h:296
application element_at(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol ..
Definition list1.h:487
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition list1.h:233
application snoc(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol <|.
Definition list1.h:359
bool is_list_enumeration_function_symbol(const atermpp::aterm &e)
Recogniser for function list_enumeration.
Namespace for system defined sort nat.
const core::identifier_string & succ_name()
Generate identifier succ.
Definition nat1.h:576
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition nat1.h:2257
application cpair(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cPair.
Definition nat1.h:227
bool is_cpair_application(const atermpp::aterm &e)
Recogniser for application of @cPair.
Definition nat1.h:248
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition nat1.h:893
const function_symbol & generalised_divmod()
Constructor for function symbol @gdivmod.
Definition nat1.h:1979
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:422
const core::identifier_string & sqrt_nat_aux_func_name()
Generate identifier @sqrt_nat.
Definition nat1.h:1715
bool is_pos2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Nat.
Definition nat1.h:310
function_symbol succ(const sort_expression &s0)
Definition nat1.h:584
const function_symbol & monus()
Constructor for function symbol @monus.
Definition nat1.h:1331
void make_sqrt(data_expression &result, const data_expression &arg0)
Make an application of function symbol sqrt.
Definition nat1.h:1697
void make_generalised_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @gdivmod.
Definition nat1.h:2017
bool is_gte_subtract_with_borrow_function_symbol(const atermpp::aterm &e)
Recogniser for function @gtesubtb.
Definition nat1.h:931
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:108
bool is_swap_zero_add_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_add.
Definition nat1.h:1509
void make_dub(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @dub.
Definition nat1.h:746
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition nat1.h:1100
application sqrt_nat_aux_func(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @sqrt_nat.
Definition nat1.h:1751
const core::identifier_string & maximum_name()
Generate identifier max.
Definition nat1.h:414
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition nat1.h:1164
application generalised_divmod(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @gdivmod.
Definition nat1.h:2005
bool is_swap_zero_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero.
Definition nat1.h:1405
bool is_cnat_application(const atermpp::aterm &e)
Recogniser for application of @cNat.
Definition nat1.h:184
const core::identifier_string & mod_name()
Generate identifier mod.
Definition nat1.h:1118
const function_symbol & gte_subtract_with_borrow()
Constructor for function symbol @gtesubtb.
Definition nat1.h:921
std::enable_if< std::is_integral< T >::value, data_expression >::type nat(T t)
Constructs expression of type pos from an integral type.
bool is_generalised_divmod_application(const atermpp::aterm &e)
Recogniser for application of @gdivmod.
Definition nat1.h:2027
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition nat1.h:1110
void make_doubly_generalised_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @ggdivmod.
Definition nat1.h:2083
const core::identifier_string & swap_zero_min_name()
Generate identifier @swap_zero_min.
Definition nat1.h:1517
const function_symbol & divmod()
Constructor for function symbol @divmod.
Definition nat1.h:1915
bool is_pos2nat_application(const atermpp::aterm &e)
Recogniser for application of Pos2Nat.
Definition nat1.h:344
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
application dubsucc(const data_expression &arg0)
Application of function symbol @dubsucc.
Definition nat1.h:798
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition nat1.h:682
bool is_nat2pos_application(const atermpp::aterm &e)
Recogniser for application of Nat2Pos.
Definition nat1.h:406
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition nat1.h:1138
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:1190
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition nat1.h:547
const core::identifier_string & times_name()
Generate identifier *.
Definition nat1.h:977
const function_symbol & dubsucc()
Constructor for function symbol @dubsucc.
Definition nat1.h:774
const function_symbol & swap_zero_add()
Constructor for function symbol @swap_zero_add.
Definition nat1.h:1459
function_symbol_vector nat_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for nat.
Definition nat1.h:2154
data_equation_vector nat_generate_equations_code()
Give all system defined equations for nat.
Definition nat1.h:2290
const function_symbol & cpair()
Constructor for function symbol @cPair.
Definition nat1.h:202
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
const core::identifier_string & nat_name()
Definition nat1.h:37
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition nat1.h:1230
const core::identifier_string & exp_name()
Generate identifier exp.
Definition nat1.h:1182
const function_symbol & swap_zero()
Constructor for function symbol @swap_zero.
Definition nat1.h:1395
application swap_zero(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @swap_zero.
Definition nat1.h:1420
bool is_first_function_symbol(const atermpp::aterm &e)
Recogniser for function @first.
Definition nat1.h:1801
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition nat1.h:491
void make_cpair(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cPair.
Definition nat1.h:238
implementation_map nat_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition nat1.h:281
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:56
bool is_doubly_generalised_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @ggdivmod.
Definition nat1.h:2055
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition nat1.h:866
function_symbol_vector nat_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for nat.
Definition nat1.h:2141
std::string natural_constant_as_string(const data_expression &n_in)
Return the string representation of a natural number.
application sqrt(const data_expression &arg0)
Application of function symbol sqrt.
Definition nat1.h:1687
application pos2nat(const data_expression &arg0)
Application of function symbol Pos2Nat.
Definition nat1.h:324
void make_nat2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Pos.
Definition nat1.h:396
application first(const data_expression &arg0)
Application of function symbol @first.
Definition nat1.h:1815
const core::identifier_string & plus_name()
Generate identifier +.
Definition nat1.h:826
const core::identifier_string & natpair_name()
Definition nat1.h:66
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition nat1.h:2245
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition nat1.h:595
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition nat1.h:481
const core::identifier_string & div_name()
Generate identifier div.
Definition nat1.h:1054
const function_symbol & mod()
Constructor for function symbol mod.
Definition nat1.h:1128
void make_monus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus.
Definition nat1.h:1367
const function_symbol & sqrt()
Constructor for function symbol sqrt.
Definition nat1.h:1663
void make_dubsucc(data_expression &result, const data_expression &arg0)
Make an application of function symbol @dubsucc.
Definition nat1.h:808
application even(const data_expression &arg0)
Application of function symbol @even.
Definition nat1.h:1293
const function_symbol & doubly_generalised_divmod()
Constructor for function symbol @ggdivmod.
Definition nat1.h:2045
const function_symbol & pred()
Constructor for function symbol pred.
Definition nat1.h:648
void make_even(data_expression &result, const data_expression &arg0)
Make an application of function symbol @even.
Definition nat1.h:1303
void make_gte_subtract_with_borrow(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @gtesubtb.
Definition nat1.h:959
bool is_sqrt_nat_aux_func_function_symbol(const atermpp::aterm &e)
Recogniser for function @sqrt_nat.
Definition nat1.h:1735
const function_symbol & even()
Constructor for function symbol @even.
Definition nat1.h:1269
const core::identifier_string & first_name()
Generate identifier @first.
Definition nat1.h:1781
void make_swap_zero_monus(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @swap_zero_monus.
Definition nat1.h:1635
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition nat1.h:630
bool is_dub_function_symbol(const atermpp::aterm &e)
Recogniser for function @dub.
Definition nat1.h:720
application cnat(const data_expression &arg0)
Application of function symbol @cNat.
Definition nat1.h:164
bool is_swap_zero_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero.
Definition nat1.h:1441
const core::identifier_string & even_name()
Generate identifier @even.
Definition nat1.h:1259
const core::identifier_string & swap_zero_name()
Generate identifier @swap_zero.
Definition nat1.h:1385
void make_pos2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Nat.
Definition nat1.h:334
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition nat1.h:568
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition nat1.h:1214
bool is_monus_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus.
Definition nat1.h:1341
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition nat1.h:1174
bool is_even_function_symbol(const atermpp::aterm &e)
Recogniser for function @even.
Definition nat1.h:1279
const core::identifier_string & pred_name()
Generate identifier pred.
Definition nat1.h:638
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition nat1.h:1251
const function_symbol & swap_zero_min()
Constructor for function symbol @swap_zero_min.
Definition nat1.h:1527
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:507
const function_symbol & sqrt_nat_aux_func()
Constructor for function symbol @sqrt_nat.
Definition nat1.h:1725
bool is_last_application(const atermpp::aterm &e)
Recogniser for application of @last.
Definition nat1.h:1897
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition nat1.h:1241
const function_symbol & div()
Constructor for function symbol div.
Definition nat1.h:1064
application last(const data_expression &arg0)
Application of function symbol @last.
Definition nat1.h:1877
const core::identifier_string & doubly_generalised_divmod_name()
Generate identifier @ggdivmod.
Definition nat1.h:2035
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition nat1.h:620
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition nat1.h:454
bool is_gte_subtract_with_borrow_application(const atermpp::aterm &e)
Recogniser for application of @gtesubtb.
Definition nat1.h:969
bool is_swap_zero_min_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_min.
Definition nat1.h:1577
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:834
const core::identifier_string & dubsucc_name()
Generate identifier @dubsucc.
Definition nat1.h:764
bool is_first_application(const atermpp::aterm &e)
Recogniser for application of @first.
Definition nat1.h:1835
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition nat1.h:277
bool is_sqrt_application(const atermpp::aterm &e)
Recogniser for application of sqrt.
Definition nat1.h:1707
const function_symbol & first()
Constructor for function symbol @first.
Definition nat1.h:1791
void make_first(data_expression &result, const data_expression &arg0)
Make an application of function symbol @first.
Definition nat1.h:1825
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition nat1.h:658
bool is_generalised_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @gdivmod.
Definition nat1.h:1989
application swap_zero_add(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_add.
Definition nat1.h:1486
void make_swap_zero_add(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @swap_zero_add.
Definition nat1.h:1499
const core::identifier_string & swap_zero_monus_name()
Generate identifier @swap_zero_monus.
Definition nat1.h:1585
application gte_subtract_with_borrow(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @gtesubtb.
Definition nat1.h:947
function_symbol_vector nat_generate_functions_code()
Give all system defined mappings for nat.
Definition nat1.h:2100
bool is_cpair_function_symbol(const atermpp::aterm &e)
Recogniser for function @cPair.
Definition nat1.h:212
application div(const data_expression &arg0, const data_expression &arg1)
Application of function symbol div.
Definition nat1.h:1089
bool is_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @divmod.
Definition nat1.h:1925
const function_symbol & swap_zero_monus()
Constructor for function symbol @swap_zero_monus.
Definition nat1.h:1595
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition nat1.h:1036
application swap_zero_min(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_min.
Definition nat1.h:1554
bool is_c0_function_symbol(const atermpp::aterm &e)
Recogniser for function @c0.
Definition nat1.h:118
const core::identifier_string & generalised_divmod_name()
Generate identifier @gdivmod.
Definition nat1.h:1969
application doubly_generalised_divmod(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @ggdivmod.
Definition nat1.h:2071
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:362
const core::identifier_string & monus_name()
Generate identifier @monus.
Definition nat1.h:1321
application monus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus.
Definition nat1.h:1356
const core::identifier_string & cpair_name()
Generate identifier @cPair.
Definition nat1.h:192
const core::identifier_string & nat2pos_name()
Generate identifier Nat2Pos.
Definition nat1.h:352
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition nat1.h:2269
void make_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @divmod.
Definition nat1.h:1951
application dub(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @dub.
Definition nat1.h:735
implementation_map nat_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for nat.
Definition nat1.h:2198
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition nat1.h:2233
const core::identifier_string & gte_subtract_with_borrow_name()
Generate identifier @gtesubtb.
Definition nat1.h:911
const basic_sort & natpair()
Constructor for sort expression @NatPair.
Definition nat1.h:75
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition nat1.h:672
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition nat1.h:610
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition nat1.h:2221
bool is_swap_zero_monus_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_monus.
Definition nat1.h:1645
void make_swap_zero_min(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @swap_zero_min.
Definition nat1.h:1567
const core::identifier_string & dub_name()
Generate identifier @dub.
Definition nat1.h:700
const core::identifier_string & cnat_name()
Generate identifier @cNat.
Definition nat1.h:130
const core::identifier_string & c0_name()
Generate identifier @c0.
Definition nat1.h:98
application divmod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @divmod.
Definition nat1.h:1940
bool is_swap_zero_add_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_add.
Definition nat1.h:1469
bool is_natpair(const sort_expression &e)
Recogniser for sort expression @NatPair.
Definition nat1.h:85
bool is_swap_zero_monus_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_monus.
Definition nat1.h:1605
const core::identifier_string & pos2nat_name()
Generate identifier Pos2Nat.
Definition nat1.h:290
const core::identifier_string & last_name()
Generate identifier @last.
Definition nat1.h:1843
const core::identifier_string & minimum_name()
Generate identifier min.
Definition nat1.h:499
void make_sqrt_nat_aux_func(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @sqrt_nat.
Definition nat1.h:1763
bool is_sqrt_nat_aux_func_application(const atermpp::aterm &e)
Recogniser for application of @sqrt_nat.
Definition nat1.h:1773
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition nat1.h:2209
bool is_sqrt_function_symbol(const atermpp::aterm &e)
Recogniser for function sqrt.
Definition nat1.h:1673
application mod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol mod.
Definition nat1.h:1153
bool is_cnat_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNat.
Definition nat1.h:150
NUMERIC_TYPE natural_constant_to_value(const data_expression &n)
Return the NUMERIC_VALUE representation of a natural number.
function_symbol_vector nat_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for nat.
Definition nat1.h:267
const function_symbol & last()
Constructor for function symbol @last.
Definition nat1.h:1853
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition nat1.h:692
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition nat1.h:903
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition nat1.h:470
void make_swap_zero(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @swap_zero.
Definition nat1.h:1431
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition nat1.h:558
const core::identifier_string & swap_zero_add_name()
Generate identifier @swap_zero_add.
Definition nat1.h:1449
bool is_dubsucc_function_symbol(const atermpp::aterm &e)
Recogniser for function @dubsucc.
Definition nat1.h:784
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition nat1.h:882
bool is_dubsucc_application(const atermpp::aterm &e)
Recogniser for application of @dubsucc.
Definition nat1.h:818
bool is_swap_zero_min_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_min.
Definition nat1.h:1537
function_symbol_vector nat_generate_constructors_code()
Give all system defined constructors for nat.
Definition nat1.h:255
const core::identifier_string & sqrt_name()
Generate identifier sqrt.
Definition nat1.h:1653
bool is_doubly_generalised_divmod_application(const atermpp::aterm &e)
Recogniser for application of @ggdivmod.
Definition nat1.h:2093
bool is_last_function_symbol(const atermpp::aterm &e)
Recogniser for function @last.
Definition nat1.h:1863
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition nat1.h:1025
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition nat1.h:1046
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition nat1.h:1074
const core::identifier_string & divmod_name()
Generate identifier @divmod.
Definition nat1.h:1905
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition nat1.h:531
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:985
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition nat1.h:1009
bool is_dub_application(const atermpp::aterm &e)
Recogniser for application of @dub.
Definition nat1.h:756
bool is_nat2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Pos.
Definition nat1.h:372
const function_symbol & dub()
Constructor for function symbol @dub.
Definition nat1.h:710
void make_cnat(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNat.
Definition nat1.h:174
application swap_zero_monus(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_monus.
Definition nat1.h:1622
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:300
void make_last(data_expression &result, const data_expression &arg0)
Make an application of function symbol @last.
Definition nat1.h:1887
application nat2pos(const data_expression &arg0)
Application of function symbol Nat2Pos.
Definition nat1.h:386
bool is_natural_constant(const data_expression &n)
Determines whether n is a natural constant.
bool is_monus_application(const atermpp::aterm &e)
Recogniser for application of @monus.
Definition nat1.h:1377
bool is_divmod_application(const atermpp::aterm &e)
Recogniser for application of @divmod.
Definition nat1.h:1961
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition nat1.h:2281
bool is_even_application(const atermpp::aterm &e)
Recogniser for application of @even.
Definition nat1.h:1313
Namespace for system defined sort pos.
void make_powerlog2_pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol @powerlog2.
Definition pos1.h:686
bool is_pos_predecessor_function_symbol(const atermpp::aterm &e)
Recogniser for function @pospred.
Definition pos1.h:406
bool is_add_with_carry_function_symbol(const atermpp::aterm &e)
Recogniser for function @addc.
Definition pos1.h:532
std::string positive_constant_as_string(const data_expression &n_in)
Return the string representation of a positive number.
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition pos1.h:295
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition pos1.h:788
void make_add_with_carry(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @addc.
Definition pos1.h:560
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition pos1.h:624
bool is_cdub_function_symbol(const atermpp::aterm &e)
Recogniser for function @cDub.
Definition pos1.h:120
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition pos1.h:216
implementation_map pos_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for pos.
Definition pos1.h:753
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition pos1.h:358
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition pos1.h:242
const function_symbol & powerlog2_pos()
Constructor for function symbol @powerlog2.
Definition pos1.h:652
bool is_positive_constant(const data_expression &n)
Determines whether n is a positive constant.
bool is_pos(const sort_expression &e)
Recogniser for sort expression Pos.
Definition pos1.h:55
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition pos1.h:824
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:78
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition pos1.h:368
const function_symbol & add_with_carry()
Constructor for function symbol @addc.
Definition pos1.h:522
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition pos1.h:800
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition pos1.h:613
bool is_cdub_application(const atermpp::aterm &e)
Recogniser for application of @cDub.
Definition pos1.h:156
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition pos1.h:306
function_symbol_vector pos_generate_functions_code()
Give all system defined mappings for pos.
Definition pos1.h:703
const function_symbol & pos_predecessor()
Constructor for function symbol @pospred.
Definition pos1.h:396
const core::identifier_string & cdub_name()
Generate identifier @cDub.
Definition pos1.h:100
std::enable_if< std::is_integral< T >::value, data_expression >::type pos(const T t)
Constructs expression of type Bool from an integral type Type T is an unsigned integral type.
const core::identifier_string & c1_name()
Generate identifier @c1.
Definition pos1.h:68
const function_symbol & plus()
Constructor for function symbol +.
Definition pos1.h:458
bool is_add_with_carry_application(const atermpp::aterm &e)
Recogniser for application of @addc.
Definition pos1.h:570
const function_symbol & maximum()
Constructor for function symbol max.
Definition pos1.h:206
const core::identifier_string & powerlog2_pos_name()
Generate identifier @powerlog2.
Definition pos1.h:642
bool is_powerlog2_pos_application(const atermpp::aterm &e)
Recogniser for application of @powerlog2.
Definition pos1.h:696
const core::identifier_string & times_name()
Generate identifier *.
Definition pos1.h:578
function_symbol_vector pos_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for pos.
Definition pos1.h:174
bool is_c1_function_symbol(const atermpp::aterm &e)
Recogniser for function @c1.
Definition pos1.h:88
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition pos1.h:812
const core::identifier_string & plus_name()
Generate identifier +.
Definition pos1.h:448
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition pos1.h:280
const function_symbol & cdub()
Constructor for function symbol @cDub.
Definition pos1.h:110
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition pos1.h:776
application add_with_carry(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @addc.
Definition pos1.h:548
implementation_map pos_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition pos1.h:187
application powerlog2_pos(const data_expression &arg0)
Application of function symbol @powerlog2.
Definition pos1.h:676
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition pos1.h:483
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition pos1.h:634
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition pos1.h:598
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition pos1.h:494
const core::identifier_string & add_with_carry_name()
Generate identifier @addc.
Definition pos1.h:512
const function_symbol & times()
Constructor for function symbol *.
Definition pos1.h:588
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition pos1.h:344
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition pos1.h:468
const core::identifier_string & minimum_name()
Generate identifier min.
Definition pos1.h:260
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition pos1.h:316
data_equation_vector pos_generate_equations_code()
Give all system defined equations for pos.
Definition pos1.h:833
application pos_predecessor(const data_expression &arg0)
Application of function symbol @pospred.
Definition pos1.h:420
bool is_powerlog2_pos_function_symbol(const atermpp::aterm &e)
Recogniser for function @powerlog2.
Definition pos1.h:662
application cdub(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cDub.
Definition pos1.h:135
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition pos1.h:378
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition pos1.h:231
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
const core::identifier_string & maximum_name()
Generate identifier max.
Definition pos1.h:196
const core::identifier_string & pos_name()
Definition pos1.h:36
const function_symbol & minimum()
Constructor for function symbol min.
Definition pos1.h:270
NUMERIC_TYPE positive_constant_to_value(const data_expression &n)
Returns the NUMERIC_TYPE representation of a positive number.
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition pos1.h:764
function_symbol_vector pos_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for pos.
Definition pos1.h:720
function_symbol_vector pos_generate_constructors_code()
Give all system defined constructors for pos.
Definition pos1.h:163
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition pos1.h:252
bool is_pos_predecessor_application(const atermpp::aterm &e)
Recogniser for application of @pospred.
Definition pos1.h:440
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition pos1.h:183
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition pos1.h:504
const function_symbol & succ()
Constructor for function symbol succ.
Definition pos1.h:334
void make_cdub(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cDub.
Definition pos1.h:146
const core::identifier_string & pos_predecessor_name()
Generate identifier @pospred.
Definition pos1.h:386
function_symbol_vector pos_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for pos.
Definition pos1.h:733
const core::identifier_string & succ_name()
Generate identifier succ.
Definition pos1.h:324
void make_pos_predecessor(data_expression &result, const data_expression &arg0)
Make an application of function symbol @pospred.
Definition pos1.h:430
Namespace for system defined sort real_.
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:650
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition real1.h:784
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
bool is_real2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Int.
Definition real1.h:491
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition real1.h:1370
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition real1.h:1211
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:107
void make_reduce_fraction(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @redfrac.
Definition real1.h:1695
const core::identifier_string & maximum_name()
Generate identifier max.
Definition real1.h:533
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition real1.h:867
const core::identifier_string & minus_name()
Generate identifier -.
Definition real1.h:1144
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition real1.h:925
application reduce_fraction_helper(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @redfrachlp.
Definition real1.h:1814
const core::identifier_string & real_name()
Definition real1.h:39
const function_symbol & pos2real()
Constructor for function symbol Pos2Real.
Definition real1.h:171
const core::identifier_string & reduce_fraction_where_name()
Generate identifier @redfracwhr.
Definition real1.h:1713
const function_symbol & round()
Constructor for function symbol round.
Definition real1.h:1597
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition real1.h:1099
std::enable_if< std::is_integral< T >::value, data_expression >::type real_(T t)
Constructs expression of type Real from an integral type.
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
application divides(const data_expression &arg0, const data_expression &arg1)
Application of function symbol /.
Definition real1.h:1434
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition real1.h:794
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
const core::identifier_string & int2real_name()
Generate identifier Int2Real.
Definition real1.h:285
const function_symbol & real2nat()
Constructor for function symbol Real2Nat.
Definition real1.h:419
bool is_divides_function_symbol(const atermpp::aterm &e)
Recogniser for function /.
Definition real1.h:1418
const core::identifier_string & creal_name()
Generate identifier @cReal.
Definition real1.h:97
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition real1.h:950
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition real1.h:1391
application real2nat(const data_expression &arg0)
Application of function symbol Real2Nat.
Definition real1.h:443
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition real1.h:1965
bool is_int2real_application(const atermpp::aterm &e)
Recogniser for application of Int2Real.
Definition real1.h:339
const function_symbol & ceil()
Constructor for function symbol ceil.
Definition real1.h:1535
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition real1.h:1989
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1136
bool is_divides_application(const atermpp::aterm &e)
Recogniser for application of /.
Definition real1.h:1455
bool is_reduce_fraction_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrac.
Definition real1.h:1669
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition real1.h:597
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition real1.h:1381
const core::identifier_string & divides_name()
Generate identifier /.
Definition real1.h:1399
bool is_real2int_application(const atermpp::aterm &e)
Recogniser for application of Real2Int.
Definition real1.h:525
const core::identifier_string & ceil_name()
Generate identifier ceil.
Definition real1.h:1525
bool is_creal_function_symbol(const atermpp::aterm &e)
Recogniser for function @cReal.
Definition real1.h:117
void make_real2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Nat.
Definition real1.h:453
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:1184
application creal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cReal.
Definition real1.h:132
bool is_reduce_fraction_where_application(const atermpp::aterm &e)
Recogniser for application of @redfracwhr.
Definition real1.h:1771
function_symbol succ(const sort_expression &s0)
Definition real1.h:893
application negate(const data_expression &arg0)
Application of function symbol -.
Definition real1.h:857
bool is_floor_function_symbol(const atermpp::aterm &e)
Recogniser for function floor.
Definition real1.h:1483
void make_int2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Real.
Definition real1.h:329
void make_divides(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol /.
Definition real1.h:1445
const core::identifier_string & floor_name()
Generate identifier floor.
Definition real1.h:1463
const core::identifier_string & times_name()
Generate identifier *.
Definition real1.h:1229
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition real1.h:759
bool is_ceil_application(const atermpp::aterm &e)
Recogniser for application of ceil.
Definition real1.h:1579
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition real1.h:940
const function_symbol & real2int()
Constructor for function symbol Real2Int.
Definition real1.h:481
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition real1.h:634
application nat2real(const data_expression &arg0)
Application of function symbol Nat2Real.
Definition real1.h:257
const function_symbol & reduce_fraction()
Constructor for function symbol @redfrac.
Definition real1.h:1659
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:153
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition real1.h:1043
const core::identifier_string & negate_name()
Generate identifier -.
Definition real1.h:802
void make_reduce_fraction_helper(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @redfrachlp.
Definition real1.h:1825
NUMERIC_TYPE value(const data_expression &r, typename std::enable_if< std::is_floating_point< NUMERIC_TYPE >::value >::type *=nullptr)
Yields the real value of a data expression.
void make_pos2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Real.
Definition real1.h:205
function_symbol pred(const sort_expression &s0)
Definition real1.h:976
bool is_round_function_symbol(const atermpp::aterm &e)
Recogniser for function round.
Definition real1.h:1607
const core::identifier_string & succ_name()
Generate identifier succ.
Definition real1.h:885
const function_symbol & reduce_fraction_helper()
Constructor for function symbol @redfrachlp.
Definition real1.h:1789
const core::identifier_string & abs_name()
Generate identifier abs.
Definition real1.h:727
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
Definition real1.h:2010
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition real1.h:1269
const core::identifier_string & round_name()
Generate identifier round.
Definition real1.h:1587
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:842
application int2real(const data_expression &arg0)
Application of function symbol Int2Real.
Definition real1.h:319
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition real1.h:682
const function_symbol & floor()
Constructor for function symbol floor.
Definition real1.h:1473
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition real1.h:709
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition real1.h:1296
const core::identifier_string & reduce_fraction_helper_name()
Generate identifier @redfrachlp.
Definition real1.h:1779
function_symbol_vector real_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for real_.
Definition real1.h:78
std::enable_if< std::is_integral< T >::value, data_expression >::type real_(T numerator, T denominator)
Constructs expression of type Real from an integral type.
bool is_real2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Pos.
Definition real1.h:367
void make_real2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Int.
Definition real1.h:515
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
Definition real1.h:70
void make_nat2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Real.
Definition real1.h:267
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition real1.h:624
bool is_floor_application(const atermpp::aterm &e)
Recogniser for application of floor.
Definition real1.h:1517
application reduce_fraction_where(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @redfracwhr.
Definition real1.h:1749
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
const function_symbol & reduce_fraction_where()
Constructor for function symbol @redfracwhr.
Definition real1.h:1723
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition real1.h:1115
implementation_map real_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for real_.
Definition real1.h:1930
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1285
bool is_ceil_function_symbol(const atermpp::aterm &e)
Recogniser for function ceil.
Definition real1.h:1545
application real2int(const data_expression &arg0)
Application of function symbol Real2Int.
Definition real1.h:505
const core::identifier_string & pred_name()
Generate identifier pred.
Definition real1.h:968
const function_symbol & nat2real()
Constructor for function symbol Nat2Real.
Definition real1.h:233
const core::identifier_string & minimum_name()
Generate identifier min.
Definition real1.h:642
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition real1.h:1953
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition real1.h:960
application pos2real(const data_expression &arg0)
Application of function symbol Pos2Real.
Definition real1.h:195
void make_round(data_expression &result, const data_expression &arg0)
Make an application of function symbol round.
Definition real1.h:1631
bool is_pos2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Real.
Definition real1.h:181
function_symbol_vector real_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for real_.
Definition real1.h:1891
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition real1.h:1977
const core::identifier_string & plus_name()
Generate identifier +.
Definition real1.h:1051
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition real1.h:1941
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1306
void make_ceil(data_expression &result, const data_expression &arg0)
Make an application of function symbol ceil.
Definition real1.h:1569
const core::identifier_string & reduce_fraction_name()
Generate identifier @redfrac.
Definition real1.h:1649
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition real1.h:1200
application abs(const data_expression &arg0)
Application of function symbol abs.
Definition real1.h:774
bool is_real2pos_application(const atermpp::aterm &e)
Recogniser for application of Real2Pos.
Definition real1.h:401
bool is_reduce_fraction_application(const atermpp::aterm &e)
Recogniser for application of @redfrac.
Definition real1.h:1705
bool is_int2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Real.
Definition real1.h:305
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:877
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition real1.h:84
bool is_reduce_fraction_helper_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrachlp.
Definition real1.h:1799
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition real1.h:719
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1221
const core::identifier_string & pos2real_name()
Generate identifier Pos2Real.
Definition real1.h:161
bool is_round_application(const atermpp::aterm &e)
Recogniser for application of round.
Definition real1.h:1641
application reduce_fraction(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @redfrac.
Definition real1.h:1684
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition real1.h:2001
const core::identifier_string & exp_name()
Generate identifier exp.
Definition real1.h:1314
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition real1.h:613
bool is_real2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Nat.
Definition real1.h:429
const core::identifier_string & real2nat_name()
Generate identifier Real2Nat.
Definition real1.h:409
const core::identifier_string & real2int_name()
Generate identifier Real2Int.
Definition real1.h:471
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:295
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition real1.h:1008
const core::identifier_string & nat2real_name()
Generate identifier Nat2Real.
Definition real1.h:223
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1322
application real2pos(const data_expression &arg0)
Application of function symbol Real2Pos.
Definition real1.h:381
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition real1.h:1033
bool is_real2nat_application(const atermpp::aterm &e)
Recogniser for application of Real2Nat.
Definition real1.h:463
bool is_pos2real_application(const atermpp::aterm &e)
Recogniser for application of Pos2Real.
Definition real1.h:215
application floor(const data_expression &arg0)
Application of function symbol floor.
Definition real1.h:1497
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition real1.h:698
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition real1.h:1126
bool is_reduce_fraction_helper_application(const atermpp::aterm &e)
Recogniser for application of @redfrachlp.
Definition real1.h:1835
void make_floor(data_expression &result, const data_expression &arg0)
Make an application of function symbol floor.
Definition real1.h:1507
const function_symbol & real2pos()
Constructor for function symbol Real2Pos.
Definition real1.h:357
implementation_map real_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition real1.h:88
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:541
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
Definition real1.h:1842
void make_reduce_fraction_where(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @redfracwhr.
Definition real1.h:1761
function_symbol_vector real_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for real_.
Definition real1.h:1878
const core::identifier_string & real2pos_name()
Generate identifier Real2Pos.
Definition real1.h:347
void make_real2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Pos.
Definition real1.h:391
application round(const data_expression &arg0)
Application of function symbol round.
Definition real1.h:1621
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition real1.h:1354
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition real1.h:1023
void make_creal(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cReal.
Definition real1.h:143
application ceil(const data_expression &arg0)
Application of function symbol ceil.
Definition real1.h:1559
bool is_reduce_fraction_where_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfracwhr.
Definition real1.h:1733
bool is_nat2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Real.
Definition real1.h:243
bool is_nat2real_application(const atermpp::aterm &e)
Recogniser for application of Nat2Real.
Definition real1.h:277
Namespace for system defined sort set_.
Definition set1.h:36
const core::identifier_string & fset_intersection_name()
Generate identifier @fset_inter.
Definition set1.h:1039
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition set1.h:334
function_symbol true_function(const sort_expression &s)
Constructor for function symbol @true_.
Definition set1.h:729
const core::identifier_string & or_function_name()
Generate identifier @or_.
Definition set1.h:907
bool is_set_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @setcomp.
Definition set1.h:280
const core::identifier_string & constructor_name()
Generate identifier @set.
Definition set1.h:66
application fset_intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fset_inter.
Definition set1.h:1076
bool is_false_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @false_.
Definition set1.h:677
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition set1.h:612
bool is_not_function_application(const atermpp::aterm &e)
Recogniser for application of @not_.
Definition set1.h:835
bool is_and_function_application(const atermpp::aterm &e)
Recogniser for application of @and_.
Definition set1.h:899
void make_or_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @or_.
Definition set1.h:953
function_symbol_vector set_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for set_.
Definition set1.h:1134
application or_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @or_.
Definition set1.h:942
data_expression set_enumeration(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=0)
Application of function symbol set_enumeration.
bool is_fset_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_inter.
Definition set1.h:1059
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set1.h:53
function_symbol or_function(const sort_expression &s)
Constructor for function symbol @or_.
Definition set1.h:917
void make_complement(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol !.
Definition set1.h:396
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition set1.h:483
core::identifier_string const & set_enumeration_name()
Generate identifier set_enumeration.
const core::identifier_string & false_function_name()
Generate identifier @false_.
Definition set1.h:657
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition set1.h:307
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition set1.h:1262
bool is_true_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @true_.
Definition set1.h:739
bool is_complement_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition set1.h:406
bool is_or_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @or_.
Definition set1.h:927
function_symbol fset_intersection(const sort_expression &s)
Constructor for function symbol @fset_inter.
Definition set1.h:1049
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition set1.h:149
const core::identifier_string & set_comprehension_name()
Generate identifier @setcomp.
Definition set1.h:226
void make_fset_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fset_union.
Definition set1.h:1021
bool is_fset_union_application(const atermpp::aterm &e)
Recogniser for application of @fset_union.
Definition set1.h:1031
bool is_false_function_application(const atermpp::aterm &e)
Recogniser for application of @false_.
Definition set1.h:711
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition set1.h:1190
bool is_not_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @not_.
Definition set1.h:801
function_symbol and_function(const sort_expression &s)
Constructor for function symbol @and_.
Definition set1.h:853
bool is_set_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @setcomp.
Definition set1.h:246
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition set1.h:344
function_symbol set_enumeration(const sort_expression &s)
Constructor for function symbol set_enumeration.
const core::identifier_string & not_function_name()
Generate identifier @not_.
Definition set1.h:781
application not_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @not_.
Definition set1.h:815
const core::identifier_string & in_name()
Generate identifier in.
Definition set1.h:288
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
Definition set1.h:130
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_.
Definition set1.h:1178
bool is_fset_intersection_application(const atermpp::aterm &e)
Recogniser for application of @fset_inter.
Definition set1.h:1099
data_expression set_enumeration(const sort_expression &s, data_expression_list const &range)
Application of function symbol set_enumeration.
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition set1.h:649
function_symbol not_function(const sort_expression &s)
Constructor for function symbol @not_.
Definition set1.h:791
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition set1.h:1214
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition set1.h:462
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @set.
Definition set1.h:122
const core::identifier_string & fset_union_name()
Generate identifier @fset_union.
Definition set1.h:971
bool is_set_fset_application(const atermpp::aterm &e)
Recogniser for application of @setfset.
Definition set1.h:218
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...
Definition set1.h:154
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition set1.h:558
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition set1.h:628
application complement(const sort_expression &s, const data_expression &arg0)
Application of function symbol !.
Definition set1.h:386
const core::identifier_string & complement_name()
Generate identifier !.
Definition set1.h:352
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:499
application set_fset(const sort_expression &s, const data_expression &arg0)
Application of function symbol @setfset.
Definition set1.h:198
const core::identifier_string & and_function_name()
Generate identifier @and_.
Definition set1.h:843
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition set1.h:547
bool is_fset_union_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_union.
Definition set1.h:991
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition set1.h:1238
function_symbol fset_union(const sort_expression &s)
Constructor for function symbol @fset_union.
Definition set1.h:981
void make_and_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @and_.
Definition set1.h:889
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
bool is_set_fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @setfset.
Definition set1.h:184
application set_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @setcomp.
Definition set1.h:260
const core::identifier_string & intersection_name()
Generate identifier *.
Definition set1.h:491
bool is_set_enumeration_application(const atermpp::aterm &e)
Recogniser for application of set_enumeration.
void make_fset_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fset_inter.
Definition set1.h:1089
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:76
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition set1.h:1250
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition set1.h:1202
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:667
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @set.
Definition set1.h:112
const core::identifier_string & set_fset_name()
Generate identifier @setfset.
Definition set1.h:164
const core::identifier_string & union_name()
Generate identifier +.
Definition set1.h:414
bool is_complement_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition set1.h:372
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:296
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:422
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @set.
Definition set1.h:86
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
Definition set1.h:1107
application fset_union(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fset_union.
Definition set1.h:1008
function_symbol_vector set_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for set_.
Definition set1.h:141
const core::identifier_string & difference_name()
Generate identifier -.
Definition set1.h:576
void make_set_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @setcomp.
Definition set1.h:270
bool is_set_enumeration_function_symbol(const atermpp::aterm &e)
Recogniser for function set_enumeration.
application true_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @true_.
Definition set1.h:753
void make_not_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @not_.
Definition set1.h:825
bool is_or_function_application(const atermpp::aterm &e)
Recogniser for application of @or_.
Definition set1.h:963
const core::identifier_string & true_function_name()
Generate identifier @true_.
Definition set1.h:719
void make_false_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @false_.
Definition set1.h:701
void make_true_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @true_.
Definition set1.h:763
application false_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @false_.
Definition set1.h:691
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:584
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition set1.h:446
function_symbol complement(const sort_expression &s)
Constructor for function symbol !.
Definition set1.h:362
bool is_true_function_application(const atermpp::aterm &e)
Recogniser for application of @true_.
Definition set1.h:773
function_symbol set_fset(const sort_expression &s)
Constructor for function symbol @setfset.
Definition set1.h:174
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition set1.h:639
void make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition set1.h:473
function_symbol set_comprehension(const sort_expression &s)
Constructor for function symbol @setcomp.
Definition set1.h:236
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition set1.h:323
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition set1.h:568
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
Definition set1.h:1272
application and_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @and_.
Definition set1.h:878
function_symbol_vector set_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for set_.
Definition set1.h:1148
bool is_and_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @and_.
Definition set1.h:863
void make_set_fset(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @setfset.
Definition set1.h:208
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition set1.h:531
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @set.
Definition set1.h:101
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition set1.h:1226
Namespace for all data library functionality.
Definition data.cpp:22
void make_set_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
std::set< data::variable > find_free_variables(const T &x)
Definition find.h:335
void swap(exists_binder &t1, exists_binder &t2)
\brief swap overload
std::vector< machine_number > machine_number_vector
\brief vector of machine_numbers
void make_data_expression(data_expression &result)
atermpp::term_list< assignment_expression > assignment_expression_list
\brief list of assignment_expressions
Definition assignment.h:50
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
bool is_convertible(const sort_expression &s1, const sort_expression &s2)
Returns true if and only if s1 == s2, or if s1 is a less specific numeric type than s2.
void make_function_symbol(atermpp::aterm &t, const ARGUMENTS &... args)
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
Definition data.cpp:83
constexpr std::size_t undefined_index()
Returns an index that corresponds to 'undefined'.
Definition undefined.h:27
std::string pp(const data::untyped_set_or_bag_comprehension_binder &x)
Definition data.cpp:78
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:343
std::string pp(const data::set_comprehension_binder &x)
Definition data.cpp:67
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
Definition data.cpp:85
std::string pp(const data::exists &x)
Definition data.cpp:54
bool is_greater_function_symbol(const DataExpression &e)
Recogniser for function >
Definition standard.h:323
int precedence(const application &x)
Definition print.h:317
std::string pp(const data::untyped_sort_variable &x)
Definition data.cpp:80
void if_always_else_manual_implementation(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
The data expression of an application of the function symbol @if_always_else.
atermpp::term_list< function_sort > function_sort_list
list of function sorts
std::string pp(const data::untyped_set_or_bag_comprehension &x)
Definition data.cpp:77
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:66
void typecheck_sort_expression(const sort_expression &sort_expr, const data_specification &data_spec)
Type check a sort expression. Throws an exception if something went wrong.
Definition typecheck.h:287
std::string pp(const data::assignment_expression &x)
Definition data.cpp:43
bool is_if_always_else_function_symbol(const atermpp::aterm &e)
Recogniser for function @if_always_else.
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
data::data_equation_list normalize_sorts(const data::data_equation_list &x, const data::sort_specification &sortspec)
Definition data.cpp:84
std::string pp(const data::function_symbol_list &x)
Definition data.cpp:33
void normalize_sorts(T &x, const data::sort_specification &sort_spec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
constexpr int precedence(const forall &)
Definition print.h:409
bool is_data_equation(const atermpp::aterm &t)
Recognizer function.
std::set< data::data_expression > find_data_expressions(const T &x)
Returns all data expressions that occur in an object.
Definition find.h:432
application function_update(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @func_update.
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:359
std::set< data::function_symbol > find_function_symbols(const T &x)
Definition find.h:410
function_symbol_vector function_update_mCRL2_usable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that can be used in mCRL2 specs for function_update.
variable_list free_variables(const data_expression &x)
Definition data.cpp:195
bool is_is_not_a_function_update_application(const atermpp::aterm &e)
Recogniser for application of @is_not_an_update.
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
std::set< data::sort_expression > find_sort_expressions(const T &x)
Definition find.h:389
void make_bag_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
void swap(container_sort &t1, container_sort &t2)
\brief swap overload
std::string pp(const data::set_container &x)
Definition data.cpp:68
void swap(machine_number &t1, machine_number &t2)
\brief swap overload
bool is_set_container(const atermpp::aterm &x)
constexpr int precedence(const bag_comprehension &)
Definition print.h:413
int precedence(const data_expression &x)
Definition print.h:415
std::string pp(const data::abstraction &x)
Definition data.cpp:39
void swap(structured_sort &t1, structured_sort &t2)
\brief swap overload
void swap(lambda_binder &t1, lambda_binder &t2)
\brief swap overload
std::string pp(const data::application &x)
Definition data.cpp:41
std::string pp(const data::bag_comprehension_binder &x)
Definition data.cpp:45
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
Definition standard.h:388
void find_free_variables_with_bound(const T &x, OutputIterator o, const VariableContainer &bound)
Definition find.h:326
void make_machine_number(atermpp::aterm &t, size_t n)
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
Definition data.cpp:95
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
void swap(abstraction &t1, abstraction &t2)
\brief swap overload
std::string pp(const data::fbag_container &x)
Definition data.cpp:56
void swap(untyped_sort_variable &t1, untyped_sort_variable &t2)
\brief swap overload
bool is_application_no_check(const atermpp::aterm &x)
Returns true if the term t is an application, but it does not check whether an application symbol of ...
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
std::vector< sort_expression > sort_expression_vector
\brief vector of sort_expressions
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
void make_where_clause(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_data_parameter(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_equal_to_function_symbol(const DataExpression &e)
Recogniser for function ==.
Definition standard.h:135
function_symbol_vector function_update_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for function_update.
data_expression_list make_data_expression_list(Container const &r, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
Converts an container with data expressions to data_expression_list.
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
Definition data.cpp:92
function_symbol find_mapping(data_specification const &data, std::string const &s)
Finds a mapping in a data specification.
void swap(list_container &t1, list_container &t2)
\brief swap overload
const data::variable & undefined_variable()
Returns a data variable that corresponds to 'undefined'.
Definition undefined.h:34
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:90
std::string pp(const data::untyped_data_parameter &x)
Definition data.cpp:73
std::string pp(const data::fset_container &x)
Definition data.cpp:59
bool is_application(const data_expression &t)
Returns true if the term t is an application.
bool is_list_container(const atermpp::aterm &x)
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:232
void make_basic_sort(atermpp::aterm &t, const ARGUMENTS &... args)
Definition basic_sort.h:66
void make_function_update_stable(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @func_update_stable.
void swap(set_comprehension &t1, set_comprehension &t2)
\brief swap overload
bool search_data_expression(Container const &container, const data_expression &s)
Returns true if the term has a given data expression as subterm.
Definition find.h:479
std::set< data::variable > find_all_variables(const T &x)
Definition find.h:303
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &codomain)
Convenience constructor for function sort with domain size 4.
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.
atermpp::term_list< function_symbol > function_symbol_list
\brief list of function_symbols
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:192
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
void find_all_variables(const T &x, OutputIterator o)
Definition find.h:294
function_symbol if_always_else(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @if_always_else.
atermpp::term_list< untyped_data_parameter > untyped_data_parameter_list
\brief list of untyped_data_parameters
void swap(untyped_identifier_assignment &t1, untyped_identifier_assignment &t2)
\brief swap overload
Definition assignment.h:270
std::string pp(const data::untyped_identifier_assignment &x)
Definition data.cpp:75
std::string pp(const data::lambda &x)
Definition data.cpp:62
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
void make_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @func_update.
std::string pp(const data::container_sort &x)
Definition data.cpp:49
atermpp::term_list< sort_expression_list > sorts_list
Definition typecheck.h:369
void make_untyped_set_or_bag_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
constexpr int precedence(const set_comprehension &)
Definition print.h:412
const core::identifier_string & function_update_name()
Generate identifier @func_update.
bool is_untyped_possible_sorts(const atermpp::aterm &x)
Returns true if the term t is an expression for multiple possible sorts.
void swap(assignment &t1, assignment &t2)
\brief swap overload
Definition assignment.h:174
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
application less_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <=.
Definition standard.h:295
std::vector< container_sort > container_sort_vector
list of function sorts
void swap(structured_sort_constructor &t1, structured_sort_constructor &t2)
\brief swap overload
std::string pp(const data::variable &x)
Definition data.cpp:81
std::string pp(const data::untyped_sort &x)
Definition data.cpp:79
void swap(fset_container &t1, fset_container &t2)
\brief swap overload
constexpr int precedence(const where_clause &)
Definition print.h:414
void if_always_else_application(data_expression &result, const data_expression &a1)
Application of a function that is user defined instead of by rewrite rules. It does not have sort par...
void swap(untyped_possible_sorts &t1, untyped_possible_sorts &t2)
\brief swap overload
void swap(alias &t1, alias &t2)
\brief swap overload
Definition alias.h:100
std::string pp(const data::machine_number &x)
Definition data.cpp:65
bool search_free_variable(const T &x, const variable &v)
Returns true if the term has a given free variable as subterm.
Definition find.h:456
atermpp::term_list< alias > alias_list
\brief list of aliass
Definition alias.h:72
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:380
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:258
void swap(lambda &t1, lambda &t2)
\brief swap overload
Definition lambda.h:99
std::string pp(const data::lambda_binder &x)
Definition data.cpp:63
atermpp::term_list< binder_type > binder_type_list
\brief list of binder_types
Definition binder_type.h:50
data::data_expression translate_user_notation(const data::data_expression &x)
Definition data.cpp:89
function_symbol_vector function_update_generate_constructors_and_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings and constructors for function_update.
void typecheck_data_specification(data_specification &data_spec)
Type check a parsed mCRL2 data specification. Throws an exception if something went wrong.
Definition typecheck.h:345
bool is_if_always_else_application(const atermpp::aterm &e)
Recogniser for application of @if_always_else.
std::vector< untyped_identifier_assignment > untyped_identifier_assignment_vector
\brief vector of untyped_identifier_assignments
Definition assignment.h:245
void swap(fbag_container &t1, fbag_container &t2)
\brief swap overload
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
void make_variable(atermpp::aterm &t, const ARGUMENTS &... args)
Definition variable.h:80
data_expression typecheck_data_expression(const data_expression &x, const VariableContainer &variables, const data_specification &dataspec=data_specification())
Type check a data expression. Throws an exception if something went wrong.
Definition typecheck.h:309
application not_equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol !=.
Definition standard.h:181
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::vector< structured_sort > structured_sort_vector
\brief vector of structured_sorts
constexpr int precedence(const exists &)
Definition print.h:410
std::vector< binder_type > binder_type_vector
\brief vector of binder_types
Definition binder_type.h:53
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
function_symbol_vector function_update_generate_constructors_code()
Give all system defined constructors for function_update.
atermpp::term_list< machine_number > machine_number_list
\brief list of machine_numbers
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
void swap(bag_comprehension_binder &t1, bag_comprehension_binder &t2)
\brief swap overload
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
Definition standard.h:219
atermpp::term_list< structured_sort_constructor_argument > structured_sort_constructor_argument_list
\brief list of structured_sort_constructor_arguments
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
data_equation_vector standard_generate_equations_code(const sort_expression &s)
Give all standard system defined equations for sort s.
Definition standard.h:405
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 data::data_equation_list &x)
Definition data.cpp:37
bool is_left_associative(const data_expression &x)
Definition print.h:428
void make_untyped_identifier(atermpp::aterm &t, const ARGUMENTS &... args)
data_expression typecheck_data_expression(const data_expression &x, const data_specification &dataspec=data_specification())
Type check a data expression. Throws an exception if something went wrong.
Definition typecheck.h:334
void find_function_symbols(const T &x, OutputIterator o)
Definition find.h:401
void make_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition assignment.h:140
std::string pp(const data::data_equation &x)
Definition data.cpp:51
const core::identifier_string & if_always_else_name()
Generate identifier @if_always_else.
std::string pp(const data::function_sort &x)
Definition data.cpp:60
void make_untyped_identifier_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition assignment.h:236
bool is_set_comprehension_binder(const atermpp::aterm &x)
void swap(sort_expression &t1, sort_expression &t2)
\brief swap overload
atermpp::term_list< sort_expression > sort_expression_list
\brief list of sort_expressions
void swap(set_container &t1, set_container &t2)
\brief swap overload
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:315
bool is_exists_binder(const atermpp::aterm &x)
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
void swap(structured_sort_constructor_argument &t1, structured_sort_constructor_argument &t2)
\brief swap overload
std::set< data::variable > find_all_variables(const data::function_symbol &x)
Definition data.cpp:96
void swap(data_expression &t1, data_expression &t2)
\brief swap overload
std::string pp(const data::bag_comprehension &x)
Definition data.cpp:44
bool is_not_equal_to_function_symbol(const DataExpression &e)
Recogniser for function !=.
Definition standard.h:172
void make_structured_sort_constructor_argument(atermpp::aterm &t, const ARGUMENTS &... args)
function_symbol find_constructor(data_specification const &data, std::string const &s)
Finds a constructor in a data specification.
std::string pp(const T &x)
Returns a string representation of the object x.
Definition print.h:2541
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
Definition alias.h:66
void swap(untyped_set_or_bag_comprehension_binder &t1, untyped_set_or_bag_comprehension_binder &t2)
\brief swap overload
void swap(untyped_sort &t1, untyped_sort &t2)
\brief swap overload
atermpp::term_list< basic_sort > basic_sort_list
list of basic sorts
Definition basic_sort.h:92
const core::identifier_string & is_not_a_function_update_name()
Generate identifier @is_not_an_update.
void make_lambda(atermpp::aterm &result, ARGUMENTS... arguments)
Definition lambda.h:78
application function_update_stable(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @func_update_stable.
std::string pp(const data::exists_binder &x)
Definition data.cpp:55
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:351
void swap(bag_comprehension &t1, bag_comprehension &t2)
\brief swap overload
bool is_assignment_expression(const atermpp::aterm &x)
Definition assignment.h:63
void swap(function_symbol &t1, function_symbol &t2)
\brief swap overload
bool search_sort_expression(Container const &container, const sort_expression &s)
Returns true if the term has a given sort expression as subterm.
Definition find.h:468
std::string pp(const data::forall_binder &x)
Definition data.cpp:58
bool is_structured_sort_constructor_argument(const atermpp::aterm &x)
std::string pp(const data::structured_sort_constructor_list &x)
Definition data.cpp:35
bool is_function_update_function_symbol(const atermpp::aterm &e)
Recogniser for function @func_update.
atermpp::term_list< structured_sort > structured_sort_list
\brief list of structured_sorts
void is_not_a_function_update_application(data_expression &result, const data_expression &a1)
Application of a function that is user defined instead of by rewrite rules. It does not have sort par...
application is_not_a_function_update(const sort_expression &s, const sort_expression &t, const data_expression &arg0)
Application of function symbol @is_not_an_update.
atermpp::term_list< container_type > container_type_list
\brief list of container_types
void make_if_always_else(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Make an application of function symbol @if_always_else.
bool is_system_defined(const sort_expression &s)
Returns true iff the expression represents a standard sort.
bool is_function_update_stable_function_symbol(const atermpp::aterm &e)
Recogniser for function @func_update_stable.
std::string pp(const data::untyped_possible_sorts &x)
Definition data.cpp:76
sort_expression find_sort(data_specification const &data, std::string const &s)
Finds a sort in a data specification.
void swap(where_clause &t1, where_clause &t2)
\brief swap overload
std::vector< container_type > container_type_vector
\brief vector of container_types
bool is_right_associative(const data_expression &x)
Definition print.h:434
std::string pp(const data::data_expression_list &x)
Definition data.cpp:27
std::vector< structured_sort_constructor > structured_sort_constructor_vector
\brief vector of structured_sort_constructors
void make_forall(atermpp::aterm &result, ARGUMENTS... arguments)
Definition forall.h:64
data_expression typecheck_untyped_data_parameter(data_type_checker &typechecker, const core::identifier_string &name, const data_expression_list &parameters, const data::sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:352
bool is_structured_sort_constructor(const atermpp::aterm &x)
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
variable_list left_hand_sides(const assignment_list &x)
Returns the left hand sides of an assignment list.
Definition assignment.h:310
void swap(function_sort &t1, function_sort &t2)
\brief swap overload
bool is_lambda_binder(const atermpp::aterm &x)
std::string pp(const data::assignment_list &x)
Definition data.cpp:29
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
atermpp::term_list< data_equation > data_equation_list
\brief list of data_equations
void swap(untyped_data_parameter &t1, untyped_data_parameter &t2)
\brief swap overload
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
std::set< data::variable > find_all_variables(const data::machine_number &x)
bool is_fset_container(const atermpp::aterm &x)
bool is_less_function_symbol(const DataExpression &e)
Recogniser for function <.
Definition standard.h:249
std::string pp(const data::structured_sort_constructor &x)
Definition data.cpp:71
void swap(untyped_identifier &t1, untyped_identifier &t2)
\brief swap overload
std::set< core::identifier_string > find_identifiers(const T &x)
Definition find.h:368
void swap(container_type &t1, container_type &t2)
\brief swap overload
std::string pp(const data::assignment &x)
Definition data.cpp:42
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
bool is_untyped_sort_variable(const atermpp::aterm &x)
void swap(untyped_set_or_bag_comprehension &t1, untyped_set_or_bag_comprehension &t2)
\brief swap overload
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &dom5, const sort_expression &dom6, const sort_expression &codomain)
Convenience constructor for function sort with domain size 6.
data_equation_vector function_update_generate_equations_code(const sort_expression &s, const sort_expression &t)
Give all system defined equations for function_update.
std::list< data_expression > split_disjunction(const data_expression &condition)
Split a disjunctive expression into a set of clauses.
bool is_untyped_set_or_bag_comprehension_binder(const atermpp::aterm &x)
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:91
void swap(data_equation &t1, data_equation &t2)
\brief swap overload
bool is_function_update_stable_application(const atermpp::aterm &e)
Recogniser for application of @func_update_stable.
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:101
application if_always_else(const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @if_always_else.
void swap(assignment_expression &t1, assignment_expression &t2)
\brief swap overload
Definition assignment.h:83
bool is_if_function_symbol(const DataExpression &e)
Recogniser for function if.
Definition standard.h:209
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:332
std::string pp(const data::bag_container &x)
Definition data.cpp:46
void make_abstraction(atermpp::aterm &result, ARGUMENTS... arguments)
Definition abstraction.h:75
std::vector< assignment_expression > assignment_expression_vector
\brief vector of assignment_expressions
Definition assignment.h:53
std::set< data::variable > find_all_variables(const data::variable_list &x)
Definition data.cpp:98
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
std::pair< core::identifier_string, sort_expression > function_symbol_key_type
T normalize_sorts(const T &x, const data::sort_specification &sort_spec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_untyped_data_parameter(const atermpp::aterm &x)
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:155
std::string pp(const data::structured_sort &x)
Definition data.cpp:70
std::list< data_expression > split_conjunction(const data_expression &condition)
Split a disjunctive expression into a set of clauses.
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
Definition data.cpp:93
constexpr int precedence(const lambda &)
Definition print.h:411
atermpp::term_list< variable > variable_list
\brief list of variables
void find_data_expressions(const T &x, OutputIterator o)
Returns all data expressions that occur in an object.
Definition find.h:423
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &codomain)
Convenience constructor for function sort with domain size 3.
void is_not_a_function_update_manual_implementation(data_expression &result, const data_expression &arg0)
The data expression of an application of the function symbol @is_not_an_update.
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
Definition data.cpp:258
std::string pp(const data::data_specification &x)
Definition data.cpp:53
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:87
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
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.
std::vector< function_sort > function_sort_vector
vector of function sorts
std::string pp(const data::container_type &x)
Definition data.cpp:50
application greater_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >=.
Definition standard.h:369
void find_sort_expressions(const T &x, OutputIterator o)
Definition find.h:380
std::string pp(const data::function_symbol &x)
Definition data.cpp:61
bool is_less_equal_function_symbol(const DataExpression &e)
Recogniser for function <=.
Definition standard.h:286
void make_data_equation(atermpp::aterm &t, const ARGUMENTS &... args)
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.
bool is_greater_equal_function_symbol(const DataExpression &e)
Recogniser for function >=.
Definition standard.h:360
assignment_vector make_assignment_vector(VariableSequence const &variables, ExpressionSequence const &expressions)
Constructs an assignment_list by pairwise combining a variable and expression.
Definition assignment.h:281
std::set< data::variable > find_free_variables(const data::data_expression_list &x)
Definition data.cpp:100
void swap(set_comprehension_binder &t1, set_comprehension_binder &t2)
\brief swap overload
std::string pp(const data::basic_sort &x)
Definition data.cpp:47
implementation_map function_update_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
std::string pp(const data::alias &x)
Definition data.cpp:40
std::string pp(const data::list_container &x)
Definition data.cpp:64
std::string pp(const data::forall &x)
Definition data.cpp:57
void swap(bag_container &t1, bag_container &t2)
\brief swap overload
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
std::string pp(const data::sort_expression &x)
Definition data.cpp:69
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
std::string max_machine_number_string()
A string representation indicating the maximal machine number + 1.
bool is_bag_container(const atermpp::aterm &x)
void swap(variable &t1, variable &t2)
\brief swap overload
Definition variable.h:105
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
Definition data.cpp:88
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
function_symbol function_update_stable(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update_stable.
bool is_function_update_application(const atermpp::aterm &e)
Recogniser for application of @func_update.
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
data_expression_list right_hand_sides(const assignment_list &x)
Returns the right hand sides of an assignment list.
Definition assignment.h:318
void make_is_not_a_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0)
Make an application of function symbol @is_not_an_update.
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &codomain)
Convenience constructor for function sort with domain size 2.
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:144
bool is_fbag_container(const atermpp::aterm &x)
atermpp::term_list< container_sort > container_sort_list
list of function sorts
std::string pp(const data::structured_sort_constructor_argument &x)
Definition data.cpp:72
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
const data::variable & undefined_real_variable()
Returns a data variable that corresponds to 'undefined'.
Definition undefined.h:42
void swap(exists &t1, exists &t2)
\brief swap overload
Definition exists.h:85
bool is_untyped_identifier_assignment(const atermpp::aterm &x)
Definition assignment.h:251
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)
Definition alias.h:81
bool is_is_not_a_function_update_function_symbol(const atermpp::aterm &e)
Recogniser for function @is_not_an_update.
void swap(forall &t1, forall &t2)
\brief swap overload
Definition forall.h:84
std::set< data::variable > find_all_variables(const data::variable &x)
Definition data.cpp:97
void make_exists(atermpp::aterm &result, ARGUMENTS... arguments)
Definition exists.h:64
function_symbol function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update.
bool is_constant(const data_expression &x)
bool is_forall_binder(const atermpp::aterm &x)
const core::identifier_string & function_update_stable_name()
Generate identifier @func_update_stable.
void swap(forall_binder &t1, forall_binder &t2)
\brief swap overload
bool search_variable(const T &x, const variable &v)
Returns true if the term has a given variable as subterm.
Definition find.h:444
assignment_list make_assignment_list(const VariableSequence &variables, const ExpressionSequence &expressions)
Converts an iterator range to data_expression_list.
Definition assignment.h:301
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:269
void make_structured_sort(atermpp::aterm &t, const ARGUMENTS &... args)
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
Definition data.cpp:102
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
Definition basic_sort.h:94
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:103
const data::data_expression & undefined_data_expression()
Returns a data expression that corresponds to 'undefined'.
Definition undefined.h:58
const data::sort_expression & undefined_sort_expression()
Returns a sort expression that corresponds to 'undefined'.
Definition undefined.h:50
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.
void make_container_sort(atermpp::aterm &t, const ARGUMENTS &... args)
void make_function_sort(atermpp::aterm &t, const ARGUMENTS &... args)
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &dom5, const sort_expression &codomain)
Convenience constructor for function sort with domain size 5.
void make_structured_sort_constructor(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::set_comprehension &x)
Definition data.cpp:66
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
void make_untyped_possible_sorts(atermpp::aterm &t, const ARGUMENTS &... args)
std::vector< untyped_data_parameter > untyped_data_parameter_vector
\brief vector of untyped_data_parameters
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
void swap(basic_sort &t1, basic_sort &t2)
\brief swap overload
Definition basic_sort.h:85
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
atermpp::term_list< untyped_identifier_assignment > untyped_identifier_assignment_list
\brief list of untyped_identifier_assignments
Definition assignment.h:242
std::string pp(const data::variable_list &x)
Definition data.cpp:31
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
Definition data.cpp:185
std::string pp(const data::where_clause &x)
Definition data.cpp:82
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:306
std::vector< structured_sort_constructor_argument > structured_sort_constructor_argument_vector
\brief vector of structured_sort_constructor_arguments
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
std::string pp(const machine_number_list &x)
bool is_bag_comprehension_binder(const atermpp::aterm &x)
std::set< data::variable > find_free_variables_with_bound(const T &x, VariableContainer const &bound)
Definition find.h:347
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
function_symbol is_not_a_function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @is_not_an_update.
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
std::string pp(const data::data_expression &x)
Definition data.cpp:52
void swap(binder_type &t1, binder_type &t2)
\brief swap overload
Definition binder_type.h:69
std::string pp(const data::untyped_identifier &x)
Definition data.cpp:74
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
std::string pp(const data::sort_expression_vector &x)
Definition data.cpp:26
std::string pp(const data::binder_type &x)
Definition data.cpp:48
bool is_sort_expression(const atermpp::aterm &x)
Test for a sort_expression expression.
atermpp::term_list< structured_sort_constructor > structured_sort_constructor_list
\brief list of structured_sort_constructors
std::string pp(const data::sort_expression_list &x)
Definition data.cpp:25
void make_untyped_sort_variable(atermpp::aterm &t, const ARGUMENTS &... args)
std::pair< atermpp::aterm, atermpp::aterm > machine_number_key_type
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
T join(FwdIt first, FwdIt last, BinaryOperation op, T empty_sequence_result)
Given a sequence [t1, t2, ..., tn] of elements of type T, returns op(t1, op(t2, .....
Definition join.h:55
T join_balanced(RndIt first, RndIt last, BinaryOperation op)
Given a non-empty sequence [t1, t2, ..., tn] of elements of type T, returns op(op(t1,...
Definition join.h:76
void split(const T &t, OutputIterator i, MatchFunction match, AccessorFunction1 lhs, AccessorFunction2 rhs)
Splits a binary tree T into a sequence, and writes the result to the output range given by an output ...
Definition join.h:34
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
expression builder that visits all sub expressions
Definition builder.h:42
void update(T &x, typename atermpp::disable_if_container< T >::type *=nullptr)
Definition builder.h:54
void leave(const T &)
Definition builder.h:50
void apply(atermpp::term_list< T > &result, const atermpp::term_list< U > &x)
Definition builder.h:89
void update(std::set< T > &x)
Definition builder.h:75
void enter(const T &)
Definition builder.h:45
core::identifier_string parse_Id(const parse_node &node) const
Definition parse.h:233
atermpp::term_list< T > parse_list(const parse_node &node, const std::string &type, const Function &f) const
Definition parse.h:218
default_parser_actions(const parser &parser_)
Definition parse.h:213
std::vector< T > parse_vector(const parse_node &node, const std::string &type, const Function &f) const
Definition parse.h:226
core::identifier_string_list parse_IdList(const parse_node &node) const
Definition parse.h:243
core::identifier_string parse_Number(const parse_node &node) const
Definition parse.h:238
static const atermpp::aterm DataVarIdInit
static const atermpp::aterm SortFSet
static const atermpp::aterm DataVarId
static const atermpp::aterm BindingOperator
static const atermpp::aterm SortArrow
static const atermpp::aterm UntypedSetBagComp
static const atermpp::aterm Lambda
static const atermpp::aterm SortExpr
static const atermpp::aterm SortConsType
static const atermpp::aterm SortId
static const atermpp::aterm UntypedSortsPossible
static const atermpp::aterm Binder
static const atermpp::aterm UntypedSortVariable
static const atermpp::aterm DataEqn
static const atermpp::aterm SortRef
static const atermpp::aterm DataExpr
static const atermpp::aterm UntypedSortUnknown
static const atermpp::aterm SortSet
static const atermpp::aterm Exists
static const atermpp::aterm SortCons
static const atermpp::aterm SortBag
static const atermpp::aterm OpId
static const atermpp::aterm StructProj
static const atermpp::aterm Whr
static const atermpp::aterm UntypedIdentifierAssignment
static const atermpp::aterm SortStruct
static const atermpp::aterm SetComp
static const atermpp::aterm StructCons
static const atermpp::aterm BagComp
static const atermpp::aterm UntypedIdentifier
static const atermpp::aterm SortFBag
static const atermpp::aterm SortList
static const atermpp::aterm WhrDecl
static const atermpp::aterm Forall
static const atermpp::aterm UntypedDataParameter
void operator()(const parse_node &x)
find_and_or(const parser_table &table_)
find_left_merge_merge(const parser_table &table_)
static const atermpp::function_symbol ProcEqnSpec
static const atermpp::function_symbol Lambda
static const atermpp::function_symbol PRInit
static const atermpp::function_symbol PBESTrue
static const atermpp::function_symbol UntypedRegFrm
static const atermpp::function_symbol ProcessInit
static const atermpp::function_symbol PRESTrue
static const atermpp::function_symbol StateMu
static const atermpp::function_symbol PREqnSpec
static const atermpp::function_symbol ActMultAct
static const atermpp::function_symbol RegSeq
static const atermpp::function_symbol Rename
static const atermpp::function_symbol BagComp
static const atermpp::function_symbol StateConstantMultiply
static const atermpp::function_symbol ActNot
static const atermpp::function_symbol Allow
static const atermpp::function_symbol StateSum
static const atermpp::function_symbol ActionRenameRules
static const atermpp::function_symbol ProcEqn
static const atermpp::function_symbol ActAnd
static const atermpp::function_symbol PRESCondEq
static const atermpp::function_symbol Forall
static const atermpp::function_symbol Delta
static const atermpp::function_symbol PropVarDecl
static const atermpp::function_symbol DataEqn
static const atermpp::function_symbol UntypedDataParameter
static const atermpp::function_symbol StructProj
static const atermpp::function_symbol ProcessAssignment
static const atermpp::function_symbol ActSpec
static const atermpp::function_symbol PRESImp
static const atermpp::function_symbol StateConstantMultiplyAlt
static const atermpp::function_symbol MultAct
static const atermpp::function_symbol Whr
static const atermpp::function_symbol SortFSet
static const atermpp::function_symbol IfThenElse
static const atermpp::function_symbol StateForall
static const atermpp::function_symbol PBESForall
static const atermpp::function_symbol StateOr
static const atermpp::function_symbol PRES
static const atermpp::function_symbol ActFalse
static const atermpp::function_symbol PBESFalse
static const atermpp::function_symbol RegTransOrNil
static const atermpp::function_symbol Hide
static const atermpp::function_symbol PRESEqInf
static const atermpp::function_symbol UntypedProcessAssignment
static const atermpp::function_symbol StateYaledTimed
static const atermpp::function_symbol SortList
static const atermpp::function_symbol Exists
static const atermpp::function_symbol ActId
static const atermpp::function_symbol TimedMultAct
static const atermpp::function_symbol StateExists
static const atermpp::function_symbol ActExists
static const atermpp::function_symbol ProcVarId
static const atermpp::function_symbol ConsSpec
static const atermpp::function_symbol BInit
static const atermpp::function_symbol RenameExpr
static const atermpp::function_symbol UntypedMultiAction
static const atermpp::function_symbol PRESMinus
static const atermpp::function_symbol PBES
static const atermpp::function_symbol StructCons
static const atermpp::function_symbol StochasticOperator
static const atermpp::function_symbol StateVar
static const atermpp::function_symbol StateTrue
static const atermpp::function_symbol LinProcSpec
static const atermpp::function_symbol SortRef
static const atermpp::function_symbol StateFalse
static const atermpp::function_symbol Choice
static const atermpp::function_symbol SortArrow
static const atermpp::function_symbol OpId
static const atermpp::function_symbol SortFBag
static const atermpp::function_symbol StateImp
static const atermpp::function_symbol Sync
static const atermpp::function_symbol Sum
static const atermpp::function_symbol PRESEqNInf
static const atermpp::function_symbol PBESNot
static const atermpp::function_symbol ProcSpec
static const atermpp::function_symbol MapSpec
static const atermpp::function_symbol PRESCondSm
static const atermpp::function_symbol RegAlt
static const atermpp::function_symbol RegTrans
static const atermpp::function_symbol Action
static const atermpp::function_symbol StateMinus
static const atermpp::function_symbol SetComp
static const atermpp::function_symbol PBESImp
static const atermpp::function_symbol StateNot
static const atermpp::function_symbol CommExpr
static const atermpp::function_symbol Comm
static const atermpp::function_symbol SortCons
static const atermpp::function_symbol SortSet
static const atermpp::function_symbol PBESAnd
static const atermpp::function_symbol AtTime
static const atermpp::function_symbol Nu
static const atermpp::function_symbol Binder
static const atermpp::function_symbol StateInfimum
static const atermpp::function_symbol SortSpec
static const atermpp::function_symbol StateDelay
static const atermpp::function_symbol PRESOr
static const atermpp::function_symbol StateYaled
static const atermpp::function_symbol MultActName
static const atermpp::function_symbol ActAt
static const atermpp::function_symbol PropVarInst
static const atermpp::function_symbol PBInit
static const atermpp::function_symbol StateMay
static const atermpp::function_symbol LinearProcess
static const atermpp::function_symbol Process
static const atermpp::function_symbol SortStruct
static const atermpp::function_symbol StateDelayTimed
static const atermpp::function_symbol ActImp
static const atermpp::function_symbol ActTrue
static const atermpp::function_symbol Merge
static const atermpp::function_symbol ActForall
static const atermpp::function_symbol LinearProcessInit
static const atermpp::function_symbol Block
static const atermpp::function_symbol Seq
static const atermpp::function_symbol ActionRenameRule
static const atermpp::function_symbol Mu
static const atermpp::function_symbol PRESSupremum
static const atermpp::function_symbol StatePlus
static const atermpp::function_symbol UntypedSortsPossible
static const atermpp::function_symbol IfThen
static const atermpp::function_symbol LinearProcessSummand
static const atermpp::function_symbol StateMust
static const atermpp::function_symbol PBESExists
static const atermpp::function_symbol DataVarId
static const atermpp::function_symbol ActionRenameSpec
static const atermpp::function_symbol DataSpec
static const atermpp::function_symbol SortId
static const atermpp::function_symbol GlobVarSpec
static const atermpp::function_symbol UntypedIdentifier
static const atermpp::function_symbol StateNu
static const atermpp::function_symbol PBESOr
static const atermpp::function_symbol Distribution
static const atermpp::function_symbol UntypedSortVariable
static const atermpp::function_symbol DataVarIdInit
static const atermpp::function_symbol PREqn
static const atermpp::function_symbol StateAnd
static const atermpp::function_symbol PRESPlus
static const atermpp::function_symbol SortBag
static const atermpp::function_symbol PRESInfimum
static const atermpp::function_symbol PBEqnSpec
static const atermpp::function_symbol PRESFalse
static const atermpp::function_symbol ActOr
static const atermpp::function_symbol DataEqnSpec
static const atermpp::function_symbol PRESConstantMultiply
static const atermpp::function_symbol UntypedIdentifierAssignment
static const atermpp::function_symbol PRESConstantMultiplyAlt
static const atermpp::function_symbol UntypedSetBagComp
static const atermpp::function_symbol StateSupremum
static const atermpp::function_symbol PBEqn
static const atermpp::function_symbol UntypedSortUnknown
static const atermpp::function_symbol PRESSum
static const atermpp::function_symbol PRESAnd
static const atermpp::function_symbol RegNil
static const atermpp::function_symbol LMerge
static const atermpp::function_symbol Tau
Checks if a node is the binary operation '&&'.
is_and_node(const parser_table &table_)
Checks if a node is of type 'x && (y || z)'.
is_and_or_node(const parser_table &table_)
bool operator()(const parse_node &x)
Checks if a node is the binary operation op.
is_binary_operator_node(const parser_table &table_, const std::string &op_)
Checks if a node is of type 'x ||_ (y || z)'.
is_left_merge_merge(const parser_table &table_)
Checks if a node is the left merge operation '||_'.
is_left_merge_node(const parser_table &table_)
Checks if a node is the merge operation '||'.
is_merge_node(const parser_table &table_)
Checks if a node is the binary operation '||'.
is_or_node(const parser_table &table_)
Wrapper for D_ParseNode.
Definition dparser.h:86
parse_node child(int i) const
Definition dparser.cpp:43
int child_count() const
Definition dparser.cpp:37
std::string add_context(const std::string &message) const
Definition dparser.cpp:27
bool operator()(const parse_node &node) const
Definition parse.h:155
collector(const parser_table &table_, const std::string &type_, Container &container_, const Function &f_)
Definition parse.h:148
set_collector(const parser_table &table_, const std::string &type_, SetContainer &container_, const Function &f_)
Definition parse.h:181
bool operator()(const parse_node &node) const
Definition parse.h:188
visitor(const parser_table &table_, const std::string &type_, const Function &f_)
Definition parse.h:116
const parser_table & table
Definition parse.h:112
bool operator()(const parse_node &node) const
Definition parse.h:122
std::string symbol_name(const parse_node &node) const
Definition parse.h:205
parser_actions(const parser &parser_)
Definition parse.h:87
void traverse(const parse_node &node, const Function &f) const
Definition parse.h:93
const parser & m_parser
Definition parse.h:85
set_collector< SetContainer, Function > make_set_collector(const parser_table &table, const std::string &type, SetContainer &container, const Function &f) const
Definition parse.h:200
visitor< Function > make_visitor(const parser_table &table, const std::string &type, const Function &f) const
Definition parse.h:134
collector< Container, Function > make_collector(const parser_table &table, const std::string &type, Container &container, const Function &f) const
Definition parse.h:167
Wrapper for D_ParserTables.
Definition dparser.h:117
std::string symbol_name(const parse_node &node) const
Definition dparser.cpp:132
std::string symbol_name(unsigned int i) const
Definition dparser.cpp:115
Wrapper for D_Parser and its corresponding D_ParserTables.
Definition dparser.h:148
void print_node(std::ostream &out, const parse_node &node) const
Definition dparser.h:180
parse_node parse(const std::string &text, unsigned int start_symbol_index=0, bool partial_parses=false)
Parses a string. N.B. The user is responsible for destruction of the returned value by calling destro...
Definition dparser.cpp:209
const parser_table & symbol_table() const
Definition dparser.cpp:199
parser(D_ParserTables &tables, D_AmbiguityFn ambiguity_fn=nullptr, D_SyntaxErrorFn syntax_error_fn=nullptr, std::size_t max_error_message_count=1)
Definition dparser.cpp:174
unsigned int start_symbol_index(const std::string &name) const
Definition dparser.cpp:204
void apply(T &result, const argument_type &x)
Definition builder.h:186
Builder< update_apply_builder< Builder, Function > > super
Definition builder.h:174
update_apply_builder(const Function &f)
Definition builder.h:192
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:563
void apply(T &result, const data::machine_number &x)
Definition builder.h:487
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:518
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:635
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:572
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:498
void apply(T &result, const data::data_equation &x)
Definition builder.h:581
void apply(T &result, const data::function_symbol &x)
Definition builder.h:454
void apply(T &result, const data::assignment &x)
Definition builder.h:509
void apply(T &result, const data::abstraction &x)
Definition builder.h:651
void apply(T &result, const data::forall &x)
Definition builder.h:527
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:590
void apply(T &result, const data::exists &x)
Definition builder.h:536
void apply(T &result, const data::where_clause &x)
Definition builder.h:478
void apply(T &result, const data::application &x)
Definition builder.h:465
void apply(T &result, const data::variable &x)
Definition builder.h:443
void apply(T &result, const data::data_expression &x)
Definition builder.h:599
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:554
void apply(T &result, const data::lambda &x)
Definition builder.h:545
Maintains a multiset of bound data variables during traversal.
Definition add_binding.h:34
void decrease_bind_count(const assignment_list &assignments)
Definition add_binding.h:51
void leave(const data::exists &x)
Definition add_binding.h:84
void enter(const data::forall &x)
Definition add_binding.h:69
void leave(const data::forall &x)
Definition add_binding.h:74
void leave(const data::data_equation &x)
void enter(const data::set_comprehension &x)
Definition add_binding.h:99
core::add_binding< Builder, Derived, variable > super
Definition add_binding.h:35
void enter(const data::data_equation &x)
void leave(const data::set_comprehension &x)
void enter(const data::exists &x)
Definition add_binding.h:79
void leave(const data::bag_comprehension &x)
void enter(const data::lambda &x)
Definition add_binding.h:89
void leave(const data::untyped_set_or_bag_comprehension &x)
void increase_bind_count(const assignment_list &assignments)
Definition add_binding.h:43
void enter(const data::bag_comprehension &x)
void leave(const data::lambda &x)
Definition add_binding.h:94
void enter(const data::untyped_set_or_bag_comprehension &x)
void enter(const data::where_clause &x)
Definition add_binding.h:59
void leave(const data::where_clause &x)
Definition add_binding.h:64
add_data_variable_binding< Builder, Derived > super
void apply(T &result, const data::where_clause &x)
add_data_variable_binding< Builder, Derived > super
void apply(const data::where_clause &x)
void apply(T &result, const data::assignment &x)
Definition builder.h:117
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:231
void apply(T &result, const data::structured_sort_constructor_argument &x)
Definition builder.h:258
void apply(T &result, const data::container_sort &x)
Definition builder.h:146
void apply(T &result, const data::alias &x)
Definition builder.h:276
void apply(T &result, const data::exists &x)
Definition builder.h:213
void apply(T &result, const data::machine_number &x)
Definition builder.h:95
void apply(T &result, const data::function_symbol &x)
Definition builder.h:64
void apply(T &result, const data::untyped_possible_sorts &x)
Definition builder.h:184
void apply(T &result, const data::forall &x)
Definition builder.h:204
void apply(T &result, const data::basic_sort &x)
Definition builder.h:135
Builder< Derived > super
Definition builder.h:48
void apply(T &result, const data::data_equation &x)
Definition builder.h:285
void apply(T &result, const data::untyped_sort &x)
Definition builder.h:173
void apply(T &result, const data::abstraction &x)
Definition builder.h:391
void apply(T &result, const data::application &x)
Definition builder.h:73
void apply(T &result, const data::variable &x)
Definition builder.h:55
void apply(T &result, const data::structured_sort &x)
Definition builder.h:155
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:126
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:294
void apply(T &result, const data::function_sort &x)
Definition builder.h:164
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:106
void apply(T &result, const data::structured_sort_constructor &x)
Definition builder.h:267
void apply(T &result, const data::lambda &x)
Definition builder.h:222
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:249
void apply(T &result, const data::where_clause &x)
Definition builder.h:86
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:339
void apply(T &result, const data::data_expression &x)
Definition builder.h:303
void apply(T &result, const data::sort_expression &x)
Definition builder.h:355
void apply(T &result, const data::untyped_sort_variable &x)
Definition builder.h:193
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:240
void apply(const data::function_symbol &x)
Definition traverser.h:378
void apply(const data::set_comprehension &x)
Definition traverser.h:450
void apply(const data::untyped_identifier &x)
Definition traverser.h:408
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:464
void apply(const data::application &x)
Definition traverser.h:385
void apply(const data::forall &x)
Definition traverser.h:429
void apply(const data::data_equation &x)
Definition traverser.h:471
void apply(const data::exists &x)
Definition traverser.h:436
void apply(const data::lambda &x)
Definition traverser.h:443
void apply(const data::machine_number &x)
Definition traverser.h:401
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:422
void apply(const data::data_expression &x)
Definition traverser.h:487
void apply(const data::where_clause &x)
Definition traverser.h:393
void apply(const data::bag_comprehension &x)
Definition traverser.h:457
void apply(const data::abstraction &x)
Definition traverser.h:535
void apply(const data::assignment_expression &x)
Definition traverser.h:521
void apply(const data::variable &x)
Definition traverser.h:371
void apply(const data::assignment &x)
Definition traverser.h:415
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:480
void apply(const data::untyped_possible_sorts &x)
Definition traverser.h:901
void apply(const data::structured_sort_constructor_argument &x)
Definition traverser.h:963
void apply(const data::application &x)
Definition traverser.h:819
void apply(const data::untyped_sort_variable &x)
Definition traverser.h:908
void apply(const data::basic_sort &x)
Definition traverser.h:865
void apply(const data::bag_comprehension &x)
Definition traverser.h:947
void apply(const data::assignment_expression &x)
Definition traverser.h:1040
void apply(const data::untyped_sort &x)
Definition traverser.h:894
void apply(const data::assignment &x)
Definition traverser.h:849
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:955
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:998
void apply(const data::structured_sort &x)
Definition traverser.h:879
void apply(const data::function_sort &x)
Definition traverser.h:886
void apply(const data::data_equation &x)
Definition traverser.h:988
void apply(const data::container_sort &x)
Definition traverser.h:872
void apply(const data::machine_number &x)
Definition traverser.h:835
void apply(const data::abstraction &x)
Definition traverser.h:1088
void apply(const data::structured_sort_constructor &x)
Definition traverser.h:971
void apply(const data::variable &x)
Definition traverser.h:803
void apply(const data::function_symbol &x)
Definition traverser.h:811
void apply(const data::untyped_identifier &x)
Definition traverser.h:842
void apply(const data::data_expression &x)
Definition traverser.h:1006
void apply(const data::set_comprehension &x)
Definition traverser.h:939
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:857
void apply(const data::sort_expression &x)
Definition traverser.h:1054
void apply(const data::where_clause &x)
Definition traverser.h:827
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:98
void apply(const data::assignment &x)
Definition traverser.h:90
void apply(const data::sort_expression &x)
Definition traverser.h:289
void apply(const data::where_clause &x)
Definition traverser.h:68
void apply(const data::data_expression &x)
Definition traverser.h:241
void apply(const data::lambda &x)
Definition traverser.h:171
void apply(const data::basic_sort &x)
Definition traverser.h:105
void apply(const data::variable &x)
Definition traverser.h:46
void apply(const data::untyped_possible_sorts &x)
Definition traverser.h:141
void apply(const data::untyped_identifier &x)
Definition traverser.h:83
void apply(const data::untyped_sort_variable &x)
Definition traverser.h:148
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:195
void apply(const data::forall &x)
Definition traverser.h:155
void apply(const data::application &x)
Definition traverser.h:60
void apply(const data::structured_sort_constructor_argument &x)
Definition traverser.h:203
void apply(const data::structured_sort_constructor &x)
Definition traverser.h:210
void apply(const data::untyped_sort &x)
Definition traverser.h:134
void apply(const data::machine_number &x)
Definition traverser.h:76
void apply(const data::function_sort &x)
Definition traverser.h:126
void apply(const data::container_sort &x)
Definition traverser.h:112
void apply(const data::set_comprehension &x)
Definition traverser.h:179
void apply(const data::data_equation &x)
Definition traverser.h:224
void apply(const data::structured_sort &x)
Definition traverser.h:119
void apply(const data::assignment_expression &x)
Definition traverser.h:275
void apply(const data::bag_comprehension &x)
Definition traverser.h:187
void apply(const data::exists &x)
Definition traverser.h:163
void apply(const data::abstraction &x)
Definition traverser.h:323
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:234
void apply(const data::function_symbol &x)
Definition traverser.h:53
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:682
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:635
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:700
void apply(const data::data_expression &x)
Definition traverser.h:707
void apply(const data::bag_comprehension &x)
Definition traverser.h:674
void apply(const data::data_equation &x)
Definition traverser.h:690
void apply(const data::where_clause &x)
Definition traverser.h:605
void apply(const data::set_comprehension &x)
Definition traverser.h:666
void apply(const data::exists &x)
Definition traverser.h:650
void apply(const data::untyped_identifier &x)
Definition traverser.h:620
void apply(const data::variable &x)
Definition traverser.h:583
void apply(const data::abstraction &x)
Definition traverser.h:755
void apply(const data::forall &x)
Definition traverser.h:642
void apply(const data::assignment_expression &x)
Definition traverser.h:741
void apply(const data::assignment &x)
Definition traverser.h:627
void apply(const data::application &x)
Definition traverser.h:597
void apply(const data::function_symbol &x)
Definition traverser.h:590
void apply(const data::lambda &x)
Definition traverser.h:658
void apply(const data::machine_number &x)
Definition traverser.h:613
void apply(T &result, const data::abstraction &x)
Definition builder.h:910
void apply(T &result, const data::application &x)
Definition builder.h:724
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:849
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:757
void apply(T &result, const data::data_expression &x)
Definition builder.h:858
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:894
void apply(T &result, const data::where_clause &x)
Definition builder.h:737
Builder< Derived > super
Definition builder.h:695
void apply(T &result, const data::forall &x)
Definition builder.h:786
void apply(T &result, const data::function_symbol &x)
Definition builder.h:713
void apply(T &result, const data::exists &x)
Definition builder.h:795
void apply(T &result, const data::lambda &x)
Definition builder.h:804
void apply(T &result, const data::variable &x)
Definition builder.h:702
void apply(T &result, const data::assignment &x)
Definition builder.h:768
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:777
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:831
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:813
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:822
void apply(T &result, const data::machine_number &x)
Definition builder.h:746
void apply(T &result, const data::data_equation &x)
Definition builder.h:840
Tests if a term is a sort, and if it is equal to s.
bool operator()(const atermpp::aterm &t) const
bool operator()(Term2 t) const
Function call operator.
Function object that determines if a term is equal to a given data variable.
data_expression make_untyped_set_or_bag_comprehension(const variable &v, const data_expression &x) const
Definition parse_impl.h:145
data::variable_list parse_VarsDeclList(const core::parse_node &node) const
Definition parse_impl.h:204
data::data_expression_list parse_DataExprList(const core::parse_node &node) const
Definition parse_impl.h:287
data_expression make_list_enumeration(const data_expression_list &x) const
Definition parse_impl.h:150
data_expression make_function_update(const data_expression &x, const data_expression &y, const data_expression &z) const
Definition parse_impl.h:168
data_expression make_set_enumeration(const data_expression_list &x) const
Definition parse_impl.h:156
data::sort_expression_list get_sorts(const ExpressionContainer &x) const
Definition parse_impl.h:174
data_expression_actions(const core::parser &parser_)
Definition parse_impl.h:141
bool callback_VarsDecl(const core::parse_node &node, variable_vector &result) const
Definition parse_impl.h:189
data::variable parse_VarDecl(const core::parse_node &node) const
Definition parse_impl.h:184
data::untyped_identifier_assignment parse_Assignment(const core::parse_node &node) const
Definition parse_impl.h:277
data::data_expression parse_DataValExpr(const core::parse_node &node) const
Definition parse_impl.h:272
data::data_expression_list parse_BagEnumEltList(const core::parse_node &node) const
Definition parse_impl.h:292
data::untyped_identifier_assignment_list parse_AssignmentList(const core::parse_node &node) const
Definition parse_impl.h:282
data_expression make_bag_enumeration(const data_expression_list &x) const
Definition parse_impl.h:162
data::data_expression parse_DataExprUnit(const core::parse_node &node) const
Definition parse_impl.h:258
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:211
bool callback_IdsDecl(const core::parse_node &node, function_symbol_vector &result) const
Definition parse_impl.h:341
data::variable_list parse_GlobVarSpec(const core::parse_node &node) const
Definition parse_impl.h:373
data_specification_actions(const core::parser &parser_)
Definition parse_impl.h:300
data::function_symbol_vector parse_MapSpec(const core::parse_node &node) const
Definition parse_impl.h:368
data::data_equation_vector parse_EqnDeclList(const core::parse_node &node, const variable_list &variables) const
Definition parse_impl.h:399
data::variable_list parse_VarSpec(const core::parse_node &node) const
Definition parse_impl.h:378
std::vector< atermpp::aterm > parse_SortDeclList(const core::parse_node &node) const
Definition parse_impl.h:329
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:461
bool callback_SortDecl(const core::parse_node &node, std::vector< atermpp::aterm > &result) const
Definition parse_impl.h:304
data::data_equation_vector parse_EqnSpec(const core::parse_node &node) const
Definition parse_impl.h:406
data::function_symbol_vector parse_IdsDeclList(const core::parse_node &node) const
Definition parse_impl.h:356
bool callback_DataSpecElement(const core::parse_node &node, untyped_data_specification &result) const
Definition parse_impl.h:413
bool callback_EqnDecl(const core::parse_node &node, const variable_list &variables, data_equation_vector &result) const
Definition parse_impl.h:383
std::vector< atermpp::aterm > parse_SortSpec(const core::parse_node &node) const
Definition parse_impl.h:336
data::function_symbol_vector parse_ConsSpec(const core::parse_node &node) const
Definition parse_impl.h:363
bool operator()(const function_symbol &c) const
Function call operator.
void apply(const data::structured_sort_constructor &)
Definition is_untyped.h:66
void apply(const data::untyped_possible_sorts &)
Definition is_untyped.h:51
void apply(const data::structured_sort_constructor_argument &)
Definition is_untyped.h:61
void apply(const data::untyped_set_or_bag_comprehension &)
Definition is_untyped.h:56
void apply(const data::untyped_identifier_assignment &)
Definition is_untyped.h:41
void apply(const data::untyped_sort &)
Definition is_untyped.h:46
sort_expression_traverser< is_untyped_traverser > super
Definition is_untyped.h:25
void apply(const data::untyped_identifier &)
Definition is_untyped.h:36
normalize_sorts_function(const sort_specification &sort_spec)
sort_expression operator()(const sort_expression &e) const
Normalise sorts.
const std::map< sort_expression, sort_expression > & m_normalised_aliases
sort_expression operator()(const T &t) const
Definition print.h:587
void print_condition(const T &x, const std::string &arrow=" -> ")
Definition print.h:749
void apply(const data::untyped_set_or_bag_comprehension_binder &x)
Definition print.h:1330
void apply(const data::untyped_sort_variable &x)
Definition print.h:1483
void apply(const data::application &x)
Definition print.h:1531
bool is_cons_list(data_expression x) const
Definition print.h:835
void apply(const machine_number &x)
Definition print.h:2306
void print_container(const Container &container, int container_precedence=-1, const std::string &separator=", ", const std::string &open_bracket="(", const std::string &close_bracket=")")
Definition print.h:547
void apply(const data::untyped_identifier &x)
Definition print.h:1491
void print_sort_list(const Container &container, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:759
void print_fset_default(const data_expression &x)
Definition print.h:1149
void apply(const data::bag_comprehension_binder &x)
Definition print.h:1342
void apply(const data::set_container &x)
Definition print.h:1407
void apply(const data::set_comprehension_binder &x)
Definition print.h:1336
void print_set_enumeration(const application &x)
Definition print.h:797
void print_binary_data_operation(const application &x, const std::string &op)
Definition print.h:476
void print_cons_list(data_expression x)
Definition print.h:919
void print_sort_declarations(const AliasContainer &aliases, const SortContainer &sorts, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:2415
void update_mappings(const data_equation &eqn, std::vector< variable > &variables, std::map< core::identifier_string, variable > &variable_map, std::set< core::identifier_string > &function_symbol_names)
Definition print.h:2355
bool is_fbag_cons_list(data_expression x)
Returns true if x is a list composed of cons, insert and cinsert applications.
Definition print.h:863
void print_assignments(const Container &container, bool print_lhs=true, const std::string &opener="", const std::string &closer="", const std::string &separator=", ", const std::string &assignment_symbol=" = ")
Definition print.h:719
void apply(const data::list_container &x)
Definition print.h:1400
void apply(const data::exists &x)
Definition print.h:2334
void apply(const data::fbag_container &x)
Definition print.h:1428
void apply(const data::function_sort &x)
Definition print.h:1459
void print_fset_lambda(const data_expression &x)
Definition print.h:1076
core::identifier_string generate_identifier(const std::string &prefix, const data_expression &context) const
Definition print.h:535
void apply(const data::data_equation &x)
Definition print.h:2344
void apply(const data::alias &x)
Definition print.h:1391
void print_sorted_declarations(const Container &container, bool print_sorts=true, bool join_sorts=true, bool maximally_shared=false, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ", SortAccessor get_sort=get_sort_default())
Definition print.h:594
void apply(const data::where_clause &x)
Definition print.h:2311
void apply(const data::data_specification &x)
Definition print.h:2484
bool is_fbag_zero(const data_expression &x)
Definition print.h:904
void apply(const data::structured_sort &x)
Definition print.h:1452
void apply(const data::untyped_identifier_assignment &x)
Definition print.h:1321
void print_equations(const Container &equations, const data_specification &data_spec, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:2455
bool is_fset_false(const data_expression &x)
Definition print.h:894
bool is_abstraction_application(const application &x) const
Definition print.h:830
void apply(const data::lambda_binder &x)
Definition print.h:1360
void apply(const data::structured_sort_constructor_argument &x)
Definition print.h:1366
void apply(const data::variable &x)
Definition print.h:1498
void apply(const data::container_type &x)
Definition print.h:1270
bool is_fbag_one(const data_expression &x)
Definition print.h:909
void apply(const data::basic_sort &x)
Definition print.h:1435
bool is_snoc_list(data_expression x) const
Definition print.h:844
void print_fbag_one(const data_expression &x)
Definition print.h:978
bool is_fbag_lambda(const data_expression &x)
Definition print.h:914
void print_abstraction(const Abstraction &x, const std::string &op)
Definition print.h:1182
void apply(const data::function_symbol &x)
Definition print.h:1505
void apply(const data::exists_binder &x)
Definition print.h:1354
void apply(const data::fset_container &x)
Definition print.h:1421
bool has_conflict(const data_equation &eqn, const std::map< core::identifier_string, variable > &variable_map)
Definition print.h:2375
bool is_numeric_expression(const application &x)
Definition print.h:872
bool is_infix_operation(const application &x) const
Definition print.h:483
void print_fbag_lambda(const data_expression &x)
Definition print.h:995
void apply(const data::untyped_data_parameter &x)
Definition print.h:1313
void apply(const data::abstraction &x)
Definition print.h:2495
void apply(const data::untyped_sort &x)
Definition print.h:1467
void apply(const data::container_sort &x)
Definition print.h:1442
void apply(const data::assignment &x)
Definition print.h:1296
void print_fbag_zero(const data_expression &x)
Definition print.h:958
data::add_traverser_sort_expressions< core::detail::printer, Derived > super
Definition print.h:450
bool is_fset_lambda(const data_expression &x)
Definition print.h:899
void print_snoc_list(data_expression x)
Definition print.h:932
void print_fset_false(const data_expression &x)
Definition print.h:1064
void print_fbag_cons_list(data_expression x)
Definition print.h:1030
bool is_standard_sort(const sort_expression &x)
Definition print.h:880
void apply(const data::untyped_possible_sorts &x)
Definition print.h:1474
void print_unary_data_operation(const application &x, const std::string &op)
Definition print.h:460
bool is_fset_cons_list(data_expression x)
Definition print.h:853
void print_setbag_comprehension(const abstraction &x)
Definition print.h:821
void print_fset_cons_list(data_expression x)
Definition print.h:945
void print_bag_enumeration(const application &x)
Definition print.h:804
void print_variables(const Container &container, bool print_sorts=true, bool join_sorts=true, bool maximally_shared=false, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:706
void apply(const data::bag_container &x)
Definition print.h:1414
void print_function_application(const application &x)
Definition print.h:1192
void print_fbag_default(const data_expression &x)
Definition print.h:1013
Iter find_conflicting_equation(Iter first, Iter last, std::vector< variable > &variables)
Searches in the range of equations [first, last) for the first equation that conflicts with one of th...
Definition print.h:2396
void print_variable(const Variable &x, bool print_sort=false)
Definition print.h:574
void apply(const data::variable_list &x)
Definition print.h:1306
void apply(const std::pair< data_expression, data_expression > &x)
Definition print.h:1262
void print_binary_data_operation(const application &x, const data_expression &x1, const data_expression &x2, const std::string &op)
Definition print.h:466
void print_list_enumeration(const application &x)
Definition print.h:790
void apply(const data::structured_sort_constructor &x)
Definition print.h:1378
void apply(const data::forall &x)
Definition print.h:2329
void apply(const data::forall_binder &x)
Definition print.h:1348
void apply(const data::lambda &x)
Definition print.h:2339
void print_fset_set_operation(const data_expression &x, const std::string &op)
Definition print.h:1086
void print_fset_true(const data_expression &x)
Definition print.h:1058
bool is_fset_true(const data_expression &x)
Definition print.h:889
data::structured_sort_constructor parse_ConstrDecl(const core::parse_node &node) const
Definition parse_impl.h:96
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
Definition parse_impl.h:35
data::structured_sort_constructor_list parse_ConstrDeclList(const core::parse_node &node) const
Definition parse_impl.h:116
data::sort_expression_list parse_SortProduct(const core::parse_node &node) const
Definition parse_impl.h:87
data::sort_expression_list parse_SortExpr_as_SortProduct(const core::parse_node &node) const
Definition parse_impl.h:76
data::structured_sort_constructor_argument_list parse_ProjDeclList(const core::parse_node &node) const
Definition parse_impl.h:133
sort_expression_actions(const core::parser &parser_)
Definition parse_impl.h:31
data::structured_sort_constructor_argument parse_ProjDecl(const core::parse_node &node) const
Definition parse_impl.h:121
bool operator()(const sort_expression &s) const
Function call operator.
sort_has_name(std::string const &name)
Function object that returns the sort of a data expression.
sort_expression operator()(const Expression &e) const
Function call operator.
Function object that returns the name of a data variable.
core::identifier_string operator()(const variable &v) const
Function call operator.
Prints the object x to a stream.
Definition print.h:2530
void operator()(const T &x, std::ostream &out)
Definition print.h:2532
sort_expression operator()(structured_sort_constructor_argument const &s) const
\brief Builder class
Definition builder.h:946
\brief Traverser class
Definition traverser.h:790
std::size_t operator()(const atermpp::aterm &t) const
Definition aterm.h:483
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const
std::size_t operator()(const mcrl2::data::container_type &v) const
std::size_t operator()(const mcrl2::data::data_expression &v) const
std::size_t operator()(const mcrl2::data::function_sort &v) const
std::size_t operator()(const mcrl2::data::sort_expression &x) const
std::size_t operator()(const mcrl2::data::variable &v) const
Definition variable.h:136