12#ifndef MCRL2_DATA_BUILDER_H
13#define MCRL2_DATA_BUILDER_H
18#ifdef MCRL2_ENABLE_MACHINENUMBERS
45template <
template <
class>
class Builder,
class Derived>
58 static_cast<Derived&
>(*this).enter(x);
60 static_cast<Derived&
>(*this).leave(x);
67 static_cast<Derived&
>(*this).enter(x);
69 static_cast<Derived&
>(*this).leave(x);
76 static_cast<Derived&
>(*this).enter(x);
82 static_cast<Derived&
>(*this).leave(x);
89 static_cast<Derived&
>(*this).enter(x);
91 static_cast<Derived&
>(*this).leave(x);
99 static_cast<Derived&
>(*this).enter(x);
101 static_cast<Derived&
>(*this).leave(x);
110 static_cast<Derived&
>(*this).enter(x);
112 static_cast<Derived&
>(*this).leave(x);
120 static_cast<Derived&
>(*this).enter(x);
122 static_cast<Derived&
>(*this).leave(x);
129 static_cast<Derived&
>(*this).enter(x);
131 static_cast<Derived&
>(*this).leave(x);
139 static_cast<Derived&
>(*this).enter(x);
141 static_cast<Derived&
>(*this).leave(x);
149 static_cast<Derived&
>(*this).enter(x);
151 static_cast<Derived&
>(*this).leave(x);
158 static_cast<Derived&
>(*this).enter(x);
160 static_cast<Derived&
>(*this).leave(x);
167 static_cast<Derived&
>(*this).enter(x);
169 static_cast<Derived&
>(*this).leave(x);
177 static_cast<Derived&
>(*this).enter(x);
179 static_cast<Derived&
>(*this).leave(x);
187 static_cast<Derived&
>(*this).enter(x);
189 static_cast<Derived&
>(*this).leave(x);
197 static_cast<Derived&
>(*this).enter(x);
199 static_cast<Derived&
>(*this).leave(x);
207 static_cast<Derived&
>(*this).enter(x);
209 static_cast<Derived&
>(*this).leave(x);
216 static_cast<Derived&
>(*this).enter(x);
218 static_cast<Derived&
>(*this).leave(x);
225 static_cast<Derived&
>(*this).enter(x);
227 static_cast<Derived&
>(*this).leave(x);
234 static_cast<Derived&
>(*this).enter(x);
236 static_cast<Derived&
>(*this).leave(x);
243 static_cast<Derived&
>(*this).enter(x);
245 static_cast<Derived&
>(*this).leave(x);
252 static_cast<Derived&
>(*this).enter(x);
254 static_cast<Derived&
>(*this).leave(x);
261 static_cast<Derived&
>(*this).enter(x);
263 static_cast<Derived&
>(*this).leave(x);
270 static_cast<Derived&
>(*this).enter(x);
272 static_cast<Derived&
>(*this).leave(x);
279 static_cast<Derived&
>(*this).enter(x);
281 static_cast<Derived&
>(*this).leave(x);
288 static_cast<Derived&
>(*this).enter(x);
290 static_cast<Derived&
>(*this).leave(x);
297 static_cast<Derived&
>(*this).enter(x);
299 static_cast<Derived&
>(*this).leave(x);
306 static_cast<Derived&
>(*this).enter(x);
309 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::abstraction>(x));
313 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
317 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::function_symbol>(x));
321 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::application>(x));
325 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::where_clause>(x));
329 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::machine_number>(x));
333 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_identifier>(x));
335 static_cast<Derived&
>(*this).leave(x);
342 static_cast<Derived&
>(*this).enter(x);
345 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::assignment>(x));
349 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_identifier_assignment>(x));
351 static_cast<Derived&
>(*this).leave(x);
358 static_cast<Derived&
>(*this).enter(x);
361 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::basic_sort>(x));
365 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::container_sort>(x));
369 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::structured_sort>(x));
373 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::function_sort>(x));
377 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_sort>(x));
381 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_possible_sorts>(x));
385 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_sort_variable>(x));
387 static_cast<Derived&
>(*this).leave(x);
394 static_cast<Derived&
>(*this).enter(x);
397 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::forall>(x));
401 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::exists>(x));
405 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::lambda>(x));
409 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::set_comprehension>(x));
413 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::bag_comprehension>(x));
417 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
419 static_cast<Derived&
>(*this).leave(x);
425template <
typename Derived>
433template <
template <
class>
class Builder,
class Derived>
447 static_cast<Derived&
>(*this).enter(x);
449 static_cast<Derived&
>(*this).leave(x);
458 static_cast<Derived&
>(*this).enter(x);
460 static_cast<Derived&
>(*this).leave(x);
468 static_cast<Derived&
>(*this).enter(x);
474 static_cast<Derived&
>(*this).leave(x);
481 static_cast<Derived&
>(*this).enter(x);
483 static_cast<Derived&
>(*this).leave(x);
491 static_cast<Derived&
>(*this).enter(x);
493 static_cast<Derived&
>(*this).leave(x);
502 static_cast<Derived&
>(*this).enter(x);
504 static_cast<Derived&
>(*this).leave(x);
512 static_cast<Derived&
>(*this).enter(x);
514 static_cast<Derived&
>(*this).leave(x);
521 static_cast<Derived&
>(*this).enter(x);
523 static_cast<Derived&
>(*this).leave(x);
530 static_cast<Derived&
>(*this).enter(x);
532 static_cast<Derived&
>(*this).leave(x);
539 static_cast<Derived&
>(*this).enter(x);
541 static_cast<Derived&
>(*this).leave(x);
548 static_cast<Derived&
>(*this).enter(x);
550 static_cast<Derived&
>(*this).leave(x);
557 static_cast<Derived&
>(*this).enter(x);
559 static_cast<Derived&
>(*this).leave(x);
566 static_cast<Derived&
>(*this).enter(x);
568 static_cast<Derived&
>(*this).leave(x);
575 static_cast<Derived&
>(*this).enter(x);
577 static_cast<Derived&
>(*this).leave(x);
584 static_cast<Derived&
>(*this).enter(x);
586 static_cast<Derived&
>(*this).leave(x);
593 static_cast<Derived&
>(*this).enter(x);
595 static_cast<Derived&
>(*this).leave(x);
602 static_cast<Derived&
>(*this).enter(x);
605 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::abstraction>(x));
609 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
613 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::function_symbol>(x));
617 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::application>(x));
621 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::where_clause>(x));
625 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::machine_number>(x));
629 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_identifier>(x));
631 static_cast<Derived&
>(*this).leave(x);
638 static_cast<Derived&
>(*this).enter(x);
641 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::assignment>(x));
645 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_identifier_assignment>(x));
647 static_cast<Derived&
>(*this).leave(x);
654 static_cast<Derived&
>(*this).enter(x);
657 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::forall>(x));
661 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::exists>(x));
665 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::lambda>(x));
669 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::set_comprehension>(x));
673 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::bag_comprehension>(x));
677 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
679 static_cast<Derived&
>(*this).leave(x);
685template <
typename Derived>
692template <
template <
class>
class Builder,
class Derived>
706 static_cast<Derived&
>(*this).enter(x);
708 static_cast<Derived&
>(*this).leave(x);
717 static_cast<Derived&
>(*this).enter(x);
719 static_cast<Derived&
>(*this).leave(x);
727 static_cast<Derived&
>(*this).enter(x);
733 static_cast<Derived&
>(*this).leave(x);
740 static_cast<Derived&
>(*this).enter(x);
742 static_cast<Derived&
>(*this).leave(x);
750 static_cast<Derived&
>(*this).enter(x);
752 static_cast<Derived&
>(*this).leave(x);
761 static_cast<Derived&
>(*this).enter(x);
763 static_cast<Derived&
>(*this).leave(x);
771 static_cast<Derived&
>(*this).enter(x);
773 static_cast<Derived&
>(*this).leave(x);
780 static_cast<Derived&
>(*this).enter(x);
782 static_cast<Derived&
>(*this).leave(x);
789 static_cast<Derived&
>(*this).enter(x);
791 static_cast<Derived&
>(*this).leave(x);
798 static_cast<Derived&
>(*this).enter(x);
800 static_cast<Derived&
>(*this).leave(x);
807 static_cast<Derived&
>(*this).enter(x);
809 static_cast<Derived&
>(*this).leave(x);
816 static_cast<Derived&
>(*this).enter(x);
818 static_cast<Derived&
>(*this).leave(x);
825 static_cast<Derived&
>(*this).enter(x);
827 static_cast<Derived&
>(*this).leave(x);
834 static_cast<Derived&
>(*this).enter(x);
836 static_cast<Derived&
>(*this).leave(x);
843 static_cast<Derived&
>(*this).enter(x);
845 static_cast<Derived&
>(*this).leave(x);
852 static_cast<Derived&
>(*this).enter(x);
854 static_cast<Derived&
>(*this).leave(x);
861 static_cast<Derived&
>(*this).enter(x);
864 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::abstraction>(x));
868 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
872 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::function_symbol>(x));
876 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::application>(x));
880 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::where_clause>(x));
884 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::machine_number>(x));
888 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_identifier>(x));
890 static_cast<Derived&
>(*this).leave(x);
897 static_cast<Derived&
>(*this).enter(x);
900 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::assignment>(x));
904 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_identifier_assignment>(x));
906 static_cast<Derived&
>(*this).leave(x);
913 static_cast<Derived&
>(*this).enter(x);
916 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::forall>(x));
920 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::exists>(x));
924 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::lambda>(x));
928 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::set_comprehension>(x));
932 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::bag_comprehension>(x));
936 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_set_or_bag_comprehension>(x));
938 static_cast<Derived&
>(*this).leave(x);
944template <
typename Derived>
add your file description here.
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
const basic_sort & name() const
An application of a data expression to a number of arguments.
const_iterator end() const
Returns an iterator pointing past the last argument of the application.
const_iterator begin() const
Returns an iterator pointing to the first argument of the application.
const data_expression & head() const
Get the function at the head of this expression.
\brief Assignment expression
\brief Assignment of a data expression to a variable
const data_expression & rhs() const
const variable & lhs() const
universal quantification.
const container_type & container_name() const
const data_expression & lhs() const
const data_expression & condition() const
const data_expression & rhs() const
const variable_list & variables() const
existential quantification.
universal quantification.
const sort_expression & codomain() const
const sort_expression_list & domain() const
const core::identifier_string & name() const
universal quantification.
\brief An argument of a constructor of a structured sort
const core::identifier_string & name() const
\brief A constructor for a structured sort
const core::identifier_string & name() const
const core::identifier_string & recogniser() const
const structured_sort_constructor_list & constructors() const
\brief An untyped parameter
const core::identifier_string & name() const
\brief Assignment of a data expression to a string
const core::identifier_string & lhs() const
\brief An untyped identifier
\brief Multiple possible sorts
const sort_expression_list & sorts() const
universal quantification.
\brief Untyped sort variable
\brief Unknown sort expression
const core::identifier_string & name() const
\brief A where expression
const data_expression & body() const
const assignment_expression_list & declarations() const
add your file description here.
The class machine_number, which is a subclass of data_expression.
void make_set_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
void make_function_symbol(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
void make_bag_comprehension(atermpp::aterm &result, ARGUMENTS... arguments)
void make_where_clause(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_data_parameter(atermpp::aterm &t, const ARGUMENTS &... args)
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.
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.
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)
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
void make_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_identifier_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
void make_structured_sort_constructor_argument(atermpp::aterm &t, const ARGUMENTS &... args)
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
void make_lambda(atermpp::aterm &result, ARGUMENTS... arguments)
void make_forall(atermpp::aterm &result, ARGUMENTS... arguments)
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
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.
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)
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
bool is_assignment(const atermpp::aterm &x)
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
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_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
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)
void make_exists(atermpp::aterm &result, ARGUMENTS... arguments)
void make_structured_sort(atermpp::aterm &t, const ARGUMENTS &... args)
void make_container_sort(atermpp::aterm &t, const ARGUMENTS &... args)
void make_function_sort(atermpp::aterm &t, const ARGUMENTS &... args)
void make_structured_sort_constructor(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_possible_sorts(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void make_application(atermpp::aterm &result)
Make function for an application.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::data_equation &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::structured_sort_constructor_argument &x)
void apply(T &result, const data::container_sort &x)
void apply(T &result, const data::alias &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::untyped_possible_sorts &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::basic_sort &x)
void apply(T &result, const data::data_equation &x)
void apply(T &result, const data::untyped_sort &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::structured_sort &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::function_sort &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::structured_sort_constructor &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::sort_expression &x)
void apply(T &result, const data::untyped_sort_variable &x)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::data_equation &x)
The class structured_sort.
add your file description here.
add your file description here.
add your file description here.
add your file description here.