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< alias >	alias_list
	\brief list of aliass
typedef std::vector< alias >	alias_vector
	\brief vector of aliass
typedef atermpp::term_list< assignment_expression >	assignment_expression_list
	\brief list of assignment_expressions
typedef std::vector< assignment_expression >	assignment_expression_vector
	\brief vector of assignment_expressions
typedef atermpp::term_list< assignment >	assignment_list
	\brief list of assignments
typedef std::vector< assignment >	assignment_vector
	\brief vector of assignments
typedef atermpp::term_list< untyped_identifier_assignment >	untyped_identifier_assignment_list
	\brief list of untyped_identifier_assignments
typedef std::vector< untyped_identifier_assignment >	untyped_identifier_assignment_vector
	\brief vector of untyped_identifier_assignments
typedef atermpp::term_list< basic_sort >	basic_sort_list
	list of basic sorts
typedef std::vector< basic_sort >	basic_sort_vector
	vector of basic sorts
typedef atermpp::term_list< binder_type >	binder_type_list
	\brief list of binder_types
typedef std::vector< binder_type >	binder_type_vector
	\brief vector of binder_types
typedef atermpp::term_list< container_sort >	container_sort_list
	list of function sorts
typedef std::vector< container_sort >	container_sort_vector
	list of function sorts
typedef atermpp::term_list< container_type >	container_type_list
	\brief list of container_types
typedef std::vector< container_type >	container_type_vector
	\brief vector of container_types
typedef atermpp::term_list< data_equation >	data_equation_list
	\brief list of data_equations
typedef std::vector< data_equation >	data_equation_vector
	\brief vector of data_equations
typedef atermpp::term_list< data_expression >	data_expression_list
	\brief list of data_expressions
typedef std::vector< data_expression >	data_expression_vector
	\brief vector of data_expressions
typedef atermpp::term_list< variable >	variable_list
	\brief list of variables
typedef std::map< untyped_sort_variable, sort_expression >	sort_substitution
typedef std::pair< sort_substitution, int >	solution
typedef std::shared_ptr< type_check_node >	type_check_node_ptr
typedef std::shared_ptr< type_check_constraint >	constraint_ptr
typedef atermpp::term_list< function_sort >	function_sort_list
	list of function sorts
typedef std::vector< function_sort >	function_sort_vector
	vector of function sorts
typedef std::pair< core::identifier_string, sort_expression >	function_symbol_key_type
typedef atermpp::term_list< function_symbol >	function_symbol_list
	\brief list of function_symbols
typedef std::vector< function_symbol >	function_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_expression >	sort_expression_list
	\brief list of sort_expressions
typedef std::vector< sort_expression >	sort_expression_vector
	\brief vector of sort_expressions
typedef atermpp::term_list< structured_sort >	structured_sort_list
	\brief list of structured_sorts
typedef std::vector< structured_sort >	structured_sort_vector
	\brief vector of structured_sorts
typedef atermpp::term_list< structured_sort_constructor >	structured_sort_constructor_list
	\brief list of structured_sort_constructors
typedef std::vector< structured_sort_constructor >	structured_sort_constructor_vector
	\brief vector of structured_sort_constructors
typedef atermpp::term_list< structured_sort_constructor_argument >	structured_sort_constructor_argument_list
	\brief list of structured_sort_constructor_arguments
typedef std::vector< structured_sort_constructor_argument >	structured_sort_constructor_argument_vector
	\brief vector of structured_sort_constructor_arguments
typedef atermpp::term_list< sort_expression_list >	sorts_list
typedef atermpp::term_list< untyped_data_parameter >	untyped_data_parameter_list
	\brief list of untyped_data_parameters
typedef std::vector< untyped_data_parameter >	untyped_data_parameter_vector
	\brief vector of untyped_data_parameters
typedef std::vector< variable >	variable_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_expression &	unary_operand (const application &x)
const data_expression &	binary_left (const application &x)
const data_expression &	binary_right (const application &x)
const data_expression &	unary_operand1 (const data_expression &x)
const data_expression &	binary_left1 (const data_expression &x)
const data_expression &	binary_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_expression &	true_ ()
const data_expression &	false_ ()
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_expression >	find_sort_expressions (const data::data_equation &x)
std::set< data::function_symbol >	find_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_expression >	find_sort_expressions (const data::data_expression &x)
std::set< data::variable >	find_all_variables (const data::data_expression &x)
std::set< data::variable >	find_all_variables (const data::data_expression_list &x)
std::set< data::variable >	find_free_variables (const data::data_expression &x)
std::set< data::variable >	find_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_list &	variable_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_istream &	operator>> (atermpp::aterm_istream &stream, data_specification &spec)
	Reads a data specification from a stream.
atermpp::aterm_ostream &	operator<< (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_string >	function_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 >
T	replace_untyped_sort (const T &x, const sort_expression &replacement)
const untyped_sort_variable &	make_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_ptr >	join_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::variable >	find_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::variable >	find_free_variables (const T &x)
template<typename T , typename VariableContainer >
std::set< data::variable >	find_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_string >	find_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_expression >	find_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_symbol >	find_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_expression >	find_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::variable >	find_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_string &	function_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_string &	function_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_string &	is_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_string &	if_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_expression &	arg1 (const data_expression &e)
	Function for projecting out argument. arg1 from an application.
const data_expression &	arg2 (const data_expression &e)
	Function for projecting out argument. arg2 from an application.
const data_expression &	arg3 (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_expression >	split_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_expression >	split_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_expression &	real_zero ()
data_expression &	real_one ()
data_expression &	real_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< variable >	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.
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 >
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_vector >	parse_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::variable >	substitution_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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
T	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 >
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 >
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 >
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 >
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_expression >	find_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_expression >	split_disjunction (const data_expression &condition)
	Split a disjunctive expression into a set of clauses.
std::list< data_expression >	split_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::variable >	substitution_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< variable >	substitution_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::variable >	substitution_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::variable >	substitution_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 >
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::variable &	undefined_variable ()
	Returns a data variable that corresponds to 'undefined'.
const data::variable &	undefined_real_variable ()
	Returns a data variable that corresponds to 'undefined'.
const data::sort_expression &	undefined_sort_expression ()
	Returns a sort expression that corresponds to 'undefined'.
const data::data_expression &	undefined_data_expression ()
	Returns a data expression that corresponds to 'undefined'.
const data::data_expression &	undefined_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::variable >	find_all_variables (const data::variable &x)
std::set< data::variable >	find_all_variables (const data::variable_list &x)
std::set< core::identifier_string >	find_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

typedef atermpp::term_list<alias> mcrl2::data::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

typedef atermpp::term_list<assignment_expression> mcrl2::data::assignment_expression_list

\brief list of assignment_expressions

Definition at line 50 of file assignment.h.

assignment_expression_vector

typedef std::vector<assignment_expression> mcrl2::data::assignment_expression_vector

\brief vector of assignment_expressions

Definition at line 53 of file assignment.h.

assignment_list

typedef atermpp::term_list<assignment> mcrl2::data::assignment_list

\brief list of assignments

Definition at line 146 of file assignment.h.

assignment_vector

typedef std::vector<assignment> mcrl2::data::assignment_vector

\brief vector of assignments

Definition at line 149 of file assignment.h.

basic_sort_list

typedef atermpp::term_list<basic_sort> mcrl2::data::basic_sort_list

list of basic sorts

Definition at line 92 of file basic_sort.h.

basic_sort_vector

typedef std::vector<basic_sort> mcrl2::data::basic_sort_vector

vector of basic sorts

Definition at line 94 of file basic_sort.h.

binder_type_list

typedef atermpp::term_list<binder_type> mcrl2::data::binder_type_list

\brief list of binder_types

Definition at line 50 of file binder_type.h.

binder_type_vector

typedef std::vector<binder_type> mcrl2::data::binder_type_vector

\brief vector of binder_types

Definition at line 53 of file binder_type.h.

constraint_ptr

typedef std::shared_ptr<type_check_constraint> mcrl2::data::constraint_ptr

Definition at line 188 of file type_check_tree.h.

container_sort_list

typedef atermpp::term_list<container_sort> mcrl2::data::container_sort_list

list of function sorts

Definition at line 94 of file container_sort.h.

container_sort_vector

typedef std::vector<container_sort> mcrl2::data::container_sort_vector

list of function sorts

Definition at line 98 of file container_sort.h.

container_type_list

typedef atermpp::term_list<container_type> mcrl2::data::container_type_list

\brief list of container_types

Definition at line 50 of file container_type.h.

container_type_vector

typedef std::vector<container_type> mcrl2::data::container_type_vector

\brief vector of container_types

Definition at line 53 of file container_type.h.

data_equation_list

typedef atermpp::term_list<data_equation> mcrl2::data::data_equation_list

\brief list of data_equations

Definition at line 122 of file data_equation.h.

data_equation_vector

typedef std::vector<data_equation> mcrl2::data::data_equation_vector

\brief vector of data_equations

Definition at line 125 of file data_equation.h.

data_expression_list

typedef atermpp::term_list<data_expression> mcrl2::data::data_expression_list

\brief list of data_expressions

Definition at line 181 of file data_expression.h.

data_expression_vector

typedef std::vector<data_expression> mcrl2::data::data_expression_vector

\brief vector of data_expressions

Definition at line 184 of file data_expression.h.

function_sort_list

typedef atermpp::term_list<function_sort> mcrl2::data::function_sort_list

list of function sorts

Definition at line 98 of file function_sort.h.

function_sort_vector

typedef std::vector<function_sort> mcrl2::data::function_sort_vector

vector of function sorts

Definition at line 100 of file function_sort.h.

function_symbol_key_type

typedef std::pair<core::identifier_string, sort_expression> mcrl2::data::function_symbol_key_type

Definition at line 23 of file function_symbol.h.

function_symbol_list

typedef atermpp::term_list<function_symbol> mcrl2::data::function_symbol_list

\brief list of function_symbols

Definition at line 88 of file function_symbol.h.

function_symbol_vector

typedef std::vector<function_symbol> mcrl2::data::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

typedef atermpp::term_list<sort_expression> mcrl2::data::sort_expression_list

\brief list of sort_expressions

Definition at line 102 of file sort_expression.h.

sort_expression_vector

typedef std::vector<sort_expression> mcrl2::data::sort_expression_vector

\brief vector of sort_expressions

Definition at line 105 of file sort_expression.h.

sort_substitution

typedef std::map<untyped_sort_variable, sort_expression> mcrl2::data::sort_substitution

Definition at line 23 of file type_check_tree.h.

sorts_list

typedef atermpp::term_list<sort_expression_list> mcrl2::data::sorts_list

Definition at line 368 of file typecheck.h.

structured_sort_constructor_argument_list

typedef atermpp::term_list<structured_sort_constructor_argument> mcrl2::data::structured_sort_constructor_argument_list

\brief list of structured_sort_constructor_arguments

Definition at line 93 of file structured_sort_constructor_argument.h.

structured_sort_constructor_argument_vector

typedef std::vector<structured_sort_constructor_argument> mcrl2::data::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

typedef atermpp::term_list<structured_sort_constructor> mcrl2::data::structured_sort_constructor_list

\brief list of structured_sort_constructors

Definition at line 199 of file structured_sort_constructor.h.

structured_sort_constructor_vector

typedef std::vector<structured_sort_constructor> mcrl2::data::structured_sort_constructor_vector

\brief vector of structured_sort_constructors

Definition at line 202 of file structured_sort_constructor.h.

structured_sort_list

typedef atermpp::term_list<structured_sort> mcrl2::data::structured_sort_list

\brief list of structured_sorts

Definition at line 445 of file structured_sort.h.

structured_sort_vector

typedef std::vector<structured_sort> mcrl2::data::structured_sort_vector

\brief vector of structured_sorts

Definition at line 448 of file structured_sort.h.

type_check_node_ptr

typedef std::shared_ptr<type_check_node> mcrl2::data::type_check_node_ptr

Definition at line 92 of file type_check_tree.h.

untyped_data_parameter_list

typedef atermpp::term_list<untyped_data_parameter> mcrl2::data::untyped_data_parameter_list

\brief list of untyped_data_parameters

Definition at line 75 of file untyped_data_parameter.h.

untyped_data_parameter_vector

typedef std::vector<untyped_data_parameter> mcrl2::data::untyped_data_parameter_vector

\brief vector of untyped_data_parameters

Definition at line 78 of file untyped_data_parameter.h.

untyped_identifier_assignment_list

typedef atermpp::term_list<untyped_identifier_assignment> mcrl2::data::untyped_identifier_assignment_list

\brief list of untyped_identifier_assignments

Definition at line 242 of file assignment.h.

untyped_identifier_assignment_vector

typedef std::vector<untyped_identifier_assignment> mcrl2::data::untyped_identifier_assignment_vector

\brief vector of untyped_identifier_assignments

Definition at line 245 of file assignment.h.

variable_list

typedef atermpp::term_list< variable > mcrl2::data::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

enum mcrl2::data::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

e	A 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

e	A 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

e	A 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

s	A sort expression.
dataspec	The data specification defining the terms of sort s.
rewr	A 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 1068 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

s	A sort expression.
dataspec	The data specification defining the terms of sort s.
rewr	A rewriter to be used to simplify terms and conditions.
id_generator	An 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 1033 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]	arg0	A data expression
[in]	arg1	A 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]

s

A 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

data	A data specification
s	A 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]

x

an 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]	x	an object containing data expressions
[in,out]	o	an 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]	specification	A data specification.
[in]	d	A 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

data	A data specification
s	A 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

data	A data specification
s	A 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_in	An input data_expression of sort Bool.
vars_in	A container with variables. Supports iterating over these variables.
e_out	The output data expression of sort Bool.
vars_out	A list of variables to store resulting variables. Initially empty.
r	A 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]

dataspec

A 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

s	A sort expression.
t	A 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

s	A sort expression.
t	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A 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

s	A sort expression
t	A 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

s	A sort expression
t	A 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

s	A sort expression
t	A 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

s	A sort expression
t	A 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

s	A sort expression
t	A 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

s	A sort expression.
t	A 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

s	A sort expression.
t	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A 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

inequalities	A list of inequalities over real numbers
resulting_equalities	A list with the resulting equalities.
resulting_inequalities	A list of the resulting inequalities
variables_begin	An iterator indicating the beginning of the eliminatable variables.
variables_end	An iterator indicating the end of the eliminatable variables.
r	A 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]	arg0	A data expression
[in]	arg1	A 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]

s

A 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]	arg0	A data expression
[in]	arg1	A 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]

s

A 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]	arg0	A data expression
[in]	arg1	A data expression
[in]	arg2	A 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]

s

A 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

s	A sort expression.
t	A 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

s	A sort expression.
t	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A 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

arg0	A data expression.
arg1	A data expression.
arg2	A 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

inequalities	A list of inequalities
i	An iterator pointing into inequalities.
r	A 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

x	a 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

t	The 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]	s1	a sort expression
[in]	s2	a 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]

t

A 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

x

A 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

x

A 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 223 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

x	a 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]

e

A 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]

e

A 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

x	a 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

e	A 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

e	A 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

e	A 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

e	A 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]

e

A 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]

e

A 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]

e

A 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]

e

A 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

e	A 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

e	A 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]

e

A 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]

e

A 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

x	a 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_in	A list of inequalities.
r	A rewriter.
use_cache	A 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

e	A 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

e	A 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]

e

A 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]

e

A 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]

e

A 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]

e

A 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

x	a 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

s	A sort expression.
t	A 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

s	A sort expression.
t	A sort expression.
arg0	A 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

arg0	A 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

x	a 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]

e

A 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]

e

A 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

x	a 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

x

A 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]

s

a 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

x	a 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

first	Start of a sequence of data expressions
last	End 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

first	Start of a sequence of data expressions
last	End 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

x	An 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]	arg0	A data expression
[in]	arg1	A 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]

s

A 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]	arg0	A data expression
[in]	arg1	A 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]

s

A 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

t	The 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

result

variable 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

result

variable 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

result

variable 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

result

variable 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

result

variable 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

result

variable 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

result

variable 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

t	The 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

variables	A sequence of variables.
expressions	A 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

variables	A sequence of data variables
expressions	A 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

t	The 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

t	The 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

t	The 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

r	A 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

v	A sequence of data variables
x	A 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

v	A sequence of data variables
x	A 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

t	The 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]	dom1	The first sort of the domain.
[in]	codomain	The 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]	dom1	The first sort of the domain.
[in]	dom2	The second sort of the domain.
[in]	codomain	The 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]	dom1	The first sort of the domain.
[in]	dom2	The second sort of the domain.
[in]	dom3	The third sort of the domain.
[in]	codomain	The 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]	dom1	The first sort of the domain.
[in]	dom2	The second sort of the domain.
[in]	dom3	The third sort of the domain.
[in]	dom4	The fourth sort of the domain.
[in]	codomain	The 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

t	The 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

result	The data expression where the @func_update expression is put.
s	A sort expression.
t	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A 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

result	The data expression where the @func_update_stable expression is put.
s	A sort expression.
t	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A 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

result	The data expression where the @if_always_else expression is put.
s	A sort expression.
t	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A 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

result	The data expression where the @is_not_an_update expression is put.
s	A sort expression.
t	A sort expression.
arg0	A 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_assignments

True 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_variables	Consider only these variables
find_all_assignments	True 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

t	The 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

t	The 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

t	The 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

t	The 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

t	The 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

t	The 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

t	The 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

t	The 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

t	The 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

t	The 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]	dataspec1	The first data specification to be merged.
[out]	dataspec2	The 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]	arg0	A data expression
[in]	arg1	A 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]

s

A 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

s	A sort expression
n	A 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]	spec1	One of the input specifications.
[in]	spec2	The 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 468 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 484 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<< ( std::ostream &  out, const untyped_possible_sorts &  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 untyped_possible_sorts.h.

operator<<() [47/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out, const untyped_set_or_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 untyped_set_or_bag_comprehension.h.

operator<<() [48/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out, const untyped_set_or_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 116 of file binder_type.h.

operator<<() [49/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out, const untyped_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 54 of file untyped_sort.h.

operator<<() [50/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out, const untyped_sort_variable &  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 87 of file untyped_sort_variable.h.

operator<<() [51/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out, const variable &  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 99 of file variable.h.

operator<<() [52/52]

std::ostream & mcrl2::data::operator<< ( std::ostream &  out, const where_clause &  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 91 of file where_clause.h.

operator>>() [1/2]

atermpp::aterm_istream & mcrl2::data::operator>>	(	atermpp::aterm_istream &	stream,
		data_specification &	spec
	)

Reads a data specification from a stream.

Definition at line 66 of file data_io.cpp.

operator>>() [2/2]

std::istream & mcrl2::data::operator>> ( std::istream &  is, rewrite_strategy &  s  )

inline

standard conversion from stream to rewrite strategy

Definition at line 45 of file rewrite_strategy.h.

optimized_and()

template<typename Term >

void mcrl2::data::optimized_and ( Term &  result, const Term &  p, const Term &  q  )

inline

Make a conjunction, and optimize if possible.

Parameters

result	Contains the optimized and.
p	A term
q	A term

Definition at line 538 of file optimized_boolean_operators.h.

optimized_exists()

template<typename Term , typename VariableSequence >

void mcrl2::data::optimized_exists ( Term &  result, const VariableSequence &  l, const Term &  p, bool  remove_variables = false  )

inline

Make an existential quantification.

Parameters

l	A sequence of variables
p	A term
remove_variables	If true, unused quantifier variables are removed

Returns

The application of existential quantification to the arguments.

Definition at line 610 of file optimized_boolean_operators.h.

optimized_exists_no_empty_domain()

template<typename Term , typename VariableSequence >

void mcrl2::data::optimized_exists_no_empty_domain ( Term &  result, const VariableSequence &  l, const Term &  p, bool  remove_variables = false  )

inline

Make an existential quantification.

Parameters

l	A sequence of variables
p	A term
remove_variables	If true, unused quantifier variables are removed

Returns

The application of existential quantification to the arguments. The optimization exists x:empty_set. phi = false is not applied.

Definition at line 624 of file optimized_boolean_operators.h.

optimized_forall()

template<typename Term , typename VariableSequence >

void mcrl2::data::optimized_forall ( Term &  result, const VariableSequence &  l, const Term &  p, bool  remove_variables = false  )

inline

Make a universal quantification.

Parameters

l	A sequence of variables
p	A term
remove_variables	If true, unused quantifier variables are removed

Returns

The application of universal quantification to the arguments.

Definition at line 583 of file optimized_boolean_operators.h.

optimized_forall_no_empty_domain()

template<typename Term , typename VariableSequence >

void mcrl2::data::optimized_forall_no_empty_domain ( Term &  result, const VariableSequence &  l, const Term &  p, bool  remove_variables = false  )

inline

Make a universal quantification.

Parameters

l	A sequence of variables
p	A term
remove_variables	If true, unused quantifier variables are removed

Returns

The application of universal quantification to the arguments. The optimization forall x:empty_set. phi = true is not applied.

Definition at line 597 of file optimized_boolean_operators.h.

optimized_imp()

template<typename Term >

void mcrl2::data::optimized_imp ( Term &  result, const Term &  p, const Term &  q  )

inline

Make an implication.

Parameters

p	A term
q	A term

Returns

The application of implication to the arguments.

Definition at line 571 of file optimized_boolean_operators.h.

optimized_not()

template<typename Term >

void mcrl2::data::optimized_not ( Term &  result, const Term &  arg  )

inline

Make a negation.

Parameters

arg

A term

Returns

The application of not to the argument.

Definition at line 527 of file optimized_boolean_operators.h.

optimized_or()

template<typename Term >

void mcrl2::data::optimized_or ( Term &  result, const Term &  p, const Term &  q  )

inline

Make a conjunction, and optimize if possible.

Parameters

p	A term
q	A term

Returns

The application of and to the arguments.

Make a disjunction

Parameters

p	A term
q	A term

Returns

The application of or to the arguments.

Definition at line 560 of file optimized_boolean_operators.h.

or_()

data_expression mcrl2::data::or_ ( const data_expression &  x, const data_expression &  y  )

inline

Returns

The disjunction of x and y

Definition at line 113 of file consistency.h.

order_variables_to_optimise_enumeration()

variable_list mcrl2::data::order_variables_to_optimise_enumeration ( const variable_list &  l, const data_specification &  data_spec  )

inline

Order the variables in a variable list such that enumeration over these variables becomes more efficient.

Parameters

[in]	l	A list of variables that are to be sorted.
[in]	data_spec	A data specification containing the constructors that are used to determine efficiency.

Returns

The same list of variables but ordered in such a way that

Definition at line 842 of file data_specification.h.

parse_data_expression() [1/4]

data_expression mcrl2::data::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  )

inline

Parses and type checks a data expression.

See parsing a data expression from a string for details.

Parameters

[in]	text	The input text containing a data expression.
[in]	data_spec	The data specification that is used for type checking.
[in]	type_check	Indication whether the expression is expected to be type checked.
[in]	translate_user_notation	Indication whether user notation such a numbers must be translated to internal format.
[in]	normalize_sorts	Indication whether the sorts must be rewritten to normal form.

Definition at line 354 of file parse.h.

parse_data_expression() [2/4]

template<typename VariableContainer >

data_expression mcrl2::data::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.

See parsing a data expression from a string for details.

Parameters

[in]	text	The input text containing a data expression.
[in]	variables	A container with variables that can occur in the data expression.
[in]	data_spec	The data specification that is used for type checking.
[in]	type_check	Indication whether the expression is expected to be type checked.
[in]	translate_user_notation	Indication whether user notation such a numbers must be translated to internal format.
[in]	normalize_sorts	Indication whether the sorts must be rewritten to normal form.

Definition at line 312 of file parse.h.

parse_data_expression() [3/4]

template<typename VariableContainer >

data_expression mcrl2::data::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.

A data expression is read from the input where it is assumed that it can contain variables from the range from begin to end. The data expression is type checked using the given data specification data_spec. The default data specification contains all standard sorts and functions. If a parse or type check error occurs this is reported using a mcrl2::runtime_error exception. It is assumed that the input contains exactly one expression, and nothing else.

Parameters

[in]	in	The input stream containing a data expression.
[in]	variables	The variables that can occur in the data expression.
[in]	dataspec	The data specification that is used for type checking.
[in]	type_check	Indication whether the expression is expected to be type checked.
[in]	translate_user_notation	Indication whether user notation such a numbers must be translated to internal format.
[in]	normalize_sorts	Indication whether the sorts must be rewritten to normal form.

Returns

The parsed data expression.

Definition at line 276 of file parse.h.

parse_data_expression() [4/4]

data_expression mcrl2::data::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  )

inline

Parses and type checks a data expression.

See parsing a data expression from a string for details.

Parameters

[in]	text	The input text containing a data expression.
[in]	data_spec	The data specification that is used for type checking.
[in]	type_check	Indication whether the expression is expected to be type checked.
[in]	translate_user_notation	Indication whether user notation such a numbers must be translated to internal format.
[in]	normalize_sorts	Indication whether the sorts must be rewritten to normal form.

Definition at line 334 of file parse.h.

parse_data_specification() [1/2]

data_specification mcrl2::data::parse_data_specification ( const std::string &  text )

inline

Parses a and type checks a data specification.

This function reads a data specification in input string text. See for an example the function parse_data_expression on a string.

Parameters

[in]

text

A textual description of the data specification.

Returns

the data specification corresponding to the input istream.

Definition at line 79 of file parse.h.

parse_data_specification() [2/2]

data_specification mcrl2::data::parse_data_specification ( std::istream &  in )

inline

Parses a and type checks a data specification.

This function reads a data specification in input string text. It is assumed that the string contains a single data specification, and nothing else. If a parse or type check error is detected an mcrl2::runtime_error exception is raised with a string that indicates the problem. A typical example of a specification is:

sort D=struct d1 | d2;
     F=D->Set(D);
     Natural;
cons zero:Natural; plus:Natural->Natural;
map  plus:Natural#Natural->Natural;
var  x,y:Natural;
eqn  y==zero -> plus(x,y)=x;
     plus(x,succ(y))=succ(plus(x,y));

Parameters

[in]

in

A input stream containing the data specification.

Returns

the data specification corresponding to text.

Definition at line 62 of file parse.h.

parse_function_symbol()

data::function_symbol mcrl2::data::parse_function_symbol ( const std::string &  text, const std::string &  dataspec_text = ""  )

inline

Definition at line 410 of file parse.h.

parse_rewrite_strategy()

rewrite_strategy mcrl2::data::parse_rewrite_strategy ( const std::string &  s )

inline

standard conversion from string to rewrite strategy

Definition at line 27 of file rewrite_strategy.h.

parse_sort_expression() [1/2]

sort_expression mcrl2::data::parse_sort_expression ( const std::string &  text, const data_specification &  data_spec = detail::default_specification()  )

inline

Parses and type checks a sort expression.

Parses and type checks the sort expression. An error is signalled using the mcrl2::runtime_error exception. This routine expects exactly one sort expression on the input. The default data specification contains all standard sorts.

Parameters

[in]	text	The input text containing a sort expression.
[in]	data_spec	The data specification that is used for type checking.

Definition at line 399 of file parse.h.

parse_sort_expression() [2/2]

sort_expression mcrl2::data::parse_sort_expression ( std::istream &  in, const data_specification &  data_spec = detail::default_specification()  )

inline

Parses and type checks a sort expression.

See parsing a sort expression from a string for details.

Parameters

[in]	in	An input stream containing a sort expression.
[in]	data_spec	The data specification that is used for type checking.

Definition at line 380 of file parse.h.

parse_sort_specification()

std::pair< basic_sort_vector, alias_vector > mcrl2::data::parse_sort_specification

(

const std::string &

text

)

Definition at line 251 of file data.cpp.

parse_variable() [1/2]

variable mcrl2::data::parse_variable ( const std::string &  text, const data_specification &  data_spec = detail::default_specification()  )

inline

Parses and type checks a data variable declaration.

See the information for reading a variable declaration from a string.

Parameters

[in]	text	A textual description of the variable declaration.
[in]	data_spec	The data specification that is used for type checking.

Returns

the variable corresponding to the input istream.

Definition at line 218 of file parse.h.

parse_variable() [2/2]

variable mcrl2::data::parse_variable ( std::istream &  text, const data_specification &  data_spec = detail::default_specification()  )

inline

Parses and type checks a data variable declaration.

A variable declaration has the form x:S where x is a string and S is a sort expression. No trailing information after the declaration of the variable is allowed. The declaration is checked using the data specification that is provided. The default data specification contains all standard data types. If a parse or typecheck error occurs an mcrl2::runtime_error exception is raised.

Parameters

[in]	text	A textual description of the variable declaration.
[in]	data_spec	The data specification that is used for type checking.

Returns

the variable corresponding to the string text.

Definition at line 250 of file parse.h.

parse_variable_declaration_list()

variable_list mcrl2::data::parse_variable_declaration_list ( const std::string &  text, const data_specification &  dataspec = detail::default_specification()  )

inline

Parses a variable declaration list.

Parameters

[in]	text	The input text.
[in]	dataspec	The data specification used to type normalize the sorts of the variables.

Returns

The parsed variable declaration list.

Definition at line 429 of file parse.h.

parse_variables() [1/5]

variable_list mcrl2::data::parse_variables ( const std::string &  text )

inline

Definition at line 365 of file parse.h.

parse_variables() [2/5]

template<typename OutputIterator >

void mcrl2::data::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.

See parse_variables on a string for more explanation.

Parameters

[in]	text	A textual description of the variable declarations to be parsed.
[out]	i	An input interator indicating where the parsed variables must be inserted.
[in]	data_spec	The data specification that is used for type checking.

Definition at line 203 of file parse.h.

parse_variables() [3/5]

template<typename OutputIterator , typename VariableIterator >

void mcrl2::data::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.

See parse_variables on a string for more explanation.

Parameters

[in]	text	A textual description of the variable declarations to be parsed.
[out]	i	An input interator indicating where the parsed variables must be inserted.
[in]	begin	The start of a variable range against which the variables are checked for double occurrences.
[in]	end	The end of the variable range against which the parsed variables are checked.
[in]	data_spec	The data specification that is used for type checking.

Definition at line 171 of file parse.h.

parse_variables() [4/5]

template<typename OutputIterator , typename VariableIterator >

void mcrl2::data::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.

The shape of the variables are x_11,...,x_1n:S_1; ... x_m1,...,x_mk:S_m where x_ij are variable strings and S_i are sort expressions. It is checked that the sort expressions are properly typed regarding the data specification and that the variable names do not clash with the names of mappings and constructors. It is also not allowed to use a variable name twice. If an optional range of variables is given, then it is also checked that there are no conflicts with variable names in this range. An mcrl2::runtime_error exception is raised when an error occurs. In this case no names added using the input iterator. The default data specification contains all standard data types.
The output iterator can be used as follows, on standard variable lists.

variable_list l;
parse_variables("x:Nat; y:Pos", std::front_inserter(l));

Parameters

[in]	in	An input stream containing the variable declarations to be parsed.
[out]	o	An output interator indicating where the parsed variables must be inserted.
[in]	begin	The start of a variable range against which the variables are checked for double occurrences.
[in]	end	The end of the variable range against which the parsed variables are checked.
[in]	data_spec	The data specification that is used for type checking.

Definition at line 114 of file parse.h.

parse_variables() [5/5]

template<typename OutputIterator >

void mcrl2::data::parse_variables	(	std::istream &	text,
		OutputIterator	i,
		const data_specification &	data_spec = detail::default_specification()
	)

Parses and type checks a data variable declaration list.

See parse_variables on a string for more explanation.

Parameters

[in]	text	A textual description of the variable declarations to be parsed.
[out]	i	An input interator indicating where the parsed variables must be inserted.
[in]	data_spec	The data specification that is used for type checking.

Definition at line 188 of file parse.h.

pivot_and_update()

static void mcrl2::data::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  )

static

Definition at line 1213 of file linear_inequalities.h.

pp() [1/61]

std::string mcrl2::data::pp

(

const abstraction &

x

)

Definition at line 39 of file data.cpp.

pp() [2/61]

std::string mcrl2::data::pp

(

const alias &

x

)

Definition at line 40 of file data.cpp.

pp() [3/61]

std::string mcrl2::data::pp

(

const application &

x

)

Definition at line 41 of file data.cpp.

pp() [4/61]

std::string mcrl2::data::pp

(

const assignment &

x

)

Definition at line 42 of file data.cpp.

pp() [5/61]

std::string mcrl2::data::pp

(

const assignment_expression &

x

)

Definition at line 43 of file data.cpp.

pp() [6/61]

std::string mcrl2::data::pp

(

const assignment_list &

x

)

Definition at line 29 of file data.cpp.

pp() [7/61]

std::string mcrl2::data::pp

(

const assignment_vector &

x

)

Definition at line 30 of file data.cpp.

pp() [8/61]

std::string mcrl2::data::pp

(

const bag_comprehension &

x

)

Definition at line 44 of file data.cpp.

pp() [9/61]

std::string mcrl2::data::pp

(

const bag_comprehension_binder &

x

)

Definition at line 45 of file data.cpp.

pp() [10/61]

std::string mcrl2::data::pp

(

const bag_container &

x

)

Definition at line 46 of file data.cpp.

pp() [11/61]

std::string mcrl2::data::pp

(

const basic_sort &

x

)

Definition at line 47 of file data.cpp.

pp() [12/61]

std::string mcrl2::data::pp

(

const binder_type &

x

)

Definition at line 48 of file data.cpp.

pp() [13/61]

std::string mcrl2::data::pp

(

const container_sort &

x

)

Definition at line 49 of file data.cpp.

pp() [14/61]

std::string mcrl2::data::pp

(

const container_type &

x

)

Definition at line 50 of file data.cpp.

pp() [15/61]

std::string mcrl2::data::pp

(

const data::data_specification &

x

)

Definition at line 53 of file data.cpp.

pp() [16/61]

std::string mcrl2::data::pp

(

const data_equation &

x

)

Definition at line 51 of file data.cpp.

pp() [17/61]

std::string mcrl2::data::pp

(

const data_equation_list &

x

)

Definition at line 37 of file data.cpp.

pp() [18/61]

std::string mcrl2::data::pp

(

const data_equation_vector &

x

)

Definition at line 38 of file data.cpp.

pp() [19/61]

std::string mcrl2::data::pp

(

const data_expression &

x

)

Definition at line 52 of file data.cpp.

pp() [20/61]

std::string mcrl2::data::pp

(

const data_expression_list &

x

)

Definition at line 27 of file data.cpp.

pp() [21/61]

std::string mcrl2::data::pp

(

const data_expression_vector &

x

)

Definition at line 28 of file data.cpp.

pp() [22/61]

std::string mcrl2::data::pp

(

const exists &

x

)

Definition at line 54 of file data.cpp.

pp() [23/61]

std::string mcrl2::data::pp

(

const exists_binder &

x

)

Definition at line 55 of file data.cpp.

pp() [24/61]

std::string mcrl2::data::pp

(

const fbag_container &

x

)

Definition at line 56 of file data.cpp.

pp() [25/61]

std::string mcrl2::data::pp

(

const forall &

x

)

Definition at line 57 of file data.cpp.

pp() [26/61]

std::string mcrl2::data::pp

(

const forall_binder &

x

)

Definition at line 58 of file data.cpp.

pp() [27/61]

std::string mcrl2::data::pp

(

const fset_container &

x

)

Definition at line 59 of file data.cpp.

pp() [28/61]

std::string mcrl2::data::pp

(

const function_sort &

x

)

Definition at line 60 of file data.cpp.

pp() [29/61]

std::string mcrl2::data::pp

(

const function_symbol &

x

)

Definition at line 61 of file data.cpp.

pp() [30/61]

std::string mcrl2::data::pp

(

const function_symbol_list &

x

)

Definition at line 33 of file data.cpp.

pp() [31/61]

std::string mcrl2::data::pp

(

const function_symbol_vector &

x

)

Definition at line 34 of file data.cpp.

pp() [32/61]

std::string mcrl2::data::pp

(

const lambda &

x

)

Definition at line 62 of file data.cpp.

pp() [33/61]

std::string mcrl2::data::pp

(

const lambda_binder &

x

)

Definition at line 63 of file data.cpp.

pp() [34/61]

std::string mcrl2::data::pp ( const linear_inequality &  l )

inline

Definition at line 909 of file linear_inequalities.h.

pp() [35/61]

std::string mcrl2::data::pp

(

const list_container &

x

)

Definition at line 64 of file data.cpp.

pp() [36/61]

std::string mcrl2::data::pp ( const rewrite_strategy  s )

inline

Pretty prints a rewrite strategy.

Parameters

[in]

s

A rewrite strategy.

Definition at line 63 of file rewrite_strategy.h.

pp() [37/61]

std::string mcrl2::data::pp

(

const set_comprehension &

x

)

Definition at line 65 of file data.cpp.

pp() [38/61]

std::string mcrl2::data::pp

(

const set_comprehension_binder &

x

)

Definition at line 66 of file data.cpp.

pp() [39/61]

std::string mcrl2::data::pp

(

const set_container &

x

)

Definition at line 67 of file data.cpp.

pp() [40/61]

std::string mcrl2::data::pp

(

const sort_expression &

x

)

Definition at line 68 of file data.cpp.

pp() [41/61]

std::string mcrl2::data::pp

(

const sort_expression_list &

x

)

Definition at line 25 of file data.cpp.

pp() [42/61]

std::string mcrl2::data::pp

(

const sort_expression_vector &

x

)

Definition at line 26 of file data.cpp.

pp() [43/61]

std::string mcrl2::data::pp

(

const std::set< variable > &

x

)

Definition at line 105 of file data.cpp.

pp() [44/61]

std::string mcrl2::data::pp

(

const structured_sort &

x

)

Definition at line 69 of file data.cpp.

pp() [45/61]

std::string mcrl2::data::pp

(

const structured_sort_constructor &

x

)

Definition at line 70 of file data.cpp.

pp() [46/61]

std::string mcrl2::data::pp

(

const structured_sort_constructor_argument &

x

)

Definition at line 71 of file data.cpp.

pp() [47/61]

std::string mcrl2::data::pp

(

const structured_sort_constructor_list &

x

)

Definition at line 35 of file data.cpp.

pp() [48/61]

std::string mcrl2::data::pp

(

const structured_sort_constructor_vector &

x

)

Definition at line 36 of file data.cpp.

pp() [49/61]

template<typename T >

std::string mcrl2::data::pp

(

const T &

x

)

Returns a string representation of the object x.

Definition at line 2314 of file print.h.

pp() [50/61]

std::string mcrl2::data::pp

(

const untyped_data_parameter &

x

)

Definition at line 72 of file data.cpp.

pp() [51/61]

std::string mcrl2::data::pp

(

const untyped_identifier &

x

)

Definition at line 73 of file data.cpp.

pp() [52/61]

std::string mcrl2::data::pp

(

const untyped_identifier_assignment &

x

)

Definition at line 74 of file data.cpp.

pp() [53/61]

std::string mcrl2::data::pp

(

const untyped_possible_sorts &

x

)

Definition at line 75 of file data.cpp.

pp() [54/61]

std::string mcrl2::data::pp

(

const untyped_set_or_bag_comprehension &

x

)

Definition at line 76 of file data.cpp.

pp() [55/61]

std::string mcrl2::data::pp

(

const untyped_set_or_bag_comprehension_binder &

x

)

Definition at line 77 of file data.cpp.

pp() [56/61]

std::string mcrl2::data::pp

(

const untyped_sort &

x

)

Definition at line 78 of file data.cpp.

pp() [57/61]

std::string mcrl2::data::pp

(

const untyped_sort_variable &

x

)

Definition at line 79 of file data.cpp.

pp() [58/61]

std::string mcrl2::data::pp

(

const variable &

x

)

Definition at line 80 of file data.cpp.

pp() [59/61]

std::string mcrl2::data::pp

(

const variable_list &

x

)

Definition at line 31 of file data.cpp.

pp() [60/61]

std::string mcrl2::data::pp

(

const variable_vector &

x

)

Definition at line 32 of file data.cpp.

pp() [61/61]

std::string mcrl2::data::pp

(

const where_clause &

x

)

Definition at line 81 of file data.cpp.

pp_vector()

template<class TYPE >

std::string mcrl2::data::pp_vector ( const TYPE &  inequalities )

inline

Print the vector of inequalities to stderr in readable form.

Definition at line 1027 of file linear_inequalities.h.

precedence() [1/8]

int mcrl2::data::precedence ( const application &  x )

inline

Definition at line 276 of file print.h.

precedence() [2/8]

constexpr int mcrl2::data::precedence ( const bag_comprehension &  )

constexpr

Definition at line 369 of file print.h.

precedence() [3/8]

int mcrl2::data::precedence ( const data_expression &  x )

inline

Definition at line 371 of file print.h.

precedence() [4/8]

constexpr int mcrl2::data::precedence ( const exists &  )

constexpr

Definition at line 366 of file print.h.

precedence() [5/8]

constexpr int mcrl2::data::precedence ( const forall &  )

constexpr

Definition at line 365 of file print.h.

precedence() [6/8]

constexpr int mcrl2::data::precedence ( const lambda &  )

constexpr

Definition at line 367 of file print.h.

precedence() [7/8]

constexpr int mcrl2::data::precedence ( const set_comprehension &  )

constexpr

Definition at line 368 of file print.h.

precedence() [8/8]

constexpr int mcrl2::data::precedence ( const where_clause &  )

constexpr

Definition at line 370 of file print.h.

print_equalities()

std::string mcrl2::data::print_equalities ( const std::map< variable, std::set< data_expression > > &  equalities )

inline

Definition at line 470 of file find_equalities.h.

print_inequalities()

std::string mcrl2::data::print_inequalities ( const std::map< variable, std::set< data_expression > > &  inequalities )

inline

Definition at line 485 of file find_equalities.h.

print_node()

void mcrl2::data::print_node ( const type_check_node_ptr &  node )

inline

Definition at line 1318 of file type_check_tree.h.

print_node_vector()

template<typename Container >

std::string mcrl2::data::print_node_vector	(	const std::string &	name,
		const Container &	nodes,
		const std::string &	sep = ", ",
		const std::string &	first = "",
		const std::string &	last = ""
	)

Definition at line 59 of file type_check_tree.h.

print_vector()

template<typename Container >

std::string mcrl2::data::print_vector	(	const std::string &	name,
		const Container &	nodes
	)

Definition at line 74 of file type_check_tree.h.

quantifiers_inside_rewrite() [1/2]

template<typename T >

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

Definition at line 329 of file quantifiers_inside_rewriter.h.

quantifiers_inside_rewrite() [2/2]

template<typename T >

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

Definition at line 323 of file quantifiers_inside_rewriter.h.

real_abs()

application mcrl2::data::real_abs ( const data_expression &  arg )

inline

Definition at line 77 of file linear_inequalities.h.

real_divides()

application mcrl2::data::real_divides ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Definition at line 56 of file linear_inequalities.h.

real_minus()

application mcrl2::data::real_minus ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Definition at line 63 of file linear_inequalities.h.

real_minus_one()

data_expression & mcrl2::data::real_minus_one ( )

inline

Definition at line 947 of file linear_inequalities.h.

real_negate()

application mcrl2::data::real_negate ( const data_expression &  arg )

inline

Definition at line 70 of file linear_inequalities.h.

real_one()

data_expression & mcrl2::data::real_one ( )

inline

Definition at line 941 of file linear_inequalities.h.

real_plus()

application mcrl2::data::real_plus ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Definition at line 49 of file linear_inequalities.h.

real_times()

application mcrl2::data::real_times ( const data_expression &  arg0, const data_expression &  arg1  )

inline

Definition at line 42 of file linear_inequalities.h.

real_zero()

data_expression & mcrl2::data::real_zero ( )

inline

Definition at line 935 of file linear_inequalities.h.

register_function_symbol_hooks()

void mcrl2::data::register_function_symbol_hooks ( )

inline

Definition at line 34 of file index_traits.h.

remove_assignments()

template<typename VariableSequence >

void mcrl2::data::remove_assignments ( data::mutable_indexed_substitution<> &  sigma, const VariableSequence &  v  )

inline

Removes assignments to variables in v from the substitution sigma.

Definition at line 39 of file substitution_utility.h.

remove_index()

atermpp::aterm mcrl2::data::remove_index

(

const atermpp::aterm &

x

)

Transforms DataVarIdNoIndex to DataVarId and transforms OpIdNoIndex to OpId.

remove_redundant_inequalities()

void mcrl2::data::remove_redundant_inequalities ( const std::vector< linear_inequality > &  inequalities, std::vector< linear_inequality > &  resulting_inequalities, const rewriter &  r  )

inline

Remove every redundant inequality from a vector of inequalities.

If inequalities is inconsistent, [false] is returned. Otherwise a list of inequalities is returned, from which no inequality can be removed without changing the vector of solutions of the inequalities. Redundancy of equalities is not checked, because this is quite expensive.

Parameters

inequalities	A list of inequalities
resulting_inequalities	A list of inequalities to which the result is stored.
r	A rewriter

Definition at line 1160 of file linear_inequalities.h.

replace_all_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::data::replace_all_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 242 of file replace.h.

replace_all_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::data::replace_all_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 233 of file replace.h.

replace_data_expressions() [1/2]

template<typename T , typename Substitution >

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

Definition at line 200 of file replace.h.

replace_data_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::data::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 190 of file replace.h.

replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >

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

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 294 of file replace.h.

replace_free_variables() [2/4]

template<typename T , typename Substitution >

T mcrl2::data::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 267 of file replace.h.

replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >

void mcrl2::data::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
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 281 of file replace.h.

replace_free_variables() [4/4]

template<typename T , typename Substitution >

void mcrl2::data::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 255 of file replace.h.

replace_sort_expressions() [1/2]

template<typename T , typename Substitution >

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

Definition at line 178 of file replace.h.

replace_sort_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::data::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 168 of file replace.h.

replace_untyped_sort()

template<typename T >

T mcrl2::data::replace_untyped_sort	(	const T &	x,
		const sort_expression &	replacement
	)

Definition at line 33 of file type_check_tree.h.

replace_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::data::replace_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 222 of file replace.h.

replace_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::data::replace_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

Definition at line 213 of file replace.h.

replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >

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

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 253 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >

T mcrl2::data::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution.

Definition at line 287 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >

void mcrl2::data::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
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 238 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >

void mcrl2::data::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution.

Definition at line 269 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

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

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the substiution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names. \return The result is the term x to which sigma has been applied.

Definition at line 280 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

void mcrl2::data::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
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the subsitution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names.

Definition at line 261 of file replace_capture_avoiding_with_an_identifier_generator.h.

rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

T mcrl2::data::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution \return the rewrite result

Definition at line 134 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter >

T mcrl2::data::rewrite	(	const T &	x,
		Rewriter	R,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter \return the rewrite result

Definition at line 104 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

void mcrl2::data::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution

Definition at line 119 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter >

void mcrl2::data::rewrite	(	T &	x,
		Rewriter	R,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= nullptr
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter

Definition at line 91 of file rewrite.h.

rewrite_with_memory()

data_expression mcrl2::data::rewrite_with_memory ( const data_expression &  t, const rewriter &  r  )

inline

Definition at line 2115 of file linear_inequalities.h.

right_hand_sides()

data_expression_list mcrl2::data::right_hand_sides ( const assignment_list &  x )

inline

Returns the right hand sides of an assignment list.

Parameters

x	An assignment list

Definition at line 318 of file assignment.h.

search_data_expression()

template<typename Container >

bool mcrl2::data::search_data_expression	(	Container const &	container,
		const data_expression &	s
	)

Returns true if the term has a given data expression as subterm.

Parameters

[in]	container	an expression or container of expressions
[in]	s	A data expression

Returns

True if the term has a given data expression as subterm.

Definition at line 479 of file find.h.

search_free_variable()

template<typename T >

bool mcrl2::data::search_free_variable	(	const T &	x,
		const variable &	v
	)

Returns true if the term has a given free variable as subterm.

Parameters

[in]	x	an expression
[in]	v	a variable

Returns

True if v occurs free in x.

Definition at line 456 of file find.h.

search_sort_expression()

template<typename Container >

bool mcrl2::data::search_sort_expression	(	Container const &	container,
		const sort_expression &	s
	)

Returns true if the term has a given sort expression as subterm.

Parameters

[in]	container	an expression or container of expressions
[in]	s	A sort expression

Returns

True if the term has a given sort expression as subterm.

Definition at line 468 of file find.h.

search_variable() [1/2]

bool mcrl2::data::search_variable	(	const data::data_expression &	x,
		const data::variable &	v
	)

Definition at line 102 of file data.cpp.

search_variable() [2/2]

template<typename T >

bool mcrl2::data::search_variable	(	const T &	x,
		const variable &	v
	)

Returns true if the term has a given variable as subterm.

Parameters

[in]	x	an expression
[in]	v	a variable

Returns

True if v occurs in x.

Definition at line 444 of file find.h.

simplify() [1/2]

template<typename T >

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

Definition at line 155 of file simplify_rewriter.h.

simplify() [2/2]

template<typename T >

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

Definition at line 149 of file simplify_rewriter.h.

split_and()

std::set< data_expression > mcrl2::data::split_and ( const data_expression &  expr )

inline

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.

Parameters

expr	A data expression

Returns

A sequence of operands

Definition at line 68 of file join.h.

split_conjunction()

std::list< data_expression > mcrl2::data::split_conjunction ( const data_expression &  condition )

inline

Split a disjunctive expression into a set of clauses.

Definition at line 242 of file standard_utility.h.

split_disjunction()

std::list< data_expression > mcrl2::data::split_disjunction ( const data_expression &  condition )

inline

Split a disjunctive expression into a set of clauses.

Definition at line 214 of file standard_utility.h.

split_or()

std::set< data_expression > mcrl2::data::split_or ( const data_expression &  expr )

inline

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.

Parameters

expr	A data expression

Returns

A sequence of operands

Definition at line 53 of file join.h.

standard_generate_equations_code()

data_equation_vector mcrl2::data::standard_generate_equations_code ( const sort_expression &  s )

inline

Give all standard system defined equations for sort s.

Parameters

[in]

s

A sort expression

Returns

All standard system defined equations for sort s

Definition at line 405 of file standard.h.

standard_generate_functions_code()

function_symbol_vector mcrl2::data::standard_generate_functions_code ( const sort_expression &  s )

inline

Give all standard system defined functions for sort s.

Parameters

[in]

s

A sort expression

Returns

All standard system defined functions for sort s

Definition at line 388 of file standard.h.

substitute()

sort_expression mcrl2::data::substitute ( const sort_expression &  x, const sort_substitution &  sigma  )

inline

Definition at line 44 of file type_check_tree.h.

substitute_constraint()

constraint_ptr mcrl2::data::substitute_constraint ( constraint_ptr  p, const sort_substitution &  sigma  )

inline

Definition at line 1332 of file type_check_tree.h.

substitute_sorts() [1/2]

template<typename T , typename Substitution >

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

Definition at line 317 of file replace.h.

substitute_sorts() [2/2]

template<typename T , typename Substitution >

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

Definition at line 308 of file replace.h.

substitution_variables() [1/5]

template<typename AssociativeContainer >

std::set< data::variable > mcrl2::data::substitution_variables

(

const map_substitution< AssociativeContainer > &

sigma

)

Definition at line 75 of file map_substitution.h.

substitution_variables() [2/5]

template<typename VariableType = variable, typename ExpressionType = data_expression>

std::multiset< variable > mcrl2::data::substitution_variables

(

const mutable_indexed_substitution< VariableType, ExpressionType > &

sigma

)

Definition at line 309 of file mutable_indexed_substitution.h.

substitution_variables() [3/5]

std::set< data::variable > mcrl2::data::substitution_variables

(

const mutable_map_substitution<> &

sigma

)

Definition at line 178 of file data.cpp.

substitution_variables() [4/5]

template<typename Substitution >

std::set< data::variable > mcrl2::data::substitution_variables

(

const Substitution &

)

Returns the variables appearing in the right hand sides of the substitution.

Definition at line 161 of file replace.h.

substitution_variables() [5/5]

std::set< data::variable > mcrl2::data::substitution_variables ( const variable_substitution &  sigma )

inline

Definition at line 50 of file variable_substitution.h.

subtract()

linear_inequality mcrl2::data::subtract ( const linear_inequality &  e1, const linear_inequality &  e2, const data_expression &  f1, const data_expression &  f2, const rewriter &  r  )

inline

Subtract the given equality, multiplied by f1/f2. The result is e1-(f1/f2)e2,.

Definition at line 916 of file linear_inequalities.h.

swap() [1/42]

void mcrl2::data::swap ( abstraction &  t1, abstraction &  t2  )

inline

\brief swap overload

Definition at line 100 of file abstraction.h.

swap() [2/42]

void mcrl2::data::swap ( alias &  t1, alias &  t2  )

inline

\brief swap overload

Definition at line 100 of file alias.h.

swap() [3/42]

void mcrl2::data::swap ( application &  t1, application &  t2  )

inline

swap overload

Definition at line 539 of file application.h.

swap() [4/42]

void mcrl2::data::swap ( assignment &  t1, assignment &  t2  )

inline

\brief swap overload

Definition at line 174 of file assignment.h.

swap() [5/42]

void mcrl2::data::swap ( assignment_expression &  t1, assignment_expression &  t2  )

inline

\brief swap overload

Definition at line 83 of file assignment.h.

swap() [6/42]

void mcrl2::data::swap ( bag_comprehension &  t1, bag_comprehension &  t2  )

inline

\brief swap overload

Definition at line 83 of file bag_comprehension.h.

swap() [7/42]

void mcrl2::data::swap ( bag_comprehension_binder &  t1, bag_comprehension_binder &  t2  )

inline

\brief swap overload

Definition at line 228 of file binder_type.h.

swap() [8/42]

void mcrl2::data::swap ( bag_container &  t1, bag_container &  t2  )

inline

\brief swap overload

Definition at line 228 of file container_type.h.

swap() [9/42]

void mcrl2::data::swap ( basic_sort &  t1, basic_sort &  t2  )

inline

\brief swap overload

Definition at line 85 of file basic_sort.h.

swap() [10/42]

void mcrl2::data::swap ( binder_type &  t1, binder_type &  t2  )

inline

\brief swap overload

Definition at line 69 of file binder_type.h.

swap() [11/42]

void mcrl2::data::swap ( container_sort &  t1, container_sort &  t2  )

inline

\brief swap overload

Definition at line 86 of file container_sort.h.

swap() [12/42]

void mcrl2::data::swap ( container_type &  t1, container_type &  t2  )

inline

\brief swap overload

Definition at line 69 of file container_type.h.

swap() [13/42]

void mcrl2::data::swap ( data_equation &  t1, data_equation &  t2  )

inline

\brief swap overload

Definition at line 141 of file data_equation.h.

swap() [14/42]

void mcrl2::data::swap ( data_expression &  t1, data_expression &  t2  )

inline

\brief swap overload

Definition at line 200 of file data_expression.h.

swap() [15/42]

void mcrl2::data::swap ( exists &  t1, exists &  t2  )

inline

\brief swap overload

Definition at line 85 of file exists.h.

swap() [16/42]

void mcrl2::data::swap ( exists_binder &  t1, exists_binder &  t2  )

inline

\brief swap overload

Definition at line 334 of file binder_type.h.

swap() [17/42]

void mcrl2::data::swap ( fbag_container &  t1, fbag_container &  t2  )

inline

\brief swap overload

Definition at line 334 of file container_type.h.

swap() [18/42]

void mcrl2::data::swap ( forall &  t1, forall &  t2  )

inline

\brief swap overload

Definition at line 84 of file forall.h.

swap() [19/42]

void mcrl2::data::swap ( forall_binder &  t1, forall_binder &  t2  )

inline

\brief swap overload

Definition at line 281 of file binder_type.h.

swap() [20/42]

void mcrl2::data::swap ( fset_container &  t1, fset_container &  t2  )

inline

\brief swap overload

Definition at line 281 of file container_type.h.

swap() [21/42]

void mcrl2::data::swap ( function_sort &  t1, function_sort &  t2  )

inline

\brief swap overload

Definition at line 91 of file function_sort.h.

swap() [22/42]

void mcrl2::data::swap ( function_symbol &  t1, function_symbol &  t2  )

inline

\brief swap overload

Definition at line 107 of file function_symbol.h.

swap() [23/42]

void mcrl2::data::swap ( lambda &  t1, lambda &  t2  )

inline

\brief swap overload

Definition at line 99 of file lambda.h.

swap() [24/42]

void mcrl2::data::swap ( lambda_binder &  t1, lambda_binder &  t2  )

inline

\brief swap overload

Definition at line 387 of file binder_type.h.

swap() [25/42]

void mcrl2::data::swap ( list_container &  t1, list_container &  t2  )

inline

\brief swap overload

Definition at line 122 of file container_type.h.

swap() [26/42]

void mcrl2::data::swap ( set_comprehension &  t1, set_comprehension &  t2  )

inline

\brief swap overload

Definition at line 83 of file set_comprehension.h.

swap() [27/42]

void mcrl2::data::swap ( set_comprehension_binder &  t1, set_comprehension_binder &  t2  )

inline

\brief swap overload

Definition at line 175 of file binder_type.h.

swap() [28/42]

void mcrl2::data::swap ( set_container &  t1, set_container &  t2  )

inline

\brief swap overload

Definition at line 175 of file container_type.h.

swap() [29/42]

void mcrl2::data::swap ( sort_expression &  t1, sort_expression &  t2  )

inline

\brief swap overload

Definition at line 121 of file sort_expression.h.

swap() [30/42]

void mcrl2::data::swap ( structured_sort &  t1, structured_sort &  t2  )

inline

\brief swap overload

Definition at line 464 of file structured_sort.h.

swap() [31/42]

void mcrl2::data::swap ( structured_sort_constructor &  t1, structured_sort_constructor &  t2  )

inline

\brief swap overload

Definition at line 227 of file structured_sort_constructor.h.

swap() [32/42]

void mcrl2::data::swap ( structured_sort_constructor_argument &  t1, structured_sort_constructor_argument &  t2  )

inline

\brief swap overload

Definition at line 121 of file structured_sort_constructor_argument.h.

swap() [33/42]

void mcrl2::data::swap ( untyped_data_parameter &  t1, untyped_data_parameter &  t2  )

inline

\brief swap overload

Definition at line 103 of file untyped_data_parameter.h.

swap() [34/42]

void mcrl2::data::swap ( untyped_identifier &  t1, untyped_identifier &  t2  )

inline

\brief swap overload

Definition at line 83 of file untyped_identifier.h.

swap() [35/42]

void mcrl2::data::swap ( untyped_identifier_assignment &  t1, untyped_identifier_assignment &  t2  )

inline

\brief swap overload

Definition at line 270 of file assignment.h.

swap() [36/42]

void mcrl2::data::swap ( untyped_possible_sorts &  t1, untyped_possible_sorts &  t2  )

inline

\brief swap overload

Definition at line 84 of file untyped_possible_sorts.h.

swap() [37/42]

void mcrl2::data::swap ( untyped_set_or_bag_comprehension &  t1, untyped_set_or_bag_comprehension &  t2  )

inline

\brief swap overload

Definition at line 83 of file untyped_set_or_bag_comprehension.h.

swap() [38/42]

void mcrl2::data::swap ( untyped_set_or_bag_comprehension_binder &  t1, untyped_set_or_bag_comprehension_binder &  t2  )

inline

\brief swap overload

Definition at line 122 of file binder_type.h.

swap() [39/42]

void mcrl2::data::swap ( untyped_sort &  t1, untyped_sort &  t2  )

inline

\brief swap overload

Definition at line 60 of file untyped_sort.h.

swap() [40/42]

void mcrl2::data::swap ( untyped_sort_variable &  t1, untyped_sort_variable &  t2  )

inline

\brief swap overload

Definition at line 93 of file untyped_sort_variable.h.

swap() [41/42]

void mcrl2::data::swap ( variable &  t1, variable &  t2  )

inline

\brief swap overload

Definition at line 105 of file variable.h.

swap() [42/42]

void mcrl2::data::swap ( where_clause &  t1, where_clause &  t2  )

inline

\brief swap overload

Definition at line 97 of file where_clause.h.

translate_user_notation() [1/4]

data::data_equation mcrl2::data::translate_user_notation

(

const data::data_equation &

x

)

Definition at line 89 of file data.cpp.

translate_user_notation() [2/4]

data::data_expression mcrl2::data::translate_user_notation

(

const data::data_expression &

x

)

Definition at line 88 of file data.cpp.

translate_user_notation() [3/4]

template<typename T >

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

Definition at line 164 of file translate_user_notation.h.

translate_user_notation() [4/4]

template<typename T >

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

Definition at line 156 of file translate_user_notation.h.

true_()

const data_expression & mcrl2::data::true_ ( )

inline

Returns

The expression true

Definition at line 92 of file consistency.h.

typecheck_data_expression() [1/2]

data_expression mcrl2::data::typecheck_data_expression ( const data_expression &  x, const data_specification &  dataspec = data_specification()  )

inline

Type check a data expression. Throws an exception if something went wrong.

Parameters

[in]	x	A data expression that has not been type checked.
[in]	dataspec	Data specification to be used as context.

Postcondition

data_expr is type checked.

Definition at line 333 of file typecheck.h.

typecheck_data_expression() [2/2]

template<typename VariableContainer >

data_expression mcrl2::data::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.

Parameters

[in]	x	A data expression that has not been type checked.
[in]	variables	A container with variables that can occur in the data expression.
[in]	dataspec	The data specification that is used for type checking.

Postcondition

data_expr is type checked.

Definition at line 308 of file typecheck.h.

typecheck_data_specification()

void mcrl2::data::typecheck_data_specification ( data_specification &  data_spec )

inline

Type check a parsed mCRL2 data specification. Throws an exception if something went wrong.

Parameters

[in]

data_spec

A data specification that has not been type checked.

Postcondition

data_spec is type checked.

Definition at line 344 of file typecheck.h.

typecheck_sort_expression()

void mcrl2::data::typecheck_sort_expression ( const sort_expression &  sort_expr, const data_specification &  data_spec  )

inline

Type check a sort expression. Throws an exception if something went wrong.

Parameters

[in]	sort_expr	A sort expression that has not been type checked.
[in]	data_spec	The data specification to use as context.

Postcondition

sort_expr is type checked.

Definition at line 286 of file typecheck.h.

typecheck_untyped_data_parameter()

data_expression mcrl2::data::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  )

inline

Definition at line 351 of file typecheck.h.

unary_operand()

const data_expression & mcrl2::data::unary_operand ( const application &  x )

inline

Definition at line 727 of file application.h.

unary_operand1()

const data_expression & mcrl2::data::unary_operand1 ( const data_expression &  x )

inline

Definition at line 745 of file application.h.

undefined_data_expression()

const data::data_expression & mcrl2::data::undefined_data_expression ( )

inline

Returns a data expression that corresponds to 'undefined'.

Definition at line 54 of file undefined.h.

undefined_index()

constexpr std::size_t mcrl2::data::undefined_index ( )

inlineconstexpr

Returns an index that corresponds to 'undefined'.

Definition at line 23 of file undefined.h.

undefined_real()

const data::data_expression & mcrl2::data::undefined_real ( )

inline

Returns a data expression of type Real that corresponds to 'undefined'.

Definition at line 62 of file undefined.h.

undefined_real_variable()

const data::variable & mcrl2::data::undefined_real_variable ( )

inline

Returns a data variable that corresponds to 'undefined'.

Definition at line 38 of file undefined.h.

undefined_sort_expression()

const data::sort_expression & mcrl2::data::undefined_sort_expression ( )

inline

Returns a sort expression that corresponds to 'undefined'.

Definition at line 46 of file undefined.h.

undefined_variable()

const data::variable & mcrl2::data::undefined_variable ( )

inline

Returns a data variable that corresponds to 'undefined'.

Definition at line 30 of file undefined.h.

unfold_pattern_matching()

template<typename StructInfo >

data_equation mcrl2::data::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.

For example, the collection of rewrite rules below:

sign_of_list_sum([]) = false; is_even(n) -> sign_of_list_sum(n |> l) = sign_of_list_sum(l); !is_even(n) -> sign_of_list_sum(n |> l) = !sign_of_list_sum(l);

gets translated into the following function specification:

sign_of_list_sum(l) = if(is_emptylist(l), false, if(is_even(head(l)), sign_of_list_sum(tail(l)), !sign_of_list_sum(tail(l))))

Two complications can arise. The rewrite rule set may contain rules that do not pattern-match on the function parameters, such as 'not(not(b)) = b‘; rules like these are discarded. More problematically, the set of rewrite rules may not be complete, or may not easily be proven complete; in the example above, if the rewriter cannot rewrite 'is_even(n) || !is_even(n)’ to 'true', the translation cannot tell that the rewrite rule set is complete. In cases where a (non-constructor )function invocation can genuinely not be rewritten any further, the MCRL2 semantics are unspecified (TODO check this); the translation resolves this situation by returning an arbitrary value in this case. Thus, in practice, the function definion above might well be translated into the following:

sign_of_list_sum(l) = if(is_emptylist(l), false, if(is_even(head(l)), sign_of_list_sum(tail(l)), if(!is_even(head(l)), !sign_of_list_sum(tail(l)), false)))

Where 'false' is a representative of sort_bool.

Definition at line 437 of file unfold_pattern_matching.h.

variable_list_to_data_expression_list()

const data_expression_list & mcrl2::data::variable_list_to_data_expression_list ( const variable_list &  l )

inline

Transform a variable_list into a data_expression_list.

Definition at line 291 of file data_expression.h.