mCRL2
Loading...
Searching...
No Matches
mcrl2::data Namespace Reference

Namespace for all data library functionality. More...

Namespaces

namespace  concepts
 
namespace  detail
 
namespace  lazy
 A collection of utilities for lazy expression construction.
 
namespace  sort_bag
 Namespace for system defined sort bag.
 
namespace  sort_bool
 Namespace for system defined sort bool_.
 
namespace  sort_fbag
 Namespace for system defined sort fbag.
 
namespace  sort_fset
 Namespace for system defined sort fset.
 
namespace  sort_int
 Namespace for system defined sort int_.
 
namespace  sort_list
 Namespace for system defined sort list.
 
namespace  sort_nat
 Namespace for system defined sort nat.
 
namespace  sort_pos
 Namespace for system defined sort pos.
 
namespace  sort_real
 Namespace for system defined sort real_.
 
namespace  sort_set
 Namespace for system defined sort set_.
 
namespace  tools
 

Classes

class  abstraction
 An abstraction expression. More...
 
struct  add_data_expressions
 
struct  add_data_variable_binding
 Maintains a multiset of bound data variables during traversal. More...
 
struct  add_data_variable_builder_binding
 
struct  add_data_variable_traverser_binding
 
struct  add_sort_expressions
 
struct  add_traverser_data_expressions
 
struct  add_traverser_identifier_strings
 
struct  add_traverser_sort_expressions
 
struct  add_traverser_variables
 
struct  add_variables
 
class  alias
 \brief A sort alias More...
 
struct  and_constraint
 
class  application
 An application of a data expression to a number of arguments. More...
 
struct  application_node
 
class  assignment
 \brief Assignment of a data expression to a variable More...
 
class  assignment_expression
 \brief Assignment expression More...
 
struct  assignment_sequence_substitution
 Substitution that maps data variables to data expressions. The substitution is stored as an assignment_list. More...
 
class  bag_comprehension
 universal quantification. More...
 
class  bag_comprehension_binder
 \brief Binder for bag comprehension More...
 
class  bag_container
 \brief Container type for bags More...
 
struct  bag_enumeration_node
 
struct  bag_or_set_enumeration_node
 
class  basic_rewriter
 Rewriter class for the mCRL2 Library. It only works for terms of type data_expression and data_expression_with_variables. More...
 
class  basic_sort
 \brief A basic sort More...
 
struct  binary_operator_node
 
class  binder_type
 \brief Binder More...
 
class  cardinality_calculator
 
struct  constant_node
 
class  container_sort
 \brief A container sort More...
 
class  container_type
 \brief Container type More...
 
class  data_equation
 \brief A data equation More...
 
class  data_expression
 data expression. More...
 
struct  data_expression_assignment
 Substitution that maps a data expression to a data expression. More...
 
struct  data_expression_builder
 \brief Builder class More...
 
struct  data_expression_traverser
 \brief Traverser class More...
 
struct  data_rewriter
 A rewriter that applies a data rewriter to data expressions in a term. More...
 
class  data_specification
 data specification. More...
 
class  data_type_checker
 
class  default_expression_generator
 Expression generator that caches values. More...
 
struct  empty_bag_node
 
struct  empty_list_node
 
struct  empty_set_node
 
class  enumerator_algorithm
 An enumerator algorithm that generates solutions of a condition. More...
 
class  enumerator_algorithm_with_iterator
 An enumerator algorithm with an iterator interface. More...
 
class  enumerator_algorithm_without_callback
 An enumerator algorithm that generates solutions of a condition. More...
 
struct  enumerator_error
 Enumerator exception. More...
 
class  enumerator_identifier_generator
 
class  enumerator_list_element
 The default element for the todo list of the enumerator. More...
 
class  enumerator_list_element_with_substitution
 An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi. More...
 
class  enumerator_queue
 Contains the enumerator queue. More...
 
struct  enumerator_substitution
 Substitution that stores the assignments as a sequence of variables and a sequence of expressions. It supports function composition efficiently. This is done by simply concatenating the variables and expressions of the two substitutions. As a result, evaluating the substitution becomes more expensive. More...
 
class  exists
 existential quantification. More...
 
class  exists_binder
 \brief Binder for existential quantification More...
 
struct  exists_node
 
struct  expression_traits
 expression traits (currently nothing more than core::term_traits) More...
 
struct  false_constraint
 
struct  false_node
 
class  fbag_container
 \brief Container type for finite bags More...
 
class  finiteness_helper
 
class  forall
 universal quantification. More...
 
class  forall_binder
 \brief Binder for universal quantification More...
 
struct  forall_node
 
struct  fourier_motzkin_sigma
 A unary function that can be used in combination with replace_data_expressions to eliminate real numbers from all quantifiers in an expression. It is adviced to first push the quantifiers inside and apply the one point rule, since that reduces the time spent on the Fourier-Motzkin procedure for large expression. Apply this function innermost first if the expresion contains nested quantifiers. More...
 
class  fset_container
 \brief Container type for finite sets More...
 
class  function_sort
 \brief A function sort More...
 
class  function_symbol
 \brief A function symbol More...
 
struct  function_update_node
 
struct  id_node
 
class  identifier_generator
 Abstract base class for identifier generators. Identifier generators generate fresh names that do not appear in a given context. A context is maintained containing already used identifiers. Using the operator()() and operator()(std::string) fresh identifiers are generated that do not appear in the context. More...
 
struct  identifier_string_traverser
 \brief Traverser class More...
 
struct  if_rewriter
 
struct  is_element_of_constraint
 
struct  is_equal_to_constraint
 
struct  is_not_false
 
struct  is_not_true
 
class  lambda
 function symbol. More...
 
class  lambda_binder
 \brief Binder for lambda abstraction More...
 
struct  lambda_node
 
class  linear_inequality
 
class  list_container
 \brief Container type for lists More...
 
struct  list_enumeration_node
 
class  maintain_variables_in_rhs
 Wrapper that extends any substitution to a substitution maintaining the vars in its rhs. More...
 
struct  map_substitution
 Generic substitution function. The substitution is stored as a mapping of variables to expressions. More...
 
class  multiset_identifier_generator
 Identifier generator that stores the identifiers of the context in a multiset. If an identifier occurs multiple times, multiple calls to remove_from_context are required to remove it. Using the operator()() and operator()(std::string) fresh identifiers can be generated that do not appear in the context. More...
 
class  mutable_indexed_substitution
 Generic substitution function. More...
 
class  mutable_map_substitution
 Generic substitution function. The substitution is stored as a mapping of variables to expressions. The substitution is mutable, meaning that substitutions to variables can be added and removed as follows: More...
 
class  mutable_substitution_composer
 An adapter that makes an arbitrary substitution function mutable. More...
 
class  mutable_substitution_composer< mutable_indexed_substitution< VariableType, ExpressionSequence > >
 Specialization for mutable_indexed_substitution. More...
 
class  mutable_substitution_composer< mutable_map_substitution< AssociativeContainer > >
 Specialization for mutable_map_substitution. More...
 
struct  no_substitution
 An empty struct that is used to denote the absence of a substitution. Used for rewriters. More...
 
struct  number_node
 
struct  one_point_rule_rewriter
 
struct  or_constraint
 
struct  quantifiers_inside_rewriter
 
class  representative_generator
 Components for generating an arbitrary element of a sort. More...
 
class  rewriter
 Rewriter that operates on data expressions. More...
 
struct  sequence_sequence_substitution
 Generic substitution function. The substitution is stored as a sequence of variables and a sequence of expressions. More...
 
class  set_comprehension
 universal quantification. More...
 
class  set_comprehension_binder
 \brief Binder for set comprehension More...
 
class  set_container
 \brief Container type for sets More...
 
struct  set_enumeration_node
 
class  set_identifier_generator
 Identifier generator that stores the identifiers of the context in a set. Using the operator()() and operator()(std::string) fresh identifiers can be generated that do not appear in the context. More...
 
struct  simplify_rewriter
 
class  sort_expression
 \brief A sort expression More...
 
struct  sort_expression_assignment
 Substitution that maps a sort expression to a sort expression. More...
 
struct  sort_expression_builder
 \brief Builder class More...
 
struct  sort_expression_traverser
 \brief Traverser class More...
 
class  sort_specification
 
class  sort_type_checker
 
struct  stream_printer
 Prints the object x to a stream. More...
 
class  structured_sort
 structured sort. More...
 
class  structured_sort_constructor
 \brief A constructor for a structured sort More...
 
class  structured_sort_constructor_argument
 \brief An argument of a constructor of a structured sort More...
 
struct  subsort_constraint
 
struct  true_constraint
 
struct  true_node
 
struct  type_check_constraint
 
struct  type_check_context
 
struct  type_check_node
 
struct  type_check_tree_generator
 
class  type_checker
 
struct  unary_operator_node
 
class  untyped_data_parameter
 \brief An untyped parameter More...
 
struct  untyped_data_specification
 
class  untyped_identifier
 \brief An untyped identifier More...
 
class  untyped_identifier_assignment
 \brief Assignment of a data expression to a string More...
 
class  untyped_possible_sorts
 \brief Multiple possible sorts More...
 
class  untyped_set_or_bag_comprehension
 universal quantification. More...
 
class  untyped_set_or_bag_comprehension_binder
 \brief Binder for untyped set or bag comprehension More...
 
class  untyped_sort
 \brief Unknown sort expression More...
 
class  untyped_sort_variable
 \brief Untyped sort variable More...
 
class  used_data_equation_selector
 Component for selecting a subset of equations that are actually used in an encompassing specification. More...
 
class  variable
 \brief A data variable More...
 
struct  variable_builder
 \brief Builder class More...
 
struct  variable_substitution
 Substitution that maps a single variable to a data expression. More...
 
struct  variable_traverser
 \brief Traverser class More...
 
class  where_clause
 \brief A where expression More...
 
struct  where_clause_node
 
class  xyz_identifier_generator
 Identifier generator that generates names from the range X, Y, Z, X0, Y0, Z0, X1, ... More...
 

Typedefs

typedef atermpp::term_list< aliasalias_list
 \brief list of aliass
 
typedef std::vector< aliasalias_vector
 \brief vector of aliass
 
typedef atermpp::term_list< assignment_expressionassignment_expression_list
 \brief list of assignment_expressions
 
typedef std::vector< assignment_expressionassignment_expression_vector
 \brief vector of assignment_expressions
 
typedef atermpp::term_list< assignmentassignment_list
 \brief list of assignments
 
typedef std::vector< assignmentassignment_vector
 \brief vector of assignments
 
typedef atermpp::term_list< untyped_identifier_assignmentuntyped_identifier_assignment_list
 \brief list of untyped_identifier_assignments
 
typedef std::vector< untyped_identifier_assignmentuntyped_identifier_assignment_vector
 \brief vector of untyped_identifier_assignments
 
typedef atermpp::term_list< basic_sortbasic_sort_list
 list of basic sorts
 
typedef std::vector< basic_sortbasic_sort_vector
 vector of basic sorts
 
typedef atermpp::term_list< binder_typebinder_type_list
 \brief list of binder_types
 
typedef std::vector< binder_typebinder_type_vector
 \brief vector of binder_types
 
typedef atermpp::term_list< container_sortcontainer_sort_list
 list of function sorts
 
typedef std::vector< container_sortcontainer_sort_vector
 list of function sorts
 
typedef atermpp::term_list< container_typecontainer_type_list
 \brief list of container_types
 
typedef std::vector< container_typecontainer_type_vector
 \brief vector of container_types
 
typedef atermpp::term_list< data_equationdata_equation_list
 \brief list of data_equations
 
typedef std::vector< data_equationdata_equation_vector
 \brief vector of data_equations
 
typedef atermpp::term_list< data_expressiondata_expression_list
 \brief list of data_expressions
 
typedef std::vector< data_expressiondata_expression_vector
 \brief vector of data_expressions
 
typedef atermpp::term_list< variablevariable_list
 \brief list of variables
 
typedef std::map< untyped_sort_variable, sort_expressionsort_substitution
 
typedef std::pair< sort_substitution, int > solution
 
typedef std::shared_ptr< type_check_nodetype_check_node_ptr
 
typedef std::shared_ptr< type_check_constraintconstraint_ptr
 
typedef atermpp::term_list< function_sortfunction_sort_list
 list of function sorts
 
typedef std::vector< function_sortfunction_sort_vector
 vector of function sorts
 
typedef std::pair< core::identifier_string, sort_expressionfunction_symbol_key_type
 
typedef atermpp::term_list< function_symbolfunction_symbol_list
 \brief list of function_symbols
 
typedef std::vector< function_symbolfunction_symbol_vector
 \brief vector of function_symbols
 
typedef std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > > implementation_map
 
typedef atermpp::term_list< sort_expressionsort_expression_list
 \brief list of sort_expressions
 
typedef std::vector< sort_expressionsort_expression_vector
 \brief vector of sort_expressions
 
typedef atermpp::term_list< structured_sortstructured_sort_list
 \brief list of structured_sorts
 
typedef std::vector< structured_sortstructured_sort_vector
 \brief vector of structured_sorts
 
typedef atermpp::term_list< structured_sort_constructorstructured_sort_constructor_list
 \brief list of structured_sort_constructors
 
typedef std::vector< structured_sort_constructorstructured_sort_constructor_vector
 \brief vector of structured_sort_constructors
 
typedef atermpp::term_list< structured_sort_constructor_argumentstructured_sort_constructor_argument_list
 \brief list of structured_sort_constructor_arguments
 
typedef std::vector< structured_sort_constructor_argumentstructured_sort_constructor_argument_vector
 \brief vector of structured_sort_constructor_arguments
 
typedef atermpp::term_list< sort_expression_listsorts_list
 
typedef atermpp::term_list< untyped_data_parameteruntyped_data_parameter_list
 \brief list of untyped_data_parameters
 
typedef std::vector< untyped_data_parameteruntyped_data_parameter_vector
 \brief vector of untyped_data_parameters
 
typedef std::vector< variablevariable_vector
 \brief vector of variables
 

Enumerations

enum  rewrite_strategy { jitty , jitty_prover }
 The strategy of the rewriter. More...
 

Functions

template<class... ARGUMENTS>
void make_abstraction (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const abstraction &x)
 
std::ostream & operator<< (std::ostream &out, const abstraction &x)
 
void swap (abstraction &t1, abstraction &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_alias (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
bool is_alias (const atermpp::aterm_appl &x)
 
std::string pp (const alias &x)
 
std::ostream & operator<< (std::ostream &out, const alias &x)
 
void swap (alias &t1, alias &t2)
 \brief swap overload
 
void anonymize (data_specification &dataspec)
 
void swap (application &t1, application &t2)
 swap overload
 
void make_application (atermpp::aterm &result)
 Make function for an application.
 
template<typename HEAD , typename TERM , typename ... Terms, typename = std::enable_if_t< std::disjunction<typename std::is_convertible<HEAD, data_expression>, typename std::is_invocable_r<void, HEAD, data_expression&>, typename std::is_invocable_r<const data_expression, HEAD, void> >::value >, typename = std::enable_if_t<std::conjunction_v< std::disjunction<typename std::is_convertible<Terms, data_expression>, typename std::is_invocable_r<void, Terms, data_expression&>, typename std::is_invocable_r<const data_expression, Terms, void> > ...>>>
void make_application (atermpp::aterm &result, const HEAD &head, const TERM &arg1, const Terms &...other_arguments)
 Constructor.
 
template<typename Container >
void make_application (data_expression &result, const data_expression &head, const Container &arguments, typename atermpp::enable_if_container< Container, data_expression >::type *=nullptr)
 Constructor.
 
template<typename FwdIter >
void make_application (atermpp::aterm &result, const data_expression &head, FwdIter first, FwdIter last, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=nullptr)
 Constructor.
 
template<typename FwdIter >
void make_application (atermpp::aterm &result, const std::size_t arity, const data_expression &head, FwdIter first, FwdIter last, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=0)
 Constructor.
 
template<typename FwdIter , class ArgumentConverter >
void make_application (atermpp::aterm &result, const data_expression &head, FwdIter first, FwdIter last, ArgumentConverter convert_arguments, const bool skip_first_argument=false, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=nullptr, typename std::enable_if< !std::is_base_of< data_expression, ArgumentConverter >::value >::type *=nullptr, typename std::enable_if< std::is_same< typename std::invoke_result< ArgumentConverter, typename FwdIter::value_type >::type, data_expression >::value >::type *=nullptr)
 Constructor.
 
template<typename FwdIter , class ArgumentConverter >
static void make_application (atermpp::aterm &result, const data_expression &head, FwdIter first, FwdIter last, ArgumentConverter convert_arguments, const bool skip_first_argument=false, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=nullptr, typename std::enable_if< !std::is_base_of< data_expression, ArgumentConverter >::value >::type *=nullptr, typename std::enable_if< std::is_same< typename std::invoke_result< ArgumentConverter, data_expression &, typename FwdIter::value_type >::type, void >::value >::type *=nullptr)
 Constructor.
 
std::string pp (const application &x)
 
std::ostream & operator<< (std::ostream &out, const application &x)
 
const data_expressionunary_operand (const application &x)
 
const data_expressionbinary_left (const application &x)
 
const data_expressionbinary_right (const application &x)
 
const data_expressionunary_operand1 (const data_expression &x)
 
const data_expressionbinary_left1 (const data_expression &x)
 
const data_expressionbinary_right1 (const data_expression &x)
 
bool is_assignment (const atermpp::aterm_appl &x)
 
bool is_untyped_identifier_assignment (const atermpp::aterm_appl &x)
 
bool is_assignment_expression (const atermpp::aterm_appl &x)
 
std::string pp (const assignment_expression &x)
 
std::ostream & operator<< (std::ostream &out, const assignment_expression &x)
 
void swap (assignment_expression &t1, assignment_expression &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_assignment (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const assignment &x)
 
std::ostream & operator<< (std::ostream &out, const assignment &x)
 
void swap (assignment &t1, assignment &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_untyped_identifier_assignment (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const untyped_identifier_assignment &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_identifier_assignment &x)
 
void swap (untyped_identifier_assignment &t1, untyped_identifier_assignment &t2)
 \brief swap overload
 
template<typename VariableSequence , typename ExpressionSequence >
assignment_vector make_assignment_vector (VariableSequence const &variables, ExpressionSequence const &expressions)
 Constructs an assignment_list by pairwise combining a variable and expression.
 
template<typename VariableSequence , typename ExpressionSequence >
assignment_list make_assignment_list (const VariableSequence &variables, const ExpressionSequence &expressions)
 Converts an iterator range to data_expression_list.
 
variable_list left_hand_sides (const assignment_list &x)
 Returns the left hand sides of an assignment list.
 
data_expression_list right_hand_sides (const assignment_list &x)
 Returns the right hand sides of an assignment list.
 
std::string pp (const assignment_list &x)
 
std::string pp (const assignment_vector &x)
 
template<class... ARGUMENTS>
void make_bag_comprehension (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const bag_comprehension &x)
 
std::ostream & operator<< (std::ostream &out, const bag_comprehension &x)
 
void swap (bag_comprehension &t1, bag_comprehension &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_basic_sort (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const basic_sort &x)
 
std::ostream & operator<< (std::ostream &out, const basic_sort &x)
 
void swap (basic_sort &t1, basic_sort &t2)
 \brief swap overload
 
std::string pp (const binder_type &x)
 
std::ostream & operator<< (std::ostream &out, const binder_type &x)
 
void swap (binder_type &t1, binder_type &t2)
 \brief swap overload
 
bool is_untyped_set_or_bag_comprehension_binder (const atermpp::aterm_appl &x)
 
std::string pp (const untyped_set_or_bag_comprehension_binder &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_set_or_bag_comprehension_binder &x)
 
void swap (untyped_set_or_bag_comprehension_binder &t1, untyped_set_or_bag_comprehension_binder &t2)
 \brief swap overload
 
bool is_set_comprehension_binder (const atermpp::aterm_appl &x)
 
std::string pp (const set_comprehension_binder &x)
 
std::ostream & operator<< (std::ostream &out, const set_comprehension_binder &x)
 
void swap (set_comprehension_binder &t1, set_comprehension_binder &t2)
 \brief swap overload
 
bool is_bag_comprehension_binder (const atermpp::aterm_appl &x)
 
std::string pp (const bag_comprehension_binder &x)
 
std::ostream & operator<< (std::ostream &out, const bag_comprehension_binder &x)
 
void swap (bag_comprehension_binder &t1, bag_comprehension_binder &t2)
 \brief swap overload
 
bool is_forall_binder (const atermpp::aterm_appl &x)
 
std::string pp (const forall_binder &x)
 
std::ostream & operator<< (std::ostream &out, const forall_binder &x)
 
void swap (forall_binder &t1, forall_binder &t2)
 \brief swap overload
 
bool is_exists_binder (const atermpp::aterm_appl &x)
 
std::string pp (const exists_binder &x)
 
std::ostream & operator<< (std::ostream &out, const exists_binder &x)
 
void swap (exists_binder &t1, exists_binder &t2)
 \brief swap overload
 
bool is_lambda_binder (const atermpp::aterm_appl &x)
 
std::string pp (const lambda_binder &x)
 
std::ostream & operator<< (std::ostream &out, const lambda_binder &x)
 
void swap (lambda_binder &t1, lambda_binder &t2)
 \brief swap overload
 
bool is_true (const data_expression &x)
 Test if x is true.
 
bool is_false (const data_expression &x)
 Test if x is false.
 
bool is_not (const data_expression &x)
 Test if x is a negation.
 
bool is_or (const data_expression &x)
 Test if x is a disjunction.
 
bool is_and (const data_expression &x)
 Test if x is a conjunction.
 
bool is_imp (const data_expression &x)
 Test if x is an implication.
 
bool is_equal_to (const data_expression &x)
 Test if x is an equality.
 
bool is_not_equal_to (const data_expression &x)
 Test if x is an inequality.
 
const data_expressiontrue_ ()
 
const data_expressionfalse_ ()
 
data_expression not_ (const data_expression &x)
 
data_expression or_ (const data_expression &x, const data_expression &y)
 
data_expression and_ (const data_expression &x, const data_expression &y)
 
data_expression imp (const data_expression &x, const data_expression &y)
 
bool is_bool (const sort_expression &x)
 
sort_expression bool_ ()
 
data_expression make_forall_ (const data::variable_list &v, const data_expression &x)
 Make a universal quantification. It checks for an empty variable list, which is not allowed.
 
data_expression make_exists_ (const data::variable_list &v, const data_expression &x)
 Make an existential quantification. It checks for an empty variable list, which is not allowed.
 
template<class... ARGUMENTS>
void make_container_sort (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const container_sort &x)
 
std::ostream & operator<< (std::ostream &out, const container_sort &x)
 
void swap (container_sort &t1, container_sort &t2)
 \brief swap overload
 
std::string pp (const container_type &x)
 
std::ostream & operator<< (std::ostream &out, const container_type &x)
 
void swap (container_type &t1, container_type &t2)
 \brief swap overload
 
bool is_list_container (const atermpp::aterm_appl &x)
 
std::string pp (const list_container &x)
 
std::ostream & operator<< (std::ostream &out, const list_container &x)
 
void swap (list_container &t1, list_container &t2)
 \brief swap overload
 
bool is_set_container (const atermpp::aterm_appl &x)
 
std::string pp (const set_container &x)
 
std::ostream & operator<< (std::ostream &out, const set_container &x)
 
void swap (set_container &t1, set_container &t2)
 \brief swap overload
 
bool is_bag_container (const atermpp::aterm_appl &x)
 
std::string pp (const bag_container &x)
 
std::ostream & operator<< (std::ostream &out, const bag_container &x)
 
void swap (bag_container &t1, bag_container &t2)
 \brief swap overload
 
bool is_fset_container (const atermpp::aterm_appl &x)
 
std::string pp (const fset_container &x)
 
std::ostream & operator<< (std::ostream &out, const fset_container &x)
 
void swap (fset_container &t1, fset_container &t2)
 \brief swap overload
 
bool is_fbag_container (const atermpp::aterm_appl &x)
 
std::string pp (const fbag_container &x)
 
std::ostream & operator<< (std::ostream &out, const fbag_container &x)
 
void swap (fbag_container &t1, fbag_container &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_data_equation (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const data_equation &x)
 
std::ostream & operator<< (std::ostream &out, const data_equation &x)
 
void swap (data_equation &t1, data_equation &t2)
 \brief swap overload
 
bool is_data_equation (const atermpp::aterm_appl &t)
 Recognizer function.
 
std::string pp (const data_equation_list &x)
 
std::string pp (const data_equation_vector &x)
 
data::data_equation translate_user_notation (const data::data_equation &x)
 
std::set< data::sort_expressionfind_sort_expressions (const data::data_equation &x)
 
std::set< data::function_symbolfind_function_symbols (const data::data_equation &x)
 
bool is_abstraction (const atermpp::aterm &x)
 Returns true if the term t is an abstraction.
 
bool is_lambda (const atermpp::aterm_appl &x)
 Returns true if the term t is a lambda abstraction.
 
bool is_forall (const atermpp::aterm_appl &x)
 Returns true if the term t is a universal quantification.
 
bool is_exists (const atermpp::aterm_appl &x)
 Returns true if the term t is an existential quantification.
 
bool is_set_comprehension (const atermpp::aterm_appl &x)
 Returns true if the term t is a set comprehension.
 
bool is_bag_comprehension (const atermpp::aterm_appl &x)
 Returns true if the term t is a bag comprehension.
 
bool is_untyped_set_or_bag_comprehension (const atermpp::aterm_appl &x)
 Returns true if the term t is a set/bag comprehension.
 
bool is_function_symbol (const atermpp::aterm_appl &x)
 Returns true if the term t is a function symbol.
 
bool is_variable (const atermpp::aterm &x)
 Returns true if the term t is a variable.
 
bool is_application (const atermpp::aterm_appl &x)
 Returns true if the term t is an application.
 
bool is_application_no_check (const atermpp::aterm_appl &x)
 Returns true if the term t is an application, but it does not check whether an application symbol of sufficient arity exists, assuming this is ok.
 
bool is_where_clause (const atermpp::aterm_appl &x)
 Returns true if the term t is a where clause.
 
bool is_untyped_identifier (const atermpp::aterm_appl &x)
 Returns true if the term t is an identifier.
 
std::string pp (const data_expression &x)
 
std::ostream & operator<< (std::ostream &out, const data_expression &x)
 
void swap (data_expression &t1, data_expression &t2)
 \brief swap overload
 
void make_data_expression (data_expression &result)
 
bool is_data_expression (const atermpp::aterm_appl &x)
 Test for a data_expression expression.
 
template<typename Container >
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::string pp (const data_expression_list &x)
 
std::string pp (const data_expression_vector &x)
 
data::data_expression translate_user_notation (const data::data_expression &x)
 
std::set< data::sort_expressionfind_sort_expressions (const data::data_expression &x)
 
std::set< data::variablefind_all_variables (const data::data_expression &x)
 
std::set< data::variablefind_all_variables (const data::data_expression_list &x)
 
std::set< data::variablefind_free_variables (const data::data_expression &x)
 
std::set< data::variablefind_free_variables (const data::data_expression_list &x)
 
bool search_variable (const data::data_expression &x, const data::variable &v)
 
bool is_constant (const data_expression &x)
 
variable_list free_variables (const data_expression &x)
 
bool is_application (const data_expression &t)
 Returns true if the term t is an application.
 
const data_expression_listvariable_list_to_data_expression_list (const variable_list &l)
 Transform a variable_list into a data_expression_list.
 
atermpp::aterm add_index (const atermpp::aterm &x)
 Transforms DataVarId to DataVarIdNoIndex and transforms OpId to OpIdNoIndex.
 
atermpp::aterm remove_index (const atermpp::aterm &x)
 Transforms DataVarIdNoIndex to DataVarId and transforms OpIdNoIndex to OpId.
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, data_specification &spec)
 Reads a data specification from a stream.
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const data_specification &spec)
 Writes the data specification to a stream.
 
data_expression normalize_sorts (const data_expression &x, const data::sort_specification &sortspec)
 
variable_list normalize_sorts (const variable_list &x, const data::sort_specification &sortspec)
 
data::data_equation normalize_sorts (const data::data_equation &x, const data::sort_specification &sortspec)
 
data_equation_list normalize_sorts (const data_equation_list &x, const data::sort_specification &sortspec)
 
void normalize_sorts (data_equation_vector &x, const data::sort_specification &sortspec)
 
std::string pp (const data::data_specification &x)
 
bool is_data_specification (const atermpp::aterm_appl &x)
 Test for a data specification expression.
 
std::ostream & operator<< (std::ostream &out, const data_specification &x)
 
data_specification operator+ (data_specification spec1, const data_specification &spec2)
 Merges two data specifications into one.
 
function_symbol find_mapping (data_specification const &data, std::string const &s)
 Finds a mapping in a data specification.
 
function_symbol find_constructor (data_specification const &data, std::string const &s)
 Finds a constructor in a data specification.
 
sort_expression find_sort (data_specification const &data, std::string const &s)
 Finds a sort in a data specification.
 
data_equation_vector find_equations (data_specification const &specification, const data_expression &d)
 Gets all equations with a data expression as head on one of its sides.
 
variable_list order_variables_to_optimise_enumeration (const variable_list &l, const data_specification &data_spec)
 Order the variables in a variable list such that enumeration over these variables becomes more efficient.
 
std::set< core::identifier_stringfunction_and_mapping_identifiers (const data_specification &dataspec)
 Returns the names of functions and mappings that occur in a data specification.
 
function_symbol function_update (const sort_expression &s, const sort_expression &t)
 Constructor for function symbol @func_update.
 
function_symbol function_update_stable (const sort_expression &s, const sort_expression &t)
 Constructor for function symbol @func_update_stable.
 
data_expression is_not_a_function_update_manual_implementation (const data_expression &arg0)
 The data expression of an application of the function symbol @is_not_an_update.
 
data_expression if_always_else_manual_implementation (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 The data expression of an application of the function symbol @if_always_else.
 
template<typename Rewriter >
static bool is_enumerable (const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort)
 
template<typename Expression >
std::ostream & operator<< (std::ostream &out, const enumerator_list_element< Expression > &p)
 
template<typename Expression >
std::ostream & operator<< (std::ostream &out, const enumerator_list_element_with_substitution< Expression > &p)
 
template<class Rewriter >
data_expression_vector enumerate_expressions (const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr, enumerator_identifier_generator &id_generator)
 Returns a vector with all expressions of sort s.
 
template<class Rewriter >
data_expression_vector enumerate_expressions (const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr)
 Returns a vector with all expressions of sort s.
 
std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > make_one_point_rule_substitution (const std::map< data::variable, std::set< data::data_expression > > &equalities, const data::variable_list &quantifier_variables, bool find_all_assignments=true)
 creates a substitution from a set of (in-)equalities for a given list of quantifier variables
 
data::mutable_map_substitution make_one_point_rule_substitution (const std::map< data::variable, std::set< data::data_expression > > &equalities, bool find_all_assignments=true)
 creates a substitution from a set of (in-)equalities
 
template<class... ARGUMENTS>
void make_exists (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const exists &x)
 
std::ostream & operator<< (std::ostream &out, const exists &x)
 
void swap (exists &t1, exists &t2)
 \brief swap overload
 
template<typename T >
bool has_untyped_sort (const T &x)
 
template<typename T >
replace_untyped_sort (const T &x, const sort_expression &replacement)
 
const untyped_sort_variablemake_untyped_sort_variable (const sort_expression &x)
 
sort_expression substitute (const sort_expression &x, const sort_substitution &sigma)
 
template<typename Container >
std::string print_node_vector (const std::string &name, const Container &nodes, const std::string &sep=", ", const std::string &first="", const std::string &last="")
 
template<typename Container >
std::string print_vector (const std::string &name, const Container &nodes)
 
constraint_ptr substitute_constraint (constraint_ptr p, const sort_substitution &sigma)
 
constraint_ptr make_and_constraint (const std::vector< constraint_ptr > &alternatives)
 
constraint_ptr make_or_constraint (const std::vector< constraint_ptr > &alternatives)
 
constraint_ptr make_is_equal_to_constraint (const sort_expression &s1, const sort_expression &s2, int cost=0)
 
constraint_ptr make_false_constraint (const std::string &message)
 
constraint_ptr make_true_constraint (int cost=0)
 
constraint_ptr make_function_sort_constraint (const function_sort &f1, const sort_expression &s2)
 
constraint_ptr make_is_element_of_constraint (const sort_expression &s, const std::vector< sort_expression > &sorts, int cost=0)
 
constraint_ptr make_subsort_constraint (const sort_expression &s1, const sort_expression &s2, int cost=0)
 
std::vector< constraint_ptrjoin_or_is_element_of_constraints (const std::vector< constraint_ptr > &constraints)
 
function_sort_list filter_sorts (const function_sort_list &sorts, std::size_t arity)
 
void print_node (const type_check_node_ptr &node)
 
template<typename T , typename OutputIterator >
void find_all_variables (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::variablefind_all_variables (const T &x)
 
template<typename T , typename OutputIterator >
void find_free_variables (const T &x, OutputIterator o)
 
template<typename T , typename OutputIterator , typename VariableContainer >
void find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
 
template<typename T >
std::set< data::variablefind_free_variables (const T &x)
 
template<typename T , typename VariableContainer >
std::set< data::variablefind_free_variables_with_bound (const T &x, VariableContainer const &bound)
 
template<typename T , typename OutputIterator >
void find_identifiers (const T &x, OutputIterator o)
 
template<typename T >
std::set< core::identifier_stringfind_identifiers (const T &x)
 
template<typename T , typename OutputIterator >
void find_sort_expressions (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::sort_expressionfind_sort_expressions (const T &x)
 
template<typename T , typename OutputIterator >
void find_function_symbols (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::function_symbolfind_function_symbols (const T &x)
 
template<typename T , typename OutputIterator >
void find_data_expressions (const T &x, OutputIterator o)
 Returns all data expressions that occur in an object.
 
template<typename T >
std::set< data::data_expressionfind_data_expressions (const T &x)
 Returns all data expressions that occur in an object.
 
template<typename T >
bool search_variable (const T &x, const variable &v)
 Returns true if the term has a given variable as subterm.
 
template<typename T >
bool search_free_variable (const T &x, const variable &v)
 Returns true if the term has a given free variable as subterm.
 
template<typename Container >
bool search_sort_expression (Container const &container, const sort_expression &s)
 Returns true if the term has a given sort expression as subterm.
 
template<typename Container >
bool search_data_expression (Container const &container, const data_expression &s)
 Returns true if the term has a given data expression as subterm.
 
std::map< variable, std::set< data_expression > > find_equalities (const data_expression &x)
 
std::map< variable, std::set< data_expression > > find_inequalities (const data_expression &x)
 
std::string print_equalities (const std::map< variable, std::set< data_expression > > &equalities)
 
std::string print_inequalities (const std::map< variable, std::set< data_expression > > &inequalities)
 
template<class... ARGUMENTS>
void make_forall (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const forall &x)
 
std::ostream & operator<< (std::ostream &out, const forall &x)
 
void swap (forall &t1, forall &t2)
 \brief swap overload
 
template<class Data_variable_iterator >
void fourier_motzkin (const std::vector< linear_inequality > &inequalities_in, Data_variable_iterator variables_begin, Data_variable_iterator variables_end, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
 
void fourier_motzkin (const data_expression &e_in, const variable_list &vars_in, data_expression &e_out, variable_list &vars_out, const rewriter &r)
 Eliminate variables from a data expression using Gauss elimination and Fourier-Motzkin elimination.
 
template<class... ARGUMENTS>
void make_function_sort (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const function_sort &x)
 
std::ostream & operator<< (std::ostream &out, const function_sort &x)
 
void swap (function_sort &t1, function_sort &t2)
 \brief swap overload
 
function_sort make_function_sort_ (const sort_expression &dom1, const sort_expression &codomain)
 Convenience constructor for function sort with domain size 1.
 
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.
 
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.
 
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.
 
template<class... ARGUMENTS>
void make_function_symbol (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const function_symbol &x)
 
std::ostream & operator<< (std::ostream &out, const function_symbol &x)
 
void swap (function_symbol &t1, function_symbol &t2)
 \brief swap overload
 
std::string pp (const function_symbol_list &x)
 
std::string pp (const function_symbol_vector &x)
 
std::set< data::variablefind_all_variables (const data::function_symbol &x)
 
function_symbol_vector function_update_generate_constructors_code ()
 Give all system defined constructors for function_update.
 
function_symbol_vector function_update_mCRL2_usable_constructors ()
 Give all defined constructors which can be used in mCRL2 specs for function_update.
 
implementation_map function_update_cpp_implementable_constructors ()
 Give all system defined constructors which have an implementation in C++ and not in rewrite rules for function_update.
 
const core::identifier_stringfunction_update_name ()
 Generate identifier @func_update.
 
bool is_function_update_function_symbol (const atermpp::aterm_appl &e)
 Recogniser for function @func_update.
 
application function_update (const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @func_update.
 
void make_function_update (data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @func_update.
 
bool is_function_update_application (const atermpp::aterm_appl &e)
 Recogniser for application of @func_update.
 
const core::identifier_stringfunction_update_stable_name ()
 Generate identifier @func_update_stable.
 
bool is_function_update_stable_function_symbol (const atermpp::aterm_appl &e)
 Recogniser for function @func_update_stable.
 
application function_update_stable (const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @func_update_stable.
 
void make_function_update_stable (data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @func_update_stable.
 
bool is_function_update_stable_application (const atermpp::aterm_appl &e)
 Recogniser for application of @func_update_stable.
 
const core::identifier_stringis_not_a_function_update_name ()
 Generate identifier @is_not_an_update.
 
function_symbol is_not_a_function_update (const sort_expression &s, const sort_expression &t)
 Constructor for function symbol @is_not_an_update.
 
bool is_is_not_a_function_update_function_symbol (const atermpp::aterm_appl &e)
 Recogniser for function @is_not_an_update.
 
application is_not_a_function_update (const sort_expression &s, const sort_expression &t, const data_expression &arg0)
 Application of function symbol @is_not_an_update.
 
void make_is_not_a_function_update (data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0)
 Make an application of function symbol @is_not_an_update.
 
bool is_is_not_a_function_update_application (const atermpp::aterm_appl &e)
 Recogniser for application of @is_not_an_update.
 
data_expression is_not_a_function_update_application (const data_expression &a1)
 Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
 
const core::identifier_stringif_always_else_name ()
 Generate identifier @if_always_else.
 
function_symbol if_always_else (const sort_expression &s, const sort_expression &t)
 Constructor for function symbol @if_always_else.
 
bool is_if_always_else_function_symbol (const atermpp::aterm_appl &e)
 Recogniser for function @if_always_else.
 
application if_always_else (const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol @if_always_else.
 
void make_if_always_else (data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Make an application of function symbol @if_always_else.
 
bool is_if_always_else_application (const atermpp::aterm_appl &e)
 Recogniser for application of @if_always_else.
 
data_expression if_always_else_application (const data_expression &a1)
 Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
 
function_symbol_vector function_update_generate_functions_code (const sort_expression &s, const sort_expression &t)
 Give all system defined mappings for function_update.
 
function_symbol_vector function_update_generate_constructors_and_functions_code (const sort_expression &s, const sort_expression &t)
 Give all system defined mappings and constructors for function_update.
 
function_symbol_vector function_update_mCRL2_usable_mappings (const sort_expression &s, const sort_expression &t)
 Give all system defined mappings that can be used in mCRL2 specs for function_update.
 
implementation_map function_update_cpp_implementable_mappings (const sort_expression &s, const sort_expression &t)
 Give all system defined mappings that are to be implemented in C++ code for function_update.
 
const data_expressionarg1 (const data_expression &e)
 Function for projecting out argument. arg1 from an application.
 
const data_expressionarg2 (const data_expression &e)
 Function for projecting out argument. arg2 from an application.
 
const data_expressionarg3 (const data_expression &e)
 Function for projecting out argument. arg3 from an application.
 
data_equation_vector function_update_generate_equations_code (const sort_expression &s, const sort_expression &t)
 Give all system defined equations for function_update.
 
void on_delete_function_symbol (const atermpp::aterm &t)
 
void register_function_symbol_hooks ()
 
template<typename Substitution >
bool is_simple_substitution (const Substitution &)
 Returns true if the substitution sigma satisfies the property that FV(sigma(x)) is included in {x} for all variables x.
 
bool is_simple_substitution (const data::variable &lhs, const data::data_expression &rhs)
 Returns true if FV(rhs) is included in {lhs}.
 
bool is_sub_sort (const sort_expression &x1, const sort_expression &x2)
 
template<typename FwdIt >
data_expression join_or (FwdIt first, FwdIt last)
 Returns or applied to the sequence of data expressions [first, last)
 
template<typename FwdIt >
data_expression join_and (FwdIt first, FwdIt last)
 Returns and applied to the sequence of data expressions [first, last)
 
std::set< data_expressionsplit_or (const data_expression &expr)
 Splits a disjunction into a sequence of operands Given a data expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.
 
std::set< data_expressionsplit_and (const data_expression &expr)
 Splits a conjunction into a sequence of operands Given a data expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.
 
template<class... ARGUMENTS>
void make_lambda (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const lambda &x)
 
std::ostream & operator<< (std::ostream &out, const lambda &x)
 
void swap (lambda &t1, lambda &t2)
 \brief swap overload
 
data_expressionreal_zero ()
 
data_expressionreal_one ()
 
data_expressionreal_minus_one ()
 
data_expression min (const data_expression &e1, const data_expression &e2, const rewriter &)
 
data_expression max (const data_expression &e1, const data_expression &e2, const rewriter &)
 
bool is_closed_real_number (const data_expression &e)
 
bool is_negative (const data_expression &e, const rewriter &r)
 
bool is_positive (const data_expression &e, const rewriter &r)
 
bool is_zero (const data_expression &e)
 
application real_times (const data_expression &arg0, const data_expression &arg1)
 
application real_plus (const data_expression &arg0, const data_expression &arg1)
 
application real_divides (const data_expression &arg0, const data_expression &arg1)
 
application real_minus (const data_expression &arg0, const data_expression &arg1)
 
application real_negate (const data_expression &arg)
 
application real_abs (const data_expression &arg)
 
data_expression rewrite_with_memory (const data_expression &t, const rewriter &r)
 
std::string pp (const linear_inequality &l)
 
template<class TYPE >
std::string pp_vector (const TYPE &inequalities)
 Print the vector of inequalities to stderr in readable form.
 
linear_inequality subtract (const linear_inequality &e1, const linear_inequality &e2, const data_expression &f1, const data_expression &f2, const rewriter &r)
 Subtract the given equality, multiplied by f1/f2. The result is e1-(f1/f2)e2,.
 
bool is_inconsistent (const std::vector< linear_inequality > &inequalities_in, const rewriter &r, const bool use_cache)
 Determine whether a list of data expressions is inconsistent.
 
void count_occurrences (const std::vector< linear_inequality > &inequalities, std::map< variable, std::size_t > &nr_positive_occurrences, std::map< variable, std::size_t > &nr_negative_occurrences, const rewriter &r)
 
template<class Variable_iterator >
std::set< variablegauss_elimination (const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_equalities, std::vector< linear_inequality > &resulting_inequalities, Variable_iterator variables_begin, Variable_iterator variables_end, const rewriter &r)
 Try to eliminate variables from a system of inequalities using Gauss elimination.
 
bool is_a_redundant_inequality (const std::vector< linear_inequality > &inequalities, const std::vector< linear_inequality > ::iterator i, const rewriter &r)
 Indicate whether an inequality from a set of inequalities is redundant.
 
void remove_redundant_inequalities (const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
 Remove every redundant inequality from a vector of inequalities.
 
static void pivot_and_update (const variable &xi, const variable &xj, const data_expression &v, const data_expression &v_delta_correction, std::map< variable, data_expression > &beta, std::map< variable, data_expression > &beta_delta_correction, std::set< variable > &basic_variables, std::map< variable, detail::lhs_t > &working_equalities, const rewriter &r)
 
data_specification merge_data_specifications (const data_specification &dataspec1, const data_specification &dataspec2)
 Merges two data specifications. Throws an exception if conflicts are detected.
 
template<typename T >
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)
 
template<typename 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)
 
template<typename Term >
void optimized_not (Term &result, const Term &arg)
 Make a negation.
 
template<typename Term >
void optimized_and (Term &result, const Term &p, const Term &q)
 Make a conjunction, and optimize if possible.
 
template<typename Term >
void optimized_or (Term &result, const Term &p, const Term &q)
 Make a conjunction, and optimize if possible.
 
template<typename Term >
void optimized_imp (Term &result, const Term &p, const Term &q)
 Make an implication.
 
template<typename Term , typename VariableSequence >
void optimized_forall (Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
 Make a universal quantification.
 
template<typename Term , typename VariableSequence >
void optimized_forall_no_empty_domain (Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
 Make a universal quantification.
 
template<typename Term , typename VariableSequence >
void optimized_exists (Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
 Make an existential quantification.
 
template<typename Term , typename VariableSequence >
void optimized_exists_no_empty_domain (Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
 Make an existential quantification.
 
std::pair< basic_sort_vector, alias_vectorparse_sort_specification (const std::string &text)
 
data_specification parse_data_specification (std::istream &in)
 Parses a and type checks a data specification.
 
data_specification parse_data_specification (const std::string &text)
 Parses a and type checks a data specification.
 
template<typename OutputIterator , typename VariableIterator >
void parse_variables (std::istream &in, OutputIterator o, VariableIterator begin, VariableIterator end, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a data variable declaration list checking for double occurrences of variables in an existing variable range.
 
template<typename OutputIterator , typename VariableIterator >
void parse_variables (const std::string &text, OutputIterator i, VariableIterator begin, VariableIterator end, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a data variable declaration list checking for double occurrences of variables in an existing variable range.
 
template<typename OutputIterator >
void parse_variables (std::istream &text, OutputIterator i, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a data variable declaration list.
 
template<typename OutputIterator >
void parse_variables (const std::string &text, OutputIterator i, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a data variable declaration list.
 
variable parse_variable (const std::string &text, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a data variable declaration.
 
variable parse_variable (std::istream &text, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a data variable declaration.
 
template<typename VariableContainer >
data_expression parse_data_expression (std::istream &in, const VariableContainer &variables, const data_specification &dataspec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
 Parses and type checks a data expression.
 
template<typename VariableContainer >
data_expression parse_data_expression (const std::string &text, const VariableContainer &variables, const data_specification &data_spec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
 Parses and type checks a data expression.
 
data_expression parse_data_expression (std::istream &text, const data_specification &data_spec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
 Parses and type checks a data expression.
 
data_expression parse_data_expression (const std::string &text, const data_specification &data_spec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
 Parses and type checks a data expression.
 
variable_list parse_variables (const std::string &text)
 
sort_expression parse_sort_expression (std::istream &in, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a sort expression.
 
sort_expression parse_sort_expression (const std::string &text, const data_specification &data_spec=detail::default_specification())
 Parses and type checks a sort expression.
 
data::function_symbol parse_function_symbol (const std::string &text, const std::string &dataspec_text="")
 
variable_list parse_variable_declaration_list (const std::string &text, const data_specification &dataspec=detail::default_specification())
 Parses a variable declaration list.
 
int precedence (const data_expression &x)
 
int precedence (const application &x)
 
constexpr int precedence (const forall &)
 
constexpr int precedence (const exists &)
 
constexpr int precedence (const lambda &)
 
constexpr int precedence (const set_comprehension &)
 
constexpr int precedence (const bag_comprehension &)
 
constexpr int precedence (const where_clause &)
 
bool is_left_associative (const data_expression &x)
 
bool is_right_associative (const data_expression &x)
 
template<typename T >
std::string pp (const T &x)
 Returns a string representation of the object x.
 
template<typename Substitution >
std::set< data::variablesubstitution_variables (const Substitution &)
 Returns the variables appearing in the right hand sides of the substitution.
 
template<typename T , typename Substitution >
void replace_sort_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_data_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_data_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_all_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_all_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_free_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_free_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename VariableContainer >
void replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename VariableContainer >
replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void substitute_sorts (T &x, const Substitution &sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T , typename Substitution >
substitute_sorts (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T , typename Substitution >
void replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename IdentifierGenerator >
void replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename IdentifierGenerator >
replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter >
void rewrite (T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter >
rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter , typename Substitution >
void rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter , typename Substitution >
rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
rewrite_strategy parse_rewrite_strategy (const std::string &s)
 standard conversion from string to rewrite strategy
 
std::istream & operator>> (std::istream &is, rewrite_strategy &s)
 standard conversion from stream to rewrite strategy
 
std::string pp (const rewrite_strategy s)
 Pretty prints a rewrite strategy.
 
std::ostream & operator<< (std::ostream &os, const rewrite_strategy s)
 standard conversion from rewrite strategy to stream
 
std::string description (const rewrite_strategy s)
 standard descriptions for rewrite strategies
 
template<typename T >
void if_rewrite (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
if_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
void one_point_rule_rewrite (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
one_point_rule_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
void quantifiers_inside_rewrite (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
quantifiers_inside_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
void simplify (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
simplify (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<class... ARGUMENTS>
void make_set_comprehension (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const set_comprehension &x)
 
std::ostream & operator<< (std::ostream &out, const set_comprehension &x)
 
void swap (set_comprehension &t1, set_comprehension &t2)
 \brief swap overload
 
bool is_basic_sort (const atermpp::aterm_appl &x)
 Returns true if the term t is a basic sort.
 
bool is_function_sort (const atermpp::aterm_appl &x)
 Returns true if the term t is a function sort.
 
bool is_container_sort (const atermpp::aterm_appl &x)
 Returns true if the term t is a container sort.
 
bool is_structured_sort (const atermpp::aterm_appl &x)
 Returns true if the term t is a structured sort.
 
bool is_untyped_sort (const atermpp::aterm_appl &x)
 Returns true if the term t is the unknown sort.
 
bool is_untyped_possible_sorts (const atermpp::aterm_appl &x)
 Returns true if the term t is an expression for multiple possible sorts.
 
std::string pp (const sort_expression &x)
 
std::ostream & operator<< (std::ostream &out, const sort_expression &x)
 
void swap (sort_expression &t1, sort_expression &t2)
 \brief swap overload
 
bool is_sort_expression (const atermpp::aterm_appl &x)
 Test for a sort_expression expression.
 
std::string pp (const sort_expression_list &x)
 
std::string pp (const sort_expression_vector &x)
 
std::set< data::sort_expressionfind_sort_expressions (const data::sort_expression &x)
 
sort_expression normalize_sorts (const sort_expression &x, const data::sort_specification &sortspec)
 
function_symbol equal_to (const sort_expression &s)
 Constructor for function symbol ==.
 
template<typename DataExpression >
bool is_equal_to_function_symbol (const DataExpression &e)
 Recogniser for function ==.
 
application equal_to (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol ==.
 
template<typename DataExpression >
bool is_equal_to_application (const DataExpression &e)
 Recogniser for application of ==.
 
function_symbol not_equal_to (const sort_expression &s)
 Constructor for function symbol !=.
 
template<typename DataExpression >
bool is_not_equal_to_function_symbol (const DataExpression &e)
 Recogniser for function !=.
 
application not_equal_to (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol !=.
 
template<typename DataExpression >
bool is_not_equal_to_application (const DataExpression &e)
 Recogniser for application of !=.
 
function_symbol if_ (const sort_expression &s)
 Constructor for function symbol if.
 
template<typename DataExpression >
bool is_if_function_symbol (const DataExpression &e)
 Recogniser for function if.
 
application if_ (const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
 Application of function symbol if.
 
template<typename DataExpression >
bool is_if_application (const DataExpression &e)
 Recogniser for application of if.
 
function_symbol less (const sort_expression &s)
 Constructor for function symbol <.
 
template<typename DataExpression >
bool is_less_function_symbol (const DataExpression &e)
 Recogniser for function <.
 
application less (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol <.
 
template<typename DataExpression >
bool is_less_application (const DataExpression &e)
 Recogniser for application of <.
 
function_symbol less_equal (const sort_expression &s)
 Constructor for function symbol <=.
 
template<typename DataExpression >
bool is_less_equal_function_symbol (const DataExpression &e)
 Recogniser for function <=.
 
application less_equal (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol <=.
 
template<typename DataExpression >
bool is_less_equal_application (const DataExpression &e)
 Recogniser for application of <=.
 
function_symbol greater (const sort_expression &s)
 Constructor for function symbol >
 
template<typename DataExpression >
bool is_greater_function_symbol (const DataExpression &e)
 Recogniser for function >
 
application greater (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol >
 
template<typename DataExpression >
bool is_greater_application (const DataExpression &e)
 Recogniser for application of >
 
function_symbol greater_equal (const sort_expression &s)
 Constructor for function symbol >=.
 
template<typename DataExpression >
bool is_greater_equal_function_symbol (const DataExpression &e)
 Recogniser for function >=.
 
application greater_equal (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol >=.
 
template<typename DataExpression >
bool is_greater_equal_application (const DataExpression &e)
 Recogniser for application of >=.
 
function_symbol_vector standard_generate_functions_code (const sort_expression &s)
 Give all standard system defined functions for sort s.
 
data_equation_vector standard_generate_equations_code (const sort_expression &s)
 Give all standard system defined equations for sort s.
 
data_expression number (const sort_expression &s, const std::string &n)
 Construct numeric expression from a string representing a number in decimal notation.
 
bool is_convertible (const sort_expression &s1, const sort_expression &s2)
 Returns true if and only if s1 == s2, or if s1 is a less specific numeric type than s2.
 
bool is_system_defined (const sort_expression &s)
 Returns true iff the expression represents a standard sort.
 
std::list< data_expressionsplit_disjunction (const data_expression &condition)
 Split a disjunctive expression into a set of clauses.
 
std::list< data_expressionsplit_conjunction (const data_expression &condition)
 Split a disjunctive expression into a set of clauses.
 
template<class... ARGUMENTS>
void make_structured_sort (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const structured_sort &x)
 
std::ostream & operator<< (std::ostream &out, const structured_sort &x)
 
void swap (structured_sort &t1, structured_sort &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_structured_sort_constructor (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
bool is_structured_sort_constructor (const atermpp::aterm_appl &x)
 
std::string pp (const structured_sort_constructor &x)
 
std::ostream & operator<< (std::ostream &out, const structured_sort_constructor &x)
 
void swap (structured_sort_constructor &t1, structured_sort_constructor &t2)
 \brief swap overload
 
std::string pp (const structured_sort_constructor_list &x)
 
std::string pp (const structured_sort_constructor_vector &x)
 
template<class... ARGUMENTS>
void make_structured_sort_constructor_argument (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
bool is_structured_sort_constructor_argument (const atermpp::aterm_appl &x)
 
std::string pp (const structured_sort_constructor_argument &x)
 
std::ostream & operator<< (std::ostream &out, const structured_sort_constructor_argument &x)
 
void swap (structured_sort_constructor_argument &t1, structured_sort_constructor_argument &t2)
 \brief swap overload
 
template<typename VariableSequence , typename DataExpressionSequence >
void add_assignments (data::mutable_indexed_substitution<> &sigma, const VariableSequence &v, const DataExpressionSequence &e)
 Adds assignments [v := e] to the substitution sigma for each variable in v.
 
template<typename VariableSequence >
void remove_assignments (data::mutable_indexed_substitution<> &sigma, const VariableSequence &v)
 Removes assignments to variables in v from the substitution sigma.
 
template<>
bool is_simple_substitution (const assignment_sequence_substitution &sigma)
 
std::ostream & operator<< (std::ostream &out, const enumerator_substitution &sigma)
 
bool is_simple_substitution (const enumerator_substitution &sigma)
 
template<typename AssociativeContainer >
map_substitution< AssociativeContainer > make_map_substitution (const AssociativeContainer &m)
 Utility function for creating a map_substitution.
 
template<typename AssociativeContainer >
std::set< data::variablesubstitution_variables (const map_substitution< AssociativeContainer > &sigma)
 
template<typename AssociativeContainer >
bool is_simple_substitution (const map_substitution< AssociativeContainer > &sigma)
 
template<typename VariableType , typename ExpressionType >
std::ostream & operator<< (std::ostream &out, const mutable_indexed_substitution< VariableType, ExpressionType > &sigma)
 
template<typename VariableType = variable, typename ExpressionType = data_expression>
std::multiset< variablesubstitution_variables (const mutable_indexed_substitution< VariableType, ExpressionType > &sigma)
 
template<typename VariableContainer , typename ExpressionContainer , typename MapContainer >
mutable_map_substitution< MapContainer > make_mutable_map_substitution (const VariableContainer &vc, const ExpressionContainer &ec)
 Utility function for creating a mutable_map_substitution.
 
template<typename VariableContainer , typename ExpressionContainer >
mutable_map_substitution< std::map< typename VariableContainer::value_type, typename ExpressionContainer::value_type > > make_mutable_map_substitution (const VariableContainer &vc, const ExpressionContainer &ec)
 
template<typename AssociativeContainer >
std::ostream & operator<< (std::ostream &out, const mutable_map_substitution< AssociativeContainer > &sigma)
 
std::set< data::variablesubstitution_variables (const mutable_map_substitution<> &sigma)
 
template<typename AssociativeContainer >
bool is_simple_substitution (const mutable_map_substitution< AssociativeContainer > &sigma)
 
std::ostream & operator<< (std::ostream &out, const no_substitution &)
 
template<typename VariableContainer , typename ExpressionContainer >
sequence_sequence_substitution< VariableContainer, ExpressionContainer > make_sequence_sequence_substitution (const VariableContainer &vc, const ExpressionContainer &ec)
 Utility function for creating a sequence_sequence_substitution.
 
template<typename VariableContainer , typename ExpressionContainer >
std::ostream & operator<< (std::ostream &out, const sequence_sequence_substitution< VariableContainer, ExpressionContainer > &sigma)
 
template<typename VariableContainer , typename ExpressionContainer >
bool is_simple_substitution (const sequence_sequence_substitution< VariableContainer, ExpressionContainer > &sigma)
 
std::set< data::variablesubstitution_variables (const variable_substitution &sigma)
 
template<typename T >
void translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
void typecheck_sort_expression (const sort_expression &sort_expr, const data_specification &data_spec)
 Type check a sort expression. Throws an exception if something went wrong.
 
template<typename VariableContainer >
data_expression typecheck_data_expression (const data_expression &x, const VariableContainer &variables, const data_specification &dataspec=data_specification())
 Type check a data expression. Throws an exception if something went wrong.
 
data_expression typecheck_data_expression (const data_expression &x, const data_specification &dataspec=data_specification())
 Type check a data expression. Throws an exception if something went wrong.
 
void typecheck_data_specification (data_specification &data_spec)
 Type check a parsed mCRL2 data specification. Throws an exception if something went wrong.
 
data_expression typecheck_untyped_data_parameter (data_type_checker &typechecker, const core::identifier_string &name, const data_expression_list &parameters, const data::sort_expression &expected_sort, const detail::variable_context &variable_context)
 
constexpr std::size_t undefined_index ()
 Returns an index that corresponds to 'undefined'.
 
const data::variableundefined_variable ()
 Returns a data variable that corresponds to 'undefined'.
 
const data::variableundefined_real_variable ()
 Returns a data variable that corresponds to 'undefined'.
 
const data::sort_expressionundefined_sort_expression ()
 Returns a sort expression that corresponds to 'undefined'.
 
const data::data_expressionundefined_data_expression ()
 Returns a data expression that corresponds to 'undefined'.
 
const data::data_expressionundefined_real ()
 Returns a data expression of type Real that corresponds to 'undefined'.
 
template<typename StructInfo >
bool is_pattern_matching_rule (StructInfo &ssf, const data_equation &rewrite_rule)
 Check whether the given rewrite rule can be classified as a pattern matching rule.
 
template<typename StructInfo >
data_equation unfold_pattern_matching (const function_symbol &mapping, const data_equation_vector &rewrite_rules, StructInfo &ssf, representative_generator &gen, set_identifier_generator &id_gen)
 This converts a collection of rewrite rules for a give function symbol into a one-rule specification of the function, using recogniser and projection functions to implement pattern matching.
 
template<class... ARGUMENTS>
void make_untyped_data_parameter (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
bool is_untyped_data_parameter (const atermpp::aterm_appl &x)
 
std::string pp (const untyped_data_parameter &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_data_parameter &x)
 
void swap (untyped_data_parameter &t1, untyped_data_parameter &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_untyped_identifier (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const untyped_identifier &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_identifier &x)
 
void swap (untyped_identifier &t1, untyped_identifier &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_untyped_possible_sorts (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const untyped_possible_sorts &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_possible_sorts &x)
 
void swap (untyped_possible_sorts &t1, untyped_possible_sorts &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_untyped_set_or_bag_comprehension (atermpp::aterm &result, ARGUMENTS... arguments)
 
std::string pp (const untyped_set_or_bag_comprehension &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_set_or_bag_comprehension &x)
 
void swap (untyped_set_or_bag_comprehension &t1, untyped_set_or_bag_comprehension &t2)
 \brief swap overload
 
std::string pp (const untyped_sort &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_sort &x)
 
void swap (untyped_sort &t1, untyped_sort &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_untyped_sort_variable (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
bool is_untyped_sort_variable (const atermpp::aterm_appl &x)
 
std::string pp (const untyped_sort_variable &x)
 
std::ostream & operator<< (std::ostream &out, const untyped_sort_variable &x)
 
void swap (untyped_sort_variable &t1, untyped_sort_variable &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_variable (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const variable &x)
 
std::ostream & operator<< (std::ostream &out, const variable &x)
 
void swap (variable &t1, variable &t2)
 \brief swap overload
 
std::string pp (const variable_list &x)
 
std::string pp (const variable_vector &x)
 
std::string pp (const std::set< variable > &x)
 
std::set< data::variablefind_all_variables (const data::variable &x)
 
std::set< data::variablefind_all_variables (const data::variable_list &x)
 
std::set< core::identifier_stringfind_identifiers (const data::variable_list &x)
 
template<class... ARGUMENTS>
void make_where_clause (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const where_clause &x)
 
std::ostream & operator<< (std::ostream &out, const where_clause &x)
 
void swap (where_clause &t1, where_clause &t2)
 \brief swap overload
 
static sort_expression find_normal_form (const sort_expression &e, const std::multimap< sort_expression, sort_expression > &map1, std::set< sort_expression > sorts_already_seen=std::set< sort_expression >())
 

Detailed Description

Namespace for all data library functionality.

Typedef Documentation

◆ alias_list

\brief list of aliass

Definition at line 72 of file alias.h.

◆ alias_vector

typedef std::vector<alias> mcrl2::data::alias_vector

\brief vector of aliass

Definition at line 75 of file alias.h.

◆ assignment_expression_list

\brief list of assignment_expressions

Definition at line 50 of file assignment.h.

◆ assignment_expression_vector

\brief vector of assignment_expressions

Definition at line 53 of file assignment.h.

◆ assignment_list

\brief list of assignments

Definition at line 146 of file assignment.h.

◆ assignment_vector

\brief vector of assignments

Definition at line 149 of file assignment.h.

◆ basic_sort_list

list of basic sorts

Definition at line 92 of file basic_sort.h.

◆ basic_sort_vector

vector of basic sorts

Definition at line 94 of file basic_sort.h.

◆ binder_type_list

\brief list of binder_types

Definition at line 50 of file binder_type.h.

◆ binder_type_vector

\brief vector of binder_types

Definition at line 53 of file binder_type.h.

◆ constraint_ptr

Definition at line 188 of file type_check_tree.h.

◆ container_sort_list

list of function sorts

Definition at line 94 of file container_sort.h.

◆ container_sort_vector

list of function sorts

Definition at line 98 of file container_sort.h.

◆ container_type_list

\brief list of container_types

Definition at line 50 of file container_type.h.

◆ container_type_vector

\brief vector of container_types

Definition at line 53 of file container_type.h.

◆ data_equation_list

\brief list of data_equations

Definition at line 122 of file data_equation.h.

◆ data_equation_vector

\brief vector of data_equations

Definition at line 125 of file data_equation.h.

◆ data_expression_list

\brief list of data_expressions

Definition at line 181 of file data_expression.h.

◆ data_expression_vector

\brief vector of data_expressions

Definition at line 184 of file data_expression.h.

◆ function_sort_list

list of function sorts

Definition at line 98 of file function_sort.h.

◆ function_sort_vector

vector of function sorts

Definition at line 100 of file function_sort.h.

◆ function_symbol_key_type

◆ function_symbol_list

\brief list of function_symbols

Definition at line 88 of file function_symbol.h.

◆ function_symbol_vector

\brief vector of function_symbols

Definition at line 91 of file function_symbol.h.

◆ implementation_map

typedef std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > > mcrl2::data::implementation_map

Definition at line 49 of file function_update.h.

◆ solution

typedef std::pair<sort_substitution, int> mcrl2::data::solution

Definition at line 24 of file type_check_tree.h.

◆ sort_expression_list

\brief list of sort_expressions

Definition at line 102 of file sort_expression.h.

◆ sort_expression_vector

\brief vector of sort_expressions

Definition at line 105 of file sort_expression.h.

◆ sort_substitution

◆ sorts_list

◆ structured_sort_constructor_argument_list

◆ structured_sort_constructor_argument_vector

\brief vector of structured_sort_constructor_arguments

Definition at line 96 of file structured_sort_constructor_argument.h.

◆ structured_sort_constructor_list

\brief list of structured_sort_constructors

Definition at line 199 of file structured_sort_constructor.h.

◆ structured_sort_constructor_vector

\brief vector of structured_sort_constructors

Definition at line 202 of file structured_sort_constructor.h.

◆ structured_sort_list

\brief list of structured_sorts

Definition at line 445 of file structured_sort.h.

◆ structured_sort_vector

\brief vector of structured_sorts

Definition at line 448 of file structured_sort.h.

◆ type_check_node_ptr

Definition at line 92 of file type_check_tree.h.

◆ untyped_data_parameter_list

\brief list of untyped_data_parameters

Definition at line 75 of file untyped_data_parameter.h.

◆ untyped_data_parameter_vector

\brief vector of untyped_data_parameters

Definition at line 78 of file untyped_data_parameter.h.

◆ untyped_identifier_assignment_list

\brief list of untyped_identifier_assignments

Definition at line 242 of file assignment.h.

◆ untyped_identifier_assignment_vector

\brief vector of untyped_identifier_assignments

Definition at line 245 of file assignment.h.

◆ variable_list

\brief list of variables

Definition at line 259 of file data_expression.h.

◆ variable_vector

typedef std::vector<variable> mcrl2::data::variable_vector

\brief vector of variables

Definition at line 89 of file variable.h.

Enumeration Type Documentation

◆ rewrite_strategy

The strategy of the rewriter.

Enumerator
jitty 
jitty_prover 

JITty.

JITty + Prover

Definition at line 13 of file rewrite_strategy.h.

Function Documentation

◆ add_assignments()

template<typename VariableSequence , typename DataExpressionSequence >
void mcrl2::data::add_assignments ( data::mutable_indexed_substitution<> &  sigma,
const VariableSequence &  v,
const DataExpressionSequence &  e 
)
inline

Adds assignments [v := e] to the substitution sigma for each variable in v.

Definition at line 25 of file substitution_utility.h.

◆ add_index()

atermpp::aterm mcrl2::data::add_index ( const atermpp::aterm x)

Transforms DataVarId to DataVarIdNoIndex and transforms OpId to OpIdNoIndex.

◆ and_()

data_expression mcrl2::data::and_ ( const data_expression x,
const data_expression y 
)
inline
Returns
The conjunction of x and y

Definition at line 120 of file consistency.h.

◆ anonymize()

void mcrl2::data::anonymize ( data_specification dataspec)
inline

Definition at line 224 of file anonymize.h.

◆ arg1()

const data_expression & mcrl2::data::arg1 ( const data_expression e)
inline

Function for projecting out argument. arg1 from an application.

Parameters
eA data expression.
Precondition
arg1 is defined for e.
Returns
The argument of e that corresponds to arg1.

Definition at line 436 of file function_update.h.

◆ arg2()

const data_expression & mcrl2::data::arg2 ( const data_expression e)
inline

Function for projecting out argument. arg2 from an application.

Parameters
eA data expression.
Precondition
arg2 is defined for e.
Returns
The argument of e that corresponds to arg2.

Definition at line 448 of file function_update.h.

◆ arg3()

const data_expression & mcrl2::data::arg3 ( const data_expression e)
inline

Function for projecting out argument. arg3 from an application.

Parameters
eA data expression.
Precondition
arg3 is defined for e.
Returns
The argument of e that corresponds to arg3.

Definition at line 460 of file function_update.h.

◆ binary_left()

const data_expression & mcrl2::data::binary_left ( const application x)
inline

Definition at line 733 of file application.h.

◆ binary_left1()

const data_expression & mcrl2::data::binary_left1 ( const data_expression x)
inline

Definition at line 752 of file application.h.

◆ binary_right()

const data_expression & mcrl2::data::binary_right ( const application x)
inline

Definition at line 739 of file application.h.

◆ binary_right1()

const data_expression & mcrl2::data::binary_right1 ( const data_expression x)
inline

Definition at line 759 of file application.h.

◆ bool_()

sort_expression mcrl2::data::bool_ ( )
inline
Returns
The boolean sort

Definition at line 141 of file consistency.h.

◆ count_occurrences()

void mcrl2::data::count_occurrences ( const std::vector< linear_inequality > &  inequalities,
std::map< variable, std::size_t > &  nr_positive_occurrences,
std::map< variable, std::size_t > &  nr_negative_occurrences,
const rewriter r 
)
inline

Definition at line 1048 of file linear_inequalities.h.

◆ description()

std::string mcrl2::data::description ( const rewrite_strategy  s)
inline

standard descriptions for rewrite strategies

Definition at line 87 of file rewrite_strategy.h.

◆ enumerate_expressions() [1/2]

template<class Rewriter >
data_expression_vector mcrl2::data::enumerate_expressions ( const sort_expression s,
const data_specification dataspec,
const Rewriter &  rewr 
)

Returns a vector with all expressions of sort s.

Parameters
sA sort expression.
dataspecThe data specification defining the terms of sort s.
rewrA rewriter to be used to simplify terms and conditions.

It is assumed that the sort s has only a finite number of elements.

Definition at line 1067 of file enumerator.h.

◆ enumerate_expressions() [2/2]

template<class Rewriter >
data_expression_vector mcrl2::data::enumerate_expressions ( const sort_expression s,
const data_specification dataspec,
const Rewriter &  rewr,
enumerator_identifier_generator id_generator 
)

Returns a vector with all expressions of sort s.

Parameters
sA sort expression.
dataspecThe data specification defining the terms of sort s.
rewrA rewriter to be used to simplify terms and conditions.
id_generatorAn identifier generator used to generate new names for variables.

It is assumed that the sort s has only a finite number of elements.

Definition at line 1032 of file enumerator.h.

◆ equal_to() [1/2]

application mcrl2::data::equal_to ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol ==.

Parameters
[in]arg0A data expression
[in]arg1A data expression
Returns
Application of == to a number of arguments

Definition at line 144 of file standard.h.

◆ equal_to() [2/2]

function_symbol mcrl2::data::equal_to ( const sort_expression s)
inline

Constructor for function symbol ==.

Parameters
[in]sA sort expression
Returns
function symbol equal_to

Definition at line 126 of file standard.h.

◆ false_()

const data_expression & mcrl2::data::false_ ( )
inline
Returns
The expression false

Definition at line 99 of file consistency.h.

◆ filter_sorts()

function_sort_list mcrl2::data::filter_sorts ( const function_sort_list sorts,
std::size_t  arity 
)
inline

Definition at line 1256 of file type_check_tree.h.

◆ find_all_variables() [1/7]

std::set< data::variable > mcrl2::data::find_all_variables ( const data::data_expression x)

Definition at line 93 of file data.cpp.

◆ find_all_variables() [2/7]

std::set< data::variable > mcrl2::data::find_all_variables ( const data::data_expression_list x)

Definition at line 94 of file data.cpp.

◆ find_all_variables() [3/7]

std::set< data::variable > mcrl2::data::find_all_variables ( const data::function_symbol x)

Definition at line 95 of file data.cpp.

◆ find_all_variables() [4/7]

std::set< data::variable > mcrl2::data::find_all_variables ( const data::variable x)

Definition at line 96 of file data.cpp.

◆ find_all_variables() [5/7]

std::set< data::variable > mcrl2::data::find_all_variables ( const data::variable_list x)

Definition at line 97 of file data.cpp.

◆ find_all_variables() [6/7]

template<typename T >
std::set< data::variable > mcrl2::data::find_all_variables ( const T &  x)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All variables that occur in the object x

Definition at line 303 of file find.h.

◆ find_all_variables() [7/7]

template<typename T , typename OutputIterator >
void mcrl2::data::find_all_variables ( const T &  x,
OutputIterator  o 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \return All variables that occur in the term x

Definition at line 294 of file find.h.

◆ find_constructor()

function_symbol mcrl2::data::find_constructor ( data_specification const &  data,
std::string const &  s 
)
inline

Finds a constructor in a data specification.

Parameters
dataA data specification
sA string
Returns
The found constructor

Definition at line 773 of file data_specification.h.

◆ find_data_expressions() [1/2]

template<typename T >
std::set< data::data_expression > mcrl2::data::find_data_expressions ( const T &  x)

Returns all data expressions that occur in an object.

Parameters
[in]xan object containing data expressions
Returns
All data expressions that occur in the object x

Definition at line 432 of file find.h.

◆ find_data_expressions() [2/2]

template<typename T , typename OutputIterator >
void mcrl2::data::find_data_expressions ( const T &  x,
OutputIterator  o 
)

Returns all data expressions that occur in an object.

Parameters
[in]xan object containing data expressions
[in,out]oan output iterator to which all data expressions occurring in x are written.
Returns
All data expressions that occur in the term x

Definition at line 423 of file find.h.

◆ find_equalities()

std::map< variable, std::set< data_expression > > mcrl2::data::find_equalities ( const data_expression x)
inline

Definition at line 450 of file find_equalities.h.

◆ find_equations()

data_equation_vector mcrl2::data::find_equations ( data_specification const &  specification,
const data_expression d 
)
inline

Gets all equations with a data expression as head on one of its sides.

Parameters
[in]specificationA data specification.
[in]dA data expression.
Returns
All equations with d as head in one of its sides.

Definition at line 801 of file data_specification.h.

◆ find_free_variables() [1/4]

std::set< data::variable > mcrl2::data::find_free_variables ( const data::data_expression x)

Definition at line 98 of file data.cpp.

◆ find_free_variables() [2/4]

std::set< data::variable > mcrl2::data::find_free_variables ( const data::data_expression_list x)

Definition at line 99 of file data.cpp.

◆ find_free_variables() [3/4]

template<typename T >
std::set< data::variable > mcrl2::data::find_free_variables ( const T &  x)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All free variables that occur in the object x

Definition at line 335 of file find.h.

◆ find_free_variables() [4/4]

template<typename T , typename OutputIterator >
void mcrl2::data::find_free_variables ( const T &  x,
OutputIterator  o 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are added. \return All free variables that occur in the object x

Definition at line 315 of file find.h.

◆ find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >
void mcrl2::data::find_free_variables_with_bound ( const T &  x,
OutputIterator  o,
const VariableContainer &  bound 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \param[in] bound a container of variables \return All free variables that occur in the object x

Definition at line 326 of file find.h.

◆ find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >
std::set< data::variable > mcrl2::data::find_free_variables_with_bound ( const T &  x,
VariableContainer const &  bound 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in] bound a bound a container of variables \return All free variables that occur in the object x

Definition at line 347 of file find.h.

◆ find_function_symbols() [1/3]

std::set< data::function_symbol > mcrl2::data::find_function_symbols ( const data::data_equation x)

Definition at line 100 of file data.cpp.

◆ find_function_symbols() [2/3]

template<typename T >
std::set< data::function_symbol > mcrl2::data::find_function_symbols ( const T &  x)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \return All function symbols that occur in the object x

Definition at line 410 of file find.h.

◆ find_function_symbols() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::data::find_function_symbols ( const T &  x,
OutputIterator  o 
)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \param[in,out] o an output iterator to which all function symbols occurring in x are written. \return All function symbols that occur in the term x

Definition at line 401 of file find.h.

◆ find_identifiers() [1/3]

std::set< core::identifier_string > mcrl2::data::find_identifiers ( const data::variable_list x)

Definition at line 101 of file data.cpp.

◆ find_identifiers() [2/3]

template<typename T >
std::set< core::identifier_string > mcrl2::data::find_identifiers ( const T &  x)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \return All identifiers that occur in the object x

Definition at line 368 of file find.h.

◆ find_identifiers() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::data::find_identifiers ( const T &  x,
OutputIterator  o 
)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \param[in,out] o an output iterator to which all identifiers occurring in x are written. \return All identifiers that occur in the term x

Definition at line 359 of file find.h.

◆ find_inequalities()

std::map< variable, std::set< data_expression > > mcrl2::data::find_inequalities ( const data_expression x)
inline

Definition at line 460 of file find_equalities.h.

◆ find_mapping()

function_symbol mcrl2::data::find_mapping ( data_specification const &  data,
std::string const &  s 
)
inline

Finds a mapping in a data specification.

Parameters
dataA data specification
sA string
Returns
The found mapping

Definition at line 760 of file data_specification.h.

◆ find_normal_form()

static sort_expression mcrl2::data::find_normal_form ( const sort_expression e,
const std::multimap< sort_expression, sort_expression > &  map1,
std::set< sort_expression sorts_already_seen = std::set < sort_expression >() 
)
static

Definition at line 213 of file data_specification.cpp.

◆ find_sort()

sort_expression mcrl2::data::find_sort ( data_specification const &  data,
std::string const &  s 
)
inline

Finds a sort in a data specification.

Parameters
dataA data specification
sA string
Returns
The found sort

Definition at line 786 of file data_specification.h.

◆ find_sort_expressions() [1/5]

std::set< data::sort_expression > mcrl2::data::find_sort_expressions ( const data::data_equation x)

Definition at line 90 of file data.cpp.

◆ find_sort_expressions() [2/5]

std::set< data::sort_expression > mcrl2::data::find_sort_expressions ( const data::data_expression x)

Definition at line 91 of file data.cpp.

◆ find_sort_expressions() [3/5]

std::set< data::sort_expression > mcrl2::data::find_sort_expressions ( const data::sort_expression x)

Definition at line 92 of file data.cpp.

◆ find_sort_expressions() [4/5]

template<typename T >
std::set< data::sort_expression > mcrl2::data::find_sort_expressions ( const T &  x)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \return All sort expressions that occur in the object x

Definition at line 389 of file find.h.

◆ find_sort_expressions() [5/5]

template<typename T , typename OutputIterator >
void mcrl2::data::find_sort_expressions ( const T &  x,
OutputIterator  o 
)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \param[in,out] o an output iterator to which all sort expressions occurring in x are written. \return All sort expressions that occur in the term x

Definition at line 380 of file find.h.

◆ fourier_motzkin() [1/2]

void mcrl2::data::fourier_motzkin ( const data_expression e_in,
const variable_list vars_in,
data_expression e_out,
variable_list vars_out,
const rewriter r 
)
inline

Eliminate variables from a data expression using Gauss elimination and Fourier-Motzkin elimination.

Deliver a data_expression e_out and a set of variables vars_out such that exists vars_in.e_in is equivalent to exists vars_out.e_out. If the resulting list of inequalities is inconsistent, then [false] is returned.

Parameters
e_inAn input data_expression of sort Bool.
vars_inA container with variables. Supports iterating over these variables.
e_outThe output data expression of sort Bool.
vars_outA list of variables to store resulting variables. Initially empty.
rA rewriter.
Postcondition
exists vars_out.e_out == exists vars_in.e_in.

Definition at line 203 of file fourier_motzkin.h.

◆ fourier_motzkin() [2/2]

template<class Data_variable_iterator >
void mcrl2::data::fourier_motzkin ( const std::vector< linear_inequality > &  inequalities_in,
Data_variable_iterator  variables_begin,
Data_variable_iterator  variables_end,
std::vector< linear_inequality > &  resulting_inequalities,
const rewriter r 
)
inline

Definition at line 28 of file fourier_motzkin.h.

◆ free_variables()

variable_list mcrl2::data::free_variables ( const data_expression x)

Definition at line 188 of file data.cpp.

◆ function_and_mapping_identifiers()

std::set< core::identifier_string > mcrl2::data::function_and_mapping_identifiers ( const data_specification dataspec)
inline

Returns the names of functions and mappings that occur in a data specification.

Parameters
[in]dataspecA data specification

Definition at line 891 of file data_specification.h.

◆ function_update() [1/2]

function_symbol mcrl2::data::function_update ( const sort_expression s,
const sort_expression t 
)
inline

Constructor for function symbol @func_update.

Parameters
sA sort expression.
tA sort expression.
Returns
Function symbol function_update.

Definition at line 73 of file function_update.h.

◆ function_update() [2/2]

application mcrl2::data::function_update ( const sort_expression s,
const sort_expression t,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @func_update.

Parameters
sA sort expression.
tA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @func_update to a number of arguments.

Definition at line 100 of file function_update.h.

◆ function_update_cpp_implementable_constructors()

implementation_map mcrl2::data::function_update_cpp_implementable_constructors ( )
inline

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for function_update.

Returns
All system defined constructors that are to be implemented in C++ for function_update.

Definition at line 53 of file function_update.h.

◆ function_update_cpp_implementable_mappings()

implementation_map mcrl2::data::function_update_cpp_implementable_mappings ( const sort_expression s,
const sort_expression t 
)
inline

Give all system defined mappings that are to be implemented in C++ code for function_update.

Parameters
sA sort expression
tA sort expression
Returns
A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for function_update

Definition at line 423 of file function_update.h.

◆ function_update_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::function_update_generate_constructors_and_functions_code ( const sort_expression s,
const sort_expression t 
)
inline

Give all system defined mappings and constructors for function_update.

Parameters
sA sort expression
tA sort expression
Returns
All system defined mappings for function_update

Definition at line 390 of file function_update.h.

◆ function_update_generate_constructors_code()

function_symbol_vector mcrl2::data::function_update_generate_constructors_code ( )
inline

Give all system defined constructors for function_update.

Returns
All system defined constructors for function_update.

Definition at line 35 of file function_update.h.

◆ function_update_generate_equations_code()

data_equation_vector mcrl2::data::function_update_generate_equations_code ( const sort_expression s,
const sort_expression t 
)
inline

Give all system defined equations for function_update.

Parameters
sA sort expression
tA sort expression
Returns
All system defined equations for sort function_update

Definition at line 471 of file function_update.h.

◆ function_update_generate_functions_code()

function_symbol_vector mcrl2::data::function_update_generate_functions_code ( const sort_expression s,
const sort_expression t 
)
inline

Give all system defined mappings for function_update.

Parameters
sA sort expression
tA sort expression
Returns
All system defined mappings for function_update

Definition at line 375 of file function_update.h.

◆ function_update_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::function_update_mCRL2_usable_constructors ( )
inline

Give all defined constructors which can be used in mCRL2 specs for function_update.

Returns
All system defined constructors that can be used in an mCRL2 specification for function_update.

Definition at line 43 of file function_update.h.

◆ function_update_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::function_update_mCRL2_usable_mappings ( const sort_expression s,
const sort_expression t 
)
inline

Give all system defined mappings that can be used in mCRL2 specs for function_update.

Parameters
sA sort expression
tA sort expression
Returns
All system defined mappings for that can be used in mCRL2 specificationis function_update

Definition at line 405 of file function_update.h.

◆ function_update_name()

const core::identifier_string & mcrl2::data::function_update_name ( )
inline

Generate identifier @func_update.

Returns
Identifier @func_update.

Definition at line 62 of file function_update.h.

◆ function_update_stable() [1/2]

function_symbol mcrl2::data::function_update_stable ( const sort_expression s,
const sort_expression t 
)
inline

Constructor for function symbol @func_update_stable.

Parameters
sA sort expression.
tA sort expression.
Returns
Function symbol function_update_stable.

Definition at line 142 of file function_update.h.

◆ function_update_stable() [2/2]

application mcrl2::data::function_update_stable ( const sort_expression s,
const sort_expression t,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @func_update_stable.

Parameters
sA sort expression.
tA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @func_update_stable to a number of arguments.

Definition at line 169 of file function_update.h.

◆ function_update_stable_name()

const core::identifier_string & mcrl2::data::function_update_stable_name ( )
inline

Generate identifier @func_update_stable.

Returns
Identifier @func_update_stable.

Definition at line 131 of file function_update.h.

◆ gauss_elimination()

template<class Variable_iterator >
std::set< variable > mcrl2::data::gauss_elimination ( const std::vector< linear_inequality > &  inequalities,
std::vector< linear_inequality > &  resulting_equalities,
std::vector< linear_inequality > &  resulting_inequalities,
Variable_iterator  variables_begin,
Variable_iterator  variables_end,
const rewriter r 
)

Try to eliminate variables from a system of inequalities using Gauss elimination.

For all variables yi in y1,...,yn indicated by variables_begin to variables_end, it attempted to find and equation among inequalities of the form yi==expression. All occurrences of yi in equalities are subsequently replaced by yi. If no equation of the form yi can be found, yi is added to the list of variables that is returned by this function. If the input contains an inconsistent inequality, resulting_equalities becomes empty, resulting_inequalities contains false and the returned list of variables is also empty. The resulting equalities and inequalities do not contain linear inequalites equivalent to true.

Parameters
inequalitiesA list of inequalities over real numbers
resulting_equalitiesA list with the resulting equalities.
resulting_inequalitiesA list of the resulting inequalities
variables_beginAn iterator indicating the beginning of the eliminatable variables.
variables_endAn iterator indicating the end of the eliminatable variables.
rA rewriter.
Postcondition
variables contains the list of variables that have not been eliminated
Returns
The variables that could not be removed by gauss elimination.

Definition at line 1944 of file linear_inequalities.h.

◆ greater() [1/2]

application mcrl2::data::greater ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol >

Parameters
[in]arg0A data expression
[in]arg1A data expression
Returns
Application of > to a number of arguments

Definition at line 332 of file standard.h.

◆ greater() [2/2]

function_symbol mcrl2::data::greater ( const sort_expression s)
inline

Constructor for function symbol >

Parameters
[in]sA sort expression
Returns
function symbol greater

Definition at line 314 of file standard.h.

◆ greater_equal() [1/2]

application mcrl2::data::greater_equal ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol >=.

Parameters
[in]arg0A data expression
[in]arg1A data expression
Returns
Application of >= to a number of arguments

Definition at line 369 of file standard.h.

◆ greater_equal() [2/2]

function_symbol mcrl2::data::greater_equal ( const sort_expression s)
inline

Constructor for function symbol >=.

Parameters
[in]sA sort expression
Returns
function symbol greater_equal

Definition at line 351 of file standard.h.

◆ has_untyped_sort()

template<typename T >
bool mcrl2::data::has_untyped_sort ( const T &  x)

Definition at line 27 of file type_check_tree.h.

◆ if_() [1/2]

application mcrl2::data::if_ ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol if.

Parameters
[in]arg0A data expression
[in]arg1A data expression
[in]arg2A data expression
Returns
Application of if to a number of arguments

Definition at line 219 of file standard.h.

◆ if_() [2/2]

function_symbol mcrl2::data::if_ ( const sort_expression s)
inline

Constructor for function symbol if.

Parameters
[in]sA sort expression
Returns
function symbol if_

Definition at line 200 of file standard.h.

◆ if_always_else() [1/2]

function_symbol mcrl2::data::if_always_else ( const sort_expression s,
const sort_expression t 
)
inline

Constructor for function symbol @if_always_else.

Parameters
sA sort expression.
tA sort expression.
Returns
Function symbol if_always_else.

Definition at line 295 of file function_update.h.

◆ if_always_else() [2/2]

application mcrl2::data::if_always_else ( const sort_expression s,
const sort_expression t,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Application of function symbol @if_always_else.

Parameters
sA sort expression.
tA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
Application of @if_always_else to a number of arguments.

Definition at line 322 of file function_update.h.

◆ if_always_else_application()

data_expression mcrl2::data::if_always_else_application ( const data_expression a1)
inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 362 of file function_update.h.

◆ if_always_else_manual_implementation()

data_expression mcrl2::data::if_always_else_manual_implementation ( const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

The data expression of an application of the function symbol @if_always_else.

This function is to be implemented manually.

Parameters
arg0A data expression.
arg1A data expression.
arg2A data expression.
Returns
The data expression corresponding to an application of @if_always_else to a number of arguments.

Definition at line 46 of file function_update.h.

◆ if_always_else_name()

const core::identifier_string & mcrl2::data::if_always_else_name ( )
inline

Generate identifier @if_always_else.

Returns
Identifier @if_always_else.

Definition at line 284 of file function_update.h.

◆ if_rewrite() [1/2]

template<typename T >
T mcrl2::data::if_rewrite ( const T &  x,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 226 of file if_rewriter.h.

◆ if_rewrite() [2/2]

template<typename T >
void mcrl2::data::if_rewrite ( T &  x,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 220 of file if_rewriter.h.

◆ imp()

data_expression mcrl2::data::imp ( const data_expression x,
const data_expression y 
)
inline
Returns
The implication of x and y

Definition at line 127 of file consistency.h.

◆ is_a_redundant_inequality()

bool mcrl2::data::is_a_redundant_inequality ( const std::vector< linear_inequality > &  inequalities,
const std::vector< linear_inequality > ::iterator  i,
const rewriter r 
)
inline

Indicate whether an inequality from a set of inequalities is redundant.

Return whether the inequality referred to by i is inconsistent. It is expected that i refers to an equality in the vector inequalities. The vector inequalities might be changed within the procedure, but will be restored to its original value when this function terminates.

Parameters
inequalitiesA list of inequalities
iAn iterator pointing into inequalities.
rA rewriter
Returns
An indication whether the inequality referred to by i is inconsistent in the context of inequalities.

Definition at line 1092 of file linear_inequalities.h.

◆ is_abstraction()

bool mcrl2::data::is_abstraction ( const atermpp::aterm x)
inline

Returns true if the term t is an abstraction.

Definition at line 26 of file data_expression.h.

◆ is_alias()

bool mcrl2::data::is_alias ( const atermpp::aterm_appl x)
inline

\brief Test for a alias expression \param x A term \return True if \a x is a alias expression

Definition at line 81 of file alias.h.

◆ is_and()

bool mcrl2::data::is_and ( const data_expression x)
inline

Test if x is a conjunction.

Parameters
xa data expression

Definition at line 61 of file consistency.h.

◆ is_application() [1/2]

bool mcrl2::data::is_application ( const atermpp::aterm_appl x)
inline

Returns true if the term t is an application.

This function is inefficient as the arity of a term must be determined and an inspection must take place in an array of function symbols. Therefore, there is an more efficient overload is_application(const data_expression& x).

Definition at line 84 of file data_expression.h.

◆ is_application() [2/2]

bool mcrl2::data::is_application ( const data_expression t)
inline

Returns true if the term t is an application.

Parameters
tThe variable that is checked.

Definition at line 280 of file data_expression.h.

◆ is_application_no_check()

bool mcrl2::data::is_application_no_check ( const atermpp::aterm_appl x)
inline

Returns true if the term t is an application, but it does not check whether an application symbol of sufficient arity exists, assuming this is ok.

Definition at line 92 of file data_expression.h.

◆ is_assignment()

bool mcrl2::data::is_assignment ( const atermpp::aterm_appl x)
inline

\brief Test for a assignment expression \param x A term \return True if \a x is a assignment expression

Definition at line 155 of file assignment.h.

◆ is_assignment_expression()

bool mcrl2::data::is_assignment_expression ( const atermpp::aterm_appl x)
inline

\brief Test for a assignment_expression expression \param x A term \return True if \a x is a assignment_expression expression

Definition at line 63 of file assignment.h.

◆ is_bag_comprehension()

bool mcrl2::data::is_bag_comprehension ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a bag comprehension.

Definition at line 56 of file data_expression.h.

◆ is_bag_comprehension_binder()

bool mcrl2::data::is_bag_comprehension_binder ( const atermpp::aterm_appl x)
inline

\brief Test for a bag_comprehension_binder expression \param x A term \return True if \a x is a bag_comprehension_binder expression

Definition at line 209 of file binder_type.h.

◆ is_bag_container()

bool mcrl2::data::is_bag_container ( const atermpp::aterm_appl x)
inline

\brief Test for a bag_container expression \param x A term \return True if \a x is a bag_container expression

Definition at line 209 of file container_type.h.

◆ is_basic_sort()

bool mcrl2::data::is_basic_sort ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a basic sort.

Definition at line 25 of file sort_expression.h.

◆ is_bool()

bool mcrl2::data::is_bool ( const sort_expression x)
inline
Returns
Test if x is the boolean sort

Definition at line 134 of file consistency.h.

◆ is_closed_real_number()

bool mcrl2::data::is_closed_real_number ( const data_expression e)
inline

Definition at line 979 of file linear_inequalities.h.

◆ is_constant()

bool mcrl2::data::is_constant ( const data_expression x)
inline

Definition at line 254 of file data_expression.h.

◆ is_container_sort()

bool mcrl2::data::is_container_sort ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a container sort.

Definition at line 37 of file sort_expression.h.

◆ is_convertible()

bool mcrl2::data::is_convertible ( const sort_expression s1,
const sort_expression s2 
)
inline

Returns true if and only if s1 == s2, or if s1 is a less specific numeric type than s2.

Parameters
[in]s1a sort expression
[in]s2a sort expression

Definition at line 515 of file standard_numbers_utility.h.

◆ is_data_equation()

bool mcrl2::data::is_data_equation ( const atermpp::aterm_appl t)
inline

Recognizer function.

Parameters
[in]tA aterm appl of which it is checked whether it is a data_equation.
Returns
True if the provided argument is a data_equation.

Definition at line 150 of file data_equation.h.

◆ is_data_expression()

bool mcrl2::data::is_data_expression ( const atermpp::aterm_appl x)
inline

Test for a data_expression expression.

Parameters
xA term
Returns
True if it is a data_expression expression

Definition at line 215 of file data_expression.h.

◆ is_data_specification()

bool mcrl2::data::is_data_specification ( const atermpp::aterm_appl x)
inline

Test for a data specification expression.

Parameters
xA term
Returns
True if x is a data specification expression

Definition at line 40 of file data_specification.h.

◆ is_enumerable()

template<typename Rewriter >
static bool mcrl2::data::is_enumerable ( const data_specification dataspec,
const Rewriter &  rewr,
const sort_expression sort 
)
static

Definition at line 222 of file enumerator.h.

◆ is_equal_to()

bool mcrl2::data::is_equal_to ( const data_expression x)
inline

Test if x is an equality.

Parameters
xa data expression

Definition at line 77 of file consistency.h.

◆ is_equal_to_application()

template<typename DataExpression >
bool mcrl2::data::is_equal_to_application ( const DataExpression &  e)
inline

Recogniser for application of ==.

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol equal_to to a number of arguments

Definition at line 155 of file standard.h.

◆ is_equal_to_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_equal_to_function_symbol ( const DataExpression &  e)
inline

Recogniser for function ==.

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching ==

Definition at line 135 of file standard.h.

◆ is_exists()

bool mcrl2::data::is_exists ( const atermpp::aterm_appl x)
inline

Returns true if the term t is an existential quantification.

Definition at line 44 of file data_expression.h.

◆ is_exists_binder()

bool mcrl2::data::is_exists_binder ( const atermpp::aterm_appl x)
inline

\brief Test for a exists_binder expression \param x A term \return True if \a x is a exists_binder expression

Definition at line 315 of file binder_type.h.

◆ is_false()

bool mcrl2::data::is_false ( const data_expression x)
inline

Test if x is false.

Parameters
xa data expression

Definition at line 37 of file consistency.h.

◆ is_fbag_container()

bool mcrl2::data::is_fbag_container ( const atermpp::aterm_appl x)
inline

\brief Test for a fbag_container expression \param x A term \return True if \a x is a fbag_container expression

Definition at line 315 of file container_type.h.

◆ is_forall()

bool mcrl2::data::is_forall ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a universal quantification.

Definition at line 38 of file data_expression.h.

◆ is_forall_binder()

bool mcrl2::data::is_forall_binder ( const atermpp::aterm_appl x)
inline

\brief Test for a forall_binder expression \param x A term \return True if \a x is a forall_binder expression

Definition at line 262 of file binder_type.h.

◆ is_fset_container()

bool mcrl2::data::is_fset_container ( const atermpp::aterm_appl x)
inline

\brief Test for a fset_container expression \param x A term \return True if \a x is a fset_container expression

Definition at line 262 of file container_type.h.

◆ is_function_sort()

bool mcrl2::data::is_function_sort ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a function sort.

Definition at line 31 of file sort_expression.h.

◆ is_function_symbol()

bool mcrl2::data::is_function_symbol ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a function symbol.

Definition at line 68 of file data_expression.h.

◆ is_function_update_application()

bool mcrl2::data::is_function_update_application ( const atermpp::aterm_appl e)
inline

Recogniser for application of @func_update.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol function_update to a number of arguments.

Definition at line 123 of file function_update.h.

◆ is_function_update_function_symbol()

bool mcrl2::data::is_function_update_function_symbol ( const atermpp::aterm_appl e)
inline

Recogniser for function @func_update.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @func_update.

Definition at line 83 of file function_update.h.

◆ is_function_update_stable_application()

bool mcrl2::data::is_function_update_stable_application ( const atermpp::aterm_appl e)
inline

Recogniser for application of @func_update_stable.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol function_update_stable to a number of arguments.

Definition at line 192 of file function_update.h.

◆ is_function_update_stable_function_symbol()

bool mcrl2::data::is_function_update_stable_function_symbol ( const atermpp::aterm_appl e)
inline

Recogniser for function @func_update_stable.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @func_update_stable.

Definition at line 152 of file function_update.h.

◆ is_greater_application()

template<typename DataExpression >
bool mcrl2::data::is_greater_application ( const DataExpression &  e)
inline

Recogniser for application of >

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol greater to a number of arguments

Definition at line 343 of file standard.h.

◆ is_greater_equal_application()

template<typename DataExpression >
bool mcrl2::data::is_greater_equal_application ( const DataExpression &  e)
inline

Recogniser for application of >=.

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol greater_equal to a number of arguments

Definition at line 380 of file standard.h.

◆ is_greater_equal_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_greater_equal_function_symbol ( const DataExpression &  e)
inline

Recogniser for function >=.

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching >=

Definition at line 360 of file standard.h.

◆ is_greater_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_greater_function_symbol ( const DataExpression &  e)
inline

Recogniser for function >

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching >

Definition at line 323 of file standard.h.

◆ is_if_always_else_application()

bool mcrl2::data::is_if_always_else_application ( const atermpp::aterm_appl e)
inline

Recogniser for application of @if_always_else.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol if_always_else to a number of arguments.

Definition at line 345 of file function_update.h.

◆ is_if_always_else_function_symbol()

bool mcrl2::data::is_if_always_else_function_symbol ( const atermpp::aterm_appl e)
inline

Recogniser for function @if_always_else.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @if_always_else.

Definition at line 305 of file function_update.h.

◆ is_if_application()

template<typename DataExpression >
bool mcrl2::data::is_if_application ( const DataExpression &  e)
inline

Recogniser for application of if.

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol if_ to a number of arguments

Definition at line 232 of file standard.h.

◆ is_if_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_if_function_symbol ( const DataExpression &  e)
inline

Recogniser for function if.

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching if_

Definition at line 209 of file standard.h.

◆ is_imp()

bool mcrl2::data::is_imp ( const data_expression x)
inline

Test if x is an implication.

Parameters
xa data expression

Definition at line 69 of file consistency.h.

◆ is_inconsistent()

bool mcrl2::data::is_inconsistent ( const std::vector< linear_inequality > &  inequalities_in,
const rewriter r,
const bool  use_cache 
)
inline

Determine whether a list of data expressions is inconsistent.

First it is checked whether false is among the input. If not, Fourier-Motzkin is applied to all variables in the inequalities. If the empty vector of equalities is the result, the input was consistent. Otherwise the resulting vector contains an inconsistent inequality. The implementation uses a feasible point detection algorithm as described by Bruno Dutertre and Leonardo de Moura. Integrating Simplex with DPLL(T). CSL Technical Report SRI-CSL-06-01, 2006.

Parameters
inequalities_inA list of inequalities.
rA rewriter.
use_cacheA boolean indicating whether results can be cahced.
Returns
true if the system of inequalities can be determined to be inconsistent, false otherwise.

Definition at line 1570 of file linear_inequalities.h.

◆ is_is_not_a_function_update_application()

bool mcrl2::data::is_is_not_a_function_update_application ( const atermpp::aterm_appl e)
inline

Recogniser for application of @is_not_an_update.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol is_not_a_function_update to a number of arguments.

Definition at line 257 of file function_update.h.

◆ is_is_not_a_function_update_function_symbol()

bool mcrl2::data::is_is_not_a_function_update_function_symbol ( const atermpp::aterm_appl e)
inline

Recogniser for function @is_not_an_update.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @is_not_an_update.

Definition at line 221 of file function_update.h.

◆ is_lambda()

bool mcrl2::data::is_lambda ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a lambda abstraction.

Definition at line 32 of file data_expression.h.

◆ is_lambda_binder()

bool mcrl2::data::is_lambda_binder ( const atermpp::aterm_appl x)
inline

\brief Test for a lambda_binder expression \param x A term \return True if \a x is a lambda_binder expression

Definition at line 368 of file binder_type.h.

◆ is_left_associative()

bool mcrl2::data::is_left_associative ( const data_expression x)
inline

Definition at line 384 of file print.h.

◆ is_less_application()

template<typename DataExpression >
bool mcrl2::data::is_less_application ( const DataExpression &  e)
inline

Recogniser for application of <.

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol less to a number of arguments

Definition at line 269 of file standard.h.

◆ is_less_equal_application()

template<typename DataExpression >
bool mcrl2::data::is_less_equal_application ( const DataExpression &  e)
inline

Recogniser for application of <=.

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol less_equal to a number of arguments

Definition at line 306 of file standard.h.

◆ is_less_equal_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_less_equal_function_symbol ( const DataExpression &  e)
inline

Recogniser for function <=.

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching <=

Definition at line 286 of file standard.h.

◆ is_less_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_less_function_symbol ( const DataExpression &  e)
inline

Recogniser for function <.

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching <

Definition at line 249 of file standard.h.

◆ is_list_container()

bool mcrl2::data::is_list_container ( const atermpp::aterm_appl x)
inline

\brief Test for a list_container expression \param x A term \return True if \a x is a list_container expression

Definition at line 103 of file container_type.h.

◆ is_negative()

bool mcrl2::data::is_negative ( const data_expression e,
const rewriter r 
)
inline

Definition at line 990 of file linear_inequalities.h.

◆ is_not()

bool mcrl2::data::is_not ( const data_expression x)
inline

Test if x is a negation.

Parameters
xa data expression

Definition at line 45 of file consistency.h.

◆ is_not_a_function_update() [1/2]

function_symbol mcrl2::data::is_not_a_function_update ( const sort_expression s,
const sort_expression t 
)
inline

Constructor for function symbol @is_not_an_update.

Parameters
sA sort expression.
tA sort expression.
Returns
Function symbol is_not_a_function_update.

Definition at line 211 of file function_update.h.

◆ is_not_a_function_update() [2/2]

application mcrl2::data::is_not_a_function_update ( const sort_expression s,
const sort_expression t,
const data_expression arg0 
)
inline

Application of function symbol @is_not_an_update.

Parameters
sA sort expression.
tA sort expression.
arg0A data expression.
Returns
Application of @is_not_an_update to a number of arguments.

Definition at line 236 of file function_update.h.

◆ is_not_a_function_update_application()

data_expression mcrl2::data::is_not_a_function_update_application ( const data_expression a1)
inline

Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.

Definition at line 272 of file function_update.h.

◆ is_not_a_function_update_manual_implementation()

data_expression mcrl2::data::is_not_a_function_update_manual_implementation ( const data_expression arg0)
inline

The data expression of an application of the function symbol @is_not_an_update.

This function is to be implemented manually.

Parameters
arg0A data expression.
Returns
The data expression corresponding to an application of @is_not_an_update to a number of arguments.

Definition at line 28 of file function_update.h.

◆ is_not_a_function_update_name()

const core::identifier_string & mcrl2::data::is_not_a_function_update_name ( )
inline

Generate identifier @is_not_an_update.

Returns
Identifier @is_not_an_update.

Definition at line 200 of file function_update.h.

◆ is_not_equal_to()

bool mcrl2::data::is_not_equal_to ( const data_expression x)
inline

Test if x is an inequality.

Parameters
xa data expression

Definition at line 85 of file consistency.h.

◆ is_not_equal_to_application()

template<typename DataExpression >
bool mcrl2::data::is_not_equal_to_application ( const DataExpression &  e)
inline

Recogniser for application of !=.

Parameters
[in]eA data expression
Returns
true iff e is an application of function symbol not_equal_to to a number of arguments

Definition at line 192 of file standard.h.

◆ is_not_equal_to_function_symbol()

template<typename DataExpression >
bool mcrl2::data::is_not_equal_to_function_symbol ( const DataExpression &  e)
inline

Recogniser for function !=.

Parameters
[in]eA data expression
Returns
true iff e is the function symbol matching !=

Definition at line 172 of file standard.h.

◆ is_or()

bool mcrl2::data::is_or ( const data_expression x)
inline

Test if x is a disjunction.

Parameters
xa data expression

Definition at line 53 of file consistency.h.

◆ is_pattern_matching_rule()

template<typename StructInfo >
bool mcrl2::data::is_pattern_matching_rule ( StructInfo &  ssf,
const data_equation rewrite_rule 
)

Check whether the given rewrite rule can be classified as a pattern matching rule.

That is, its arguments are constructed only out of unique variable occurrences and constructor function symbols and constructor function applications.

Definition at line 363 of file unfold_pattern_matching.h.

◆ is_positive()

bool mcrl2::data::is_positive ( const data_expression e,
const rewriter r 
)
inline

Definition at line 1004 of file linear_inequalities.h.

◆ is_right_associative()

bool mcrl2::data::is_right_associative ( const data_expression x)
inline

Definition at line 390 of file print.h.

◆ is_set_comprehension()

bool mcrl2::data::is_set_comprehension ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a set comprehension.

Definition at line 50 of file data_expression.h.

◆ is_set_comprehension_binder()

bool mcrl2::data::is_set_comprehension_binder ( const atermpp::aterm_appl x)
inline

\brief Test for a set_comprehension_binder expression \param x A term \return True if \a x is a set_comprehension_binder expression

Definition at line 156 of file binder_type.h.

◆ is_set_container()

bool mcrl2::data::is_set_container ( const atermpp::aterm_appl x)
inline

\brief Test for a set_container expression \param x A term \return True if \a x is a set_container expression

Definition at line 156 of file container_type.h.

◆ is_simple_substitution() [1/7]

template<>
bool mcrl2::data::is_simple_substitution ( const assignment_sequence_substitution sigma)
inline

Definition at line 52 of file assignment_sequence_substitution.h.

◆ is_simple_substitution() [2/7]

bool mcrl2::data::is_simple_substitution ( const data::variable lhs,
const data::data_expression rhs 
)
inline

Returns true if FV(rhs) is included in {lhs}.

Definition at line 34 of file is_simple_substitution.h.

◆ is_simple_substitution() [3/7]

bool mcrl2::data::is_simple_substitution ( const enumerator_substitution sigma)
inline

Definition at line 163 of file enumerator_substitution.h.

◆ is_simple_substitution() [4/7]

template<typename AssociativeContainer >
bool mcrl2::data::is_simple_substitution ( const map_substitution< AssociativeContainer > &  sigma)

Definition at line 86 of file map_substitution.h.

◆ is_simple_substitution() [5/7]

template<typename AssociativeContainer >
bool mcrl2::data::is_simple_substitution ( const mutable_map_substitution< AssociativeContainer > &  sigma)

Definition at line 207 of file mutable_map_substitution.h.

◆ is_simple_substitution() [6/7]

template<typename VariableContainer , typename ExpressionContainer >
bool mcrl2::data::is_simple_substitution ( const sequence_sequence_substitution< VariableContainer, ExpressionContainer > &  sigma)

Definition at line 91 of file sequence_sequence_substitution.h.

◆ is_simple_substitution() [7/7]

template<typename Substitution >
bool mcrl2::data::is_simple_substitution ( const Substitution &  )

Returns true if the substitution sigma satisfies the property that FV(sigma(x)) is included in {x} for all variables x.

Note
The default return value is true, so a template specialization is required to enable this check for substitutions.

Definition at line 27 of file is_simple_substitution.h.

◆ is_sort_expression()

bool mcrl2::data::is_sort_expression ( const atermpp::aterm_appl x)
inline

Test for a sort_expression expression.

Parameters
xA term
Returns
True if it is a sort_expression expression

Definition at line 131 of file sort_expression.h.

◆ is_structured_sort()

bool mcrl2::data::is_structured_sort ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a structured sort.

Definition at line 43 of file sort_expression.h.

◆ is_structured_sort_constructor()

bool mcrl2::data::is_structured_sort_constructor ( const atermpp::aterm_appl x)
inline

\brief Test for a structured_sort_constructor expression \param x A term \return True if \a x is a structured_sort_constructor expression

Definition at line 208 of file structured_sort_constructor.h.

◆ is_structured_sort_constructor_argument()

bool mcrl2::data::is_structured_sort_constructor_argument ( const atermpp::aterm_appl x)
inline

\brief Test for a structured_sort_constructor_argument expression \param x A term \return True if \a x is a structured_sort_constructor_argument expression

Definition at line 102 of file structured_sort_constructor_argument.h.

◆ is_sub_sort()

bool mcrl2::data::is_sub_sort ( const sort_expression x1,
const sort_expression x2 
)
inline

Definition at line 45 of file is_sub_sort.h.

◆ is_system_defined()

bool mcrl2::data::is_system_defined ( const sort_expression s)
inline

Returns true iff the expression represents a standard sort.

Parameters
[in]sa sort expression.

Definition at line 48 of file standard_utility.h.

◆ is_true()

bool mcrl2::data::is_true ( const data_expression x)
inline

Test if x is true.

Parameters
xa data expression

Definition at line 29 of file consistency.h.

◆ is_untyped_data_parameter()

bool mcrl2::data::is_untyped_data_parameter ( const atermpp::aterm_appl x)
inline

\brief Test for a untyped_data_parameter expression \param x A term \return True if \a x is a untyped_data_parameter expression

Definition at line 84 of file untyped_data_parameter.h.

◆ is_untyped_identifier()

bool mcrl2::data::is_untyped_identifier ( const atermpp::aterm_appl x)
inline

Returns true if the term t is an identifier.

Definition at line 104 of file data_expression.h.

◆ is_untyped_identifier_assignment()

bool mcrl2::data::is_untyped_identifier_assignment ( const atermpp::aterm_appl x)
inline

\brief Test for a untyped_identifier_assignment expression \param x A term \return True if \a x is a untyped_identifier_assignment expression

Definition at line 251 of file assignment.h.

◆ is_untyped_possible_sorts()

bool mcrl2::data::is_untyped_possible_sorts ( const atermpp::aterm_appl x)
inline

Returns true if the term t is an expression for multiple possible sorts.

Definition at line 55 of file sort_expression.h.

◆ is_untyped_set_or_bag_comprehension()

bool mcrl2::data::is_untyped_set_or_bag_comprehension ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a set/bag comprehension.

Definition at line 62 of file data_expression.h.

◆ is_untyped_set_or_bag_comprehension_binder()

bool mcrl2::data::is_untyped_set_or_bag_comprehension_binder ( const atermpp::aterm_appl x)
inline

\brief Test for a untyped_set_or_bag_comprehension_binder expression \param x A term \return True if \a x is a untyped_set_or_bag_comprehension_binder expression

Definition at line 103 of file binder_type.h.

◆ is_untyped_sort()

bool mcrl2::data::is_untyped_sort ( const atermpp::aterm_appl x)
inline

Returns true if the term t is the unknown sort.

Definition at line 49 of file sort_expression.h.

◆ is_untyped_sort_variable()

bool mcrl2::data::is_untyped_sort_variable ( const atermpp::aterm_appl x)
inline

\brief Test for a untyped_sort_variable expression \param x A term \return True if \a x is a untyped_sort_variable expression

Definition at line 74 of file untyped_sort_variable.h.

◆ is_variable()

bool mcrl2::data::is_variable ( const atermpp::aterm x)
inline

Returns true if the term t is a variable.

Definition at line 74 of file data_expression.h.

◆ is_where_clause()

bool mcrl2::data::is_where_clause ( const atermpp::aterm_appl x)
inline

Returns true if the term t is a where clause.

Definition at line 98 of file data_expression.h.

◆ is_zero()

bool mcrl2::data::is_zero ( const data_expression e)
inline

Definition at line 1018 of file linear_inequalities.h.

◆ join_and()

template<typename FwdIt >
data_expression mcrl2::data::join_and ( FwdIt  first,
FwdIt  last 
)

Returns and applied to the sequence of data expressions [first, last)

Parameters
firstStart of a sequence of data expressions
lastEnd of a sequence of of data expressions
Returns
And applied to the sequence of data expressions [first, last)

Definition at line 40 of file join.h.

◆ join_or()

template<typename FwdIt >
data_expression mcrl2::data::join_or ( FwdIt  first,
FwdIt  last 
)

Returns or applied to the sequence of data expressions [first, last)

Parameters
firstStart of a sequence of data expressions
lastEnd of a sequence of of data expressions
Returns
Or applied to the sequence of data expressions [first, last)

Definition at line 29 of file join.h.

◆ join_or_is_element_of_constraints()

std::vector< constraint_ptr > mcrl2::data::join_or_is_element_of_constraints ( const std::vector< constraint_ptr > &  constraints)
inline

Definition at line 467 of file type_check_tree.h.

◆ left_hand_sides()

variable_list mcrl2::data::left_hand_sides ( const assignment_list x)
inline

Returns the left hand sides of an assignment list.

Parameters
xAn assignment list

Definition at line 310 of file assignment.h.

◆ less() [1/2]

application mcrl2::data::less ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol <.

Parameters
[in]arg0A data expression
[in]arg1A data expression
Returns
Application of < to a number of arguments

Definition at line 258 of file standard.h.

◆ less() [2/2]

function_symbol mcrl2::data::less ( const sort_expression s)
inline

Constructor for function symbol <.

Parameters
[in]sA sort expression
Returns
function symbol less

Definition at line 240 of file standard.h.

◆ less_equal() [1/2]

application mcrl2::data::less_equal ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol <=.

Parameters
[in]arg0A data expression
[in]arg1A data expression
Returns
Application of <= to a number of arguments

Definition at line 295 of file standard.h.

◆ less_equal() [2/2]

function_symbol mcrl2::data::less_equal ( const sort_expression s)
inline

Constructor for function symbol <=.

Parameters
[in]sA sort expression
Returns
function symbol less_equal

Definition at line 277 of file standard.h.

◆ make_abstraction()

template<class... ARGUMENTS>
void mcrl2::data::make_abstraction ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 75 of file abstraction.h.

◆ make_alias()

template<class... ARGUMENTS>
void mcrl2::data::make_alias ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_alias constructs a new term into a given address. \

Parameters
tThe reference into which the new alias is constructed.

Definition at line 66 of file alias.h.

◆ make_and_constraint()

constraint_ptr mcrl2::data::make_and_constraint ( const std::vector< constraint_ptr > &  alternatives)
inline

Definition at line 556 of file type_check_tree.h.

◆ make_application() [1/7]

void mcrl2::data::make_application ( atermpp::aterm result)
inline

Make function for an application.

Parameters
resultvariable into which the application is constructed.

Definition at line 546 of file application.h.

◆ make_application() [2/7]

template<typename FwdIter , class ArgumentConverter >
static void mcrl2::data::make_application ( atermpp::aterm result,
const data_expression head,
FwdIter  first,
FwdIter  last,
ArgumentConverter  convert_arguments,
const bool  skip_first_argument = false,
typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *  = nullptr,
typename std::enable_if< !std::is_base_of< data_expression, ArgumentConverter >::value >::type *  = nullptr,
typename std::enable_if< std::is_same< typename std::invoke_result< ArgumentConverter, data_expression &, typename FwdIter::value_type >::type, void >::value >::type *  = nullptr 
)
inlinestatic

Constructor.

Construct at term head(arg_first,...,arg_last) where convert_arguments has been applied to the head and all the arguments.

Parameters
resultvariable into which the application is constructed. \parameter head This is the new head for the application. \parameter first This is a forward iterator yielding the first argument. \parameter last This is an iterator beyond the last argument. \parameter convert_arguments This is a function applied to optionally the head and the arguments. \parameter skip_first_argument A boolean which is true if the function must not be applied to the head.

Definition at line 691 of file application.h.

◆ make_application() [3/7]

template<typename FwdIter , class ArgumentConverter >
void mcrl2::data::make_application ( atermpp::aterm result,
const data_expression head,
FwdIter  first,
FwdIter  last,
ArgumentConverter  convert_arguments,
const bool  skip_first_argument = false,
typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *  = nullptr,
typename std::enable_if< !std::is_base_of< data_expression, ArgumentConverter >::value >::type *  = nullptr,
typename std::enable_if< std::is_same< typename std::invoke_result< ArgumentConverter, typename FwdIter::value_type >::type, data_expression >::value >::type *  = nullptr 
)
inline

Constructor.

Construct at term head(arg_first,...,arg_last) where convert_arguments has been applied to the head and all the arguments.

Parameters
resultvariable into which the application is constructed. \parameter head This is the new head for the application. \parameter first This is a forward iterator yielding the first argument. \parameter last This is an iterator beyond the last argument. \parameter convert_arguments This is a function applied to optionally the head and the arguments. \parameter skip_first_argument A boolean which is true if the function must not be applied to the head.

Definition at line 660 of file application.h.

◆ make_application() [4/7]

template<typename FwdIter >
void mcrl2::data::make_application ( atermpp::aterm result,
const data_expression head,
FwdIter  first,
FwdIter  last,
typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *  = nullptr 
)
inline

Constructor.

Parameters
resultvariable into which the application is constructed.

Definition at line 612 of file application.h.

◆ make_application() [5/7]

template<typename HEAD , typename TERM , typename ... Terms, typename = std::enable_if_t< std::disjunction<typename std::is_convertible<HEAD, data_expression>, typename std::is_invocable_r<void, HEAD, data_expression&>, typename std::is_invocable_r<const data_expression, HEAD, void> >::value >, typename = std::enable_if_t<std::conjunction_v< std::disjunction<typename std::is_convertible<Terms, data_expression>, typename std::is_invocable_r<void, Terms, data_expression&>, typename std::is_invocable_r<const data_expression, Terms, void> > ...>>>
void mcrl2::data::make_application ( atermpp::aterm result,
const HEAD &  head,
const TERM &  arg1,
const Terms &...  other_arguments 
)
inline

Constructor.

Parameters
resultvariable into which the application is constructed.

Definition at line 578 of file application.h.

◆ make_application() [6/7]

template<typename FwdIter >
void mcrl2::data::make_application ( atermpp::aterm result,
const std::size_t  arity,
const data_expression head,
FwdIter  first,
FwdIter  last,
typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *  = 0 
)
inline

Constructor.

Parameters
resultvariable into which the application is constructed.

Definition at line 631 of file application.h.

◆ make_application() [7/7]

template<typename Container >
void mcrl2::data::make_application ( data_expression result,
const data_expression head,
const Container &  arguments,
typename atermpp::enable_if_container< Container, data_expression >::type *  = nullptr 
)
inline

Constructor.

Parameters
resultvariable into which the application is constructed.

Definition at line 596 of file application.h.

◆ make_assignment()

template<class... ARGUMENTS>
void mcrl2::data::make_assignment ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_assignment constructs a new term into a given address. \

Parameters
tThe reference into which the new assignment is constructed.

Definition at line 140 of file assignment.h.

◆ make_assignment_list()

template<typename VariableSequence , typename ExpressionSequence >
assignment_list mcrl2::data::make_assignment_list ( const VariableSequence &  variables,
const ExpressionSequence &  expressions 
)

Converts an iterator range to data_expression_list.

Parameters
variablesA sequence of variables.
expressionsA sequence of variables.
Precondition
length(variables) == length(expressions)
Note
This function uses implementation details of the iterator type and hence is sometimes efficient than copying all elements of the list.

Definition at line 301 of file assignment.h.

◆ make_assignment_vector()

template<typename VariableSequence , typename ExpressionSequence >
assignment_vector mcrl2::data::make_assignment_vector ( VariableSequence const &  variables,
ExpressionSequence const &  expressions 
)

Constructs an assignment_list by pairwise combining a variable and expression.

Parameters
variablesA sequence of data variables
expressionsA sequence of data expressions
Returns
The corresponding assignment list.

Definition at line 281 of file assignment.h.

◆ make_bag_comprehension()

template<class... ARGUMENTS>
void mcrl2::data::make_bag_comprehension ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 62 of file bag_comprehension.h.

◆ make_basic_sort()

template<class... ARGUMENTS>
void mcrl2::data::make_basic_sort ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_basic_sort constructs a new term into a given address. \

Parameters
tThe reference into which the new basic_sort is constructed.

Definition at line 66 of file basic_sort.h.

◆ make_container_sort()

template<class... ARGUMENTS>
void mcrl2::data::make_container_sort ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_container_sort constructs a new term into a given address. \

Parameters
tThe reference into which the new container_sort is constructed.

Definition at line 67 of file container_sort.h.

◆ make_data_equation()

template<class... ARGUMENTS>
void mcrl2::data::make_data_equation ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_data_equation constructs a new term into a given address. \

Parameters
tThe reference into which the new data_equation is constructed.

Definition at line 116 of file data_equation.h.

◆ make_data_expression()

void mcrl2::data::make_data_expression ( data_expression result)
inline

Definition at line 206 of file data_expression.h.

◆ make_data_expression_list()

template<typename Container >
data_expression_list mcrl2::data::make_data_expression_list ( Container const &  r,
typename atermpp::enable_if_container< Container, data_expression >::type *  = nullptr 
)
inline

Converts an container with data expressions to data_expression_list.

Parameters
rA range of data expressions.
Note
This function uses implementation details of the iterator type and hence is sometimes efficient than copying all elements of the list.

Definition at line 235 of file data_expression.h.

◆ make_exists()

template<class... ARGUMENTS>
void mcrl2::data::make_exists ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 64 of file exists.h.

◆ make_exists_()

data_expression mcrl2::data::make_exists_ ( const data::variable_list v,
const data_expression x 
)
inline

Make an existential quantification. It checks for an empty variable list, which is not allowed.

Parameters
vA sequence of data variables
xA data expression
Returns
The value exists v.x

Definition at line 167 of file consistency.h.

◆ make_false_constraint()

constraint_ptr mcrl2::data::make_false_constraint ( const std::string &  message)
inline

Definition at line 233 of file type_check_tree.h.

◆ make_forall()

template<class... ARGUMENTS>
void mcrl2::data::make_forall ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 64 of file forall.h.

◆ make_forall_()

data_expression mcrl2::data::make_forall_ ( const data::variable_list v,
const data_expression x 
)
inline

Make a universal quantification. It checks for an empty variable list, which is not allowed.

Parameters
vA sequence of data variables
xA data expression
Returns
The value forall v.x

Definition at line 152 of file consistency.h.

◆ make_function_sort()

template<class... ARGUMENTS>
void mcrl2::data::make_function_sort ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_function_sort constructs a new term into a given address. \

Parameters
tThe reference into which the new function_sort is constructed.

Definition at line 72 of file function_sort.h.

◆ make_function_sort_() [1/4]

function_sort mcrl2::data::make_function_sort_ ( const sort_expression dom1,
const sort_expression codomain 
)
inline

Convenience constructor for function sort with domain size 1.

Parameters
[in]dom1The first sort of the domain.
[in]codomainThe codomain of the sort.
Postcondition
*this represents dom1 -> codomain

Definition at line 107 of file function_sort.h.

◆ make_function_sort_() [2/4]

function_sort mcrl2::data::make_function_sort_ ( const sort_expression dom1,
const sort_expression dom2,
const sort_expression codomain 
)
inline

Convenience constructor for function sort with domain size 2.

Parameters
[in]dom1The first sort of the domain.
[in]dom2The second sort of the domain.
[in]codomainThe codomain of the sort.
Postcondition
*this represents dom1 # dom2 -> codomain

Definition at line 119 of file function_sort.h.

◆ make_function_sort_() [3/4]

function_sort mcrl2::data::make_function_sort_ ( const sort_expression dom1,
const sort_expression dom2,
const sort_expression dom3,
const sort_expression codomain 
)
inline

Convenience constructor for function sort with domain size 3.

Parameters
[in]dom1The first sort of the domain.
[in]dom2The second sort of the domain.
[in]dom3The third sort of the domain.
[in]codomainThe codomain of the sort.
Postcondition
*this represents dom1 # dom2 # dom3 -> codomain

Definition at line 133 of file function_sort.h.

◆ make_function_sort_() [4/4]

function_sort mcrl2::data::make_function_sort_ ( const sort_expression dom1,
const sort_expression dom2,
const sort_expression dom3,
const sort_expression dom4,
const sort_expression codomain 
)
inline

Convenience constructor for function sort with domain size 4.

Parameters
[in]dom1The first sort of the domain.
[in]dom2The second sort of the domain.
[in]dom3The third sort of the domain.
[in]dom4The fourth sort of the domain.
[in]codomainThe codomain of the sort.
Postcondition
*this represents dom1 # dom2 # dom3 # dom4 -> codomain

Definition at line 149 of file function_sort.h.

◆ make_function_sort_constraint()

constraint_ptr mcrl2::data::make_function_sort_constraint ( const function_sort f1,
const sort_expression s2 
)
inline

Definition at line 265 of file type_check_tree.h.

◆ make_function_symbol()

template<class... ARGUMENTS>
void mcrl2::data::make_function_symbol ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_function_symbol constructs a new term into a given address. \

Parameters
tThe reference into which the new function_symbol is constructed.

Definition at line 82 of file function_symbol.h.

◆ make_function_update()

void mcrl2::data::make_function_update ( data_expression result,
const sort_expression s,
const sort_expression t,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @func_update.

Parameters
resultThe data expression where the @func_update expression is put.
sA sort expression.
tA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 113 of file function_update.h.

◆ make_function_update_stable()

void mcrl2::data::make_function_update_stable ( data_expression result,
const sort_expression s,
const sort_expression t,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @func_update_stable.

Parameters
resultThe data expression where the @func_update_stable expression is put.
sA sort expression.
tA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 182 of file function_update.h.

◆ make_if_always_else()

void mcrl2::data::make_if_always_else ( data_expression result,
const sort_expression s,
const sort_expression t,
const data_expression arg0,
const data_expression arg1,
const data_expression arg2 
)
inline

Make an application of function symbol @if_always_else.

Parameters
resultThe data expression where the @if_always_else expression is put.
sA sort expression.
tA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.

Definition at line 335 of file function_update.h.

◆ make_is_element_of_constraint()

constraint_ptr mcrl2::data::make_is_element_of_constraint ( const sort_expression s,
const std::vector< sort_expression > &  sorts,
int  cost = 0 
)
inline

Definition at line 290 of file type_check_tree.h.

◆ make_is_equal_to_constraint()

constraint_ptr mcrl2::data::make_is_equal_to_constraint ( const sort_expression s1,
const sort_expression s2,
int  cost = 0 
)
inline

Definition at line 335 of file type_check_tree.h.

◆ make_is_not_a_function_update()

void mcrl2::data::make_is_not_a_function_update ( data_expression result,
const sort_expression s,
const sort_expression t,
const data_expression arg0 
)
inline

Make an application of function symbol @is_not_an_update.

Parameters
resultThe data expression where the @is_not_an_update expression is put.
sA sort expression.
tA sort expression.
arg0A data expression.

Definition at line 247 of file function_update.h.

◆ make_lambda()

template<class... ARGUMENTS>
void mcrl2::data::make_lambda ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 78 of file lambda.h.

◆ make_map_substitution()

template<typename AssociativeContainer >
map_substitution< AssociativeContainer > mcrl2::data::make_map_substitution ( const AssociativeContainer &  m)

Utility function for creating a map_substitution.

Definition at line 69 of file map_substitution.h.

◆ make_mutable_map_substitution() [1/2]

template<typename VariableContainer , typename ExpressionContainer , typename MapContainer >
mutable_map_substitution< MapContainer > mcrl2::data::make_mutable_map_substitution ( const VariableContainer &  vc,
const ExpressionContainer &  ec 
)

Utility function for creating a mutable_map_substitution.

Definition at line 186 of file mutable_map_substitution.h.

◆ make_mutable_map_substitution() [2/2]

template<typename VariableContainer , typename ExpressionContainer >
mutable_map_substitution< std::map< typename VariableContainer::value_type, typename ExpressionContainer::value_type > > mcrl2::data::make_mutable_map_substitution ( const VariableContainer &  vc,
const ExpressionContainer &  ec 
)

Definition at line 193 of file mutable_map_substitution.h.

◆ make_one_point_rule_substitution() [1/2]

data::mutable_map_substitution mcrl2::data::make_one_point_rule_substitution ( const std::map< data::variable, std::set< data::data_expression > > &  equalities,
bool  find_all_assignments = true 
)
inline

creates a substitution from a set of (in-)equalities

Parameters
find_all_assignmentsTrue to find all assignments, false to find only constant assignments
Returns
the substitution

Definition at line 203 of file equality_one_point_substitution.h.

◆ make_one_point_rule_substitution() [2/2]

std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > mcrl2::data::make_one_point_rule_substitution ( const std::map< data::variable, std::set< data::data_expression > > &  equalities,
const data::variable_list quantifier_variables,
bool  find_all_assignments = true 
)
inline

creates a substitution from a set of (in-)equalities for a given list of quantifier variables

Parameters
quantifier_variablesConsider only these variables
find_all_assignmentsTrue to find all assignments, false to find only constant assignments
Returns
the substitution, and the subset of quantifier variables that are not used in the substitution

Definition at line 190 of file equality_one_point_substitution.h.

◆ make_or_constraint()

constraint_ptr mcrl2::data::make_or_constraint ( const std::vector< constraint_ptr > &  alternatives)
inline

Definition at line 506 of file type_check_tree.h.

◆ make_sequence_sequence_substitution()

template<typename VariableContainer , typename ExpressionContainer >
sequence_sequence_substitution< VariableContainer, ExpressionContainer > mcrl2::data::make_sequence_sequence_substitution ( const VariableContainer &  vc,
const ExpressionContainer &  ec 
)

Utility function for creating a sequence_sequence_substitution.

Definition at line 79 of file sequence_sequence_substitution.h.

◆ make_set_comprehension()

template<class... ARGUMENTS>
void mcrl2::data::make_set_comprehension ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 62 of file set_comprehension.h.

◆ make_structured_sort()

template<class... ARGUMENTS>
void mcrl2::data::make_structured_sort ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_structured_sort constructs a new term into a given address. \

Parameters
tThe reference into which the new structured_sort is constructed.

Definition at line 439 of file structured_sort.h.

◆ make_structured_sort_constructor()

template<class... ARGUMENTS>
void mcrl2::data::make_structured_sort_constructor ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_structured_sort_constructor constructs a new term into a given address. \

Parameters
tThe reference into which the new structured_sort_constructor is constructed.

Definition at line 193 of file structured_sort_constructor.h.

◆ make_structured_sort_constructor_argument()

template<class... ARGUMENTS>
void mcrl2::data::make_structured_sort_constructor_argument ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_structured_sort_constructor_argument constructs a new term into a given address. \

Parameters
tThe reference into which the new structured_sort_constructor_argument is constructed.

Definition at line 87 of file structured_sort_constructor_argument.h.

◆ make_subsort_constraint()

constraint_ptr mcrl2::data::make_subsort_constraint ( const sort_expression s1,
const sort_expression s2,
int  cost = 0 
)
inline

Definition at line 375 of file type_check_tree.h.

◆ make_true_constraint()

constraint_ptr mcrl2::data::make_true_constraint ( int  cost = 0)
inline

Definition at line 239 of file type_check_tree.h.

◆ make_untyped_data_parameter()

template<class... ARGUMENTS>
void mcrl2::data::make_untyped_data_parameter ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_untyped_data_parameter constructs a new term into a given address. \

Parameters
tThe reference into which the new untyped_data_parameter is constructed.

Definition at line 69 of file untyped_data_parameter.h.

◆ make_untyped_identifier()

template<class... ARGUMENTS>
void mcrl2::data::make_untyped_identifier ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_untyped_identifier constructs a new term into a given address. \

Parameters
tThe reference into which the new untyped_identifier is constructed.

Definition at line 64 of file untyped_identifier.h.

◆ make_untyped_identifier_assignment()

template<class... ARGUMENTS>
void mcrl2::data::make_untyped_identifier_assignment ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_untyped_identifier_assignment constructs a new term into a given address. \

Parameters
tThe reference into which the new untyped_identifier_assignment is constructed.

Definition at line 236 of file assignment.h.

◆ make_untyped_possible_sorts()

template<class... ARGUMENTS>
void mcrl2::data::make_untyped_possible_sorts ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_untyped_possible_sorts constructs a new term into a given address. \

Parameters
tThe reference into which the new untyped_possible_sorts is constructed.

Definition at line 65 of file untyped_possible_sorts.h.

◆ make_untyped_set_or_bag_comprehension()

template<class... ARGUMENTS>
void mcrl2::data::make_untyped_set_or_bag_comprehension ( atermpp::aterm result,
ARGUMENTS...  arguments 
)

Definition at line 62 of file untyped_set_or_bag_comprehension.h.

◆ make_untyped_sort_variable() [1/2]

template<class... ARGUMENTS>
void mcrl2::data::make_untyped_sort_variable ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_untyped_sort_variable constructs a new term into a given address. \

Parameters
tThe reference into which the new untyped_sort_variable is constructed.

Definition at line 65 of file untyped_sort_variable.h.

◆ make_untyped_sort_variable() [2/2]

const untyped_sort_variable & mcrl2::data::make_untyped_sort_variable ( const sort_expression x)
inline

Definition at line 39 of file type_check_tree.h.

◆ make_variable()

template<class... ARGUMENTS>
void mcrl2::data::make_variable ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_variable constructs a new term into a given address. \

Parameters
tThe reference into which the new variable is constructed.

Definition at line 80 of file variable.h.

◆ make_where_clause()

template<class... ARGUMENTS>
void mcrl2::data::make_where_clause ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

\brief Make_where_clause constructs a new term into a given address. \

Parameters
tThe reference into which the new where_clause is constructed.

Definition at line 78 of file where_clause.h.

◆ max()

data_expression mcrl2::data::max ( const data_expression e1,
const data_expression e2,
const rewriter r 
)
inline

Definition at line 966 of file linear_inequalities.h.

◆ merge_data_specifications()

data_specification mcrl2::data::merge_data_specifications ( const data_specification dataspec1,
const data_specification dataspec2 
)
inline

Merges two data specifications. Throws an exception if conflicts are detected.

If the data specifications have equal aliases, types, constructors or functions these are merged.

Parameters
[in]dataspec1The first data specification to be merged.
[out]dataspec2The second data specification to be merged.
Returns
The merged data specification.

Definition at line 27 of file merge_data_specifications.h.

◆ min()

data_expression mcrl2::data::min ( const data_expression e1,
const data_expression e2,
const rewriter r 
)
inline

Definition at line 953 of file linear_inequalities.h.

◆ normalize_sorts() [1/8]

data::data_equation mcrl2::data::normalize_sorts ( const data::data_equation x,
const data::sort_specification sortspec 
)

Definition at line 82 of file data.cpp.

◆ normalize_sorts() [2/8]

data::data_equation_list mcrl2::data::normalize_sorts ( const data_equation_list x,
const data::sort_specification sortspec 
)

Definition at line 83 of file data.cpp.

◆ normalize_sorts() [3/8]

data::data_expression mcrl2::data::normalize_sorts ( const data_expression x,
const data::sort_specification sortspec 
)

Definition at line 85 of file data.cpp.

◆ normalize_sorts() [4/8]

data::sort_expression mcrl2::data::normalize_sorts ( const sort_expression x,
const data::sort_specification sortspec 
)

Definition at line 86 of file data.cpp.

◆ normalize_sorts() [5/8]

template<typename T >
T mcrl2::data::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 
)

Definition at line 123 of file normalize_sorts.h.

◆ normalize_sorts() [6/8]

variable_list mcrl2::data::normalize_sorts ( const variable_list x,
const data::sort_specification sortspec 
)

Definition at line 87 of file data.cpp.

◆ normalize_sorts() [7/8]

void mcrl2::data::normalize_sorts ( data::data_equation_vector x,
const data::sort_specification sortspec 
)

Definition at line 84 of file data.cpp.

◆ normalize_sorts() [8/8]

template<typename T >
void mcrl2::data::normalize_sorts ( T &  x,
const data::sort_specification sort_spec,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 113 of file normalize_sorts.h.

◆ not_()

data_expression mcrl2::data::not_ ( const data_expression x)
inline
Returns
The negation of x

Definition at line 106 of file consistency.h.

◆ not_equal_to() [1/2]

application mcrl2::data::not_equal_to ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol !=.

Parameters
[in]arg0A data expression
[in]arg1A data expression
Returns
Application of != to a number of arguments

Definition at line 181 of file standard.h.

◆ not_equal_to() [2/2]

function_symbol mcrl2::data::not_equal_to ( const sort_expression s)
inline

Constructor for function symbol !=.

Parameters
[in]sA sort expression
Returns
function symbol not_equal_to

Definition at line 163 of file standard.h.

◆ number()

data_expression mcrl2::data::number ( const sort_expression s,
const std::string &  n 
)
inline

Construct numeric expression from a string representing a number in decimal notation.

Parameters
sA sort expression
nA string
Precondition
n is of the form [1]?[0...9]+

Definition at line 493 of file standard_numbers_utility.h.

◆ on_delete_function_symbol()

void mcrl2::data::on_delete_function_symbol ( const atermpp::aterm t)
inline

Definition at line 22 of file index_traits.h.

◆ one_point_rule_rewrite() [1/2]

template<typename T >
T mcrl2::data::one_point_rule_rewrite ( const T &  x,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 126 of file one_point_rule_rewriter.h.

◆ one_point_rule_rewrite() [2/2]

template<typename T >
void mcrl2::data::one_point_rule_rewrite ( T &  x,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 120 of file one_point_rule_rewriter.h.

◆ operator+()

data_specification mcrl2::data::operator+ ( data_specification  spec1,
const data_specification spec2 
)
inline

Merges two data specifications into one.

It is assumed that the two specs can be merged. I.e. that the second is a safe extension of the first.

Parameters
[in]spec1One of the input specifications.
[in]spec2The second input specification.
Returns
A specification that is merged.

Definition at line 719 of file data_specification.h.

◆ operator<<() [1/52]

atermpp::aterm_ostream & mcrl2::data::operator<< ( atermpp::aterm_ostream stream,
const data_specification spec 
)

Writes the data specification to a stream.

Definition at line 89 of file data_io.cpp.

◆ operator<<() [2/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  os,
const rewrite_strategy  s 
)
inline

standard conversion from rewrite strategy to stream

Definition at line 80 of file rewrite_strategy.h.

◆ operator<<() [3/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const abstraction x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 94 of file abstraction.h.

◆ operator<<() [4/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const alias x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 94 of file alias.h.

◆ operator<<() [5/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const application x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 720 of file application.h.

◆ operator<<() [6/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const assignment x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 168 of file assignment.h.

◆ operator<<() [7/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const assignment_expression x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 77 of file assignment.h.

◆ operator<<() [8/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const bag_comprehension x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 77 of file bag_comprehension.h.

◆ operator<<() [9/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const bag_comprehension_binder x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 222 of file binder_type.h.

◆ operator<<() [10/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const bag_container x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 222 of file container_type.h.

◆ operator<<() [11/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const basic_sort x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 79 of file basic_sort.h.

◆ operator<<() [12/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const binder_type x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 63 of file binder_type.h.

◆ operator<<() [13/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const container_sort x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 80 of file container_sort.h.

◆ operator<<() [14/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const container_type x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 63 of file container_type.h.

◆ operator<<() [15/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const data_equation x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 135 of file data_equation.h.

◆ operator<<() [16/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const data_expression x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 194 of file data_expression.h.

◆ operator<<() [17/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const data_specification x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 707 of file data_specification.h.

◆ operator<<() [18/52]

template<typename Expression >
std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const enumerator_list_element< Expression > &  p 
)

Definition at line 467 of file enumerator.h.

◆ operator<<() [19/52]

template<typename Expression >
std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const enumerator_list_element_with_substitution< Expression > &  p 
)

Definition at line 483 of file enumerator.h.

◆ operator<<() [20/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const enumerator_substitution sigma 
)
inline

Definition at line 157 of file enumerator_substitution.h.

◆ operator<<() [21/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const exists x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 79 of file exists.h.

◆ operator<<() [22/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const exists_binder x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 328 of file binder_type.h.

◆ operator<<() [23/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const fbag_container x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 328 of file container_type.h.

◆ operator<<() [24/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const forall x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 78 of file forall.h.

◆ operator<<() [25/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const forall_binder x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 275 of file binder_type.h.

◆ operator<<() [26/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const fset_container x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 275 of file container_type.h.

◆ operator<<() [27/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const function_sort x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 85 of file function_sort.h.

◆ operator<<() [28/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const function_symbol x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 101 of file function_symbol.h.

◆ operator<<() [29/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const lambda x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 93 of file lambda.h.

◆ operator<<() [30/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const lambda_binder x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 381 of file binder_type.h.

◆ operator<<() [31/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const list_container x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 116 of file container_type.h.

◆ operator<<() [32/52]

template<typename VariableType , typename ExpressionType >
std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const mutable_indexed_substitution< VariableType, ExpressionType > &  sigma 
)

Definition at line 303 of file mutable_indexed_substitution.h.

◆ operator<<() [33/52]

template<typename AssociativeContainer >
std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const mutable_map_substitution< AssociativeContainer > &  sigma 
)

Definition at line 199 of file mutable_map_substitution.h.

◆ operator<<() [34/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const no_substitution  
)
inline

Definition at line 28 of file no_substitution.h.

◆ operator<<() [35/52]

template<typename VariableContainer , typename ExpressionContainer >
std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const sequence_sequence_substitution< VariableContainer, ExpressionContainer > &  sigma 
)

Definition at line 85 of file sequence_sequence_substitution.h.

◆ operator<<() [36/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const set_comprehension x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 77 of file set_comprehension.h.

◆ operator<<() [37/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const set_comprehension_binder x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 169 of file binder_type.h.

◆ operator<<() [38/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const set_container x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 169 of file container_type.h.

◆ operator<<() [39/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const sort_expression x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 115 of file sort_expression.h.

◆ operator<<() [40/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const structured_sort x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 458 of file structured_sort.h.

◆ operator<<() [41/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const structured_sort_constructor x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 221 of file structured_sort_constructor.h.

◆ operator<<() [42/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const structured_sort_constructor_argument x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 115 of file structured_sort_constructor_argument.h.

◆ operator<<() [43/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const untyped_data_parameter x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 97 of file untyped_data_parameter.h.

◆ operator<<() [44/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const untyped_identifier x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 77 of file untyped_identifier.h.

◆ operator<<() [45/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out,
const untyped_identifier_assignment x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 264 of file assignment.h.

◆ operator<<() [46/52]

std::ostream & mcrl2::data::operator<< (