mCRL2
Loading...
Searching...
No Matches
construction_utility.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp
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/core/construction_utility.h
10/// \brief construction utility
11
12#ifndef MCRL2_CORE_DETAIL_CONSTRUCTION_UTILITY_H
13#define MCRL2_CORE_DETAIL_CONSTRUCTION_UTILITY_H
14
15#include "mcrl2/core/identifier_string.h"
16
17namespace mcrl2
18{
19namespace core
20{
21namespace detail
22{
23
24// Component that helps applying the Singleton design pattern
25template < typename Derived, typename Expression = atermpp::aterm >
27{
28 public:
29 static const Expression& instance()
30 {
31 static Expression single_instance = Expression(Derived::initialise());
32 return single_instance;
33 }
34
39
40 protected:
42};
43
44template < typename Derived >
46 {};
47
48} // namespace detail
49} // namespace core
50} // namespace mcrl2
51
52
53#endif
aterm_string(const std::string &s)
Constructor that allows construction from a string.
const aterm & operator[](const size_type i) const
Returns the i-th argument.
Definition aterm.h:187
aterm & operator=(const aterm &other) noexcept=default
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
term_appl_iterator< aterm > const_iterator
Const iterator used to iterate through an term_appl.
Definition aterm.h:45
bool operator!=(const function_symbol &f) const
Inequality test.
bool operator==(const function_symbol &f) const
Equality test.
A list of aterm objects.
Definition aterm_list.h:24
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
bool type_is_appl() const noexcept
Dynamic check whether the term is an aterm.
Definition aterm_core.h:55
bool type_is_int() const noexcept
Dynamic check whether the term is an aterm_int.
Definition aterm_core.h:63
Builder< apply_builder_arg1< Builder, Arg1 > > super
Definition builder.h:125
apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:133
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:157
Builder< apply_builder_arg2< Builder, Arg1, Arg2 > > super
Definition builder.h:149
Builder< apply_builder< Builder > > super
Definition builder.h:104
singleton_expression & operator=(singleton_expression &&)=delete
singleton_expression & operator=(const singleton_expression &)=delete
singleton_expression(singleton_expression &&)=delete
singleton_expression(const singleton_expression &)=delete
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
Definition builder.h:225
Builder< update_apply_builder_arg1< Builder, Function, Arg1 > > super
Definition builder.h:208
void apply(T &result, const argument_type &x)
Definition builder.h:220
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
\brief A sort alias
Definition alias.h:26
alias()
\brief Default constructor X3.
Definition alias.h:29
alias(const alias &) noexcept=default
Move semantics.
alias & operator=(const alias &) noexcept=default
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:42
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
Definition alias.h:35
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
Definition alias.h:52
const sort_expression & reference() const
Definition alias.h:57
\brief Assignment expression
Definition assignment.h:27
\brief Assignment of a data expression to a variable
Definition assignment.h:91
const data_expression & rhs() const
Definition assignment.h:122
const variable & lhs() const
Definition assignment.h:117
\brief Binder for bag comprehension
universal quantification.
\brief Container type for bags
bag_container(const bag_container &) noexcept=default
Move semantics.
bag_container(bag_container &&) noexcept=default
bag_container & operator=(bag_container &&) noexcept=default
bag_container()
\brief Default constructor X3.
bag_container(const atermpp::aterm &term)
bag_container & operator=(const bag_container &) noexcept=default
\brief A basic sort
Definition basic_sort.h:26
basic_sort(const basic_sort &) noexcept=default
Move semantics.
basic_sort()
\brief Default constructor X3.
Definition basic_sort.h:29
basic_sort & operator=(const basic_sort &) noexcept=default
const core::identifier_string & name() const
Definition basic_sort.h:57
basic_sort(basic_sort &&) noexcept=default
basic_sort(const core::identifier_string &name)
\brief Constructor Z14.
Definition basic_sort.h:42
basic_sort(const std::string &name)
\brief Constructor Z2.
Definition basic_sort.h:47
basic_sort & operator=(basic_sort &&) noexcept=default
basic_sort(const atermpp::aterm &term)
Definition basic_sort.h:35
\brief A container sort
container_sort()
\brief Default constructor X3.
container_sort & operator=(container_sort &&) noexcept=default
container_sort(const container_sort &) noexcept=default
Move semantics.
container_sort(const container_type &container_name, const sort_expression &element_sort)
\brief Constructor Z14.
container_sort(container_sort &&) noexcept=default
container_sort & operator=(const container_sort &) noexcept=default
const container_type & container_name() const
const sort_expression & element_sort() const
container_sort(const atermpp::aterm &term)
\brief Container type
container_type(container_type &&) noexcept=default
container_type(const atermpp::aterm &term)
container_type & operator=(const container_type &) noexcept=default
container_type & operator=(container_type &&) noexcept=default
container_type(const container_type &) noexcept=default
Move semantics.
container_type()
\brief Default constructor X3.
\brief A data equation
data_equation(const atermpp::aterm &term)
data_equation()
\brief Default constructor X3.
const data_expression & lhs() const
const data_expression & condition() const
data_equation & operator=(data_equation &&) noexcept=default
data_equation(const Container &variables, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
Constructor.
const data_expression & rhs() const
data_equation(data_equation &&) noexcept=default
data_equation(const Container &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs, typename atermpp::enable_if_container< Container, variable >::type *=nullptr)
\brief Constructor Z1.
data_equation(const variable_list &variables, const data_expression &condition, const data_expression &lhs, const data_expression &rhs)
\brief Constructor Z12.
const variable_list & variables() const
data_equation & operator=(const data_equation &) noexcept=default
data_equation(const data_expression &lhs, const data_expression &rhs)
Constructor.
data_equation(const data_equation &) noexcept=default
Move semantics.
data_expression & operator=(const data_expression &) noexcept=default
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const
Apply a data expression to four data expressions.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3) const
Apply a data expression to three data expressions.
data_expression(const atermpp::aterm &term)
data_expression()
\brief Default constructor X3.
application operator()(const data_expression &e1, const data_expression &e2) const
Apply a data expression to two data expressions.
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const_iterator end() const
application operator()(const data_expression &e) const
Apply a data expression to a data expression.
data_expression(const data_expression &) noexcept=default
Move semantics.
data_expression(data_expression &&) noexcept=default
const_iterator begin() const
bool is_default_data_expression() const
A function to efficiently determine whether a data expression is made by the default constructor.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const
Apply a data expression to five data expressions.
application operator()(const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const
Apply a data expression to six data expressions.
\brief Binder for existential quantification
existential quantification.
Definition exists.h:26
\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
universal quantification.
Definition forall.h:26
\brief Container type for finite sets
fset_container(fset_container &&) noexcept=default
fset_container(const fset_container &) noexcept=default
Move semantics.
fset_container(const atermpp::aterm &term)
fset_container()
\brief Default constructor X3.
fset_container & operator=(fset_container &&) noexcept=default
fset_container & operator=(const fset_container &) noexcept=default
\brief A function sort
const sort_expression & codomain() const
function_sort()
\brief Default constructor X3.
function_sort(const sort_expression_list &domain, const sort_expression &codomain)
\brief Constructor Z14.
function_sort & operator=(const function_sort &) noexcept=default
function_sort(const atermpp::aterm &term)
function_sort(const Container &domain, const sort_expression &codomain, typename atermpp::enable_if_container< Container, sort_expression >::type *=nullptr)
\brief Constructor Z2.
function_sort & operator=(function_sort &&) noexcept=default
function_sort(function_sort &&) noexcept=default
function_sort(const function_sort &) noexcept=default
Move semantics.
const sort_expression_list & domain() const
\brief A function symbol
function_symbol(const core::identifier_string &name, const sort_expression &sort)
Constructor.
function_symbol(const function_symbol &) noexcept=default
Move semantics.
function_symbol & operator=(function_symbol &&) noexcept=default
function_symbol()
Default constructor.
function_symbol(function_symbol &&) noexcept=default
function_symbol(const atermpp::aterm &term)
Constructor.
const core::identifier_string & name() const
const sort_expression & sort() const
function_symbol & operator=(const function_symbol &) noexcept=default
function_symbol(const std::string &name, const sort_expression &sort)
Constructor.
\brief Binder for lambda abstraction
function symbol.
Definition lambda.h:27
\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
\brief Binder for set comprehension
universal quantification.
\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)
\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)
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
const core::identifier_string & name() const
const core::identifier_string & recogniser() const
const structured_sort_constructor_argument_list & arguments() const
const structured_sort_constructor_list & constructors() const
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
Definition assignment.h:182
const core::identifier_string & lhs() const
Definition assignment.h:213
const data_expression & rhs() const
Definition assignment.h:218
\brief An untyped identifier
const sort_expression_list & sorts() const
\brief Binder for untyped set or bag comprehension
Definition binder_type.h:77
\brief Unknown sort expression
untyped_sort & operator=(const untyped_sort &) noexcept=default
untyped_sort(const atermpp::aterm &term)
untyped_sort(const untyped_sort &) noexcept=default
Move semantics.
untyped_sort & operator=(untyped_sort &&) noexcept=default
untyped_sort(untyped_sort &&) noexcept=default
untyped_sort()
\brief Default constructor X3.
\brief A data variable
Definition variable.h:28
variable(const variable &) noexcept=default
Move semantics.
variable(const std::string &name, const sort_expression &sort)
Constructor.
Definition variable.h:69
variable(variable &&) noexcept=default
variable()
Default constructor.
Definition variable.h:49
const core::identifier_string & name() const
Definition variable.h:38
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
Definition variable.h:43
variable & operator=(const variable &) noexcept=default
variable(const core::identifier_string &name, const sort_expression &sort)
Constructor.
Definition variable.h:62
variable(const atermpp::aterm &term)
Constructor.
Definition variable.h:55
\brief A where expression
const data_expression & body() const
const assignment_expression_list & declarations() const
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
Standard exception class for reporting runtime errors.
Definition exception.h:27
D_ParserTables parser_tables_mcrl2
Definition dparser.cpp:20
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
The main namespace for the aterm++ library.
Definition algorithm.h:21
term_list< aterm > aterm_list
A term_list with elements of type aterm.
Definition aterm_list.h:497
const aterm_string & empty_string()
Returns the empty aterm_string.
bool check_term_PREqnSpec(const Term &t)
bool check_term_MapSpec(const Term &t)
bool check_term_PBESTrue(const Term &t)
bool check_term_Seq(const Term &t)
bool check_term_DataVarIdInit(const Term &t)
bool check_rule_DataVarIdInit(const Term &t)
bool check_term_Action(const Term &t)
bool check_term_PRESOr(const Term &t)
bool check_term_SortId(const Term &t)
bool check_term_Sum(const Term &t)
bool check_term_Whr(const Term &t)
bool check_term_ActAt(const Term &t)
bool check_rule_WhrDecl(const Term &t)
bool check_term_StateInfimum(const Term &t)
bool check_term_CommExpr(const Term &t)
bool check_rule_ActSpec(const Term &t)
bool check_term_UntypedSortUnknown(const Term &t)
bool check_term_ActFalse(const Term &t)
bool check_term_ActId(const Term &t)
bool check_term_RegTrans(const Term &t)
bool check_rule_Distribution(const Term &t)
bool check_term_LinearProcessSummand(const Term &t)
bool check_rule_Number(const Term &t)
const atermpp::function_symbol & function_symbol_DataEqn()
const atermpp::function_symbol & function_symbol_DataVarId()
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)
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
Definition dparser.cpp:463
bool check_term_Delta(const Term &t)
bool check_rule_PBEqn(const Term &t)
bool check_rule_Action(const Term &t)
const atermpp::function_symbol & function_symbol_SortRef()
bool check_term_PRESTrue(const Term &t)
bool check_rule_ActionRenameSpec(const Term &t)
bool check_rule_FixPoint(const Term &t)
bool check_list_argument(const Term &t, CheckFunction f, unsigned int minimum_size)
bool check_rule_DataEqn(const Term &t)
bool check_rule_LinProcSpec(const Term &t)
bool check_term_PRES(const Term &t)
bool check_rule_SortDecl(const Term &t)
bool check_rule_RenameExpr(const Term &t)
bool check_term_ActImp(const Term &t)
bool check_term_Allow(const Term &t)
bool check_term_Choice(const Term &t)
bool check_term_LinProcSpec(const Term &t)
bool check_rule_SortId(const Term &t)
bool check_term_PBESNot(const Term &t)
bool check_term_Sync(const Term &t)
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)
D_ParseNode * ambiguity_fn(struct D_Parser *, int n, struct D_ParseNode **v)
Function for resolving parser ambiguities.
Definition dparser.cpp:332
bool check_term_ProcessInit(const Term &t)
bool check_term_BagComp(const Term &t)
bool check_rule_ProcVarId(const Term &t)
bool check_term_SortFBag(const Term &t)
bool check_rule_PRExpr(const Term &t)
bool check_term_StateYaled(const Term &t)
const atermpp::function_symbol & function_symbol_SortArrow()
bool check_term_MultActName(const Term &t)
bool check_term_Nu(const Term &t)
bool check_term_PBESExists(const Term &t)
bool check_term_BInit(const Term &t)
bool check_term_ProcessAssignment(const Term &t)
bool check_term_Lambda(const Term &t)
bool check_term_StateMay(const Term &t)
bool check_term_PRESAnd(const Term &t)
bool check_term_StateVar(const Term &t)
bool check_term_SortRef(const Term &t)
bool check_term_PRESEqInf(const Term &t)
bool check_rule_StateFrm(const Term &t)
bool check_term_ProcSpec(const Term &t)
bool check_term_SortBag(const Term &t)
bool check_term_ProcEqn(const Term &t)
bool check_rule_MultActName(const Term &t)
bool check_term_StatePlus(const Term &t)
bool check_term_TimedMultAct(const Term &t)
bool check_term_PRESInfimum(const Term &t)
bool check_term_Rename(const Term &t)
bool check_rule_MapSpec(const Term &t)
bool check_rule_ProcEqnSpec(const Term &t)
bool check_rule_ProcEqn(const Term &t)
bool check_rule_PREqn(const Term &t)
bool check_term_StateYaledTimed(const Term &t)
bool check_term_StateImp(const Term &t)
bool check_term_StateConstantMultiply(const Term &t)
bool check_rule_DataVarId(const Term &t)
bool check_rule_UntypedIdentifierAssignment(const Term &t)
bool check_term_SortCons(const Term &t)
bool check_term_PRESSupremum(const Term &t)
bool check_term_PropVarInst(const Term &t)
bool check_term_UntypedRegFrm(const Term &t)
bool check_rule_PBES(const Term &t)
bool check_term_IfThen(const Term &t)
bool check_term_ActForall(const Term &t)
bool check_term_StateTrue(const Term &t)
bool check_term_SortSpec(const Term &t)
bool check_term_StateOr(const Term &t)
bool check_term_Forall(const Term &t)
bool check_term_UntypedSetBagComp(const Term &t)
bool check_term_LinearProcess(const Term &t)
bool check_term_PBInit(const Term &t)
bool check_rule_ProcExpr(const Term &t)
bool check_term_Comm(const Term &t)
bool check_term_StateAnd(const Term &t)
bool check_term_PBESOr(const Term &t)
const atermpp::function_symbol & function_symbol_SortId()
bool check_term_StateMinus(const Term &t)
bool check_term_RenameExpr(const Term &t)
bool check_term_ActExists(const Term &t)
bool check_term_LinearProcessInit(const Term &t)
bool check_rule_SortExpr(const Term &t)
bool check_term_PREqn(const Term &t)
bool check_term_UntypedMultiAction(const Term &t)
bool check_term_PBES(const Term &t)
bool check_rule_GlobVarSpec(const Term &t)
bool check_rule_ActionRenameRuleRHS(const Term &t)
bool check_term_ActAnd(const Term &t)
bool check_rule_DataSpec(const Term &t)
bool check_term_AtTime(const Term &t)
bool check_term_ActSpec(const Term &t)
bool check_term_StateMu(const Term &t)
bool check_rule_LinearProcessSummand(const Term &t)
bool check_rule_StringOrEmpty(const Term &t)
bool check_term_StateNu(const Term &t)
bool check_term_PBEqn(const Term &t)
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)
bool check_term_SetComp(const Term &t)
bool check_term_ActOr(const Term &t)
bool check_term_StructProj(const Term &t)
bool check_term_PRESMinus(const Term &t)
bool check_rule_MultAct(const Term &t)
bool check_term_SortList(const Term &t)
bool check_term_PBEqnSpec(const Term &t)
bool check_rule_LinearProcessInit(const Term &t)
bool check_rule_PBInit(const Term &t)
bool check_term_IfThenElse(const Term &t)
bool check_term_PBESAnd(const Term &t)
bool check_rule_ProcInit(const Term &t)
bool check_term_PBESFalse(const Term &t)
bool check_rule_StructCons(const Term &t)
bool check_term_PRESPlus(const Term &t)
bool check_rule_OpId(const Term &t)
bool check_term_PropVarDecl(const Term &t)
bool check_term_SortFSet(const Term &t)
bool check_term_PRESCondSm(const Term &t)
bool check_term_Block(const Term &t)
const atermpp::function_symbol & function_symbol_SortCons()
const atermpp::function_symbol & function_symbol_OpId()
bool check_term_StateExists(const Term &t)
bool check_term_ActionRenameRules(const Term &t)
bool check_term_StateConstantMultiplyAlt(const Term &t)
bool check_term_DataAppl(const Term &t)
bool check_term_RegSeq(const Term &t)
bool check_term_PRESImp(const Term &t)
bool check_term_RegAlt(const Term &t)
bool check_rule_PRInit(const Term &t)
apply_builder< Builder > make_apply_builder()
Definition builder.h:116
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
Definition builder.h:233
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
apply_builder_arg1< Builder, Arg1 > make_apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:140
void msg(const std::string &)
Definition builder.h:29
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
Definition builder.h:199
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:164
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:224
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:235
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:246
variable_list parse_variables(const std::string &text)
Definition data.cpp:213
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:203
Namespace for system defined sort bag.
Definition bag1.h:38
function_symbol fbag2fset(const sort_expression &s)
Constructor for function symbol @fbag2fset.
Definition bag1.h:1475
bool is_bag2set_application(const atermpp::aterm &e)
Recogniser for application of Bag2Set.
Definition bag1.h:751
bool is_intersection_function_symbol(const atermpp::aterm &e)
Recogniser for function *.
Definition bag1.h:559
void make_bool2nat_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Bool2Nat_.
Definition bag1.h:1243
application difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol -.
Definition bag1.h:668
const core::identifier_string & fbag2fset_name()
Generate identifier @fbag2fset.
Definition bag1.h:1465
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bag1.h:1636
bool is_min_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @min_.
Definition bag1.h:1029
function_symbol bag_fbag(const sort_expression &s)
Constructor for function symbol @bagfbag.
Definition bag1.h:176
bool is_min_function_application(const atermpp::aterm &e)
Recogniser for application of @min_.
Definition bag1.h:1065
function_symbol monus_function(const sort_expression &s)
Constructor for function symbol @monus_.
Definition bag1.h:1083
const core::identifier_string & fbag_intersect_name()
Generate identifier @fbag_inter.
Definition bag1.h:1329
void make_bag2set(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Bag2Set.
Definition bag1.h:741
bool is_fbag_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_diff.
Definition bag1.h:1417
bool is_fbag_join_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_join.
Definition bag1.h:1281
void make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol count.
Definition bag1.h:336
function_symbol_vector bag_generate_functions_code(const sort_expression &s)
Give all system defined mappings for bag.
Definition bag1.h:1529
application zero_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @zero_.
Definition bag1.h:855
const core::identifier_string & bool2nat_function_name()
Generate identifier @Bool2Nat_.
Definition bag1.h:1199
void make_one_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @one_.
Definition bag1.h:927
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
Definition bag1.h:1684
bool is_difference_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition bag1.h:689
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:612
const core::identifier_string & set2bag_name()
Generate identifier Set2Bag.
Definition bag1.h:759
bool is_bag_fbag_application(const atermpp::aterm &e)
Recogniser for application of @bagfbag.
Definition bag1.h:220
application fbag2fset(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @fbag2fset.
Definition bag1.h:1500
function_symbol_vector bag_generate_constructors_and_functions_code(const sort_expression &s)
Give all system defined mappings and constructors for bag.
Definition bag1.h:1562
void make_add_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @add_.
Definition bag1.h:991
data_equation_vector bag_generate_equations_code(const sort_expression &s)
Give all system defined equations for bag.
Definition bag1.h:1706
bool is_fbag_difference_application(const atermpp::aterm &e)
Recogniser for application of @fbag_diff.
Definition bag1.h:1457
bool is_bag_fbag_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagfbag.
Definition bag1.h:186
const core::identifier_string & zero_function_name()
Generate identifier @zero_.
Definition bag1.h:821
const core::identifier_string & add_function_name()
Generate identifier @add_.
Definition bag1.h:945
application bag2set(const sort_expression &s, const data_expression &arg0)
Application of function symbol Bag2Set.
Definition bag1.h:731
application in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol in.
Definition bag1.h:389
function_symbol_vector bag_mCRL2_usable_constructors(const sort_expression &s)
Give all defined constructors which can be used in mCRL2 specs for bag.
Definition bag1.h:143
bool is_fbag2fset_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag2fset.
Definition bag1.h:1485
bool is_union_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition bag1.h:495
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:707
bool is_monus_function_application(const atermpp::aterm &e)
Recogniser for application of @monus_.
Definition bag1.h:1129
const core::identifier_string & nat2bool_function_name()
Generate identifier @Nat2Bool_.
Definition bag1.h:1137
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:511
bool is_zero_function_application(const atermpp::aterm &e)
Recogniser for application of @zero_.
Definition bag1.h:875
const core::identifier_string & fbag_difference_name()
Generate identifier @fbag_diff.
Definition bag1.h:1397
void make_monus_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @monus_.
Definition bag1.h:1119
implementation_map bag_cpp_implementable_mappings(const sort_expression &s)
Give all system defined mappings that are to be implemented in C++ code for bag.
Definition bag1.h:1612
bool is_count_function_symbol(const atermpp::aterm &e)
Recogniser for function count.
Definition bag1.h:309
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:298
implementation_map bag_cpp_implementable_constructors(const sort_expression &s)
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
Definition bag1.h:156
function_symbol add_function(const sort_expression &s)
Constructor for function symbol @add_.
Definition bag1.h:955
bool is_nat2bool_function_application(const atermpp::aterm &e)
Recogniser for application of @Nat2Bool_.
Definition bag1.h:1191
function_symbol fbag_intersect(const sort_expression &s)
Constructor for function symbol @fbag_inter.
Definition bag1.h:1339
void make_fbag_intersect(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_inter.
Definition bag1.h:1379
bool is_union_function_symbol(const atermpp::aterm &e)
Recogniser for function +.
Definition bag1.h:458
void make_nat2bool_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @Nat2Bool_.
Definition bag1.h:1181
application bag_fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagfbag.
Definition bag1.h:200
bool is_fbag_intersect_application(const atermpp::aterm &e)
Recogniser for application of @fbag_inter.
Definition bag1.h:1389
bool is_in_application(const atermpp::aterm &e)
Recogniser for application of in.
Definition bag1.h:410
function_symbol fbag_difference(const sort_expression &s)
Constructor for function symbol @fbag_diff.
Definition bag1.h:1407
bool is_in_function_symbol(const atermpp::aterm &e)
Recogniser for function in.
Definition bag1.h:373
application bool2nat_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Bool2Nat_.
Definition bag1.h:1233
bool is_bag_comprehension_function_symbol(const atermpp::aterm &e)
Recogniser for function @bagcomp.
Definition bag1.h:248
void make_min_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @min_.
Definition bag1.h:1055
const core::identifier_string & min_function_name()
Generate identifier @min_.
Definition bag1.h:1009
bool is_set2bag_function_symbol(const atermpp::aterm &e)
Recogniser for function Set2Bag.
Definition bag1.h:779
application union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition bag1.h:474
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bag1.h:1624
function_symbol_vector bag_mCRL2_usable_mappings(const sort_expression &s)
Give all system defined mappings that can be used in mCRL2 specs for bag.
Definition bag1.h:1576
bool is_nat2bool_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Nat2Bool_.
Definition bag1.h:1157
application one_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @one_.
Definition bag1.h:917
const core::identifier_string & monus_function_name()
Generate identifier @monus_.
Definition bag1.h:1073
const data_expression & arg4(const data_expression &e)
Function for projecting out argument. arg4 from an application.
Definition bag1.h:1696
bool is_add_function_application(const atermpp::aterm &e)
Recogniser for application of @add_.
Definition bag1.h:1001
void make_fbag2fset(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @fbag2fset.
Definition bag1.h:1511
void make_fbag_join(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_join.
Definition bag1.h:1311
function_symbol min_function(const sort_expression &s)
Constructor for function symbol @min_.
Definition bag1.h:1019
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:769
const core::identifier_string & bag_fbag_name()
Generate identifier @bagfbag.
Definition bag1.h:166
const core::identifier_string & bag2set_name()
Generate identifier Bag2Set.
Definition bag1.h:697
const core::identifier_string & intersection_name()
Generate identifier *.
Definition bag1.h:503
application nat2bool_function(const sort_expression &s, const data_expression &arg0)
Application of function symbol @Nat2Bool_.
Definition bag1.h:1171
void make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol in.
Definition bag1.h:400
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @bag.
Definition bag1.h:103
application fbag_intersect(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_inter.
Definition bag1.h:1366
function_symbol bag_comprehension(const sort_expression &s)
Constructor for function symbol @bagcomp.
Definition bag1.h:238
bool is_bag2set_function_symbol(const atermpp::aterm &e)
Recogniser for function Bag2Set.
Definition bag1.h:717
bool is_bool2nat_function_application(const atermpp::aterm &e)
Recogniser for application of @Bool2Nat_.
Definition bag1.h:1253
const core::identifier_string & fbag_join_name()
Generate identifier @fbag_join.
Definition bag1.h:1261
void make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol *.
Definition bag1.h:586
function_symbol fbag_join(const sort_expression &s)
Constructor for function symbol @fbag_join.
Definition bag1.h:1271
bool is_constructor_application(const atermpp::aterm &e)
Recogniser for application of @bag.
Definition bag1.h:124
bool is_zero_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @zero_.
Definition bag1.h:841
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:78
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition bag1.h:1672
const core::identifier_string & constructor_name()
Generate identifier @bag.
Definition bag1.h:68
bool is_bag_comprehension_application(const atermpp::aterm &e)
Recogniser for application of @bagcomp.
Definition bag1.h:282
bool is_set2bag_application(const atermpp::aterm &e)
Recogniser for application of Set2Bag.
Definition bag1.h:813
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:362
void make_zero_function(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @zero_.
Definition bag1.h:865
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition bag1.h:1660
void make_bag_fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagfbag.
Definition bag1.h:210
function_symbol bool2nat_function(const sort_expression &s)
Constructor for function symbol @Bool2Nat_.
Definition bag1.h:1209
void make_set2bag(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol Set2Bag.
Definition bag1.h:803
const core::identifier_string & union_name()
Generate identifier +.
Definition bag1.h:418
bool is_fbag_intersect_function_symbol(const atermpp::aterm &e)
Recogniser for function @fbag_inter.
Definition bag1.h:1349
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:426
bool is_intersection_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition bag1.h:596
void make_bag_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)
Make an application of function symbol @bagcomp.
Definition bag1.h:272
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bag1.h:1648
void make_fbag_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Make an application of function symbol @fbag_diff.
Definition bag1.h:1447
const core::identifier_string & count_name()
Generate identifier count.
Definition bag1.h:290
void make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol +.
Definition bag1.h:485
function_symbol nat2bool_function(const sort_expression &s)
Constructor for function symbol @Nat2Bool_.
Definition bag1.h:1147
bool is_one_function_application(const atermpp::aterm &e)
Recogniser for application of @one_.
Definition bag1.h:937
application fbag_difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_diff.
Definition bag1.h:1434
application add_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @add_.
Definition bag1.h:980
const core::identifier_string & difference_name()
Generate identifier -.
Definition bag1.h:604
application set2bag(const sort_expression &s, const data_expression &arg0)
Application of function symbol Set2Bag.
Definition bag1.h:793
bool is_bool2nat_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @Bool2Nat_.
Definition bag1.h:1219
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag1.h:55
application monus_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus_.
Definition bag1.h:1108
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:44
bool is_difference_function_symbol(const atermpp::aterm &e)
Recogniser for function -.
Definition bag1.h:652
bool is_fbag2fset_application(const atermpp::aterm &e)
Recogniser for application of @fbag2fset.
Definition bag1.h:1521
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
Definition bag1.h:151
application intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition bag1.h:575
const core::identifier_string & in_name()
Generate identifier in.
Definition bag1.h:354
bool is_constructor_function_symbol(const atermpp::aterm &e)
Recogniser for function @bag.
Definition bag1.h:88
const core::identifier_string & bag_comprehension_name()
Generate identifier @bagcomp.
Definition bag1.h:228
bool is_count_application(const atermpp::aterm &e)
Recogniser for application of count.
Definition bag1.h:346
void make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol -.
Definition bag1.h:679
application fbag_join(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @fbag_join.
Definition bag1.h:1298
const core::identifier_string & one_function_name()
Generate identifier @one_.
Definition bag1.h:883
bool is_add_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @add_.
Definition bag1.h:965
void make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Make an application of function symbol @bag.
Definition bag1.h:114
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:831
bool is_one_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @one_.
Definition bag1.h:903
application bag_comprehension(const sort_expression &s, const data_expression &arg0)
Application of function symbol @bagcomp.
Definition bag1.h:262
function_symbol one_function(const sort_expression &s)
Constructor for function symbol @one_.
Definition bag1.h:893
application count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol count.
Definition bag1.h:325
application min_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @min_.
Definition bag1.h:1044
function_symbol_vector bag_generate_constructors_code(const sort_expression &s)
Give all system defined constructors for bag.
Definition bag1.h:132
bool is_fbag_join_application(const atermpp::aterm &e)
Recogniser for application of @fbag_join.
Definition bag1.h:1321
bool is_monus_function_function_symbol(const atermpp::aterm &e)
Recogniser for function @monus_.
Definition bag1.h:1093
Namespace for system defined sort bool_.
Definition bool.h:32
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:197
application and_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol &&.
Definition bool.h:260
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
Namespace for system defined sort fbag.
Definition fbag1.h:37
application fset2fbag(const sort_expression &s, const data_expression &arg0)
Application of function symbol @fset2fbag.
Definition fbag1.h:495
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
application cinsert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_cinsert.
Definition fbag1.h:303
application cons_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fbag_cons.
Definition fbag1.h:237
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:77
Namespace for system defined sort fset.
Definition fset1.h:35
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
application cinsert(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol @fset_cinsert.
Definition fset1.h:297
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
Namespace for system defined sort nat.
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:108
application minimum(const data_expression &arg0, const data_expression &arg1)
Application of function symbol min.
Definition nat1.h:547
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
application swap_zero(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @swap_zero.
Definition nat1.h:1420
application pos2nat(const data_expression &arg0)
Application of function symbol Pos2Nat.
Definition nat1.h:324
application cnat(const data_expression &arg0)
Application of function symbol @cNat.
Definition nat1.h:164
application swap_zero_add(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_add.
Definition nat1.h:1486
application swap_zero_min(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_min.
Definition nat1.h:1554
application monus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol @monus.
Definition nat1.h:1356
application plus(const data_expression &arg0, const data_expression &arg1)
Application of function symbol +.
Definition nat1.h:882
application swap_zero_monus(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
Application of function symbol @swap_zero_monus.
Definition nat1.h:1622
application nat2pos(const data_expression &arg0)
Application of function symbol Nat2Pos.
Definition nat1.h:386
Namespace for system defined sort pos.
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:78
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
Namespace for system defined sort set_.
Definition set1.h:36
function_symbol true_function(const sort_expression &s)
Constructor for function symbol @true_.
Definition set1.h:729
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:667
application constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
Application of function symbol @set.
Definition set1.h:101
Namespace for all data library functionality.
Definition data.cpp:22
void make_data_expression(data_expression &result)
atermpp::term_list< assignment_expression > assignment_expression_list
\brief list of assignment_expressions
Definition assignment.h:50
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
void make_function_symbol(atermpp::aterm &t, const ARGUMENTS &... args)
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
Definition data.cpp:83
std::string pp(const data::untyped_set_or_bag_comprehension_binder &x)
Definition data.cpp:78
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:343
std::string pp(const data::set_comprehension_binder &x)
Definition data.cpp:67
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
Definition data.cpp:85
std::string pp(const data::exists &x)
Definition data.cpp:54
bool is_greater_function_symbol(const DataExpression &e)
Recogniser for function >
Definition standard.h:323
std::string pp(const data::untyped_sort_variable &x)
Definition data.cpp:80
atermpp::term_list< function_sort > function_sort_list
list of function sorts
std::string pp(const data::untyped_set_or_bag_comprehension &x)
Definition data.cpp:77
std::string pp(const data::assignment_expression &x)
Definition data.cpp:43
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
data::data_equation_list normalize_sorts(const data::data_equation_list &x, const data::sort_specification &sortspec)
Definition data.cpp:84
std::string pp(const data::function_symbol_list &x)
Definition data.cpp:33
void normalize_sorts(T &x, const data::sort_specification &sort_spec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_data_equation(const atermpp::aterm &t)
Recognizer function.
variable_list free_variables(const data_expression &x)
Definition data.cpp:195
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
void swap(container_sort &t1, container_sort &t2)
\brief swap overload
std::string pp(const data::set_container &x)
Definition data.cpp:68
bool is_set_container(const atermpp::aterm &x)
std::string pp(const data::abstraction &x)
Definition data.cpp:39
std::string pp(const data::application &x)
Definition data.cpp:41
std::string pp(const data::bag_comprehension_binder &x)
Definition data.cpp:45
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
Definition standard.h:388
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
Definition data.cpp:95
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
std::string pp(const data::fbag_container &x)
Definition data.cpp:56
bool is_application_no_check(const atermpp::aterm &x)
Returns true if the term t is an application, but it does not check whether an application symbol of ...
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
std::vector< sort_expression > sort_expression_vector
\brief vector of sort_expressions
bool is_equal_to_function_symbol(const DataExpression &e)
Recogniser for function ==.
Definition standard.h:135
data_expression_list make_data_expression_list(Container const &r, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
Converts an container with data expressions to data_expression_list.
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
Definition data.cpp:92
void swap(list_container &t1, list_container &t2)
\brief swap overload
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:90
std::string pp(const data::untyped_data_parameter &x)
Definition data.cpp:73
std::string pp(const data::fset_container &x)
Definition data.cpp:59
bool is_application(const data_expression &t)
Returns true if the term t is an application.
bool is_list_container(const atermpp::aterm &x)
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:232
void make_basic_sort(atermpp::aterm &t, const ARGUMENTS &... args)
Definition basic_sort.h:66
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.
atermpp::term_list< function_symbol > function_symbol_list
\brief list of function_symbols
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:192
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
std::string pp(const data::untyped_identifier_assignment &x)
Definition data.cpp:75
std::string pp(const data::lambda &x)
Definition data.cpp:62
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
std::string pp(const data::container_sort &x)
Definition data.cpp:49
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
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:295
std::vector< container_sort > container_sort_vector
list of function sorts
std::string pp(const data::variable &x)
Definition data.cpp:81
std::string pp(const data::untyped_sort &x)
Definition data.cpp:79
void swap(fset_container &t1, fset_container &t2)
\brief swap overload
void swap(alias &t1, alias &t2)
\brief swap overload
Definition alias.h:100
std::string pp(const data::machine_number &x)
Definition data.cpp:65
atermpp::term_list< alias > alias_list
\brief list of aliass
Definition alias.h:72
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:380
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:258
std::string pp(const data::lambda_binder &x)
Definition data.cpp:63
data::data_expression translate_user_notation(const data::data_expression &x)
Definition data.cpp:89
void swap(fbag_container &t1, fbag_container &t2)
\brief swap overload
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
void make_variable(atermpp::aterm &t, const ARGUMENTS &... args)
Definition variable.h:80
application not_equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol !=.
Definition standard.h:181
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
Definition standard.h:219
atermpp::term_list< structured_sort_constructor_argument > structured_sort_constructor_argument_list
\brief list of structured_sort_constructor_arguments
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
data_equation_vector standard_generate_equations_code(const sort_expression &s)
Give all standard system defined equations for sort s.
Definition standard.h:405
std::string pp(const data::data_equation_list &x)
Definition data.cpp:37
std::string pp(const data::data_equation &x)
Definition data.cpp:51
std::string pp(const data::function_sort &x)
Definition data.cpp:60
void swap(sort_expression &t1, sort_expression &t2)
\brief swap overload
atermpp::term_list< sort_expression > sort_expression_list
\brief list of sort_expressions
void swap(set_container &t1, set_container &t2)
\brief swap overload
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
std::set< data::variable > find_all_variables(const data::function_symbol &x)
Definition data.cpp:96
void swap(data_expression &t1, data_expression &t2)
\brief swap overload
std::string pp(const data::bag_comprehension &x)
Definition data.cpp:44
bool is_not_equal_to_function_symbol(const DataExpression &e)
Recogniser for function !=.
Definition standard.h:172
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
Definition alias.h:66
void swap(untyped_sort &t1, untyped_sort &t2)
\brief swap overload
atermpp::term_list< basic_sort > basic_sort_list
list of basic sorts
Definition basic_sort.h:92
std::string pp(const data::exists_binder &x)
Definition data.cpp:55
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:351
void swap(function_symbol &t1, function_symbol &t2)
\brief swap overload
std::string pp(const data::forall_binder &x)
Definition data.cpp:58
std::string pp(const data::structured_sort_constructor_list &x)
Definition data.cpp:35
atermpp::term_list< container_type > container_type_list
\brief list of container_types
std::string pp(const data::untyped_possible_sorts &x)
Definition data.cpp:76
std::vector< container_type > container_type_vector
\brief vector of container_types
std::string pp(const data::data_expression_list &x)
Definition data.cpp:27
std::vector< structured_sort_constructor > structured_sort_constructor_vector
\brief vector of structured_sort_constructors
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
void swap(function_sort &t1, function_sort &t2)
\brief swap overload
std::string pp(const data::assignment_list &x)
Definition data.cpp:29
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
atermpp::term_list< data_equation > data_equation_list
\brief list of data_equations
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
bool is_fset_container(const atermpp::aterm &x)
bool is_less_function_symbol(const DataExpression &e)
Recogniser for function <.
Definition standard.h:249
std::string pp(const data::structured_sort_constructor &x)
Definition data.cpp:71
void swap(container_type &t1, container_type &t2)
\brief swap overload
std::string pp(const data::assignment &x)
Definition data.cpp:42
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
bool is_untyped_sort_variable(const atermpp::aterm &x)
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.
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:91
void swap(data_equation &t1, data_equation &t2)
\brief swap overload
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:101
bool is_if_function_symbol(const DataExpression &e)
Recogniser for function if.
Definition standard.h:209
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:332
std::string pp(const data::bag_container &x)
Definition data.cpp:46
std::set< data::variable > find_all_variables(const data::variable_list &x)
Definition data.cpp:98
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
std::pair< core::identifier_string, sort_expression > function_symbol_key_type
T normalize_sorts(const T &x, const data::sort_specification &sort_spec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:155
std::string pp(const data::structured_sort &x)
Definition data.cpp:70
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
Definition data.cpp:93
atermpp::term_list< variable > variable_list
\brief list of variables
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::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
Definition data.cpp:258
std::string pp(const data::data_specification &x)
Definition data.cpp:53
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:87
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
std::vector< function_sort > function_sort_vector
vector of function sorts
std::string pp(const data::container_type &x)
Definition data.cpp:50
application greater_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >=.
Definition standard.h:369
std::string pp(const data::function_symbol &x)
Definition data.cpp:61
bool is_less_equal_function_symbol(const DataExpression &e)
Recogniser for function <=.
Definition standard.h:286
void make_data_equation(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
bool is_greater_equal_function_symbol(const DataExpression &e)
Recogniser for function >=.
Definition standard.h:360
std::set< data::variable > find_free_variables(const data::data_expression_list &x)
Definition data.cpp:100
std::string pp(const data::basic_sort &x)
Definition data.cpp:47
std::string pp(const data::alias &x)
Definition data.cpp:40
std::string pp(const data::list_container &x)
Definition data.cpp:64
std::string pp(const data::forall &x)
Definition data.cpp:57
void swap(bag_container &t1, bag_container &t2)
\brief swap overload
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
std::string pp(const data::sort_expression &x)
Definition data.cpp:69
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
bool is_bag_container(const atermpp::aterm &x)
void swap(variable &t1, variable &t2)
\brief swap overload
Definition variable.h:105
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
Definition data.cpp:88
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
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.
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:144
bool is_fbag_container(const atermpp::aterm &x)
atermpp::term_list< container_sort > container_sort_list
list of function sorts
std::string pp(const data::structured_sort_constructor_argument &x)
Definition data.cpp:72
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
bool is_untyped_identifier_assignment(const atermpp::aterm &x)
Definition assignment.h:251
bool is_alias(const atermpp::aterm &x)
Definition alias.h:81
std::set< data::variable > find_all_variables(const data::variable &x)
Definition data.cpp:97
bool is_constant(const data_expression &x)
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:269
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
Definition data.cpp:102
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
Definition basic_sort.h:94
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:103
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::set_comprehension &x)
Definition data.cpp:66
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
void swap(basic_sort &t1, basic_sort &t2)
\brief swap overload
Definition basic_sort.h:85
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
std::string pp(const data::variable_list &x)
Definition data.cpp:31
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
Definition data.cpp:185
std::string pp(const data::where_clause &x)
Definition data.cpp:82
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:306
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
std::string pp(const data::data_expression &x)
Definition data.cpp:52
std::string pp(const data::untyped_identifier &x)
Definition data.cpp:74
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
std::string pp(const data::sort_expression_vector &x)
Definition data.cpp:26
std::string pp(const data::binder_type &x)
Definition data.cpp:48
bool is_sort_expression(const atermpp::aterm &x)
Test for a sort_expression expression.
atermpp::term_list< structured_sort_constructor > structured_sort_constructor_list
\brief list of structured_sort_constructors
std::string pp(const data::sort_expression_list &x)
Definition data.cpp:25
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
expression builder that visits all sub expressions
Definition builder.h:42
void update(T &x, typename atermpp::disable_if_container< T >::type *=nullptr)
Definition builder.h:54
void leave(const T &)
Definition builder.h:50
void apply(atermpp::term_list< T > &result, const atermpp::term_list< U > &x)
Definition builder.h:89
void update(std::set< T > &x)
Definition builder.h:75
void enter(const T &)
Definition builder.h:45
static const atermpp::aterm SortFSet
static const atermpp::aterm DataVarId
static const atermpp::aterm SortArrow
static const atermpp::aterm SortExpr
static const atermpp::aterm SortConsType
static const atermpp::aterm SortId
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 SortCons
static const atermpp::aterm SortBag
static const atermpp::aterm OpId
static const atermpp::aterm SortFBag
static const atermpp::aterm SortList
static const atermpp::function_symbol ProcEqnSpec
static const atermpp::function_symbol Lambda
static const atermpp::function_symbol PRInit
static const atermpp::function_symbol PBESTrue
static const atermpp::function_symbol UntypedRegFrm
static const atermpp::function_symbol ProcessInit
static const atermpp::function_symbol PRESTrue
static const atermpp::function_symbol StateMu
static const atermpp::function_symbol PREqnSpec
static const atermpp::function_symbol ActMultAct
static const atermpp::function_symbol RegSeq
static const atermpp::function_symbol Rename
static const atermpp::function_symbol BagComp
static const atermpp::function_symbol StateConstantMultiply
static const atermpp::function_symbol ActNot
static const atermpp::function_symbol Allow
static const atermpp::function_symbol StateSum
static const atermpp::function_symbol ActionRenameRules
static const atermpp::function_symbol ProcEqn
static const atermpp::function_symbol ActAnd
static const atermpp::function_symbol PRESCondEq
static const atermpp::function_symbol Forall
static const atermpp::function_symbol Delta
static const atermpp::function_symbol PropVarDecl
static const atermpp::function_symbol DataEqn
static const atermpp::function_symbol UntypedDataParameter
static const atermpp::function_symbol StructProj
static const atermpp::function_symbol ProcessAssignment
static const atermpp::function_symbol ActSpec
static const atermpp::function_symbol PRESImp
static const atermpp::function_symbol StateConstantMultiplyAlt
static const atermpp::function_symbol MultAct
static const atermpp::function_symbol Whr
static const atermpp::function_symbol SortFSet
static const atermpp::function_symbol IfThenElse
static const atermpp::function_symbol StateForall
static const atermpp::function_symbol PBESForall
static const atermpp::function_symbol StateOr
static const atermpp::function_symbol PRES
static const atermpp::function_symbol ActFalse
static const atermpp::function_symbol PBESFalse
static const atermpp::function_symbol RegTransOrNil
static const atermpp::function_symbol Hide
static const atermpp::function_symbol PRESEqInf
static const atermpp::function_symbol UntypedProcessAssignment
static const atermpp::function_symbol StateYaledTimed
static const atermpp::function_symbol SortList
static const atermpp::function_symbol Exists
static const atermpp::function_symbol ActId
static const atermpp::function_symbol TimedMultAct
static const atermpp::function_symbol StateExists
static const atermpp::function_symbol ActExists
static const atermpp::function_symbol ProcVarId
static const atermpp::function_symbol ConsSpec
static const atermpp::function_symbol BInit
static const atermpp::function_symbol RenameExpr
static const atermpp::function_symbol UntypedMultiAction
static const atermpp::function_symbol PRESMinus
static const atermpp::function_symbol PBES
static const atermpp::function_symbol StructCons
static const atermpp::function_symbol StochasticOperator
static const atermpp::function_symbol StateVar
static const atermpp::function_symbol StateTrue
static const atermpp::function_symbol LinProcSpec
static const atermpp::function_symbol SortRef
static const atermpp::function_symbol StateFalse
static const atermpp::function_symbol Choice
static const atermpp::function_symbol SortArrow
static const atermpp::function_symbol OpId
static const atermpp::function_symbol SortFBag
static const atermpp::function_symbol StateImp
static const atermpp::function_symbol Sync
static const atermpp::function_symbol Sum
static const atermpp::function_symbol PRESEqNInf
static const atermpp::function_symbol PBESNot
static const atermpp::function_symbol ProcSpec
static const atermpp::function_symbol MapSpec
static const atermpp::function_symbol PRESCondSm
static const atermpp::function_symbol RegAlt
static const atermpp::function_symbol RegTrans
static const atermpp::function_symbol Action
static const atermpp::function_symbol StateMinus
static const atermpp::function_symbol SetComp
static const atermpp::function_symbol PBESImp
static const atermpp::function_symbol StateNot
static const atermpp::function_symbol CommExpr
static const atermpp::function_symbol Comm
static const atermpp::function_symbol SortCons
static const atermpp::function_symbol SortSet
static const atermpp::function_symbol PBESAnd
static const atermpp::function_symbol AtTime
static const atermpp::function_symbol Nu
static const atermpp::function_symbol Binder
static const atermpp::function_symbol StateInfimum
static const atermpp::function_symbol SortSpec
static const atermpp::function_symbol StateDelay
static const atermpp::function_symbol PRESOr
static const atermpp::function_symbol StateYaled
static const atermpp::function_symbol MultActName
static const atermpp::function_symbol ActAt
static const atermpp::function_symbol PropVarInst
static const atermpp::function_symbol PBInit
static const atermpp::function_symbol StateMay
static const atermpp::function_symbol LinearProcess
static const atermpp::function_symbol Process
static const atermpp::function_symbol SortStruct
static const atermpp::function_symbol StateDelayTimed
static const atermpp::function_symbol ActImp
static const atermpp::function_symbol ActTrue
static const atermpp::function_symbol Merge
static const atermpp::function_symbol ActForall
static const atermpp::function_symbol LinearProcessInit
static const atermpp::function_symbol Block
static const atermpp::function_symbol Seq
static const atermpp::function_symbol ActionRenameRule
static const atermpp::function_symbol Mu
static const atermpp::function_symbol PRESSupremum
static const atermpp::function_symbol StatePlus
static const atermpp::function_symbol UntypedSortsPossible
static const atermpp::function_symbol IfThen
static const atermpp::function_symbol LinearProcessSummand
static const atermpp::function_symbol StateMust
static const atermpp::function_symbol PBESExists
static const atermpp::function_symbol DataVarId
static const atermpp::function_symbol ActionRenameSpec
static const atermpp::function_symbol DataSpec
static const atermpp::function_symbol SortId
static const atermpp::function_symbol GlobVarSpec
static const atermpp::function_symbol UntypedIdentifier
static const atermpp::function_symbol StateNu
static const atermpp::function_symbol PBESOr
static const atermpp::function_symbol Distribution
static const atermpp::function_symbol UntypedSortVariable
static const atermpp::function_symbol DataVarIdInit
static const atermpp::function_symbol PREqn
static const atermpp::function_symbol StateAnd
static const atermpp::function_symbol PRESPlus
static const atermpp::function_symbol SortBag
static const atermpp::function_symbol PRESInfimum
static const atermpp::function_symbol PBEqnSpec
static const atermpp::function_symbol PRESFalse
static const atermpp::function_symbol ActOr
static const atermpp::function_symbol DataEqnSpec
static const atermpp::function_symbol PRESConstantMultiply
static const atermpp::function_symbol UntypedIdentifierAssignment
static const atermpp::function_symbol PRESConstantMultiplyAlt
static const atermpp::function_symbol UntypedSetBagComp
static const atermpp::function_symbol StateSupremum
static const atermpp::function_symbol PBEqn
static const atermpp::function_symbol UntypedSortUnknown
static const atermpp::function_symbol PRESSum
static const atermpp::function_symbol PRESAnd
static const atermpp::function_symbol RegNil
static const atermpp::function_symbol LMerge
static const atermpp::function_symbol Tau
Wrapper for D_ParseNode.
Definition dparser.h:86
Wrapper for D_Parser and its corresponding D_ParserTables.
Definition dparser.h:148
parse_node parse(const std::string &text, unsigned int start_symbol_index=0, bool partial_parses=false)
Parses a string. N.B. The user is responsible for destruction of the returned value by calling destro...
Definition dparser.cpp:209
parser(D_ParserTables &tables, D_AmbiguityFn ambiguity_fn=nullptr, D_SyntaxErrorFn syntax_error_fn=nullptr, std::size_t max_error_message_count=1)
Definition dparser.cpp:174
unsigned int start_symbol_index(const std::string &name) const
Definition dparser.cpp:204
void apply(T &result, const argument_type &x)
Definition builder.h:186
Builder< update_apply_builder< Builder, Function > > super
Definition builder.h:174
update_apply_builder(const Function &f)
Definition builder.h:192
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:563
void apply(T &result, const data::machine_number &x)
Definition builder.h:487
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:518
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:635
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:572
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:498
void apply(T &result, const data::data_equation &x)
Definition builder.h:581
void apply(T &result, const data::function_symbol &x)
Definition builder.h:454
void apply(T &result, const data::assignment &x)
Definition builder.h:509
void apply(T &result, const data::abstraction &x)
Definition builder.h:651
void apply(T &result, const data::forall &x)
Definition builder.h:527
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:590
void apply(T &result, const data::exists &x)
Definition builder.h:536
void apply(T &result, const data::where_clause &x)
Definition builder.h:478
void apply(T &result, const data::application &x)
Definition builder.h:465
void apply(T &result, const data::variable &x)
Definition builder.h:443
void apply(T &result, const data::data_expression &x)
Definition builder.h:599
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:554
void apply(T &result, const data::lambda &x)
Definition builder.h:545
void apply(T &result, const data::assignment &x)
Definition builder.h:117
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:231
void apply(T &result, const data::structured_sort_constructor_argument &x)
Definition builder.h:258
void apply(T &result, const data::container_sort &x)
Definition builder.h:146
void apply(T &result, const data::alias &x)
Definition builder.h:276
void apply(T &result, const data::exists &x)
Definition builder.h:213
void apply(T &result, const data::machine_number &x)
Definition builder.h:95
void apply(T &result, const data::function_symbol &x)
Definition builder.h:64
void apply(T &result, const data::untyped_possible_sorts &x)
Definition builder.h:184
void apply(T &result, const data::forall &x)
Definition builder.h:204
void apply(T &result, const data::basic_sort &x)
Definition builder.h:135
Builder< Derived > super
Definition builder.h:48
void apply(T &result, const data::data_equation &x)
Definition builder.h:285
void apply(T &result, const data::untyped_sort &x)
Definition builder.h:173
void apply(T &result, const data::abstraction &x)
Definition builder.h:391
void apply(T &result, const data::application &x)
Definition builder.h:73
void apply(T &result, const data::variable &x)
Definition builder.h:55
void apply(T &result, const data::structured_sort &x)
Definition builder.h:155
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:126
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:294
void apply(T &result, const data::function_sort &x)
Definition builder.h:164
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:106
void apply(T &result, const data::structured_sort_constructor &x)
Definition builder.h:267
void apply(T &result, const data::lambda &x)
Definition builder.h:222
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:249
void apply(T &result, const data::where_clause &x)
Definition builder.h:86
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:339
void apply(T &result, const data::data_expression &x)
Definition builder.h:303
void apply(T &result, const data::sort_expression &x)
Definition builder.h:355
void apply(T &result, const data::untyped_sort_variable &x)
Definition builder.h:193
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:240
void apply(T &result, const data::abstraction &x)
Definition builder.h:910
void apply(T &result, const data::application &x)
Definition builder.h:724
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:849
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:757
void apply(T &result, const data::data_expression &x)
Definition builder.h:858
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:894
void apply(T &result, const data::where_clause &x)
Definition builder.h:737
Builder< Derived > super
Definition builder.h:695
void apply(T &result, const data::forall &x)
Definition builder.h:786
void apply(T &result, const data::function_symbol &x)
Definition builder.h:713
void apply(T &result, const data::exists &x)
Definition builder.h:795
void apply(T &result, const data::lambda &x)
Definition builder.h:804
void apply(T &result, const data::variable &x)
Definition builder.h:702
void apply(T &result, const data::assignment &x)
Definition builder.h:768
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:777
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:831
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:813
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:822
void apply(T &result, const data::machine_number &x)
Definition builder.h:746
void apply(T &result, const data::data_equation &x)
Definition builder.h:840
data_expression_actions(const core::parser &parser_)
Definition parse_impl.h:141
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:211
data_specification_actions(const core::parser &parser_)
Definition parse_impl.h:300
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:461
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
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
Definition parse_impl.h:35
\brief Builder class
Definition builder.h:946
std::size_t operator()(const atermpp::aterm &t) const
Definition aterm.h:483
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const
std::size_t operator()(const mcrl2::data::container_type &v) const
std::size_t operator()(const mcrl2::data::data_expression &v) const
std::size_t operator()(const mcrl2::data::function_sort &v) const
std::size_t operator()(const mcrl2::data::sort_expression &x) const
std::size_t operator()(const mcrl2::data::variable &v) const
Definition variable.h:136