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::data::detail
18{
19
21{
23 using super::enter;
24 using super::leave;
25 using super::apply;
26
27 bool result = false;
28
30 {
31 result = true;
32 }
33
35 {
36 result = true;
37 }
38
39 void apply(const data::untyped_sort& )
40 {
41 result = true;
42 }
43
45 {
46 result = true;
47 }
48
50 {
51 result = true;
52 }
53
55 {
56 result = true;
57 }
58
60 {
61 result = true;
62 }
63};
64
65inline
67{
69 f.apply(x);
70 return f.result;
71}
72
73} // namespace mcrl2::data::detail
74
75#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_string & operator=(aterm_string &&t) noexcept=default
aterm_string & operator=(const aterm_string &t) noexcept=default
aterm & operator=(const aterm &other) noexcept=default
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A list of aterm objects.
Definition aterm_list.h:26
A unordered_map class in which aterms can be stored.
apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:120
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:144
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:47
parse_node_exception(const parse_node &node, const std::string &message)
Definition parse.h:52
static std::string get_error_message(const parse_node &node, const std::string &user_message)
Definition parse.h:35
parse_node_unexpected_exception(const parser &p, const parse_node &node)
Definition parse.h:76
static std::string get_error_message(const parser &p, const parse_node &node)
Definition parse.h:60
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
Definition builder.h:212
void apply(T &result, const argument_type &x)
Definition builder.h:207
An abstraction expression.
Definition abstraction.h:23
const variable_list & variables() const
Definition abstraction.h:60
abstraction(const atermpp::aterm &term)
Constructor.
Definition abstraction.h:32
abstraction(const binder_type &binding_operator, const variable_list &variables, const data_expression &body)
Constructor.
Definition abstraction.h:39
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:45
abstraction & operator=(abstraction &&) noexcept=default
const data_expression & body() const
Definition abstraction.h:65
abstraction(abstraction &&) noexcept=default
abstraction()
Default constructor.
Definition abstraction.h:26
const binder_type & binding_operator() const
Definition abstraction.h:55
abstraction & operator=(const abstraction &) noexcept=default
\brief A sort alias
Definition alias.h:23
alias()
\brief Default constructor X3.
Definition alias.h:26
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:39
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
Definition alias.h:32
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
Definition alias.h:49
const sort_expression & reference() const
Definition alias.h:54
\brief Assignment expression
Definition assignment.h:24
assignment_expression(assignment_expression &&) noexcept=default
assignment_expression()
\brief Default constructor X3.
Definition assignment.h:27
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:33
\brief Assignment of a data expression to a variable
Definition assignment.h:88
assignment(const variable &lhs, const data_expression &rhs)
\brief Constructor Z14.
Definition assignment.h:104
const data_expression & rhs() const
Definition assignment.h:119
assignment(const atermpp::aterm &term)
Definition assignment.h:97
assignment(assignment &&) noexcept=default
assignment & operator=(assignment &&) noexcept=default
const variable & lhs() const
Definition assignment.h:114
assignment & operator=(const assignment &) noexcept=default
assignment(const assignment &) noexcept=default
Move semantics.
assignment()
\brief Default constructor X3.
Definition assignment.h:91
const data_expression & operator()(const variable &x) const
Applies the assignment to a variable.
Definition assignment.h:127
\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:25
basic_sort(const basic_sort &) noexcept=default
Move semantics.
basic_sort()
\brief Default constructor X3.
Definition basic_sort.h:28
basic_sort & operator=(const basic_sort &) noexcept=default
const core::identifier_string & name() const
Definition basic_sort.h:56
basic_sort(basic_sort &&) noexcept=default
basic_sort(const core::identifier_string &name)
\brief Constructor Z14.
Definition basic_sort.h:41
basic_sort(const std::string &name)
\brief Constructor Z2.
Definition basic_sort.h:46
basic_sort & operator=(basic_sort &&) noexcept=default
basic_sort(const atermpp::aterm &term)
Definition basic_sort.h:34
binder_type()
\brief Default constructor X3.
Definition binder_type.h:27
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:33
\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 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_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:107
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 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.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
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.
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, bool skip_equations=false) const
Adds the system defined sorts to the sets with constructors, mappings, and equations for.
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
data_specification()=default
Default constructor. Generate a data specification that contains only booleans and positive numbers.
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:29
bool MatchIf(const function_sort &type, sort_expression &result) const
bool MatchFalseFunction(const function_sort &type, sort_expression &result) const
bool MatchListOpCons(const function_sort &type, sort_expression &result) const
bool match_fset_fbag_pick(const function_sort &type, sort_expression &result) const
std::map< core::identifier_string, sort_expression_list > system_constants
Definition typecheck.h:28
bool UnifyMinType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const
bool MatchListOpEltAt(const function_sort &type, sort_expression &result) const
sort_expression TraverseVarConsTypeDN(const detail::variable_context &DeclaredVars, data_expression &DataTerm, sort_expression PosType, bool strictly_ambiguous=true, std::size_t nFactPars=std::string::npos, bool warn_upcasting=false, bool print_cast_error=true) const
bool EqTypesA(const sort_expression &Type1, const sort_expression &Type2) const
std::map< core::identifier_string, sort_expression_list > user_functions
Definition typecheck.h:31
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:87
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:94
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)
sort_expression TraverseVarConsTypeD(const detail::variable_context &DeclaredVars, data_expression &DataTerm, const sort_expression &PosType, bool strictly_ambiguous=true, bool warn_upcasting=false, bool print_cast_error=true) const
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:72
assignment typecheck_assignment(const assignment &x, const detail::variable_context &variable_context)
Definition typecheck.h:87
bool MatchSetOpSetCompl(const function_sort &type, sort_expression &result) const
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:30
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_specification operator()() const
Yields a type checked data specification, provided typechecking was successful. If not successful an ...
sort_expression UpCastNumericType(sort_expression NeededType, sort_expression Type, data_expression &Par, const detail::variable_context &DeclaredVars, bool strictly_ambiguous, bool warn_upcasting=false, bool print_cast_error=false) const
data_expression upcast_numeric_type(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:256
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:117
bool MatchListOpHead(const function_sort &type, sort_expression &result) const
bool match_fset_insert(const function_sort &type, sort_expression &result) 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:32
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:170
void typecheck_variable(const data_type_checker &typechecker, const variable &v) const
Definition typecheck.cpp:28
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:23
exists(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition exists.h:44
exists & operator=(exists &&) noexcept=default
exists(const aterm &d)
Definition exists.h:31
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:25
forall(forall &&) noexcept=default
forall(const aterm &d)
Definition forall.h:33
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:46
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 & operator=(function_sort &&) noexcept=default
function_sort(function_sort &&) noexcept=default
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:24
lambda(const Container &variables, const data_expression &body, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Definition lambda.h:57
lambda(const variable &variable, const data_expression &body)
Definition lambda.h:45
lambda & operator=(const lambda &) noexcept=default
lambda(const aterm &d)
Definition lambda.h:33
lambda()=default
Constructor.
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).
void check_for_alias_loop(const sort_expression &s, std::set< sort_expression > sorts_already_seen, bool toplevel=true) const
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 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(const std::string &name, const structured_sort_constructor_argument_list &arguments, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=0)
Constructor.
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 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.
structured_sort_constructor(const std::string &name, const std::string &recogniser)
Constructor.
function_symbol_vector projection_functions(const sort_expression &s) const
Returns the projection functions for this constructor.
structured_sort_constructor(const std::string &name)
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...
structured_sort_constructor(const std::string &name, const Container &arguments, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
Constructor.
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
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
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:179
const core::identifier_string & lhs() const
Definition assignment.h:210
untyped_identifier_assignment(const std::string &lhs, const data_expression &rhs)
\brief Constructor Z2.
Definition assignment.h:200
untyped_identifier_assignment(const atermpp::aterm &term)
Definition assignment.h:188
untyped_identifier_assignment()
\brief Default constructor X3.
Definition assignment.h:182
const data_expression & rhs() const
Definition assignment.h:215
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:195
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:223
\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 & operator=(const untyped_possible_sorts &) noexcept=default
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:74
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:83
untyped_set_or_bag_comprehension_binder()
\brief Default constructor X3.
Definition binder_type.h:77
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:25
variable(const variable &) noexcept=default
Move semantics.
variable(const std::string &name, const sort_expression &sort)
Constructor.
Definition variable.h:66
variable(variable &&) noexcept=default
variable()
Default constructor.
Definition variable.h:46
const core::identifier_string & name() const
Definition variable.h:35
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
Definition variable.h:40
variable & operator=(const variable &) noexcept=default
variable(const core::identifier_string &name, const sort_expression &sort)
Constructor.
Definition variable.h:59
variable(const atermpp::aterm &term)
Constructor.
Definition variable.h:52
\brief A where expression
where_clause & operator=(where_clause &&) noexcept=default
const assignment_list & assignments() const
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(where_clause &&) noexcept=default
where_clause(const data_expression &body, const assignment_expression_list &declarations)
\brief Constructor Z14.
D_ParserTables parser_tables_fsm
D_ParserTables parser_tables_dot
D_ParserTables parser_tables_mcrl2
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:393
const aterm_string & empty_string()
Returns the empty aterm_string.
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)
bool check_term_StateFalse(const Term &t)
bool check_term_argument(const Term &t, CheckFunction f)
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)
bool check_term_Delta(const Term &t)
bool check_rule_PBEqn(const Term &t)
bool check_rule_Action(const Term &t)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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.
apply_builder< Builder > make_apply_builder()
Definition builder.h:103
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:220
void print_aterm(const T &)
Definition parse.h:248
void print_aterm(const atermpp::aterm &x)
Definition parse.h:254
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:127
identifier_string parse_identifier(const std::string &text)
Parse an identifier.
Definition parse.h:261
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
Definition builder.h:186
bool is_user_identifier(std::string const &s)
Definition parse.h:272
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:151
bool is_greater(const application &x)
Definition print.h:217
bool is_minus(const application &x)
Definition print.h:99
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:223
bool is_equal_to(const application &x)
Definition print.h:193
bool is_snoc_list(data_expression x)
Definition print.h:279
bool is_in(const application &x)
Definition print.h:229
bool head_matches_undefined_symbol(const data_expression &x, const core::identifier_string &s)
Definition print.h:70
bool is_bag_intersection(const application &x)
Definition print.h:257
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:234
bool is_set_difference(const application &x)
Definition print.h:163
bool is_not_equal_to(const application &x)
Definition print.h:199
bool is_numeric_cast(const data_expression &x)
Definition print.h:43
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:245
bool is_divides(const application &x)
Definition print.h:141
bool is_set_union(const application &x)
Definition print.h:157
variable_list parse_variables(const std::string &text)
Definition data.cpp:212
bool is_bag_difference(const application &x)
Definition print.h:175
bool is_less_equal(const application &x)
Definition print.h:211
bool is_set_intersection(const application &x)
Definition print.h:251
bool is_plus(const application &x)
Definition print.h:85
bool is_or(const application &x)
Definition print.h:187
bool is_greater_equal(const application &x)
Definition print.h:223
bool is_untyped(const data_expression &x)
Definition is_untyped.h:66
bool is_one(const data_expression &x)
Definition print.h:28
bool is_element_at(const application &x)
Definition print.h:245
bool is_bag_join(const application &x)
Definition print.h:169
bool is_concat(const application &x)
Definition print.h:263
bool is_and(const application &x)
Definition print.h:181
bool look_through_numeric_casts(const data_expression &x, std::function< bool(const data_expression &)> f)
Definition print.h:59
bool is_snoc(const application &x)
Definition print.h:295
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:202
bool is_implies(const application &x)
Definition print.h:151
bool is_cons_list(data_expression x)
Definition print.h:269
bool is_mod(const application &x)
Definition print.h:110
bool is_divmod(const application &x)
Definition print.h:131
bool is_div(const application &x)
Definition print.h:120
bool is_times(const application &x)
Definition print.h:235
bool is_cons(const application &x)
Definition print.h:289
bool is_less(const application &x)
Definition print.h:205
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:35
function_symbol fbag2fset(const sort_expression &s)
Constructor for function symbol @fbag2fset.
Definition bag1.h:1471
bool is_bag2set_application(const atermpp::aterm &e)
Recogniser for application of Bag2Set.
Definition bag1.h:747
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition bag1.h:555
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:1239
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition bag1.h:664
const core::identifier_string & fbag2fset_name()
Generate identifier @fbag2fset.
Definition bag1.h:1461
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bag1.h:1631
bool is_min_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @min_.
Definition bag1.h:1025
function_symbol bag_fbag(const sort_expression &s)
Constructor for function symbol @bagfbag.
Definition bag1.h:172
bool is_min_function_application(const atermpp::aterm &e)
Recogniser for application of @min_.
Definition bag1.h:1061
function_symbol monus_function(const sort_expression &s)
Constructor for function symbol @monus_.
Definition bag1.h:1079
const core::identifier_string & fbag_intersect_name()
Generate identifier @fbag_inter.
Definition bag1.h:1325
void make_bag2set(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Bag2Set.
Definition bag1.h:737
bool is_fbag_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_diff.
Definition bag1.h:1413
bool is_fbag_join_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_join.
Definition bag1.h:1277
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:332
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
Definition bag1.h:1525
application zero_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @zero_.
Definition bag1.h:851
const core::identifier_string & bool2nat_function_name()
Generate identifier @Bool2Nat_.
Definition bag1.h:1195
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:923
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition bag1.h:1679
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition bag1.h:685
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:608
const core::identifier_string & set2bag_name()
Generate identifier Set2Bag.
Definition bag1.h:755
bool is_bag_fbag_application(const atermpp::aterm &e)
Recogniser for application of @bagfbag.
Definition bag1.h:216
application fbag2fset(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fbag2fset.
Definition bag1.h:1496
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:1558
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:987
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag1.h:1701
bool is_fbag_difference_application(const atermpp::aterm &e)
Recogniser for application of @fbag_diff.
Definition bag1.h:1453
bool is_bag_fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagfbag.
Definition bag1.h:182
const core::identifier_string & zero_function_name()
Generate identifier @zero_.
Definition bag1.h:817
const core::identifier_string & add_function_name()
Generate identifier @add_.
Definition bag1.h:941
application bag2set(const sort_expression &s, const data_expression &arg0)
Application of function symbol Bag2Set.
Definition bag1.h:727
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition bag1.h:385
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:140
bool is_fbag2fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag2fset.
Definition bag1.h:1481
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition bag1.h:491
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:703
bool is_monus_function_application(const atermpp::aterm &e)
Recogniser for application of @monus_.
Definition bag1.h:1125
const core::identifier_string & nat2bool_function_name()
Generate identifier @Nat2Bool_.
Definition bag1.h:1133
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:507
bool is_zero_function_application(const atermpp::aterm &e)
Recogniser for application of @zero_.
Definition bag1.h:871
const core::identifier_string & fbag_difference_name()
Generate identifier @fbag_diff.
Definition bag1.h:1393
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:1115
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition bag1.h:305
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:294
function_symbol add_function(const sort_expression &s)
Constructor for function symbol @add_.
Definition bag1.h:951
bool is_nat2bool_function_application(const atermpp::aterm &e)
Recogniser for application of @Nat2Bool_.
Definition bag1.h:1187
function_symbol fbag_intersect(const sort_expression &s)
Constructor for function symbol @fbag_inter.
Definition bag1.h:1335
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:1375
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition bag1.h:454
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:1177
application bag_fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagfbag.
Definition bag1.h:196
bool is_fbag_intersect_application(const atermpp::aterm &e)
Recogniser for application of @fbag_inter.
Definition bag1.h:1385
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition bag1.h:406
function_symbol fbag_difference(const sort_expression &s)
Constructor for function symbol @fbag_diff.
Definition bag1.h:1403
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition bag1.h:369
application bool2nat_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Bool2Nat_.
Definition bag1.h:1229
bool is_bag_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagcomp.
Definition bag1.h:244
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:1051
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:1005
bool is_set2bag_function_symbol(const atermpp::aterm &e)
Recogniser for function Set2Bag.
Definition bag1.h:775
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition bag1.h:470
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bag1.h:1619
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:1572
bool is_nat2bool_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Nat2Bool_.
Definition bag1.h:1153
application one_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @one_.
Definition bag1.h:913
const core::identifier_string & monus_function_name()
Generate identifier @monus_.
Definition bag1.h:1069
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition bag1.h:1691
bool is_add_function_application(const atermpp::aterm &e)
Recogniser for application of @add_.
Definition bag1.h:997
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:1507
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:1307
function_symbol min_function(const sort_expression &s)
Constructor for function symbol @min_.
Definition bag1.h:1015
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:765
const core::identifier_string & bag_fbag_name()
Generate identifier @bagfbag.
Definition bag1.h:162
const core::identifier_string & bag2set_name()
Generate identifier Bag2Set.
Definition bag1.h:693
const core::identifier_string & intersection_name()
Generate identifier *.
Definition bag1.h:499
application nat2bool_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Nat2Bool_.
Definition bag1.h:1167
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:396
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @bag.
Definition bag1.h:100
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:1362
function_symbol bag_comprehension(const sort_expression &s)
Constructor for function symbol @bagcomp.
Definition bag1.h:234
bool is_bag2set_function_symbol(const atermpp::aterm &e)
Recogniser for function Bag2Set.
Definition bag1.h:713
implementation_map bag_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition bag1.h:153
bool is_bool2nat_function_application(const atermpp::aterm &e)
Recogniser for application of @Bool2Nat_.
Definition bag1.h:1249
const core::identifier_string & fbag_join_name()
Generate identifier @fbag_join.
Definition bag1.h:1257
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:582
function_symbol fbag_join(const sort_expression &s)
Constructor for function symbol @fbag_join.
Definition bag1.h:1267
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @bag.
Definition bag1.h:121
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:837
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:75
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition bag1.h:1667
const core::identifier_string & constructor_name()
Generate identifier @bag.
Definition bag1.h:65
bool is_bag_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @bagcomp.
Definition bag1.h:278
bool is_set2bag_application(const atermpp::aterm &e)
Recogniser for application of Set2Bag.
Definition bag1.h:809
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:358
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:861
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition bag1.h:1655
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:206
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:1205
void make_set2bag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Set2Bag.
Definition bag1.h:799
const core::identifier_string & union_name()
Generate identifier +.
Definition bag1.h:414
bool is_fbag_intersect_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_inter.
Definition bag1.h:1345
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:422
implementation_map bag_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for bag.
Definition bag1.h:1608
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition bag1.h:592
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:268
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bag1.h:1643
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:1443
const core::identifier_string & count_name()
Generate identifier count.
Definition bag1.h:286
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:481
function_symbol nat2bool_function(const sort_expression &s)
Constructor for function symbol @Nat2Bool_.
Definition bag1.h:1143
bool is_one_function_application(const atermpp::aterm &e)
Recogniser for application of @one_.
Definition bag1.h:933
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:1430
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:976
const core::identifier_string & difference_name()
Generate identifier -.
Definition bag1.h:600
application set2bag(const sort_expression &s, const data_expression &arg0)
Application of function symbol Set2Bag.
Definition bag1.h:789
bool is_bool2nat_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Bool2Nat_.
Definition bag1.h:1215
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag1.h:52
application monus_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus_.
Definition bag1.h:1104
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:41
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition bag1.h:648
bool is_fbag2fset_application(const atermpp::aterm &e)
Recogniser for application of @fbag2fset.
Definition bag1.h:1517
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition bag1.h:571
const core::identifier_string & in_name()
Generate identifier in.
Definition bag1.h:350
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @bag.
Definition bag1.h:85
const core::identifier_string & bag_comprehension_name()
Generate identifier @bagcomp.
Definition bag1.h:224
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition bag1.h:342
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:675
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:1294
const core::identifier_string & one_function_name()
Generate identifier @one_.
Definition bag1.h:879
bool is_add_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @add_.
Definition bag1.h:961
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:111
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:827
bool is_one_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_.
Definition bag1.h:899
application bag_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagcomp.
Definition bag1.h:258
function_symbol one_function(const sort_expression &s)
Constructor for function symbol @one_.
Definition bag1.h:889
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition bag1.h:321
application min_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @min_.
Definition bag1.h:1040
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag1.h:129
bool is_fbag_join_application(const atermpp::aterm &e)
Recogniser for application of @fbag_join.
Definition bag1.h:1317
bool is_monus_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus_.
Definition bag1.h:1089
Namespace for system defined sort bool_.
Definition bool.h:29
data_equation_vector bool_generate_equations_code()
Give all system defined equations for bool_.
Definition bool.h:499
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:116
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bool.h:466
function_symbol_vector bool_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for bool_.
Definition bool.h:439
function_symbol_vector bool_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for bool_.
Definition bool.h:138
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:342
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:51
const core::identifier_string & implies_name()
Generate identifier =>.
Definition bool.h:350
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:41
const core::identifier_string & or_name()
Generate identifier ||.
Definition bool.h:286
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:151
const function_symbol & implies()
Constructor for function symbol =>.
Definition bool.h:360
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:490
bool is_not_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition bool.h:180
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:406
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:194
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:232
application and_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol &&.
Definition bool.h:257
function_symbol_vector bool_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for bool_.
Definition bool.h:426
const core::identifier_string & not_name()
Generate identifier !.
Definition bool.h:160
application implies(const data_expression &arg0, const data_expression &arg1)
Application of function symbol =>.
Definition bool.h:385
function_symbol_vector bool_generate_constructors_code()
Give all system defined constructors for bool_.
Definition bool.h:127
implementation_map bool_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for bool_.
Definition bool.h:455
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:321
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:106
const core::identifier_string & bool_name()
Definition bool.h:32
bool is_and_function_symbol(const atermpp::aterm &e)
Recogniser for function &&.
Definition bool.h:242
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:278
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:296
bool is_or_function_symbol(const atermpp::aterm &e)
Recogniser for function ||.
Definition bool.h:306
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:84
const core::identifier_string & false_name()
Generate identifier false.
Definition bool.h:96
const core::identifier_string & true_name()
Generate identifier true.
Definition bool.h:64
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:214
function_symbol_vector bool_generate_functions_code()
Give all system defined mappings for bool_.
Definition bool.h:413
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:170
void make_not_(data_expression &result, const data_expression &arg0)
Make an application of function symbol !.
Definition bool.h:204
void make_and_(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol &&.
Definition bool.h:268
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:74
bool is_implies_function_symbol(const atermpp::aterm &e)
Recogniser for function =>.
Definition bool.h:370
void make_or_(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol ||.
Definition bool.h:332
void make_implies(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol =>.
Definition bool.h:396
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:478
const core::identifier_string & and_name()
Generate identifier &&.
Definition bool.h:222
Namespace for system defined sort fbag.
Definition fbag1.h:34
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {:}.
Definition fbag1.h:84
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:375
const core::identifier_string & count_all_name()
Generate identifier #.
Definition fbag1.h:711
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:855
implementation_map fbag_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition fbag1.h:188
const core::identifier_string & fset2fbag_name()
Generate identifier @fset2fbag.
Definition fbag1.h:457
application fset2fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @fset2fbag.
Definition fbag1.h:491
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:40
application pick(const sort_expression &s, const data_expression &arg0)
Application of function symbol pick.
Definition fbag1.h:807
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition fbag1.h:554
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition fbag1.h:413
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition fbag1.h:667
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition fbag1.h:618
function_symbol pick(const sort_expression &s)
Constructor for function symbol pick.
Definition fbag1.h:783
const core::identifier_string & count_name()
Generate identifier count.
Definition fbag1.h:329
const core::identifier_string & cinsert_name()
Generate identifier @fbag_cinsert.
Definition fbag1.h:263
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fbag1.h:575
function_symbol intersection(const sort_expression &s)
Constructor for function symbol *.
Definition fbag1.h:593
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fbag1.h:927
function_symbol union_(const sort_expression &s)
Constructor for function symbol +.
Definition fbag1.h:529
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fbag1.h:963
bool is_cinsert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_cinsert.
Definition fbag1.h:283
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fbag_cons.
Definition fbag1.h:207
bool is_insert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_insert.
Definition fbag1.h:116
implementation_map fbag_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for fbag.
Definition fbag1.h:892
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fbag1.h:639
function_symbol count_all(const sort_expression &s)
Constructor for function symbol #.
Definition fbag1.h:721
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:629
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_cons.
Definition fbag1.h:217
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition fbag1.h:428
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fbag_insert.
Definition fbag1.h:106
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:132
void make_fset2fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @fset2fbag.
Definition fbag1.h:501
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:245
const core::identifier_string & cons_name()
Generate identifier @fbag_cons.
Definition fbag1.h:197
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:299
bool is_fset2fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset2fbag.
Definition fbag1.h:477
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fbag1.h:449
const core::identifier_string & empty_name()
Generate identifier {:}.
Definition fbag1.h:64
const core::identifier_string & difference_name()
Generate identifier -.
Definition fbag1.h:647
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fbag1.h:703
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition fbag1.h:385
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cons.
Definition fbag1.h:255
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:439
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fbag1.h:939
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fbag1.h:915
void make_count_all(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition fbag1.h:755
bool is_pick_function_symbol(const atermpp::aterm &e)
Recogniser for function pick.
Definition fbag1.h:793
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition fbag1.h:349
application count_all(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition fbag1.h:745
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition fbag1.h:603
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:233
const core::identifier_string & intersection_name()
Generate identifier *.
Definition fbag1.h:583
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fbag1.h:951
bool is_pick_application(const atermpp::aterm &e)
Recogniser for application of pick.
Definition fbag1.h:827
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition fbag1.h:403
function_symbol_vector fbag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fbag.
Definition fbag1.h:162
bool is_count_all_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fbag1.h:765
function_symbol count(const sort_expression &s)
Constructor for function symbol count.
Definition fbag1.h:339
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:565
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
Definition fbag1.h:51
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:311
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition fbag1.h:682
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:74
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:693
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:273
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_cinsert.
Definition fbag1.h:321
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:144
bool is_fset2fbag_application(const atermpp::aterm &e)
Recogniser for application of @fset2fbag.
Definition fbag1.h:511
bool is_count_all_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition fbag1.h:731
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:869
function_symbol fset2fbag(const sort_expression &s)
Constructor for function symbol @fset2fbag.
Definition fbag1.h:467
const core::identifier_string & pick_name()
Generate identifier pick.
Definition fbag1.h:773
const core::identifier_string & union_name()
Generate identifier +.
Definition fbag1.h:519
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition fbag1.h:364
function_symbol difference(const sort_expression &s)
Constructor for function symbol -.
Definition fbag1.h:657
function_symbol_vector fbag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fbag.
Definition fbag1.h:835
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fbag_insert.
Definition fbag1.h:154
const core::identifier_string & insert_name()
Generate identifier @fbag_insert.
Definition fbag1.h:96
data_equation_vector fbag_generate_equations_code(const sort_expression &s)
Give all system defined equations for fbag.
Definition fbag1.h:973
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition fbag1.h:539
void make_pick(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol pick.
Definition fbag1.h:817
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fbag1.h:903
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:174
const core::identifier_string & in_name()
Generate identifier in.
Definition fbag1.h:393
Namespace for system defined sort fset.
Definition fset1.h:32
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:104
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
Definition fset1.h:49
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:735
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:497
void make_pick(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol pick.
Definition fset1.h:685
const core::identifier_string & pick_name()
Generate identifier pick.
Definition fset1.h:641
application count(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition fset1.h:613
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function {}.
Definition fset1.h:82
application insert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fset_insert.
Definition fset1.h:129
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition fset1.h:379
bool is_cinsert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_cinsert.
Definition fset1.h:277
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition fset1.h:599
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:721
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fset_cinsert.
Definition fset1.h:267
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:170
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_cons.
Definition fset1.h:213
function_symbol_vector fset_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for fset.
Definition fset1.h:158
const core::identifier_string & empty_name()
Generate identifier {}.
Definition fset1.h:62
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:515
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition fset1.h:358
bool is_insert_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_insert.
Definition fset1.h:114
function_symbol_vector fset_generate_functions_code(const sort_expression &s)
Give all system defined mappings for fset.
Definition fset1.h:703
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fset_cons.
Definition fset1.h:228
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition fset1.h:407
function_symbol cons_(const sort_expression &s)
Constructor for function symbol @fset_cons.
Definition fset1.h:203
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:561
implementation_map fset_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for fset.
Definition fset1.h:756
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:72
const core::identifier_string & difference_name()
Generate identifier -.
Definition fset1.h:387
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition fset1.h:471
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:433
function_symbol intersection(const sort_expression &s)
Constructor for function symbol *.
Definition fset1.h:525
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:305
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition fset1.h:779
function_symbol difference(const sort_expression &s)
Constructor for function symbol -.
Definition fset1.h:397
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:140
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition fset1.h:535
const core::identifier_string & cinsert_name()
Generate identifier @fset_cinsert.
Definition fset1.h:257
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition fset1.h:343
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition fset1.h:623
bool is_pick_application(const atermpp::aterm &e)
Recogniser for application of pick.
Definition fset1.h:695
implementation_map fset_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition fset1.h:184
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition fset1.h:767
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition fset1.h:333
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition fset1.h:443
const core::identifier_string & count_name()
Generate identifier #.
Definition fset1.h:579
bool is_pick_function_symbol(const atermpp::aterm &e)
Recogniser for function pick.
Definition fset1.h:661
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition fset1.h:803
data_equation_vector fset_generate_equations_code(const sort_expression &s)
Give all system defined equations for fset.
Definition fset1.h:837
const core::identifier_string & union_name()
Generate identifier +.
Definition fset1.h:451
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition fset1.h:791
function_symbol pick(const sort_expression &s)
Constructor for function symbol pick.
Definition fset1.h:651
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:369
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition fset1.h:815
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition fset1.h:633
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition fset1.h:589
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of @fset_cons.
Definition fset1.h:249
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:293
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition fset1.h:571
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition fset1.h:422
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:94
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:239
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:38
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition fset1.h:486
const core::identifier_string & cons_name()
Generate identifier @fset_cons.
Definition fset1.h:193
application pick(const sort_expression &s, const data_expression &arg0)
Application of function symbol pick.
Definition fset1.h:675
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition fset1.h:827
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition fset1.h:550
function_symbol union_(const sort_expression &s)
Constructor for function symbol +.
Definition fset1.h:461
const core::identifier_string & in_name()
Generate identifier in.
Definition fset1.h:323
bool is_cinsert_application(const atermpp::aterm &e)
Recogniser for application of @fset_cinsert.
Definition fset1.h:315
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition fset1.h:507
bool is_insert_application(const atermpp::aterm &e)
Recogniser for application of @fset_insert.
Definition fset1.h:150
Namespace for system defined sort int_.
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition int1.h:649
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition int1.h:1513
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition int1.h:639
const core::identifier_string & cint_name()
Generate identifier @cInt.
Definition int1.h:67
application cint(const data_expression &arg0)
Application of function symbol @cInt.
Definition int1.h:101
application abs(const data_expression &arg0)
Application of function symbol abs.
Definition int1.h:691
application nat2int(const data_expression &arg0)
Application of function symbol Nat2Int.
Definition int1.h:257
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition int1.h:832
application cneg(const data_expression &arg0)
Application of function symbol @cNeg.
Definition int1.h:163
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:1047
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition int1.h:568
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition int1.h:817
const core::identifier_string & abs_name()
Generate identifier abs.
Definition int1.h:657
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition int1.h:612
bool is_int2pos_application(const atermpp::aterm &e)
Recogniser for application of Int2Pos.
Definition int1.h:463
const core::identifier_string & pred_name()
Generate identifier pred.
Definition int1.h:860
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition int1.h:1350
bool is_int2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Pos.
Definition int1.h:429
const function_symbol & pos2int()
Constructor for function symbol Pos2Int.
Definition int1.h:357
const core::identifier_string & nat2int_name()
Generate identifier Nat2Int.
Definition int1.h:223
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition int1.h:1489
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition int1.h:1074
application negate(const data_expression &arg0)
Application of function symbol -.
Definition int1.h:753
bool is_cneg_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNeg.
Definition int1.h:149
const core::identifier_string & int2pos_name()
Generate identifier Int2Pos.
Definition int1.h:409
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:479
void make_cneg(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNeg.
Definition int1.h:173
application int2nat(const data_expression &arg0)
Application of function symbol Int2Nat.
Definition int1.h:319
function_symbol pred(const sort_expression &s0)
Definition int1.h:868
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition int1.h:999
const core::identifier_string & cneg_name()
Generate identifier @cNeg.
Definition int1.h:129
const core::identifier_string & exp_name()
Generate identifier exp.
Definition int1.h:1314
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition int1.h:1377
const core::identifier_string & minimum_name()
Generate identifier min.
Definition int1.h:576
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition int1.h:1306
const core::identifier_string & int_name()
Definition int1.h:35
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition int1.h:1269
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition int1.h:547
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition int1.h:1144
function_symbol_vector int_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for int_.
Definition int1.h:1441
const core::identifier_string & pos2int_name()
Generate identifier Pos2Int.
Definition int1.h:347
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:295
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:54
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1036
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition int1.h:931
const function_symbol & nat2int()
Constructor for function symbol Nat2Int.
Definition int1.h:233
application div(const data_expression &arg0, const data_expression &arg1)
Application of function symbol div.
Definition int1.h:1221
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition int1.h:1165
const core::identifier_string & maximum_name()
Generate identifier max.
Definition int1.h:471
bool is_int2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Nat.
Definition int1.h:305
bool is_cneg_application(const atermpp::aterm &e)
Recogniser for application of @cNeg.
Definition int1.h:183
const core::identifier_string & succ_name()
Generate identifier succ.
Definition int1.h:781
const function_symbol & cneg()
Constructor for function symbol @cNeg.
Definition int1.h:139
void make_pos2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Int.
Definition int1.h:391
const function_symbol & abs()
Constructor for function symbol abs.
Definition int1.h:667
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1322
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:121
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition int1.h:1128
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition int1.h:1020
const core::identifier_string & mod_name()
Generate identifier mod.
Definition int1.h:1250
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition int1.h:1010
data_equation_vector int_generate_equations_code()
Give all system defined equations for int_.
Definition int1.h:1522
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition int1.h:1063
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:947
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition int1.h:628
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:419
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:939
function_symbol_vector int_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for int_.
Definition int1.h:1428
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition int1.h:1232
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:773
function_symbol negate(const sort_expression &s0)
Definition int1.h:727
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition int1.h:1242
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition int1.h:1296
bool is_pos2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Int.
Definition int1.h:367
function_symbol_vector int_generate_constructors_code()
Give all system defined constructors for int_.
Definition int1.h:190
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition int1.h:711
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition int1.h:558
function_symbol_vector int_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for int_.
Definition int1.h:201
application int2pos(const data_expression &arg0)
Application of function symbol Int2Pos.
Definition int1.h:443
function_symbol succ(const sort_expression &s0)
Definition int1.h:789
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition int1.h:763
const core::identifier_string & negate_name()
Generate identifier -.
Definition int1.h:719
bool is_cint_function_symbol(const atermpp::aterm &e)
Recogniser for function @cInt.
Definition int1.h:87
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:701
function_symbol_vector int_generate_functions_code()
Give all system defined mappings for int_.
Definition int1.h:1394
data_expression int_(const std::string &n)
Constructs expression of type Int from a string.
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:214
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition int1.h:1387
application mod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol mod.
Definition int1.h:1285
void make_nat2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Int.
Definition int1.h:267
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:77
implementation_map int_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for int_.
Definition int1.h:1478
application pos2int(const data_expression &arg0)
Application of function symbol Pos2Int.
Definition int1.h:381
bool is_nat2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Int.
Definition int1.h:243
bool is_int2nat_application(const atermpp::aterm &e)
Recogniser for application of Int2Nat.
Definition int1.h:339
const core::identifier_string & minus_name()
Generate identifier -.
Definition int1.h:1028
data_expression int_(T t)
Constructs expression of type pos from an integral type.
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1258
const core::identifier_string & int2nat_name()
Generate identifier Int2Nat.
Definition int1.h:285
const core::identifier_string & div_name()
Generate identifier div.
Definition int1.h:1173
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition int1.h:531
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition int1.h:1366
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition int1.h:1205
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition int1.h:911
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition int1.h:738
void make_int2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Pos.
Definition int1.h:453
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1100
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition int1.h:983
bool is_nat2int_application(const atermpp::aterm &e)
Recogniser for application of Nat2Int.
Definition int1.h:277
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition int1.h:1084
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition int1.h:1155
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:584
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition int1.h:896
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1181
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition int1.h:842
bool is_pos2int_application(const atermpp::aterm &e)
Recogniser for application of Pos2Int.
Definition int1.h:401
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition int1.h:921
void make_cint(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cInt.
Definition int1.h:111
void make_int2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Nat.
Definition int1.h:329
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition int1.h:677
const core::identifier_string & times_name()
Generate identifier *.
Definition int1.h:1092
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition int1.h:1501
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:852
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:44
Namespace for system defined sort list.
Definition list1.h:33
const core::identifier_string & rtail_name()
Generate identifier rtail.
Definition list1.h:698
const core::identifier_string & snoc_name()
Generate identifier <|.
Definition list1.h:320
bool is_rhead_function_symbol(const atermpp::aterm &e)
Recogniser for function rhead.
Definition list1.h:656
bool is_rhead_application(const atermpp::aterm &e)
Recogniser for application of rhead.
Definition list1.h:690
bool is_snoc_function_symbol(const atermpp::aterm &e)
Recogniser for function <|.
Definition list1.h:340
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function #.
Definition list1.h:278
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:171
const core::identifier_string & tail_name()
Generate identifier tail.
Definition list1.h:574
application head(const sort_expression &s, const data_expression &arg0)
Application of function symbol head.
Definition list1.h:546
bool is_tail_application(const atermpp::aterm &e)
Recogniser for application of tail.
Definition list1.h:628
bool is_element_at_function_symbol(const atermpp::aterm &e)
Recogniser for function ..
Definition list1.h:468
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:366
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:214
const core::identifier_string & rhead_name()
Generate identifier rhead.
Definition list1.h:636
function_symbol_vector list_generate_functions_code(const sort_expression &s)
Give all system defined mappings for list.
Definition list1.h:760
const core::identifier_string & in_name()
Generate identifier in.
Definition list1.h:194
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition list1.h:204
bool is_rtail_function_symbol(const atermpp::aterm &e)
Recogniser for function rtail.
Definition list1.h:718
bool is_concat_application(const atermpp::aterm &e)
Recogniser for application of ++.
Definition list1.h:440
const core::identifier_string & head_name()
Generate identifier head.
Definition list1.h:512
application concat(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol ++.
Definition list1.h:419
const core::identifier_string & cons_name()
Generate identifier |>.
Definition list1.h:95
const core::identifier_string & concat_name()
Generate identifier ++.
Definition list1.h:384
function_symbol rtail(const sort_expression &s)
Constructor for function symbol rtail.
Definition list1.h:708
const core::identifier_string & count_name()
Generate identifier #.
Definition list1.h:258
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:141
data_equation_vector list_generate_equations_code(const sort_expression &s)
Give all system defined equations for list.
Definition list1.h:860
void make_rhead(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rhead.
Definition list1.h:680
bool is_tail_function_symbol(const atermpp::aterm &e)
Recogniser for function tail.
Definition list1.h:594
application rhead(const sort_expression &s, const data_expression &arg0)
Application of function symbol rhead.
Definition list1.h:670
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:793
implementation_map list_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition list1.h:185
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition list1.h:250
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:779
application rtail(const sort_expression &s, const data_expression &arg0)
Application of function symbol rtail.
Definition list1.h:732
bool is_rtail_application(const atermpp::aterm &e)
Recogniser for application of rtail.
Definition list1.h:752
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
Definition list1.h:73
application tail(const sort_expression &s, const data_expression &arg0)
Application of function symbol tail.
Definition list1.h:608
function_symbol element_at(const sort_expression &s)
Constructor for function symbol ..
Definition list1.h:458
const core::identifier_string & empty_name()
Generate identifier [].
Definition list1.h:63
function_symbol_vector list_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for list.
Definition list1.h:159
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:430
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol |>.
Definition list1.h:130
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:240
const core::identifier_string & element_at_name()
Generate identifier ..
Definition list1.h:448
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:522
bool is_cons_application(const atermpp::aterm &e)
Recogniser for application of |>.
Definition list1.h:151
bool is_snoc_application(const atermpp::aterm &e)
Recogniser for application of <|.
Definition list1.h:376
function_symbol list_enumeration(const sort_expression &s)
Constructor for function symbol list_enumeration.
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list1.h:39
function_symbol snoc(const sort_expression &s)
Constructor for function symbol <|.
Definition list1.h:330
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition list1.h:268
bool is_element_at_application(const atermpp::aterm &e)
Recogniser for application of ..
Definition list1.h:504
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:826
implementation_map list_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for list.
Definition list1.h:815
void make_head(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol head.
Definition list1.h:556
function_symbol rhead(const sort_expression &s)
Constructor for function symbol rhead.
Definition list1.h:646
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:494
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of #.
Definition list1.h:312
void make_rtail(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol rtail.
Definition list1.h:742
bool is_head_application(const atermpp::aterm &e)
Recogniser for application of head.
Definition list1.h:566
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol #.
Definition list1.h:302
function_symbol tail(const sort_expression &s)
Constructor for function symbol tail.
Definition list1.h:584
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:618
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
Definition list1.h:105
bool is_cons_function_symbol(const atermpp::aterm &e)
Recogniser for function |>.
Definition list1.h:115
bool is_concat_function_symbol(const atermpp::aterm &e)
Recogniser for function ++.
Definition list1.h:404
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition list1.h:850
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition list1.h:838
bool is_head_function_symbol(const atermpp::aterm &e)
Recogniser for function head.
Definition list1.h:532
bool is_empty_function_symbol(const atermpp::aterm &e)
Recogniser for function [].
Definition list1.h:83
function_symbol concat(const sort_expression &s)
Constructor for function symbol ++.
Definition list1.h:394
bool is_list(const sort_expression &e)
Recogniser for sort expression List(s)
Definition list1.h:50
application count(const sort_expression &s, const data_expression &arg0)
Application of function symbol #.
Definition list1.h:292
application element_at(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol ..
Definition list1.h:483
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition list1.h:229
application snoc(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol <|.
Definition list1.h:355
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:573
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition nat1.h:2254
application cpair(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cPair.
Definition nat1.h:224
bool is_cpair_application(const atermpp::aterm &e)
Recogniser for application of @cPair.
Definition nat1.h:245
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition nat1.h:890
const function_symbol & generalised_divmod()
Constructor for function symbol @gdivmod.
Definition nat1.h:1976
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:419
const core::identifier_string & sqrt_nat_aux_func_name()
Generate identifier @sqrt_nat.
Definition nat1.h:1712
bool is_pos2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Nat.
Definition nat1.h:307
function_symbol succ(const sort_expression &s0)
Definition nat1.h:581
const function_symbol & monus()
Constructor for function symbol @monus.
Definition nat1.h:1328
void make_sqrt(data_expression &result, const data_expression &arg0)
Make an application of function symbol sqrt.
Definition nat1.h:1694
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:2014
bool is_gte_subtract_with_borrow_function_symbol(const atermpp::aterm &e)
Recogniser for function @gtesubtb.
Definition nat1.h:928
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:105
bool is_swap_zero_add_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_add.
Definition nat1.h:1506
void make_dub(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @dub.
Definition nat1.h:743
void make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol div.
Definition nat1.h:1097
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:1748
const core::identifier_string & maximum_name()
Generate identifier max.
Definition nat1.h:411
void make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol mod.
Definition nat1.h:1161
application generalised_divmod(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @gdivmod.
Definition nat1.h:2002
bool is_swap_zero_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero.
Definition nat1.h:1402
bool is_cnat_application(const atermpp::aterm &e)
Recogniser for application of @cNat.
Definition nat1.h:181
const core::identifier_string & mod_name()
Generate identifier mod.
Definition nat1.h:1115
const function_symbol & gte_subtract_with_borrow()
Constructor for function symbol @gtesubtb.
Definition nat1.h:918
bool is_generalised_divmod_application(const atermpp::aterm &e)
Recogniser for application of @gdivmod.
Definition nat1.h:2024
bool is_div_application(const atermpp::aterm &e)
Recogniser for application of div.
Definition nat1.h:1107
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:2080
const core::identifier_string & swap_zero_min_name()
Generate identifier @swap_zero_min.
Definition nat1.h:1514
const function_symbol & divmod()
Constructor for function symbol @divmod.
Definition nat1.h:1912
bool is_pos2nat_application(const atermpp::aterm &e)
Recogniser for application of Pos2Nat.
Definition nat1.h:341
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:137
application dubsucc(const data_expression &arg0)
Application of function symbol @dubsucc.
Definition nat1.h:795
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition nat1.h:679
bool is_nat2pos_application(const atermpp::aterm &e)
Recogniser for application of Nat2Pos.
Definition nat1.h:403
bool is_mod_function_symbol(const atermpp::aterm &e)
Recogniser for function mod.
Definition nat1.h:1135
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:1187
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition nat1.h:544
const core::identifier_string & times_name()
Generate identifier *.
Definition nat1.h:974
const function_symbol & dubsucc()
Constructor for function symbol @dubsucc.
Definition nat1.h:771
const function_symbol & swap_zero_add()
Constructor for function symbol @swap_zero_add.
Definition nat1.h:1456
function_symbol_vector nat_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for nat.
Definition nat1.h:2151
data_equation_vector nat_generate_equations_code()
Give all system defined equations for nat.
Definition nat1.h:2287
const function_symbol & cpair()
Constructor for function symbol @cPair.
Definition nat1.h:199
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:43
const core::identifier_string & nat_name()
Definition nat1.h:34
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition nat1.h:1227
const core::identifier_string & exp_name()
Generate identifier exp.
Definition nat1.h:1179
const function_symbol & swap_zero()
Constructor for function symbol @swap_zero.
Definition nat1.h:1392
application swap_zero(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @swap_zero.
Definition nat1.h:1417
bool is_first_function_symbol(const atermpp::aterm &e)
Recogniser for function @first.
Definition nat1.h:1798
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition nat1.h:488
void make_cpair(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cPair.
Definition nat1.h:235
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:278
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:53
bool is_doubly_generalised_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @ggdivmod.
Definition nat1.h:2052
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition nat1.h:863
function_symbol_vector nat_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for nat.
Definition nat1.h:2138
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:1684
application pos2nat(const data_expression &arg0)
Application of function symbol Pos2Nat.
Definition nat1.h:321
void make_nat2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Pos.
Definition nat1.h:393
application first(const data_expression &arg0)
Application of function symbol @first.
Definition nat1.h:1812
const core::identifier_string & plus_name()
Generate identifier +.
Definition nat1.h:823
const core::identifier_string & natpair_name()
Definition nat1.h:63
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition nat1.h:2242
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition nat1.h:592
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition nat1.h:478
const core::identifier_string & div_name()
Generate identifier div.
Definition nat1.h:1051
const function_symbol & mod()
Constructor for function symbol mod.
Definition nat1.h:1125
void make_monus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus.
Definition nat1.h:1364
const function_symbol & sqrt()
Constructor for function symbol sqrt.
Definition nat1.h:1660
void make_dubsucc(data_expression &result, const data_expression &arg0)
Make an application of function symbol @dubsucc.
Definition nat1.h:805
application even(const data_expression &arg0)
Application of function symbol @even.
Definition nat1.h:1290
const function_symbol & doubly_generalised_divmod()
Constructor for function symbol @ggdivmod.
Definition nat1.h:2042
const function_symbol & pred()
Constructor for function symbol pred.
Definition nat1.h:645
void make_even(data_expression &result, const data_expression &arg0)
Make an application of function symbol @even.
Definition nat1.h:1300
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:956
bool is_sqrt_nat_aux_func_function_symbol(const atermpp::aterm &e)
Recogniser for function @sqrt_nat.
Definition nat1.h:1732
const function_symbol & even()
Constructor for function symbol @even.
Definition nat1.h:1266
const core::identifier_string & first_name()
Generate identifier @first.
Definition nat1.h:1778
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:1632
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition nat1.h:627
bool is_dub_function_symbol(const atermpp::aterm &e)
Recogniser for function @dub.
Definition nat1.h:717
application cnat(const data_expression &arg0)
Application of function symbol @cNat.
Definition nat1.h:161
bool is_swap_zero_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero.
Definition nat1.h:1438
const core::identifier_string & even_name()
Generate identifier @even.
Definition nat1.h:1256
const core::identifier_string & swap_zero_name()
Generate identifier @swap_zero.
Definition nat1.h:1382
void make_pos2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Nat.
Definition nat1.h:331
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition nat1.h:565
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition nat1.h:1211
bool is_monus_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus.
Definition nat1.h:1338
bool is_mod_application(const atermpp::aterm &e)
Recogniser for application of mod.
Definition nat1.h:1171
bool is_even_function_symbol(const atermpp::aterm &e)
Recogniser for function @even.
Definition nat1.h:1276
const core::identifier_string & pred_name()
Generate identifier pred.
Definition nat1.h:635
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition nat1.h:1248
const function_symbol & swap_zero_min()
Constructor for function symbol @swap_zero_min.
Definition nat1.h:1524
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:504
const function_symbol & sqrt_nat_aux_func()
Constructor for function symbol @sqrt_nat.
Definition nat1.h:1722
bool is_last_application(const atermpp::aterm &e)
Recogniser for application of @last.
Definition nat1.h:1894
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition nat1.h:1238
const function_symbol & div()
Constructor for function symbol div.
Definition nat1.h:1061
application last(const data_expression &arg0)
Application of function symbol @last.
Definition nat1.h:1874
const core::identifier_string & doubly_generalised_divmod_name()
Generate identifier @ggdivmod.
Definition nat1.h:2032
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition nat1.h:617
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition nat1.h:451
bool is_gte_subtract_with_borrow_application(const atermpp::aterm &e)
Recogniser for application of @gtesubtb.
Definition nat1.h:966
bool is_swap_zero_min_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_min.
Definition nat1.h:1574
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:831
const core::identifier_string & dubsucc_name()
Generate identifier @dubsucc.
Definition nat1.h:761
bool is_first_application(const atermpp::aterm &e)
Recogniser for application of @first.
Definition nat1.h:1832
bool is_sqrt_application(const atermpp::aterm &e)
Recogniser for application of sqrt.
Definition nat1.h:1704
const function_symbol & first()
Constructor for function symbol @first.
Definition nat1.h:1788
void make_first(data_expression &result, const data_expression &arg0)
Make an application of function symbol @first.
Definition nat1.h:1822
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition nat1.h:655
bool is_generalised_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @gdivmod.
Definition nat1.h:1986
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:1483
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:1496
const core::identifier_string & swap_zero_monus_name()
Generate identifier @swap_zero_monus.
Definition nat1.h:1582
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:944
function_symbol_vector nat_generate_functions_code()
Give all system defined mappings for nat.
Definition nat1.h:2097
bool is_cpair_function_symbol(const atermpp::aterm &e)
Recogniser for function @cPair.
Definition nat1.h:209
application div(const data_expression &arg0, const data_expression &arg1)
Application of function symbol div.
Definition nat1.h:1086
bool is_divmod_function_symbol(const atermpp::aterm &e)
Recogniser for function @divmod.
Definition nat1.h:1922
const function_symbol & swap_zero_monus()
Constructor for function symbol @swap_zero_monus.
Definition nat1.h:1592
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition nat1.h:1033
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:1551
bool is_c0_function_symbol(const atermpp::aterm &e)
Recogniser for function @c0.
Definition nat1.h:115
const core::identifier_string & generalised_divmod_name()
Generate identifier @gdivmod.
Definition nat1.h:1966
application doubly_generalised_divmod(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @ggdivmod.
Definition nat1.h:2068
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:359
const core::identifier_string & monus_name()
Generate identifier @monus.
Definition nat1.h:1318
application monus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus.
Definition nat1.h:1353
const core::identifier_string & cpair_name()
Generate identifier @cPair.
Definition nat1.h:189
const core::identifier_string & nat2pos_name()
Generate identifier Nat2Pos.
Definition nat1.h:349
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition nat1.h:2266
void make_divmod(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @divmod.
Definition nat1.h:1948
application dub(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @dub.
Definition nat1.h:732
implementation_map nat_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for nat.
Definition nat1.h:2195
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition nat1.h:2230
const core::identifier_string & gte_subtract_with_borrow_name()
Generate identifier @gtesubtb.
Definition nat1.h:908
const basic_sort & natpair()
Constructor for sort expression @NatPair.
Definition nat1.h:72
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition nat1.h:669
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition nat1.h:607
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition nat1.h:2218
bool is_swap_zero_monus_application(const atermpp::aterm &e)
Recogniser for application of @swap_zero_monus.
Definition nat1.h:1642
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:1564
const core::identifier_string & dub_name()
Generate identifier @dub.
Definition nat1.h:697
const core::identifier_string & cnat_name()
Generate identifier @cNat.
Definition nat1.h:127
const core::identifier_string & c0_name()
Generate identifier @c0.
Definition nat1.h:95
application divmod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @divmod.
Definition nat1.h:1937
bool is_swap_zero_add_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_add.
Definition nat1.h:1466
bool is_natpair(const sort_expression &e)
Recogniser for sort expression @NatPair.
Definition nat1.h:82
bool is_swap_zero_monus_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_monus.
Definition nat1.h:1602
const core::identifier_string & pos2nat_name()
Generate identifier Pos2Nat.
Definition nat1.h:287
const core::identifier_string & last_name()
Generate identifier @last.
Definition nat1.h:1840
const core::identifier_string & minimum_name()
Generate identifier min.
Definition nat1.h:496
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:1760
bool is_sqrt_nat_aux_func_application(const atermpp::aterm &e)
Recogniser for application of @sqrt_nat.
Definition nat1.h:1770
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition nat1.h:2206
bool is_sqrt_function_symbol(const atermpp::aterm &e)
Recogniser for function sqrt.
Definition nat1.h:1670
application mod(const data_expression &arg0, const data_expression &arg1)
Application of function symbol mod.
Definition nat1.h:1150
bool is_cnat_function_symbol(const atermpp::aterm &e)
Recogniser for function @cNat.
Definition nat1.h:147
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:264
const function_symbol & last()
Constructor for function symbol @last.
Definition nat1.h:1850
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition nat1.h:689
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition nat1.h:900
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition nat1.h:467
data_expression nat(T t)
Constructs expression of type pos from an integral type.
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:1428
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition nat1.h:555
const core::identifier_string & swap_zero_add_name()
Generate identifier @swap_zero_add.
Definition nat1.h:1446
bool is_dubsucc_function_symbol(const atermpp::aterm &e)
Recogniser for function @dubsucc.
Definition nat1.h:781
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition nat1.h:879
bool is_dubsucc_application(const atermpp::aterm &e)
Recogniser for application of @dubsucc.
Definition nat1.h:815
bool is_swap_zero_min_function_symbol(const atermpp::aterm &e)
Recogniser for function @swap_zero_min.
Definition nat1.h:1534
function_symbol_vector nat_generate_constructors_code()
Give all system defined constructors for nat.
Definition nat1.h:252
const core::identifier_string & sqrt_name()
Generate identifier sqrt.
Definition nat1.h:1650
bool is_doubly_generalised_divmod_application(const atermpp::aterm &e)
Recogniser for application of @ggdivmod.
Definition nat1.h:2090
bool is_last_function_symbol(const atermpp::aterm &e)
Recogniser for function @last.
Definition nat1.h:1860
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition nat1.h:1022
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition nat1.h:1043
bool is_div_function_symbol(const atermpp::aterm &e)
Recogniser for function div.
Definition nat1.h:1071
const core::identifier_string & divmod_name()
Generate identifier @divmod.
Definition nat1.h:1902
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition nat1.h:528
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition nat1.h:982
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition nat1.h:1006
data_expression nat(const std::string &n)
Constructs expression of type Nat from a string.
bool is_dub_application(const atermpp::aterm &e)
Recogniser for application of @dub.
Definition nat1.h:753
bool is_nat2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Pos.
Definition nat1.h:369
const function_symbol & dub()
Constructor for function symbol @dub.
Definition nat1.h:707
void make_cnat(data_expression &result, const data_expression &arg0)
Make an application of function symbol @cNat.
Definition nat1.h:171
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:1619
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:297
void make_last(data_expression &result, const data_expression &arg0)
Make an application of function symbol @last.
Definition nat1.h:1884
application nat2pos(const data_expression &arg0)
Application of function symbol Nat2Pos.
Definition nat1.h:383
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:1374
bool is_divmod_application(const atermpp::aterm &e)
Recogniser for application of @divmod.
Definition nat1.h:1958
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition nat1.h:2278
bool is_even_application(const atermpp::aterm &e)
Recogniser for application of @even.
Definition nat1.h:1310
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:683
bool is_pos_predecessor_function_symbol(const atermpp::aterm &e)
Recogniser for function @pospred.
Definition pos1.h:403
bool is_add_with_carry_function_symbol(const atermpp::aterm &e)
Recogniser for function @addc.
Definition pos1.h:529
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:292
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition pos1.h:785
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:557
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition pos1.h:621
data_expression pos(const T t)
Constructs expression of type Bool from an integral type Type T is an unsigned integral type.
bool is_cdub_function_symbol(const atermpp::aterm &e)
Recogniser for function @cDub.
Definition pos1.h:117
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition pos1.h:213
implementation_map pos_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for pos.
Definition pos1.h:750
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition pos1.h:355
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition pos1.h:239
const function_symbol & powerlog2_pos()
Constructor for function symbol @powerlog2.
Definition pos1.h:649
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:52
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition pos1.h:821
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:75
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition pos1.h:365
const function_symbol & add_with_carry()
Constructor for function symbol @addc.
Definition pos1.h:519
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition pos1.h:797
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition pos1.h:610
bool is_cdub_application(const atermpp::aterm &e)
Recogniser for application of @cDub.
Definition pos1.h:153
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition pos1.h:303
function_symbol_vector pos_generate_functions_code()
Give all system defined mappings for pos.
Definition pos1.h:700
const function_symbol & pos_predecessor()
Constructor for function symbol @pospred.
Definition pos1.h:393
data_expression pos(const std::string &n)
Constructs expression of type Pos from a string.
const core::identifier_string & cdub_name()
Generate identifier @cDub.
Definition pos1.h:97
const core::identifier_string & c1_name()
Generate identifier @c1.
Definition pos1.h:65
const function_symbol & plus()
Constructor for function symbol +.
Definition pos1.h:455
bool is_add_with_carry_application(const atermpp::aterm &e)
Recogniser for application of @addc.
Definition pos1.h:567
const function_symbol & maximum()
Constructor for function symbol max.
Definition pos1.h:203
const core::identifier_string & powerlog2_pos_name()
Generate identifier @powerlog2.
Definition pos1.h:639
bool is_powerlog2_pos_application(const atermpp::aterm &e)
Recogniser for application of @powerlog2.
Definition pos1.h:693
const core::identifier_string & times_name()
Generate identifier *.
Definition pos1.h:575
function_symbol_vector pos_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for pos.
Definition pos1.h:171
bool is_c1_function_symbol(const atermpp::aterm &e)
Recogniser for function @c1.
Definition pos1.h:85
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition pos1.h:809
const core::identifier_string & plus_name()
Generate identifier +.
Definition pos1.h:445
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition pos1.h:277
const function_symbol & cdub()
Constructor for function symbol @cDub.
Definition pos1.h:107
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition pos1.h:773
application add_with_carry(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @addc.
Definition pos1.h:545
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:184
application powerlog2_pos(const data_expression &arg0)
Application of function symbol @powerlog2.
Definition pos1.h:673
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition pos1.h:480
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition pos1.h:631
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition pos1.h:595
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition pos1.h:491
const core::identifier_string & add_with_carry_name()
Generate identifier @addc.
Definition pos1.h:509
const function_symbol & times()
Constructor for function symbol *.
Definition pos1.h:585
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition pos1.h:341
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition pos1.h:465
const core::identifier_string & minimum_name()
Generate identifier min.
Definition pos1.h:257
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition pos1.h:313
data_equation_vector pos_generate_equations_code()
Give all system defined equations for pos.
Definition pos1.h:830
application pos_predecessor(const data_expression &arg0)
Application of function symbol @pospred.
Definition pos1.h:417
bool is_powerlog2_pos_function_symbol(const atermpp::aterm &e)
Recogniser for function @powerlog2.
Definition pos1.h:659
application cdub(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cDub.
Definition pos1.h:132
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition pos1.h:375
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition pos1.h:228
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:42
const core::identifier_string & maximum_name()
Generate identifier max.
Definition pos1.h:193
const core::identifier_string & pos_name()
Definition pos1.h:33
const function_symbol & minimum()
Constructor for function symbol min.
Definition pos1.h:267
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:761
function_symbol_vector pos_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for pos.
Definition pos1.h:717
function_symbol_vector pos_generate_constructors_code()
Give all system defined constructors for pos.
Definition pos1.h:160
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition pos1.h:249
bool is_pos_predecessor_application(const atermpp::aterm &e)
Recogniser for application of @pospred.
Definition pos1.h:437
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition pos1.h:501
const function_symbol & succ()
Constructor for function symbol succ.
Definition pos1.h:331
void make_cdub(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cDub.
Definition pos1.h:143
const core::identifier_string & pos_predecessor_name()
Generate identifier @pospred.
Definition pos1.h:383
function_symbol_vector pos_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for pos.
Definition pos1.h:730
const core::identifier_string & succ_name()
Generate identifier succ.
Definition pos1.h:321
void make_pos_predecessor(data_expression &result, const data_expression &arg0)
Make an application of function symbol @pospred.
Definition pos1.h:427
Namespace for system defined sort real_.
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:647
void make_abs(data_expression &result, const data_expression &arg0)
Make an application of function symbol abs.
Definition real1.h:781
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1056
bool is_real2int_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Int.
Definition real1.h:488
data_expression real_(T numerator, T denominator)
Constructs expression of type Real from an integral type.
application exp(const data_expression &arg0, const data_expression &arg1)
Application of function symbol exp.
Definition real1.h:1367
void make_minus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition real1.h:1208
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:104
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:1692
const core::identifier_string & maximum_name()
Generate identifier max.
Definition real1.h:530
void make_negate(data_expression &result, const data_expression &arg0)
Make an application of function symbol -.
Definition real1.h:864
const core::identifier_string & minus_name()
Generate identifier -.
Definition real1.h:1141
bool is_succ_function_symbol(const atermpp::aterm &e)
Recogniser for function succ.
Definition real1.h:922
application reduce_fraction_helper(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @redfrachlp.
Definition real1.h:1811
const core::identifier_string & real_name()
Definition real1.h:36
const function_symbol & pos2real()
Constructor for function symbol Pos2Real.
Definition real1.h:168
const core::identifier_string & reduce_fraction_where_name()
Generate identifier @redfracwhr.
Definition real1.h:1710
const function_symbol & round()
Constructor for function symbol round.
Definition real1.h:1594
bool is_plus_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition real1.h:1096
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1234
application divides(const data_expression &arg0, const data_expression &arg1)
Application of function symbol /.
Definition real1.h:1431
bool is_abs_application(const atermpp::aterm &e)
Recogniser for application of abs.
Definition real1.h:791
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1404
const core::identifier_string & int2real_name()
Generate identifier Int2Real.
Definition real1.h:282
data_expression real_(T t)
Constructs expression of type Real from an integral type.
const function_symbol & real2nat()
Constructor for function symbol Real2Nat.
Definition real1.h:416
bool is_divides_function_symbol(const atermpp::aterm &e)
Recogniser for function /.
Definition real1.h:1415
const core::identifier_string & creal_name()
Generate identifier @cReal.
Definition real1.h:94
void make_succ(data_expression &result, const data_expression &arg0)
Make an application of function symbol succ.
Definition real1.h:947
bool is_exp_application(const atermpp::aterm &e)
Recogniser for application of exp.
Definition real1.h:1388
application real2nat(const data_expression &arg0)
Application of function symbol Real2Nat.
Definition real1.h:440
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition real1.h:1962
bool is_int2real_application(const atermpp::aterm &e)
Recogniser for application of Int2Real.
Definition real1.h:336
const function_symbol & ceil()
Constructor for function symbol ceil.
Definition real1.h:1532
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition real1.h:1986
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1133
bool is_divides_application(const atermpp::aterm &e)
Recogniser for application of /.
Definition real1.h:1452
bool is_reduce_fraction_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrac.
Definition real1.h:1666
bool is_maximum_function_symbol(const atermpp::aterm &e)
Recogniser for function max.
Definition real1.h:594
void make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol exp.
Definition real1.h:1378
const core::identifier_string & divides_name()
Generate identifier /.
Definition real1.h:1396
bool is_real2int_application(const atermpp::aterm &e)
Recogniser for application of Real2Int.
Definition real1.h:522
const core::identifier_string & ceil_name()
Generate identifier ceil.
Definition real1.h:1522
bool is_creal_function_symbol(const atermpp::aterm &e)
Recogniser for function @cReal.
Definition real1.h:114
void make_real2nat(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Nat.
Definition real1.h:450
bool is_minus_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:1181
application creal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @cReal.
Definition real1.h:129
bool is_reduce_fraction_where_application(const atermpp::aterm &e)
Recogniser for application of @redfracwhr.
Definition real1.h:1768
function_symbol succ(const sort_expression &s0)
Definition real1.h:890
application negate(const data_expression &arg0)
Application of function symbol -.
Definition real1.h:854
bool is_floor_function_symbol(const atermpp::aterm &e)
Recogniser for function floor.
Definition real1.h:1480
void make_int2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Int2Real.
Definition real1.h:326
void make_divides(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol /.
Definition real1.h:1442
const core::identifier_string & floor_name()
Generate identifier floor.
Definition real1.h:1460
const core::identifier_string & times_name()
Generate identifier *.
Definition real1.h:1226
bool is_abs_function_symbol(const atermpp::aterm &e)
Recogniser for function abs.
Definition real1.h:756
bool is_ceil_application(const atermpp::aterm &e)
Recogniser for application of ceil.
Definition real1.h:1576
application succ(const data_expression &arg0)
Application of function symbol succ.
Definition real1.h:937
const function_symbol & real2int()
Constructor for function symbol Real2Int.
Definition real1.h:478
bool is_maximum_application(const atermpp::aterm &e)
Recogniser for application of max.
Definition real1.h:631
application nat2real(const data_expression &arg0)
Application of function symbol Nat2Real.
Definition real1.h:254
const function_symbol & reduce_fraction()
Constructor for function symbol @redfrac.
Definition real1.h:1656
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:150
bool is_pred_application(const atermpp::aterm &e)
Recogniser for application of pred.
Definition real1.h:1040
const core::identifier_string & negate_name()
Generate identifier -.
Definition real1.h:799
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:1822
void make_pos2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Pos2Real.
Definition real1.h:202
function_symbol pred(const sort_expression &s0)
Definition real1.h:973
bool is_round_function_symbol(const atermpp::aterm &e)
Recogniser for function round.
Definition real1.h:1604
const core::identifier_string & succ_name()
Generate identifier succ.
Definition real1.h:882
const function_symbol & reduce_fraction_helper()
Constructor for function symbol @redfrachlp.
Definition real1.h:1786
const core::identifier_string & abs_name()
Generate identifier abs.
Definition real1.h:724
data_equation_vector real_generate_equations_code()
Give all system defined equations for real_.
Definition real1.h:2007
bool is_times_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition real1.h:1266
const core::identifier_string & round_name()
Generate identifier round.
Definition real1.h:1584
bool is_negate_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition real1.h:839
application int2real(const data_expression &arg0)
Application of function symbol Int2Real.
Definition real1.h:316
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1149
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:45
bool is_minimum_function_symbol(const atermpp::aterm &e)
Recogniser for function min.
Definition real1.h:679
const function_symbol & floor()
Constructor for function symbol floor.
Definition real1.h:1470
void make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol min.
Definition real1.h:706
void make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition real1.h:1293
const core::identifier_string & reduce_fraction_helper_name()
Generate identifier @redfrachlp.
Definition real1.h:1776
function_symbol_vector real_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for real_.
Definition real1.h:75
bool is_real2pos_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Pos.
Definition real1.h:364
void make_real2int(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Int.
Definition real1.h:512
function_symbol_vector real_generate_constructors_code()
Give all system defined constructors for real_.
Definition real1.h:67
void make_nat2real(data_expression &result, const data_expression &arg0)
Make an application of function symbol Nat2Real.
Definition real1.h:264
void make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol max.
Definition real1.h:621
bool is_floor_application(const atermpp::aterm &e)
Recogniser for application of floor.
Definition real1.h:1514
application reduce_fraction_where(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @redfracwhr.
Definition real1.h:1746
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:55
const function_symbol & reduce_fraction_where()
Constructor for function symbol @redfracwhr.
Definition real1.h:1720
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition real1.h:1112
implementation_map real_cpp_implementable_mappings()
Give all system defined mappings that are to be implemented in C++ code for real_.
Definition real1.h:1927
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1282
bool is_ceil_function_symbol(const atermpp::aterm &e)
Recogniser for function ceil.
Definition real1.h:1542
data_expression real_(const std::string &numerator, const std::string &denominator)
Constructs expression of type Real from two number strings.
application real2int(const data_expression &arg0)
Application of function symbol Real2Int.
Definition real1.h:502
const core::identifier_string & pred_name()
Generate identifier pred.
Definition real1.h:965
const function_symbol & nat2real()
Constructor for function symbol Nat2Real.
Definition real1.h:230
const core::identifier_string & minimum_name()
Generate identifier min.
Definition real1.h:639
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition real1.h:1950
bool is_succ_application(const atermpp::aterm &e)
Recogniser for application of succ.
Definition real1.h:957
application pos2real(const data_expression &arg0)
Application of function symbol Pos2Real.
Definition real1.h:192
void make_round(data_expression &result, const data_expression &arg0)
Make an application of function symbol round.
Definition real1.h:1628
bool is_pos2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Pos2Real.
Definition real1.h:178
function_symbol_vector real_mCRL2_usable_mappings()
Give all system defined mappings that can be used in mCRL2 specs for real_.
Definition real1.h:1888
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition real1.h:1974
const core::identifier_string & plus_name()
Generate identifier +.
Definition real1.h:1048
function_symbol abs(const sort_expression &s0)
Definition real1.h:732
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition real1.h:1938
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1303
void make_ceil(data_expression &result, const data_expression &arg0)
Make an application of function symbol ceil.
Definition real1.h:1566
const core::identifier_string & reduce_fraction_name()
Generate identifier @redfrac.
Definition real1.h:1646
function_symbol negate(const sort_expression &s0)
Definition real1.h:807
application minus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition real1.h:1197
application abs(const data_expression &arg0)
Application of function symbol abs.
Definition real1.h:771
bool is_real2pos_application(const atermpp::aterm &e)
Recogniser for application of Real2Pos.
Definition real1.h:398
bool is_reduce_fraction_application(const atermpp::aterm &e)
Recogniser for application of @redfrac.
Definition real1.h:1702
bool is_int2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Int2Real.
Definition real1.h:302
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:874
bool is_reduce_fraction_helper_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfrachlp.
Definition real1.h:1796
bool is_minimum_application(const atermpp::aterm &e)
Recogniser for application of min.
Definition real1.h:716
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1218
const core::identifier_string & pos2real_name()
Generate identifier Pos2Real.
Definition real1.h:158
bool is_round_application(const atermpp::aterm &e)
Recogniser for application of round.
Definition real1.h:1638
application reduce_fraction(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @redfrac.
Definition real1.h:1681
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition real1.h:1998
const core::identifier_string & exp_name()
Generate identifier exp.
Definition real1.h:1311
application maximum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol max.
Definition real1.h:610
bool is_real2nat_function_symbol(const atermpp::aterm &e)
Recogniser for function Real2Nat.
Definition real1.h:426
const core::identifier_string & real2nat_name()
Generate identifier Real2Nat.
Definition real1.h:406
const core::identifier_string & real2int_name()
Generate identifier Real2Int.
Definition real1.h:468
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:292
bool is_pred_function_symbol(const atermpp::aterm &e)
Recogniser for function pred.
Definition real1.h:1005
const core::identifier_string & nat2real_name()
Generate identifier Nat2Real.
Definition real1.h:220
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1319
application real2pos(const data_expression &arg0)
Application of function symbol Real2Pos.
Definition real1.h:378
void make_pred(data_expression &result, const data_expression &arg0)
Make an application of function symbol pred.
Definition real1.h:1030
bool is_real2nat_application(const atermpp::aterm &e)
Recogniser for application of Real2Nat.
Definition real1.h:460
bool is_pos2real_application(const atermpp::aterm &e)
Recogniser for application of Pos2Real.
Definition real1.h:212
application floor(const data_expression &arg0)
Application of function symbol floor.
Definition real1.h:1494
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition real1.h:695
void make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition real1.h:1123
bool is_reduce_fraction_helper_application(const atermpp::aterm &e)
Recogniser for application of @redfrachlp.
Definition real1.h:1832
void make_floor(data_expression &result, const data_expression &arg0)
Make an application of function symbol floor.
Definition real1.h:1504
const function_symbol & real2pos()
Constructor for function symbol Real2Pos.
Definition real1.h:354
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:85
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:538
function_symbol_vector real_generate_functions_code()
Give all system defined mappings for real_.
Definition real1.h:1839
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:1758
function_symbol_vector real_generate_constructors_and_functions_code()
Give all system defined mappings and constructors for real_.
Definition real1.h:1875
const core::identifier_string & real2pos_name()
Generate identifier Real2Pos.
Definition real1.h:344
data_expression real_(const std::string &n)
Constructs expression of type Real from a string.
void make_real2pos(data_expression &result, const data_expression &arg0)
Make an application of function symbol Real2Pos.
Definition real1.h:388
application round(const data_expression &arg0)
Application of function symbol round.
Definition real1.h:1618
bool is_exp_function_symbol(const atermpp::aterm &e)
Recogniser for function exp.
Definition real1.h:1351
application pred(const data_expression &arg0)
Application of function symbol pred.
Definition real1.h:1020
void make_creal(data_expression &result, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @cReal.
Definition real1.h:140
application ceil(const data_expression &arg0)
Application of function symbol ceil.
Definition real1.h:1556
bool is_reduce_fraction_where_function_symbol(const atermpp::aterm &e)
Recogniser for function @redfracwhr.
Definition real1.h:1730
bool is_nat2real_function_symbol(const atermpp::aterm &e)
Recogniser for function Nat2Real.
Definition real1.h:240
bool is_nat2real_application(const atermpp::aterm &e)
Recogniser for application of Nat2Real.
Definition real1.h:274
Namespace for system defined sort set_.
Definition set1.h:33
const core::identifier_string & fset_intersection_name()
Generate identifier @fset_inter.
Definition set1.h:1035
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:330
function_symbol true_function(const sort_expression &s)
Constructor for function symbol @true_.
Definition set1.h:725
const core::identifier_string & or_function_name()
Generate identifier @or_.
Definition set1.h:903
bool is_set_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @setcomp.
Definition set1.h:276
const core::identifier_string & constructor_name()
Generate identifier @set.
Definition set1.h:63
implementation_map set_cpp_implementable_mappings(const sort_expression &)
Give all system defined mappings that are to be implemented in C++ code for set_.
Definition set1.h:1174
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:1072
bool is_false_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @false_.
Definition set1.h:673
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition set1.h:608
bool is_not_function_application(const atermpp::aterm &e)
Recogniser for application of @not_.
Definition set1.h:831
bool is_and_function_application(const atermpp::aterm &e)
Recogniser for application of @and_.
Definition set1.h:895
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:949
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:1130
application or_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @or_.
Definition set1.h:938
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:1055
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set1.h:50
function_symbol or_function(const sort_expression &s)
Constructor for function symbol @or_.
Definition set1.h:913
void make_complement(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol !.
Definition set1.h:392
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition set1.h:479
core::identifier_string const & set_enumeration_name()
Generate identifier set_enumeration.
const core::identifier_string & false_function_name()
Generate identifier @false_.
Definition set1.h:653
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition set1.h:303
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition set1.h:1257
bool is_true_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @true_.
Definition set1.h:735
bool is_complement_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition set1.h:402
bool is_or_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @or_.
Definition set1.h:923
function_symbol fset_intersection(const sort_expression &s)
Constructor for function symbol @fset_inter.
Definition set1.h:1045
const core::identifier_string & set_comprehension_name()
Generate identifier @setcomp.
Definition set1.h:222
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:1017
bool is_fset_union_application(const atermpp::aterm &e)
Recogniser for application of @fset_union.
Definition set1.h:1027
bool is_false_function_application(const atermpp::aterm &e)
Recogniser for application of @false_.
Definition set1.h:707
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition set1.h:1185
bool is_not_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @not_.
Definition set1.h:797
function_symbol and_function(const sort_expression &s)
Constructor for function symbol @and_.
Definition set1.h:849
bool is_set_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @setcomp.
Definition set1.h:242
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition set1.h:340
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:777
application not_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @not_.
Definition set1.h:811
const core::identifier_string & in_name()
Generate identifier in.
Definition set1.h:284
function_symbol_vector set_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for set_.
Definition set1.h:127
bool is_fset_intersection_application(const atermpp::aterm &e)
Recogniser for application of @fset_inter.
Definition set1.h:1095
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:645
function_symbol not_function(const sort_expression &s)
Constructor for function symbol @not_.
Definition set1.h:787
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition set1.h:1209
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition set1.h:458
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @set.
Definition set1.h:119
const core::identifier_string & fset_union_name()
Generate identifier @fset_union.
Definition set1.h:967
bool is_set_fset_application(const atermpp::aterm &e)
Recogniser for application of @setfset.
Definition set1.h:214
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:554
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition set1.h:624
application complement(const sort_expression &s, const data_expression &arg0)
Application of function symbol !.
Definition set1.h:382
const core::identifier_string & complement_name()
Generate identifier !.
Definition set1.h:348
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:495
application set_fset(const sort_expression &s, const data_expression &arg0)
Application of function symbol @setfset.
Definition set1.h:194
const core::identifier_string & and_function_name()
Generate identifier @and_.
Definition set1.h:839
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition set1.h:543
bool is_fset_union_function_symbol(const atermpp::aterm &e)
Recogniser for function @fset_union.
Definition set1.h:987
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition set1.h:1233
function_symbol fset_union(const sort_expression &s)
Constructor for function symbol @fset_union.
Definition set1.h:977
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:885
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:39
bool is_set_fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @setfset.
Definition set1.h:180
application set_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @setcomp.
Definition set1.h:256
const core::identifier_string & intersection_name()
Generate identifier *.
Definition set1.h:487
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:1085
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:73
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition set1.h:1245
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition set1.h:1197
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:663
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:109
const core::identifier_string & set_fset_name()
Generate identifier @setfset.
Definition set1.h:160
const core::identifier_string & union_name()
Generate identifier +.
Definition set1.h:410
bool is_complement_function_symbol(const atermpp::aterm &e)
Recogniser for function !.
Definition set1.h:368
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:292
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:418
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @set.
Definition set1.h:83
function_symbol_vector set_generate_functions_code(const sort_expression &s)
Give all system defined mappings for set_.
Definition set1.h:1103
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:1004
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:138
const core::identifier_string & difference_name()
Generate identifier -.
Definition set1.h:572
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:266
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:749
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:821
bool is_or_function_application(const atermpp::aterm &e)
Recogniser for application of @or_.
Definition set1.h:959
const core::identifier_string & true_function_name()
Generate identifier @true_.
Definition set1.h:715
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:697
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:759
application false_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @false_.
Definition set1.h:687
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:580
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition set1.h:442
function_symbol complement(const sort_expression &s)
Constructor for function symbol !.
Definition set1.h:358
bool is_true_function_application(const atermpp::aterm &e)
Recogniser for application of @true_.
Definition set1.h:769
function_symbol set_fset(const sort_expression &s)
Constructor for function symbol @setfset.
Definition set1.h:170
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:635
implementation_map set_cpp_implementable_constructors(const sort_expression &)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition set1.h:151
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:469
function_symbol set_comprehension(const sort_expression &s)
Constructor for function symbol @setcomp.
Definition set1.h:232
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition set1.h:319
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition set1.h:564
data_equation_vector set_generate_equations_code(const sort_expression &s)
Give all system defined equations for set_.
Definition set1.h:1267
application and_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @and_.
Definition set1.h:874
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:1144
bool is_and_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @and_.
Definition set1.h:859
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:204
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition set1.h:527
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @set.
Definition set1.h:98
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition set1.h:1221
std::string pp(const data::structured_sort_constructor_argument &x, bool arg0)
Definition data.cpp:71
void make_set_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
std::set< data::variable > find_free_variables(const T &x)
Definition find.h:332
void swap(fset_container &t1, fset_container &t2) noexcept
\brief swap overload
void make_data_expression(data_expression &result)
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:82
constexpr std::size_t undefined_index()
Returns an index that corresponds to 'undefined'.
Definition undefined.h:27
void swap(assignment &t1, assignment &t2) noexcept
\brief swap overload
Definition assignment.h:171
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:339
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
Definition data.cpp:84
void swap(function_sort &t1, function_sort &t2) noexcept
\brief swap overload
bool is_greater_function_symbol(const DataExpression &e)
Recogniser for function >
Definition standard.h:319
int precedence(const application &x)
Definition print.h:305
void swap(container_sort &t1, container_sort &t2) noexcept
\brief swap overload
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.
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:282
void swap(untyped_identifier_assignment &t1, untyped_identifier_assignment &t2) noexcept
\brief swap overload
Definition assignment.h:267
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:83
constexpr int precedence(const forall &)
Definition print.h:396
std::string pp(const data::exists &x, bool arg0)
Definition data.cpp:53
std::ostream & operator<<(std::ostream &out, const untyped_sort_variable &x)
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:449
std::ostream & operator<<(std::ostream &out, const untyped_data_parameter &x)
std::string pp(const data::untyped_identifier_assignment &x, bool arg0)
Definition data.cpp:74
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.
data_equation_vector find_equations(const data_specification &specification, const data_expression &d)
Gets all equations with a data expression as head on one of its sides.
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:356
std::set< data::function_symbol > find_function_symbols(const T &x)
Definition find.h:407
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.
std::ostream & operator<<(std::ostream &out, const bag_comprehension_binder &x)
void swap(structured_sort_constructor &t1, structured_sort_constructor &t2) noexcept
\brief swap overload
variable_list free_variables(const data_expression &x)
Definition data.cpp:194
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:273
std::set< data::sort_expression > find_sort_expressions(const T &x)
Definition find.h:386
void make_bag_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
void swap(exists &t1, exists &t2) noexcept
\brief swap overload
Definition exists.h:82
std::ostream & operator<<(std::ostream &out, const set_comprehension_binder &x)
bool is_set_container(const atermpp::aterm &x)
constexpr int precedence(const bag_comprehension &)
Definition print.h:400
std::ostream & operator<<(std::ostream &out, const container_sort &x)
int precedence(const data_expression &x)
Definition print.h:402
void swap(untyped_sort &t1, untyped_sort &t2) noexcept
\brief swap overload
data_expression number(const sort_expression &s, const std::string &n)
Construct numeric expression from a string representing a number in decimal notation.
std::ostream & operator<<(std::ostream &out, const basic_sort &x)
Definition basic_sort.h:78
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
Definition standard.h:384
void swap(structured_sort_constructor_argument &t1, structured_sort_constructor_argument &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const machine_number &x)
void find_free_variables_with_bound(const T &x, OutputIterator o, const VariableContainer &bound)
Definition find.h:323
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:94
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
std::string pp(const data::list_container &x, bool arg0)
Definition data.cpp:63
void swap(untyped_identifier &t1, untyped_identifier &t2) noexcept
\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:159
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:131
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:91
function_symbol find_mapping(data_specification const &data, std::string const &s)
Finds a mapping in a data specification.
void swap(set_comprehension_binder &t1, set_comprehension_binder &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const container_type &x)
const data::variable & undefined_variable()
Returns a data variable that corresponds to 'undefined'.
Definition undefined.h:34
void swap(structured_sort &t1, structured_sort &t2) noexcept
\brief swap overload
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:89
std::ostream & operator<<(std::ostream &out, const list_container &x)
std::ostream & operator<<(std::ostream &out, const structured_sort_constructor &x)
std::ostream & operator<<(std::ostream &out, const untyped_set_or_bag_comprehension_binder &x)
bool is_application(const data_expression &t)
Returns true if the term t is an application.
bool is_list_container(const atermpp::aterm &x)
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:228
void make_basic_sort(atermpp::aterm &t, const ARGUMENTS &... args)
Definition basic_sort.h:65
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.
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:496
std::set< data::variable > find_all_variables(const T &x)
Definition find.h:300
void swap(untyped_sort_variable &t1, untyped_sort_variable &t2) noexcept
\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 &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.
void swap(fbag_container &t1, fbag_container &t2) noexcept
\brief swap overload
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:188
void swap(basic_sort &t1, basic_sort &t2) noexcept
\brief swap overload
Definition basic_sort.h:84
std::string pp(const data::container_type &x, bool arg0)
Definition data.cpp:49
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:93
void find_all_variables(const T &x, OutputIterator o)
Definition find.h:291
function_symbol if_always_else(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @if_always_else.
void swap(list_container &t1, list_container &t2) noexcept
\brief swap overload
void swap(exists_binder &t1, exists_binder &t2) noexcept
\brief swap overload
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:236
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.
void swap(assignment_expression &t1, assignment_expression &t2) noexcept
\brief swap overload
Definition assignment.h:80
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:399
std::string pp(const data::set_container &x, bool arg0)
Definition data.cpp:67
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.
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:291
const data_expression & find_rhs(const variable &v, const ASSIGNMENT_CONTAINER &c)
Returns the right hand sides of an assignment list.
Definition assignment.h:324
std::string pp(const structured_sort_constructor_vector &x)
constexpr int precedence(const where_clause &)
Definition print.h:401
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...
std::ostream & operator<<(std::ostream &out, const fset_container &x)
void swap(where_clause &t1, where_clause &t2) noexcept
\brief swap overload
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:473
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:376
std::string pp(const data::untyped_set_or_bag_comprehension_binder &x, bool arg0)
Definition data.cpp:77
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:254
std::ostream & operator<<(std::ostream &out, const untyped_possible_sorts &x)
data::data_expression translate_user_notation(const data::data_expression &x)
Definition data.cpp:88
std::string pp(const data::sort_expression_vector &x, bool arg0)
Definition data.cpp:25
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.
std::string pp(const data::untyped_sort &x, bool arg0)
Definition data.cpp:78
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:339
std::string pp(const data::data_equation &x, bool arg0)
Definition data.cpp:50
bool is_if_always_else_application(const atermpp::aterm &e)
Recogniser for application of @if_always_else.
std::set< core::identifier_string > find_identifiers(const data_specification &specification)
std::string pp(const data::forall &x, bool arg0)
Definition data.cpp:56
void swap(set_container &t1, set_container &t2) noexcept
\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:77
std::string pp(const data::assignment_list &x, bool arg0)
Definition data.cpp:28
std::ostream & operator<<(std::ostream &out, const assignment_expression &x)
Definition assignment.h:74
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:303
std::string pp(const data::untyped_identifier &x, bool arg0)
Definition data.cpp:73
application not_equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol !=.
Definition standard.h:177
std::string pp(const data::function_symbol_list &x, bool arg0)
Definition data.cpp:32
constexpr int precedence(const exists &)
Definition print.h:397
std::ostream & operator<<(std::ostream &out, const untyped_sort &x)
function_symbol_vector function_update_generate_constructors_code()
Give all system defined constructors for function_update.
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
void swap(container_type &t1, container_type &t2) noexcept
\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:215
std::ostream & operator<<(std::ostream &out, const forall &x)
Definition forall.h:77
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:401
bool is_left_associative(const data_expression &x)
Definition print.h:418
void swap(bag_container &t1, bag_container &t2) noexcept
\brief swap overload
std::string pp(const data::lambda_binder &x, bool arg0)
Definition data.cpp:62
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:328
void find_function_symbols(const T &x, OutputIterator o)
Definition find.h:398
void make_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition assignment.h:137
std::ostream & operator<<(std::ostream &out, const untyped_identifier_assignment &x)
Definition assignment.h:261
const core::identifier_string & if_always_else_name()
Generate identifier @if_always_else.
void swap(untyped_set_or_bag_comprehension_binder &t1, untyped_set_or_bag_comprehension_binder &t2) noexcept
\brief swap overload
std::string pp(const structured_sort_constructor_list &x)
void make_untyped_identifier_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition assignment.h:233
void swap(bag_comprehension_binder &t1, bag_comprehension_binder &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const exists &x)
Definition exists.h:76
bool is_set_comprehension_binder(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const alias &x)
Definition alias.h:91
void swap(forall_binder &t1, forall_binder &t2) noexcept
\brief swap overload
void swap(data_equation &t1, data_equation &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const lambda &x)
Definition lambda.h:89
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:312
std::ostream & operator<<(std::ostream &out, const forall_binder &x)
bool is_exists_binder(const atermpp::aterm &x)
std::set< data::variable > find_all_variables(const data::function_symbol &x)
Definition data.cpp:95
std::vector< data::variable > find_free_variables_in_order(const T &x)
Definition find.h:420
std::string pp(const data::application &x, bool arg0)
Definition data.cpp:40
bool is_not_equal_to_function_symbol(const DataExpression &e)
Recogniser for function !=.
Definition standard.h:168
void make_structured_sort_constructor_argument(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(lambda &t1, lambda &t2) noexcept
\brief swap overload
Definition lambda.h:95
function_symbol find_constructor(data_specification const &data, std::string const &s)
Finds a constructor in a data specification.
std::string pp(const data::function_sort &x, bool arg0)
Definition data.cpp:59
void swap(untyped_data_parameter &t1, untyped_data_parameter &t2) noexcept
\brief swap overload
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
Definition alias.h:63
std::string pp(const data::abstraction &x, bool arg0)
Definition data.cpp:38
const core::identifier_string & is_not_a_function_update_name()
Generate identifier @is_not_an_update.
std::string pp(const data::bag_comprehension_binder &x, bool arg0)
Definition data.cpp:44
void make_lambda(atermpp::aterm &result, ARGUMENTS... arguments)
Definition lambda.h:74
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.
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:347
std::ostream & operator<<(std::ostream &out, const structured_sort &x)
std::ostream & operator<<(std::ostream &out, const set_container &x)
std::string pp(const data::set_comprehension_binder &x, bool arg0)
Definition data.cpp:66
bool is_assignment_expression(const atermpp::aterm &x)
Definition assignment.h:60
std::string pp(const data::assignment &x, bool arg0)
Definition data.cpp:41
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:485
std::string pp(const data::structured_sort &x, bool arg0)
Definition data.cpp:69
std::ostream & operator<<(std::ostream &out, const bag_container &x)
std::string pp(const data::basic_sort &x, bool arg0)
Definition data.cpp:46
bool is_structured_sort_constructor_argument(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const exists_binder &x)
bool is_function_update_function_symbol(const atermpp::aterm &e)
Recogniser for function @func_update.
void swap(bag_comprehension &t1, bag_comprehension &t2) noexcept
\brief swap overload
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...
std::ostream & operator<<(std::ostream &out, const assignment &x)
Definition assignment.h:165
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.
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.
std::string pp(const data::exists_binder &x, bool arg0)
Definition data.cpp:54
void swap(forall &t1, forall &t2) noexcept
\brief swap overload
Definition forall.h:83
bool is_function_update_stable_function_symbol(const atermpp::aterm &e)
Recogniser for function @func_update_stable.
sort_expression find_sort(data_specification const &data, std::string const &s)
Finds a sort in a data specification.
bool is_right_associative(const data_expression &x)
Definition print.h:424
void swap(binder_type &t1, binder_type &t2) noexcept
\brief swap overload
Definition binder_type.h:66
std::string pp(const data::bag_comprehension &x, bool arg0)
Definition data.cpp:43
void make_forall(atermpp::aterm &result, ARGUMENTS... arguments)
Definition forall.h:63
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:346
bool is_structured_sort_constructor(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const lambda_binder &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:307
bool is_lambda_binder(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
std::string pp(const data::variable &x, bool arg0)
Definition data.cpp:80
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
void swap(set_comprehension &t1, set_comprehension &t2) noexcept
\brief swap overload
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:245
std::ostream & operator<<(std::ostream &out, const data_equation &x)
std::ostream & operator<<(std::ostream &out, const bag_comprehension &x)
std::set< core::identifier_string > find_identifiers(const T &x)
Definition find.h:365
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)
std::string pp(const T &x, bool precendence_aware=true)
Returns a string representation of the object x.
Definition print.h:2549
std::ostream & operator<<(std::ostream &out, const structured_sort_constructor_argument &x)
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.
bool is_untyped_set_or_bag_comprehension_binder(const atermpp::aterm &x)
std::string pp(const data::where_clause &x, bool arg0)
Definition data.cpp:81
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:90
std::ostream & operator<<(std::ostream &out, const function_sort &x)
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:100
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.
std::string pp(const data::bag_container &x, bool arg0)
Definition data.cpp:45
void swap(function_symbol &t1, function_symbol &t2) noexcept
\brief swap overload
std::string pp(const data::alias &x, bool arg0)
Definition data.cpp:39
bool is_if_function_symbol(const DataExpression &e)
Recogniser for function if.
Definition standard.h:205
std::ostream & operator<<(std::ostream &out, const fbag_container &x)
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:98
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:328
void make_abstraction(atermpp::aterm &result, ARGUMENTS... arguments)
Definition abstraction.h:72
void swap(sort_expression &t1, sort_expression &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const data::variable_list &x)
Definition data.cpp:97
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
void swap(abstraction &t1, abstraction &t2) noexcept
\brief swap overload
Definition abstraction.h:97
bool is_untyped_data_parameter(const atermpp::aterm &x)
void swap(alias &t1, alias &t2) noexcept
\brief swap overload
Definition alias.h:97
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:152
std::string pp(const data::structured_sort_constructor &x, bool arg0)
Definition data.cpp:70
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
Definition data.cpp:92
std::string pp(const data::data_specification &x, bool arg0)
Definition data.cpp:52
std::string pp(const data::data_equation_list &x, bool arg0)
Definition data.cpp:36
constexpr int precedence(const lambda &)
Definition print.h:398
void find_data_expressions(const T &x, OutputIterator o)
Returns all data expressions that occur in an object.
Definition find.h:440
std::string pp(const data::fset_container &x, bool arg0)
Definition data.cpp:58
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.
std::string pp(const data::sort_expression &x, bool arg0)
Definition data.cpp:68
std::ostream & operator<<(std::ostream &out, const binder_type &x)
Definition binder_type.h:60
std::string pp(const data::untyped_set_or_bag_comprehension &x, bool arg0)
Definition data.cpp:76
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:257
void swap(lambda_binder &t1, lambda_binder &t2) noexcept
\brief swap overload
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
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::string pp(const data::variable_list &x, bool arg0)
Definition data.cpp:30
std::ostream & operator<<(std::ostream &out, const data_expression &x)
application greater_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >=.
Definition standard.h:365
void find_sort_expressions(const T &x, OutputIterator o)
Definition find.h:377
bool is_less_equal_function_symbol(const DataExpression &e)
Recogniser for function <=.
Definition standard.h:282
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:356
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:278
std::set< data::variable > find_free_variables(const data::data_expression_list &x)
Definition data.cpp:99
void swap(untyped_set_or_bag_comprehension &t1, untyped_set_or_bag_comprehension &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const untyped_identifier &x)
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 machine_number_list &x, bool precedence_aware=true)
std::string pp(const data::data_expression &x, bool arg0)
Definition data.cpp:51
std::string pp(const data::lambda &x, bool arg0)
Definition data.cpp:61
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
std::string pp(const data::fbag_container &x, bool arg0)
Definition data.cpp:55
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
std::ostream & operator<<(std::ostream &out, const function_symbol &x)
std::string max_machine_number_string()
A string representation indicating the maximal machine number + 1.
std::ostream & operator<<(std::ostream &out, const where_clause &x)
bool is_bag_container(const atermpp::aterm &x)
std::string pp(const data::structured_sort_constructor_list &x, bool arg0)
Definition data.cpp:34
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:122
std::string pp(const data::container_sort &x, bool arg0)
Definition data.cpp:48
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
Definition data.cpp:87
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:85
std::ostream & operator<<(std::ostream &out, const variable &x)
Definition variable.h:96
data_expression_list right_hand_sides(const assignment_list &x)
Returns the right hand sides of an assignment list.
Definition assignment.h:315
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::string pp(const data::untyped_sort_variable &x, bool arg0)
Definition data.cpp:79
std::string pp(const data::untyped_data_parameter &x, bool arg0)
Definition data.cpp:72
std::string pp(const data::binder_type &x, bool arg0)
Definition data.cpp:47
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:140
bool is_fbag_container(const atermpp::aterm &x)
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
bool is_untyped_identifier_assignment(const atermpp::aterm &x)
Definition assignment.h:248
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:78
bool is_is_not_a_function_update_function_symbol(const atermpp::aterm &e)
Recogniser for function @is_not_an_update.
std::set< data::variable > find_all_variables(const data::variable &x)
Definition data.cpp:96
void make_exists(atermpp::aterm &result, ARGUMENTS... arguments)
Definition exists.h:61
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.
bool search_variable(const T &x, const variable &v)
Returns true if the term has a given variable as subterm.
Definition find.h:461
assignment_list make_assignment_list(const VariableSequence &variables, const ExpressionSequence &expressions)
Converts an iterator range to data_expression_list.
Definition assignment.h:298
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:265
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:101
std::ostream & operator<<(std::ostream &out, const sort_expression &x)
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:102
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.
std::ostream & operator<<(std::ostream &out, const data_specification &x)
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.
std::string pp(const data::sort_expression_list &x, bool arg0)
Definition data.cpp:24
void make_structured_sort_constructor(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::forall_binder &x, bool arg0)
Definition data.cpp:57
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::string pp(const data::untyped_possible_sorts &x, bool arg0)
Definition data.cpp:75
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
void swap(machine_number &t1, machine_number &t2) noexcept
\brief swap overload
std::string pp(const data::function_symbol &x, bool arg0)
Definition data.cpp:60
std::ostream & operator<<(std::ostream &out, const set_comprehension &x)
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
Definition data.cpp:184
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:302
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
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:344
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:196
std::ostream & operator<<(std::ostream &out, const untyped_set_or_bag_comprehension &x)
function_symbol is_not_a_function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @is_not_an_update.
std::string pp(const data::machine_number &x, bool arg0)
Definition data.cpp:64
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:151
void swap(data_expression &t1, data_expression &t2) noexcept
\brief swap overload
void swap(variable &t1, variable &t2) noexcept
\brief swap overload
Definition variable.h:102
std::string pp(const data::assignment_expression &x, bool arg0)
Definition data.cpp:42
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void swap(untyped_possible_sorts &t1, untyped_possible_sorts &t2) noexcept
\brief swap overload
bool is_sort_expression(const atermpp::aterm &x)
Test for a sort_expression expression.
std::string pp(const data::set_comprehension &x, bool arg0)
Definition data.cpp:65
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:91
void make_untyped_sort_variable(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::data_expression_list &x, bool arg0)
Definition data.cpp:26
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:310
expression builder that visits all sub expressions
Definition builder.h:32
void leave(const T &)
Definition builder.h:40
void enter(const T &)
Definition builder.h:35
core::identifier_string parse_Id(const parse_node &node) const
Definition parse.h:231
atermpp::term_list< T > parse_list(const parse_node &node, const std::string &type, const Function &f) const
Definition parse.h:216
default_parser_actions(const parser &parser_)
Definition parse.h:211
std::vector< T > parse_vector(const parse_node &node, const std::string &type, const Function &f) const
Definition parse.h:224
core::identifier_string_list parse_IdList(const parse_node &node) const
Definition parse.h:241
core::identifier_string parse_Number(const parse_node &node) const
Definition parse.h:236
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_)
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_)
bool operator()(const parse_node &node) const
Definition parse.h:153
collector(const parser_table &table_, const std::string &type_, Container &container_, const Function &f_)
Definition parse.h:146
set_collector(const parser_table &table_, const std::string &type_, SetContainer &container_, const Function &f_)
Definition parse.h:179
bool operator()(const parse_node &node) const
Definition parse.h:186
visitor(const parser_table &table_, const std::string &type_, const Function &f_)
Definition parse.h:114
const parser_table & table
Definition parse.h:110
bool operator()(const parse_node &node) const
Definition parse.h:120
std::string symbol_name(const parse_node &node) const
Definition parse.h:203
parser_actions(const parser &parser_)
Definition parse.h:85
void traverse(const parse_node &node, const Function &f) const
Definition parse.h:91
const parser & m_parser
Definition parse.h:83
set_collector< SetContainer, Function > make_set_collector(const parser_table &table, const std::string &type, SetContainer &container, const Function &f) const
Definition parse.h:198
visitor< Function > make_visitor(const parser_table &table, const std::string &type, const Function &f) const
Definition parse.h:132
collector< Container, Function > make_collector(const parser_table &table, const std::string &type, Container &container, const Function &f) const
Definition parse.h:165
void apply(T &result, const argument_type &x)
Definition builder.h:173
update_apply_builder(const Function &f)
Definition builder.h:179
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:511
void apply(T &result, const data::machine_number &x)
Definition builder.h:445
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:471
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:578
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:519
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:454
void apply(T &result, const data::data_equation &x)
Definition builder.h:527
void apply(T &result, const data::function_symbol &x)
Definition builder.h:416
void apply(T &result, const data::assignment &x)
Definition builder.h:463
void apply(T &result, const data::abstraction &x)
Definition builder.h:593
void apply(T &result, const data::forall &x)
Definition builder.h:479
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:535
void apply(T &result, const data::exists &x)
Definition builder.h:487
void apply(T &result, const data::where_clause &x)
Definition builder.h:437
void apply(T &result, const data::application &x)
Definition builder.h:425
void apply(T &result, const data::variable &x)
Definition builder.h:407
void apply(T &result, const data::data_expression &x)
Definition builder.h:543
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:503
void apply(T &result, const data::lambda &x)
Definition builder.h:495
Maintains a multiset of bound data variables during traversal.
Definition add_binding.h:30
void decrease_bind_count(const assignment_list &assignments)
Definition add_binding.h:47
void leave(const data::exists &x)
Definition add_binding.h:80
void enter(const data::forall &x)
Definition add_binding.h:65
void leave(const data::forall &x)
Definition add_binding.h:70
void leave(const data::data_equation &x)
void enter(const data::set_comprehension &x)
Definition add_binding.h:95
void enter(const data::data_equation &x)
void leave(const data::set_comprehension &x)
void enter(const data::exists &x)
Definition add_binding.h:75
void leave(const data::bag_comprehension &x)
void enter(const data::lambda &x)
Definition add_binding.h:85
void leave(const data::untyped_set_or_bag_comprehension &x)
void increase_bind_count(const assignment_list &assignments)
Definition add_binding.h:39
void enter(const data::bag_comprehension &x)
void leave(const data::lambda &x)
Definition add_binding.h:90
void enter(const data::untyped_set_or_bag_comprehension &x)
void enter(const data::where_clause &x)
Definition add_binding.h:55
void leave(const data::where_clause &x)
Definition add_binding.h:60
void apply(T &result, const data::where_clause &x)
void apply(const data::where_clause &x)
void apply(T &result, const data::assignment &x)
Definition builder.h:108
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:207
void apply(T &result, const data::structured_sort_constructor_argument &x)
Definition builder.h:231
void apply(T &result, const data::container_sort &x)
Definition builder.h:133
void apply(T &result, const data::alias &x)
Definition builder.h:247
void apply(T &result, const data::exists &x)
Definition builder.h:191
void apply(T &result, const data::machine_number &x)
Definition builder.h:90
void apply(T &result, const data::function_symbol &x)
Definition builder.h:62
void apply(T &result, const data::untyped_possible_sorts &x)
Definition builder.h:166
void apply(T &result, const data::forall &x)
Definition builder.h:183
void apply(T &result, const data::basic_sort &x)
Definition builder.h:124
void apply(T &result, const data::data_equation &x)
Definition builder.h:255
void apply(T &result, const data::untyped_sort &x)
Definition builder.h:157
void apply(T &result, const data::abstraction &x)
Definition builder.h:356
void apply(T &result, const data::application &x)
Definition builder.h:70
void apply(T &result, const data::variable &x)
Definition builder.h:54
void apply(T &result, const data::structured_sort &x)
Definition builder.h:141
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:116
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:263
void apply(T &result, const data::function_sort &x)
Definition builder.h:149
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:99
void apply(T &result, const data::structured_sort_constructor &x)
Definition builder.h:239
void apply(T &result, const data::lambda &x)
Definition builder.h:199
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:223
void apply(T &result, const data::where_clause &x)
Definition builder.h:82
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:306
void apply(T &result, const data::data_expression &x)
Definition builder.h:271
void apply(T &result, const data::sort_expression &x)
Definition builder.h:321
void apply(T &result, const data::untyped_sort_variable &x)
Definition builder.h:174
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:215
void apply(const data::function_symbol &x)
Definition traverser.h:377
void apply(const data::set_comprehension &x)
Definition traverser.h:449
void apply(const data::untyped_identifier &x)
Definition traverser.h:407
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:463
void apply(const data::application &x)
Definition traverser.h:384
void apply(const data::forall &x)
Definition traverser.h:428
void apply(const data::data_equation &x)
Definition traverser.h:470
void apply(const data::exists &x)
Definition traverser.h:435
void apply(const data::lambda &x)
Definition traverser.h:442
void apply(const data::machine_number &x)
Definition traverser.h:400
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:421
void apply(const data::data_expression &x)
Definition traverser.h:486
void apply(const data::where_clause &x)
Definition traverser.h:392
void apply(const data::bag_comprehension &x)
Definition traverser.h:456
void apply(const data::abstraction &x)
Definition traverser.h:534
void apply(const data::assignment_expression &x)
Definition traverser.h:520
void apply(const data::variable &x)
Definition traverser.h:370
void apply(const data::assignment &x)
Definition traverser.h:414
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:479
void apply(const data::untyped_possible_sorts &x)
Definition traverser.h:900
void apply(const data::structured_sort_constructor_argument &x)
Definition traverser.h:962
void apply(const data::application &x)
Definition traverser.h:818
void apply(const data::untyped_sort_variable &x)
Definition traverser.h:907
void apply(const data::basic_sort &x)
Definition traverser.h:864
void apply(const data::bag_comprehension &x)
Definition traverser.h:946
void apply(const data::assignment_expression &x)
Definition traverser.h:1039
void apply(const data::untyped_sort &x)
Definition traverser.h:893
void apply(const data::assignment &x)
Definition traverser.h:848
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:954
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:997
void apply(const data::structured_sort &x)
Definition traverser.h:878
void apply(const data::function_sort &x)
Definition traverser.h:885
void apply(const data::data_equation &x)
Definition traverser.h:987
void apply(const data::container_sort &x)
Definition traverser.h:871
void apply(const data::machine_number &x)
Definition traverser.h:834
void apply(const data::abstraction &x)
Definition traverser.h:1087
void apply(const data::structured_sort_constructor &x)
Definition traverser.h:970
void apply(const data::variable &x)
Definition traverser.h:802
void apply(const data::function_symbol &x)
Definition traverser.h:810
void apply(const data::untyped_identifier &x)
Definition traverser.h:841
void apply(const data::data_expression &x)
Definition traverser.h:1005
void apply(const data::set_comprehension &x)
Definition traverser.h:938
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:856
void apply(const data::sort_expression &x)
Definition traverser.h:1053
void apply(const data::where_clause &x)
Definition traverser.h:826
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:97
void apply(const data::assignment &x)
Definition traverser.h:89
void apply(const data::sort_expression &x)
Definition traverser.h:288
void apply(const data::where_clause &x)
Definition traverser.h:67
void apply(const data::data_expression &x)
Definition traverser.h:240
void apply(const data::lambda &x)
Definition traverser.h:170
void apply(const data::basic_sort &x)
Definition traverser.h:104
void apply(const data::variable &x)
Definition traverser.h:45
void apply(const data::untyped_possible_sorts &x)
Definition traverser.h:140
void apply(const data::untyped_identifier &x)
Definition traverser.h:82
void apply(const data::untyped_sort_variable &x)
Definition traverser.h:147
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:194
void apply(const data::forall &x)
Definition traverser.h:154
void apply(const data::application &x)
Definition traverser.h:59
void apply(const data::structured_sort_constructor_argument &x)
Definition traverser.h:202
void apply(const data::structured_sort_constructor &x)
Definition traverser.h:209
void apply(const data::untyped_sort &x)
Definition traverser.h:133
void apply(const data::machine_number &x)
Definition traverser.h:75
void apply(const data::function_sort &x)
Definition traverser.h:125
void apply(const data::container_sort &x)
Definition traverser.h:111
void apply(const data::set_comprehension &x)
Definition traverser.h:178
void apply(const data::data_equation &x)
Definition traverser.h:223
void apply(const data::structured_sort &x)
Definition traverser.h:118
void apply(const data::assignment_expression &x)
Definition traverser.h:274
void apply(const data::bag_comprehension &x)
Definition traverser.h:186
void apply(const data::exists &x)
Definition traverser.h:162
void apply(const data::abstraction &x)
Definition traverser.h:322
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:233
void apply(const data::function_symbol &x)
Definition traverser.h:52
void apply(const data::untyped_set_or_bag_comprehension &x)
Definition traverser.h:681
void apply(const data::untyped_identifier_assignment &x)
Definition traverser.h:634
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:699
void apply(const data::data_expression &x)
Definition traverser.h:706
void apply(const data::bag_comprehension &x)
Definition traverser.h:673
void apply(const data::data_equation &x)
Definition traverser.h:689
void apply(const data::where_clause &x)
Definition traverser.h:604
void apply(const data::set_comprehension &x)
Definition traverser.h:665
void apply(const data::exists &x)
Definition traverser.h:649
void apply(const data::untyped_identifier &x)
Definition traverser.h:619
void apply(const data::variable &x)
Definition traverser.h:582
void apply(const data::abstraction &x)
Definition traverser.h:754
void apply(const data::forall &x)
Definition traverser.h:641
void apply(const data::assignment_expression &x)
Definition traverser.h:740
void apply(const data::assignment &x)
Definition traverser.h:626
void apply(const data::application &x)
Definition traverser.h:596
void apply(const data::function_symbol &x)
Definition traverser.h:589
void apply(const data::lambda &x)
Definition traverser.h:657
void apply(const data::machine_number &x)
Definition traverser.h:612
void apply(T &result, const data::abstraction &x)
Definition builder.h:829
void apply(T &result, const data::application &x)
Definition builder.h:661
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:771
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:690
void apply(T &result, const data::data_expression &x)
Definition builder.h:779
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:814
void apply(T &result, const data::where_clause &x)
Definition builder.h:673
void apply(T &result, const data::forall &x)
Definition builder.h:715
void apply(T &result, const data::function_symbol &x)
Definition builder.h:652
void apply(T &result, const data::exists &x)
Definition builder.h:723
void apply(T &result, const data::lambda &x)
Definition builder.h:731
void apply(T &result, const data::variable &x)
Definition builder.h:643
void apply(T &result, const data::assignment &x)
Definition builder.h:699
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:707
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:755
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:739
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:747
void apply(T &result, const data::machine_number &x)
Definition builder.h:681
void apply(T &result, const data::data_equation &x)
Definition builder.h:763
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:142
data::variable_list parse_VarsDeclList(const core::parse_node &node) const
Definition parse_impl.h:201
data::data_expression_list parse_DataExprList(const core::parse_node &node) const
Definition parse_impl.h:284
data_expression make_list_enumeration(const data_expression_list &x) const
Definition parse_impl.h:147
data_expression make_function_update(const data_expression &x, const data_expression &y, const data_expression &z) const
Definition parse_impl.h:165
data_expression make_set_enumeration(const data_expression_list &x) const
Definition parse_impl.h:153
data::sort_expression_list get_sorts(const ExpressionContainer &x) const
Definition parse_impl.h:171
data_expression_actions(const core::parser &parser_)
Definition parse_impl.h:138
bool callback_VarsDecl(const core::parse_node &node, variable_vector &result) const
Definition parse_impl.h:186
data::variable parse_VarDecl(const core::parse_node &node) const
Definition parse_impl.h:181
data::untyped_identifier_assignment parse_Assignment(const core::parse_node &node) const
Definition parse_impl.h:274
data::data_expression parse_DataValExpr(const core::parse_node &node) const
Definition parse_impl.h:269
data::data_expression_list parse_BagEnumEltList(const core::parse_node &node) const
Definition parse_impl.h:289
data::untyped_identifier_assignment_list parse_AssignmentList(const core::parse_node &node) const
Definition parse_impl.h:279
data_expression make_bag_enumeration(const data_expression_list &x) const
Definition parse_impl.h:159
data::data_expression parse_DataExprUnit(const core::parse_node &node) const
Definition parse_impl.h:255
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:208
bool callback_IdsDecl(const core::parse_node &node, function_symbol_vector &result) const
Definition parse_impl.h:338
data::variable_list parse_GlobVarSpec(const core::parse_node &node) const
Definition parse_impl.h:370
data_specification_actions(const core::parser &parser_)
Definition parse_impl.h:297
data::function_symbol_vector parse_MapSpec(const core::parse_node &node) const
Definition parse_impl.h:365
data::data_equation_vector parse_EqnDeclList(const core::parse_node &node, const variable_list &variables) const
Definition parse_impl.h:396
data::variable_list parse_VarSpec(const core::parse_node &node) const
Definition parse_impl.h:375
std::vector< atermpp::aterm > parse_SortDeclList(const core::parse_node &node) const
Definition parse_impl.h:326
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:458
bool callback_SortDecl(const core::parse_node &node, std::vector< atermpp::aterm > &result) const
Definition parse_impl.h:301
data::data_equation_vector parse_EqnSpec(const core::parse_node &node) const
Definition parse_impl.h:403
data::function_symbol_vector parse_IdsDeclList(const core::parse_node &node) const
Definition parse_impl.h:353
bool callback_DataSpecElement(const core::parse_node &node, untyped_data_specification &result) const
Definition parse_impl.h:410
bool callback_EqnDecl(const core::parse_node &node, const variable_list &variables, data_equation_vector &result) const
Definition parse_impl.h:380
std::vector< atermpp::aterm > parse_SortSpec(const core::parse_node &node) const
Definition parse_impl.h:333
data::function_symbol_vector parse_ConsSpec(const core::parse_node &node) const
Definition parse_impl.h:360
bool operator()(const function_symbol &c) const
Function call operator.
void apply(const data::structured_sort_constructor &)
Definition is_untyped.h:59
void apply(const data::untyped_possible_sorts &)
Definition is_untyped.h:44
void apply(const data::structured_sort_constructor_argument &)
Definition is_untyped.h:54
void apply(const data::untyped_set_or_bag_comprehension &)
Definition is_untyped.h:49
void apply(const data::untyped_identifier_assignment &)
Definition is_untyped.h:34
void apply(const data::untyped_sort &)
Definition is_untyped.h:39
void apply(const data::untyped_identifier &)
Definition is_untyped.h:29
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:578
void print_condition(const T &x, const std::string &arrow=" -> ")
Definition print.h:736
void apply(const data::untyped_set_or_bag_comprehension_binder &x)
Definition print.h:1317
void apply(const data::untyped_sort_variable &x)
Definition print.h:1470
void apply(const data::application &x)
Definition print.h:1518
bool is_cons_list(data_expression x) const
Definition print.h:822
void apply(const machine_number &x)
Definition print.h:2315
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:538
void apply(const data::untyped_identifier &x)
Definition print.h:1478
void print_sort_list(const Container &container, const std::string &opener="(", const std::string &closer=")", const std::string &separator=", ")
Definition print.h:746
void print_fset_default(const data_expression &x)
Definition print.h:1136
void apply(const data::bag_comprehension_binder &x)
Definition print.h:1329
void apply(const data::set_container &x)
Definition print.h:1394
void apply(const data::set_comprehension_binder &x)
Definition print.h:1323
void print_set_enumeration(const application &x)
Definition print.h:784
void print_binary_data_operation(const application &x, const std::string &op)
Definition print.h:467
void print_cons_list(data_expression x)
Definition print.h:906
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:2424
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:2364
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:850
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:706
void apply(const data::list_container &x)
Definition print.h:1387
void apply(const data::exists &x)
Definition print.h:2343
void apply(const data::fbag_container &x)
Definition print.h:1415
void apply(const data::function_sort &x)
Definition print.h:1446
void print_fset_lambda(const data_expression &x)
Definition print.h:1063
core::identifier_string generate_identifier(const std::string &prefix, const data_expression &context) const
Definition print.h:526
void apply(const data::data_equation &x)
Definition print.h:2353
void apply(const data::alias &x)
Definition print.h:1378
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:585
void apply(const data::where_clause &x)
Definition print.h:2320
void apply(const data::data_specification &x)
Definition print.h:2492
bool is_fbag_zero(const data_expression &x)
Definition print.h:891
void apply(const data::structured_sort &x)
Definition print.h:1439
void apply(const data::untyped_identifier_assignment &x)
Definition print.h:1308
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:2464
bool is_fset_false(const data_expression &x)
Definition print.h:881
bool is_abstraction_application(const application &x) const
Definition print.h:817
void apply(const data::lambda_binder &x)
Definition print.h:1347
void apply(const data::structured_sort_constructor_argument &x)
Definition print.h:1353
void apply(const data::variable &x)
Definition print.h:1485
void apply(const data::container_type &x)
Definition print.h:1257
bool is_fbag_one(const data_expression &x)
Definition print.h:896
void apply(const data::basic_sort &x)
Definition print.h:1422
bool is_snoc_list(data_expression x) const
Definition print.h:831
void print_fbag_one(const data_expression &x)
Definition print.h:965
bool is_fbag_lambda(const data_expression &x)
Definition print.h:901
void print_abstraction(const Abstraction &x, const std::string &op)
Definition print.h:1169
void apply(const data::function_symbol &x)
Definition print.h:1492
void apply(const data::exists_binder &x)
Definition print.h:1341
void apply(const data::fset_container &x)
Definition print.h:1408
bool has_conflict(const data_equation &eqn, const std::map< core::identifier_string, variable > &variable_map)
Definition print.h:2384
bool is_numeric_expression(const application &x)
Definition print.h:859
bool is_infix_operation(const application &x) const
Definition print.h:474
void print_fbag_lambda(const data_expression &x)
Definition print.h:982
void apply(const data::untyped_data_parameter &x)
Definition print.h:1300
void apply(const data::abstraction &x)
Definition print.h:2503
void apply(const data::untyped_sort &x)
Definition print.h:1454
void apply(const data::container_sort &x)
Definition print.h:1429
void apply(const data::assignment &x)
Definition print.h:1283
void print_fbag_zero(const data_expression &x)
Definition print.h:945
bool is_fset_lambda(const data_expression &x)
Definition print.h:886
void print_snoc_list(data_expression x)
Definition print.h:919
void print_fset_false(const data_expression &x)
Definition print.h:1051
void print_fbag_cons_list(data_expression x)
Definition print.h:1017
bool is_standard_sort(const sort_expression &x)
Definition print.h:867
void apply(const data::untyped_possible_sorts &x)
Definition print.h:1461
void print_unary_data_operation(const application &x, const std::string &op)
Definition print.h:451
bool is_fset_cons_list(data_expression x)
Definition print.h:840
void print_setbag_comprehension(const abstraction &x)
Definition print.h:808
void print_fset_cons_list(data_expression x)
Definition print.h:932
void print_bag_enumeration(const application &x)
Definition print.h:791
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:693
void apply(const data::bag_container &x)
Definition print.h:1401
void print_function_application(const application &x)
Definition print.h:1179
void print_fbag_default(const data_expression &x)
Definition print.h:1000
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:2405
void print_variable(const Variable &x, bool print_sort=false)
Definition print.h:565
void apply(const data::variable_list &x)
Definition print.h:1293
void apply(const std::pair< data_expression, data_expression > &x)
Definition print.h:1249
void print_binary_data_operation(const application &x, const data_expression &x1, const data_expression &x2, const std::string &op)
Definition print.h:457
void print_list_enumeration(const application &x)
Definition print.h:777
void apply(const data::structured_sort_constructor &x)
Definition print.h:1365
void apply(const data::forall &x)
Definition print.h:2338
void apply(const data::forall_binder &x)
Definition print.h:1335
void apply(const data::lambda &x)
Definition print.h:2348
void print_fset_set_operation(const data_expression &x, const std::string &op)
Definition print.h:1073
void print_fset_true(const data_expression &x)
Definition print.h:1045
bool is_fset_true(const data_expression &x)
Definition print.h:876
data::structured_sort_constructor parse_ConstrDecl(const core::parse_node &node) const
Definition parse_impl.h:93
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
Definition parse_impl.h:32
data::structured_sort_constructor_list parse_ConstrDeclList(const core::parse_node &node) const
Definition parse_impl.h:113
data::sort_expression_list parse_SortProduct(const core::parse_node &node) const
Definition parse_impl.h:84
data::sort_expression_list parse_SortExpr_as_SortProduct(const core::parse_node &node) const
Definition parse_impl.h:73
data::structured_sort_constructor_argument_list parse_ProjDeclList(const core::parse_node &node) const
Definition parse_impl.h:130
sort_expression_actions(const core::parser &parser_)
Definition parse_impl.h:28
data::structured_sort_constructor_argument parse_ProjDecl(const core::parse_node &node) const
Definition parse_impl.h:118
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:2538
void operator()(const T &x, std::ostream &out, bool precendence_aware)
Definition print.h:2540
sort_expression operator()(structured_sort_constructor_argument const &s) const
\brief Builder class
Definition builder.h:864
\brief Traverser class
Definition traverser.h:789
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:128