Contains type information for data expressions. More...

#include <expression_traits.h>

Public Types
typedef data::data_expression	term_type
	The term type.

typedef data::variable	variable_type
	The variable type.

typedef data::variable_list	variable_sequence_type
	The variable sequence type.

Static Public Member Functions
static const term_type &	true_ ()
	The value true.

static const term_type &	false_ ()
	The value false.

static term_type	not_ (const term_type &p)
	Operator not.

static void	make_not_ (term_type &result, const term_type &p)
	Operator not.

static term_type	and_ (const term_type &p, const term_type &q)
	Operator and.

static void	make_and_ (term_type &result, const term_type &p, const term_type &q)
	Operator and.

static term_type	or_ (const term_type &p, const term_type &q)
	Operator or.

static void	make_or_ (term_type &result, const term_type &p, const term_type &q)
	Operator or.

static term_type	imp (const term_type &p, const term_type &q)
	Operator imp.

static void	make_imp (term_type &result, const term_type &p, const term_type &q)
	Operator imp.

static term_type	forall (const variable_sequence_type &d, const term_type &p)
	Operator forall.

static void	make_forall (term_type &result, const variable_sequence_type &d, const term_type &p)
	Construct a forall.

static term_type	exists (const variable_sequence_type &d, const term_type &p)
	Operator exists.

static void	make_exists (term_type &result, const variable_sequence_type &d, const term_type &p)
	Construct an exists.

static bool	is_true (const term_type &t)
	Test for value true.

static bool	is_false (const term_type &t)
	Test for value false.

static bool	is_not (const term_type &t)
	Test for operator not.

static bool	is_and (const term_type &t)
	Test for operator and.

static bool	is_or (const term_type &t)
	Test for operator or.

static bool	is_imp (const term_type &t)
	Test for implication.

static bool	is_forall (const term_type &t)
	Test for universal quantification.

static bool	is_exists (const term_type &t)
	Test for existential quantification.

static bool	is_lambda (const term_type &t)
	Test for lambda abstraction.

static const term_type &	variable2term (const variable_type &v)
	Conversion from variable to term.

static bool	is_variable (const term_type &t)
	Test if a term is a variable.

static const term_type &	argument (const term_type &t, const std::size_t n)
	Get the n-th argument of a data expression, provided it is an application.

static const term_type &	left (const term_type &t)

static const term_type &	right (const term_type &t)

static const term_type &	not_arg (const term_type &t)

static std::string	pp (const term_type &t)
	Pretty print function.

Detailed Description

Contains type information for data expressions.

Definition at line 28 of file expression_traits.h.

Member Typedef Documentation

◆ term_type

typedef data::data_expression mcrl2::core::term_traits< data::data_expression >::term_type

The term type.

Definition at line 31 of file expression_traits.h.

◆ variable_sequence_type

typedef data::variable_list mcrl2::core::term_traits< data::data_expression >::variable_sequence_type

The variable sequence type.

Definition at line 37 of file expression_traits.h.

◆ variable_type

typedef data::variable mcrl2::core::term_traits< data::data_expression >::variable_type

The variable type.

Definition at line 34 of file expression_traits.h.

Member Function Documentation

◆ and_()

static term_type mcrl2::core::term_traits< data::data_expression >::and_	(	const term_type &	p,
		const term_type &	q
	)

inlinestatic

Operator and.

Parameters

p	A term
q	A term

Returns: Operator and applied to p and q

Definition at line 78 of file expression_traits.h.

◆ argument()

static const term_type & mcrl2::core::term_traits< data::data_expression >::argument	(	const term_type &	t,
		const std::size_t	n
	)

inlinestatic

Get the n-th argument of a data expression, provided it is an application.

Parameters

t	A term which is an application.
n	The index of the argument. The first index has number 0.

Returns: the n-th argument of t.

This function is linear in n.

Definition at line 278 of file expression_traits.h.

◆ exists()

static term_type mcrl2::core::term_traits< data::data_expression >::exists	(	const variable_sequence_type &	d,
		const term_type &	p
	)

inlinestatic

Operator exists.

Parameters

d	A sequence of variables
p	A term

Returns: Operator exists applied to d and p

Definition at line 158 of file expression_traits.h.

◆ false_()

static const term_type & mcrl2::core::term_traits< data::data_expression >::false_ ( )

inlinestatic

The value false.

Returns: The value false

Definition at line 50 of file expression_traits.h.

◆ forall()

static term_type mcrl2::core::term_traits< data::data_expression >::forall	(	const variable_sequence_type &	d,
		const term_type &	p
	)

inlinestatic

Operator forall.

Parameters

d	A sequence of variables
p	A term

Returns: Operator forall applied to d and p

Definition at line 138 of file expression_traits.h.

◆ imp()

static term_type mcrl2::core::term_traits< data::data_expression >::imp	(	const term_type &	p,
		const term_type &	q
	)

inlinestatic

Operator imp.

Parameters

p	A term
q	A term

Returns: Operator or applied to p and q

Definition at line 118 of file expression_traits.h.

◆ is_and()

static bool mcrl2::core::term_traits< data::data_expression >::is_and ( const term_type & t )

inlinestatic

Test for operator and.

Parameters

t A term

Returns: True if the term is of type and

Definition at line 204 of file expression_traits.h.

◆ is_exists()

static bool mcrl2::core::term_traits< data::data_expression >::is_exists ( const term_type & t )

inlinestatic

Test for existential quantification.

Parameters

t A term

Returns: True if the term is an existential quantification

Definition at line 240 of file expression_traits.h.

◆ is_false()

static bool mcrl2::core::term_traits< data::data_expression >::is_false ( const term_type & t )

inlinestatic

Test for value false.

Parameters

t A term

Returns: True if the term has the value false

Definition at line 186 of file expression_traits.h.

◆ is_forall()

static bool mcrl2::core::term_traits< data::data_expression >::is_forall ( const term_type & t )

inlinestatic

Test for universal quantification.

Parameters

t A term

Returns: True if the term is an universal quantification

Definition at line 231 of file expression_traits.h.

◆ is_imp()

static bool mcrl2::core::term_traits< data::data_expression >::is_imp ( const term_type & t )

inlinestatic

Test for implication.

Parameters

t A term

Returns: True if the term is an implication

Definition at line 222 of file expression_traits.h.

◆ is_lambda()

static bool mcrl2::core::term_traits< data::data_expression >::is_lambda ( const term_type & t )

inlinestatic

Test for lambda abstraction.

Parameters

t A term

Returns: True if the term is a lambda expression

Definition at line 249 of file expression_traits.h.

◆ is_not()

static bool mcrl2::core::term_traits< data::data_expression >::is_not ( const term_type & t )

inlinestatic

Test for operator not.

Parameters

t A term

Returns: True if the term is of type not

Definition at line 195 of file expression_traits.h.

◆ is_or()

static bool mcrl2::core::term_traits< data::data_expression >::is_or ( const term_type & t )

inlinestatic

Test for operator or.

Parameters

t A term

Returns: True if the term is of type or

Definition at line 213 of file expression_traits.h.

◆ is_true()

static bool mcrl2::core::term_traits< data::data_expression >::is_true ( const term_type & t )

inlinestatic

Test for value true.

Parameters

t A term

Returns: True if the term has the value true

Definition at line 177 of file expression_traits.h.

◆ is_variable()

static bool mcrl2::core::term_traits< data::data_expression >::is_variable ( const term_type & t )

inlinestatic

Test if a term is a variable.

Parameters

t A term

Returns: True if the term is a variable

Definition at line 267 of file expression_traits.h.

◆ left()

static const term_type & mcrl2::core::term_traits< data::data_expression >::left ( const term_type & t )

inlinestatic

Definition at line 293 of file expression_traits.h.

◆ make_and_()

static void mcrl2::core::term_traits< data::data_expression >::make_and_	(	term_type &	result,
		const term_type &	p,
		const term_type &	q
	)

inlinestatic

Operator and.

Parameters

result	Operator and applied to p and q
p	A term
q	A term

Definition at line 88 of file expression_traits.h.

◆ make_exists()

static void mcrl2::core::term_traits< data::data_expression >::make_exists	(	term_type &	result,
		const variable_sequence_type &	d,
		const term_type &	p
	)

inlinestatic

Construct an exists.

Parameters

result	Place where the forall is put.
d	A sequence of variables
p	A term

Definition at line 168 of file expression_traits.h.

◆ make_forall()

static void mcrl2::core::term_traits< data::data_expression >::make_forall	(	term_type &	result,
		const variable_sequence_type &	d,
		const term_type &	p
	)

inlinestatic

Construct a forall.

Parameters

result	Place where the forall is put.
d	A sequence of variables
p	A term

Definition at line 148 of file expression_traits.h.

◆ make_imp()

static void mcrl2::core::term_traits< data::data_expression >::make_imp	(	term_type &	result,
		const term_type &	p,
		const term_type &	q
	)

inlinestatic

Operator imp.

Parameters

result	Operator and applied to p and q
p	A term
q	A term

Definition at line 128 of file expression_traits.h.

◆ make_not_()

static void mcrl2::core::term_traits< data::data_expression >::make_not_	(	term_type &	result,
		const term_type &	p
	)

inlinestatic

Operator not.

Parameters

result	Operator not applied to p
p	A term

Definition at line 68 of file expression_traits.h.

◆ make_or_()

static void mcrl2::core::term_traits< data::data_expression >::make_or_	(	term_type &	result,
		const term_type &	p,
		const term_type &	q
	)

inlinestatic

Operator or.

Parameters

result	Operator or applied to p and q
p	A term
q	A term

Definition at line 108 of file expression_traits.h.

◆ not_()

static term_type mcrl2::core::term_traits< data::data_expression >::not_ ( const term_type & p )

inlinestatic

Operator not.

Parameters

p A term

Returns: Operator not applied to p

Definition at line 59 of file expression_traits.h.

◆ not_arg()

static const term_type & mcrl2::core::term_traits< data::data_expression >::not_arg ( const term_type & t )

inlinestatic

Definition at line 311 of file expression_traits.h.

◆ or_()

static term_type mcrl2::core::term_traits< data::data_expression >::or_	(	const term_type &	p,
		const term_type &	q
	)

inlinestatic

Operator or.

Parameters

p	A term
q	A term

Returns: Operator or applied to p and q

Definition at line 98 of file expression_traits.h.

◆ pp()

static std::string mcrl2::core::term_traits< data::data_expression >::pp ( const term_type & t )

inlinestatic

Pretty print function.

Parameters

t A term

Returns: A pretty print representation of the term

Definition at line 324 of file expression_traits.h.

◆ right()

static const term_type & mcrl2::core::term_traits< data::data_expression >::right ( const term_type & t )

inlinestatic

Definition at line 302 of file expression_traits.h.

◆ true_()

static const term_type & mcrl2::core::term_traits< data::data_expression >::true_ ( )

inlinestatic

The value true.

Returns: The value true

Definition at line 42 of file expression_traits.h.

◆ variable2term()

static const term_type & mcrl2::core::term_traits< data::data_expression >::variable2term ( const variable_type & v )

inlinestatic

Conversion from variable to term.

Parameters

v	A variable

Returns: The converted variable

Definition at line 258 of file expression_traits.h.

The documentation for this struct was generated from the following file:

data/include/mcrl2/data/expression_traits.h

Public Types

Static Public Member Functions

Detailed Description

Member Typedef Documentation

◆ term_type

◆ variable_sequence_type

◆ variable_type

Member Function Documentation

◆ and_()

◆ argument()

◆ exists()

◆ false_()

◆ forall()

◆ imp()

◆ is_and()

◆ is_exists()

◆ is_false()

◆ is_forall()

◆ is_imp()

◆ is_lambda()

◆ is_not()

◆ is_or()

◆ is_true()

◆ is_variable()

◆ left()

◆ make_and_()

◆ make_exists()

◆ make_forall()

◆ make_imp()

◆ make_not_()

◆ make_or_()

◆ not_()

◆ not_arg()

◆ or_()

◆ pp()

◆ right()

◆ true_()

◆ variable2term()