Contains type information for pbes expressions. More...

#include <pbes_expression.h>

Inheritance diagram for mcrl2::core::term_traits< pbes_system::pbes_expression >:

Public Types
typedef pbes_system::pbes_expression	term_type
	The term type.

typedef data::data_expression	data_term_type
	The data term type.

typedef data::data_expression_list	data_term_sequence_type
	The data term sequence type.

typedef data::variable	variable_type
	The variable type.

typedef data::variable_list	variable_sequence_type
	The variable sequence type.

typedef pbes_system::propositional_variable	propositional_variable_decl_type
	The propositional variable declaration type.

typedef pbes_system::propositional_variable_instantiation	propositional_variable_type
	The propositional variable instantiation type.

typedef core::identifier_string	string_type
	The string type.

Static Public Member Functions
static term_type	true_ ()
	Make the value true.

static term_type	false_ ()
	Make the value false.

static term_type	not_ (const term_type &p)
	Make a negation.

static void	make_not_ (term_type &result, const term_type &p)
	Make a negation.

static term_type	and_ (const term_type &p, const term_type &q)
	Make a conjunction.

static void	make_and_ (term_type &result, const term_type &p, const term_type &q)
	Make a conjunction.

static term_type	or_ (const term_type &p, const term_type &q)
	Make a disjunction.

static void	make_or_ (term_type &result, const term_type &p, const term_type &q)
	Make a disjunction.

template<typename FwdIt >
static term_type	join_or (FwdIt first, FwdIt last)

template<typename FwdIt >
static term_type	join_and (FwdIt first, FwdIt last)

static term_type	imp (const term_type &p, const term_type &q)
	Make an implication.

static void	make_imp (term_type &result, const term_type &p, const term_type &q)
	Make an implication.

static term_type	forall (const variable_sequence_type &l, const term_type &p)
	Make a universal quantification.

static void	make_forall (term_type &result, const variable_sequence_type &l, const term_type &p)
	Make a universal quantification.

static term_type	exists (const variable_sequence_type &l, const term_type &p)
	Make an existential quantification.

static void	make_exists (term_type &result, const variable_sequence_type &l, const term_type &p)
	Make an existential quantification.

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

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

static bool	is_not (const term_type &t)
	Test for a negation.

static bool	is_and (const term_type &t)
	Test for a conjunction.

static bool	is_or (const term_type &t)
	Test for a disjunction.

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

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

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

static bool	is_data (const term_type &t)
	Test for data term.

static bool	is_prop_var (const term_type &t)
	Test for propositional variable instantiation.

static term_type	left (const term_type &t)
	Returns the left argument of a term of type and, or or imp.

static term_type	right (const term_type &t)
	Returns the right argument of a term of type and, or or imp.

static const term_type &	not_arg (const term_type &t)
	Returns the argument of a term of type not.

static const variable_sequence_type &	var (const term_type &t)
	Returns the quantifier variables of a quantifier expression.

static const string_type &	name (const term_type &t)
	Returns the name of a propositional variable instantiation.

static const data_term_sequence_type &	param (const term_type &t)
	Returns the parameter list of a propositional variable instantiation.

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 std::string	pp (const term_type &t)
	Pretty print function.

Detailed Description

Contains type information for pbes expressions.

Definition at line 1085 of file pbes_expression.h.

Member Typedef Documentation

◆ data_term_sequence_type

typedef data::data_expression_list mcrl2::core::term_traits< pbes_system::pbes_expression >::data_term_sequence_type

The data term sequence type.

Definition at line 1094 of file pbes_expression.h.

◆ data_term_type

typedef data::data_expression mcrl2::core::term_traits< pbes_system::pbes_expression >::data_term_type

The data term type.

Definition at line 1091 of file pbes_expression.h.

◆ propositional_variable_decl_type

typedef pbes_system::propositional_variable mcrl2::core::term_traits< pbes_system::pbes_expression >::propositional_variable_decl_type

The propositional variable declaration type.

Definition at line 1103 of file pbes_expression.h.

◆ propositional_variable_type

typedef pbes_system::propositional_variable_instantiation mcrl2::core::term_traits< pbes_system::pbes_expression >::propositional_variable_type

The propositional variable instantiation type.

Definition at line 1106 of file pbes_expression.h.

◆ string_type

typedef core::identifier_string mcrl2::core::term_traits< pbes_system::pbes_expression >::string_type

The string type.

Definition at line 1109 of file pbes_expression.h.

◆ term_type

typedef pbes_system::pbes_expression mcrl2::core::term_traits< pbes_system::pbes_expression >::term_type

The term type.

Definition at line 1088 of file pbes_expression.h.

◆ variable_sequence_type

typedef data::variable_list mcrl2::core::term_traits< pbes_system::pbes_expression >::variable_sequence_type

The variable sequence type.

Definition at line 1100 of file pbes_expression.h.

◆ variable_type

typedef data::variable mcrl2::core::term_traits< pbes_system::pbes_expression >::variable_type

The variable type.

Definition at line 1097 of file pbes_expression.h.

Member Function Documentation

◆ and_()

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

inlinestatic

Make a conjunction.

Parameters

p	A term
q	A term

Returns: The value p && q

Definition at line 1150 of file pbes_expression.h.

◆ exists()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::exists	(	const variable_sequence_type &	l,
		const term_type &	p
	)

inlinestatic

Make an existential quantification.

Parameters

l	A sequence of variables
p	A term

Returns: The value exists l.p

Definition at line 1253 of file pbes_expression.h.

◆ false_()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::false_ ( )

inlinestatic

Make the value false.

Returns: The value false

Definition at line 1122 of file pbes_expression.h.

◆ forall()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::forall	(	const variable_sequence_type &	l,
		const term_type &	p
	)

inlinestatic

Make a universal quantification.

Parameters

l	A sequence of variables
p	A term

Returns: The value forall l.p

Definition at line 1224 of file pbes_expression.h.

◆ imp()

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

inlinestatic

Make an implication.

Parameters

p	A term
q	A term

Returns: The value p => q

Definition at line 1204 of file pbes_expression.h.

◆ is_and()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_and ( const term_type & t )

inlinestatic

Test for a conjunction.

Parameters

t A term

Returns: True if it is a conjunction

Definition at line 1308 of file pbes_expression.h.

◆ is_data()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_data ( const term_type & t )

inlinestatic

Test for data term.

Parameters

t A term

Returns: True if the term is a data term

Definition at line 1353 of file pbes_expression.h.

◆ is_exists()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_exists ( const term_type & t )

inlinestatic

Test for an existential quantification.

Parameters

t A term

Returns: True if it is an existential quantification

Definition at line 1344 of file pbes_expression.h.

◆ is_false()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_false ( const term_type & t )

inlinestatic

Test for the value false.

Parameters

t A term

Returns: True if it is the value false

Definition at line 1290 of file pbes_expression.h.

◆ is_forall()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_forall ( const term_type & t )

inlinestatic

Test for an universal quantification.

Parameters

t A term

Returns: True if it is a universal quantification

Definition at line 1335 of file pbes_expression.h.

◆ is_imp()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_imp ( const term_type & t )

inlinestatic

Test for an implication.

Parameters

t A term

Returns: True if it is an implication

Definition at line 1326 of file pbes_expression.h.

◆ is_not()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_not ( const term_type & t )

inlinestatic

Test for a negation.

Parameters

t A term

Returns: True if it is a negation

Definition at line 1299 of file pbes_expression.h.

◆ is_or()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_or ( const term_type & t )

inlinestatic

Test for a disjunction.

Parameters

t A term

Returns: True if it is a disjunction

Definition at line 1317 of file pbes_expression.h.

◆ is_prop_var()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_prop_var ( const term_type & t )

inlinestatic

Test for propositional variable instantiation.

Parameters

t A term

Returns: True if the term is a propositional variable instantiation

Definition at line 1362 of file pbes_expression.h.

◆ is_true()

static bool mcrl2::core::term_traits< pbes_system::pbes_expression >::is_true ( const term_type & t )

inlinestatic

Test for the value true.

Parameters

t A term

Returns: True if it is the value true

Definition at line 1281 of file pbes_expression.h.

◆ is_variable()

static bool mcrl2::core::term_traits< pbes_system::pbes_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 1441 of file pbes_expression.h.

◆ join_and()

template<typename FwdIt >

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::join_and	(	FwdIt	first,
		FwdIt	last
	)

inlinestatic

Definition at line 1194 of file pbes_expression.h.

◆ join_or()

template<typename FwdIt >

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::join_or	(	FwdIt	first,
		FwdIt	last
	)

inlinestatic

Definition at line 1187 of file pbes_expression.h.

◆ left()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::left ( const term_type & t )

inlinestatic

Returns the left argument of a term of type and, or or imp.

Parameters

t A term

Returns: The left argument of the term. Also works for data terms

Definition at line 1371 of file pbes_expression.h.

◆ make_and_()

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

inlinestatic

Make a conjunction.

Parameters

result	The value `p && q`
p	A term
q	A term

Definition at line 1160 of file pbes_expression.h.

◆ make_exists()

static void mcrl2::core::term_traits< pbes_system::pbes_expression >::make_exists	(	term_type &	result,
		const variable_sequence_type &	l,
		const term_type &	p
	)

inlinestatic

Make an existential quantification.

Parameters

result	The value `exists l.p`
l	A sequence of variables
p	A term

Definition at line 1267 of file pbes_expression.h.

◆ make_forall()

static void mcrl2::core::term_traits< pbes_system::pbes_expression >::make_forall	(	term_type &	result,
		const variable_sequence_type &	l,
		const term_type &	p
	)

inlinestatic

Make a universal quantification.

Parameters

result	The value `forall l.p`
l	A sequence of variables
p	A term

Definition at line 1238 of file pbes_expression.h.

◆ make_imp()

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

inlinestatic

Make an implication.

Parameters

result	The value `p => q`
p	A term
q	A term

Definition at line 1214 of file pbes_expression.h.

◆ make_not_()

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

inlinestatic

Make a negation.

Parameters

result	The value `!p`
p	A term

Definition at line 1140 of file pbes_expression.h.

◆ make_or_()

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

inlinestatic

Make a disjunction.

Parameters

result	The value `p \|\| q`
p	A term
q	A term

Definition at line 1180 of file pbes_expression.h.

◆ name()

static const string_type & mcrl2::core::term_traits< pbes_system::pbes_expression >::name ( const term_type & t )

inlinestatic

Returns the name of a propositional variable instantiation.

Parameters

t A term

Returns: The name of the propositional variable instantiation

Definition at line 1412 of file pbes_expression.h.

◆ not_()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::not_ ( const term_type & p )

inlinestatic

Make a negation.

Parameters

p A term

Returns: The value !p

Definition at line 1131 of file pbes_expression.h.

◆ not_arg()

static const term_type & mcrl2::core::term_traits< pbes_system::pbes_expression >::not_arg ( const term_type & t )

inlinestatic

Returns the argument of a term of type not.

Parameters

t A term

Definition at line 1388 of file pbes_expression.h.

◆ or_()

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

inlinestatic

Make a disjunction.

Parameters

p	A term
q	A term

Returns: The value p || q

Definition at line 1170 of file pbes_expression.h.

◆ param()

static const data_term_sequence_type & mcrl2::core::term_traits< pbes_system::pbes_expression >::param ( const term_type & t )

inlinestatic

Returns the parameter list of a propositional variable instantiation.

Parameters

t A term

Returns: The parameter list of the propositional variable instantiation

Definition at line 1422 of file pbes_expression.h.

◆ pp()

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

inlinestatic

Pretty print function.

Parameters

t A term

Returns: Returns a pretty print representation of the term

Definition at line 1450 of file pbes_expression.h.

◆ right()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::right ( const term_type & t )

inlinestatic

Returns the right argument of a term of type and, or or imp.

Parameters

t A term

Returns: The right argument of the term. Also works for data terms

Definition at line 1380 of file pbes_expression.h.

◆ true_()

static term_type mcrl2::core::term_traits< pbes_system::pbes_expression >::true_ ( )

inlinestatic

Make the value true.

Returns: The value true

Definition at line 1114 of file pbes_expression.h.

◆ var()

static const variable_sequence_type & mcrl2::core::term_traits< pbes_system::pbes_expression >::var ( const term_type & t )

inlinestatic

Returns the quantifier variables of a quantifier expression.

Parameters

t A term

Returns: The requested argument. Doesn't work for data terms

Definition at line 1398 of file pbes_expression.h.

◆ variable2term()

static const term_type & mcrl2::core::term_traits< pbes_system::pbes_expression >::variable2term ( const variable_type & v )

inlinestatic

Conversion from variable to term.

Parameters

v	A variable

Returns: The converted variable

Definition at line 1432 of file pbes_expression.h.

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

pbes/include/mcrl2/pbes/pbes_expression.h

Public Types

Static Public Member Functions

Detailed Description

Member Typedef Documentation

◆ data_term_sequence_type

◆ data_term_type

◆ propositional_variable_decl_type

◆ propositional_variable_type

◆ string_type

◆ term_type

◆ variable_sequence_type

◆ variable_type

Member Function Documentation

◆ and_()

◆ exists()

◆ false_()

◆ forall()

◆ imp()

◆ is_and()

◆ is_data()

◆ is_exists()

◆ is_false()

◆ is_forall()

◆ is_imp()

◆ is_not()

◆ is_or()

◆ is_prop_var()

◆ is_true()

◆ is_variable()

◆ join_and()

◆ join_or()

◆ left()

◆ make_and_()

◆ make_exists()

◆ make_forall()

◆ make_imp()

◆ make_not_()

◆ make_or_()

◆ name()

◆ not_()

◆ not_arg()

◆ or_()

◆ param()

◆ pp()

◆ right()

◆ true_()

◆ var()

◆ variable2term()