Substitution function for propositional variables. More...

#include <substitutions.h>

Classes
class	assignment
	Wrapper class for internal storage and substitution updates using operator() More...

Public Types
using	map_type = std::map< core::identifier_string, std::pair< pbes_expression, data::variable_list > >

using	iterator = map_type::iterator

using	const_iterator = map_type::const_iterator

using	variable_type = propositional_variable_instantiation
	type used to represent variables

using	expression_type = pbes_expression
	type used to represent expressions

Public Member Functions
pbes_expression	operator() (const variable_type &v) const
	Apply this substitution to a single variable expression.

	propositional_variable_substitution ()=default

	propositional_variable_substitution (const map_type &other)

assignment	operator[] (const propositional_variable &v)
	Update substitution for a single variable.

	propositional_variable_substitution (const propositional_variable &X, const pbes_expression &phi)
	Constructor. Initializes the substitution with the assignment X := phi.

const_iterator	begin () const
	Returns an iterator pointing to the beginning of the sequence of assignments.

const_iterator	end () const
	Returns an iterator pointing past the end of the sequence of assignments.

iterator	begin ()
	Returns an iterator pointing to the beginning of the sequence of assignments.

iterator	end ()
	Returns an iterator pointing past the end of the sequence of assignments.

iterator	find (const variable_type &v)
	Returns an iterator that references the expression associated with v or is equal to m_map.end()

map_type::size_type	erase (const propositional_variable &v)
	Removes the substitution to the propositional variable v.

const_iterator	find (variable_type const &v) const
	Returns an iterator that references the expression associated with v or is equal to m_map.end()

bool	empty () const
	Returns true if the sequence of assignments is empty.

Protected Attributes
map_type	m_map

Detailed Description

Substitution function for propositional variables.

Model of Substitution.

Definition at line 33 of file substitutions.h.

Member Typedef Documentation

◆ const_iterator

using mcrl2::pbes_system::propositional_variable_substitution::const_iterator = map_type::const_iterator

Definition at line 40 of file substitutions.h.

◆ expression_type

using mcrl2::pbes_system::propositional_variable_substitution::expression_type = pbes_expression

type used to represent expressions

Definition at line 50 of file substitutions.h.

◆ iterator

using mcrl2::pbes_system::propositional_variable_substitution::iterator = map_type::iterator

Definition at line 39 of file substitutions.h.

◆ map_type

using mcrl2::pbes_system::propositional_variable_substitution::map_type = std::map<core::identifier_string, std::pair<pbes_expression, data::variable_list> >

Definition at line 37 of file substitutions.h.

◆ variable_type

using mcrl2::pbes_system::propositional_variable_substitution::variable_type = propositional_variable_instantiation

type used to represent variables

Definition at line 47 of file substitutions.h.

Constructor & Destructor Documentation

◆ propositional_variable_substitution() [1/3]

mcrl2::pbes_system::propositional_variable_substitution::propositional_variable_substitution ( )

default

◆ propositional_variable_substitution() [2/3]

mcrl2::pbes_system::propositional_variable_substitution::propositional_variable_substitution ( const map_type & other )

inline

Definition at line 116 of file substitutions.h.

◆ propositional_variable_substitution() [3/3]

mcrl2::pbes_system::propositional_variable_substitution::propositional_variable_substitution	(	const propositional_variable &	X,
		const pbes_expression &	phi
	)

inline

Constructor. Initializes the substitution with the assignment X := phi.

Definition at line 146 of file substitutions.h.

Member Function Documentation

◆ begin() [1/2]

iterator mcrl2::pbes_system::propositional_variable_substitution::begin ( )

inline

Returns an iterator pointing to the beginning of the sequence of assignments.

Definition at line 164 of file substitutions.h.

◆ begin() [2/2]

const_iterator mcrl2::pbes_system::propositional_variable_substitution::begin ( ) const

inline

Returns an iterator pointing to the beginning of the sequence of assignments.

Definition at line 152 of file substitutions.h.

◆ empty()

bool mcrl2::pbes_system::propositional_variable_substitution::empty ( ) const

inline

Returns true if the sequence of assignments is empty.

Definition at line 194 of file substitutions.h.

◆ end() [1/2]

iterator mcrl2::pbes_system::propositional_variable_substitution::end ( )

inline

Returns an iterator pointing past the end of the sequence of assignments.

Definition at line 170 of file substitutions.h.

◆ end() [2/2]

const_iterator mcrl2::pbes_system::propositional_variable_substitution::end ( ) const

inline

Returns an iterator pointing past the end of the sequence of assignments.

Definition at line 158 of file substitutions.h.

◆ erase()

map_type::size_type mcrl2::pbes_system::propositional_variable_substitution::erase ( const propositional_variable & v )

inline

Removes the substitution to the propositional variable v.

Definition at line 182 of file substitutions.h.

◆ find() [1/2]

iterator mcrl2::pbes_system::propositional_variable_substitution::find ( const variable_type & v )

inline

Returns an iterator that references the expression associated with v or is equal to m_map.end()

Definition at line 176 of file substitutions.h.

◆ find() [2/2]

const_iterator mcrl2::pbes_system::propositional_variable_substitution::find ( variable_type const & v ) const

inline

Returns an iterator that references the expression associated with v or is equal to m_map.end()

Definition at line 188 of file substitutions.h.

◆ operator()()

pbes_expression mcrl2::pbes_system::propositional_variable_substitution::operator() ( const variable_type & v ) const

inline

Apply this substitution to a single variable expression.

Parameters

[in] v The variable for which to give the associated expression.

Returns: expression equivalent to s(e), or a reference to such an expression.

Definition at line 55 of file substitutions.h.

◆ operator[]()

assignment mcrl2::pbes_system::propositional_variable_substitution::operator[] ( const propositional_variable & v )

inline

Update substitution for a single variable.

Parameters

[in] v the variable for which to update the value

template< typename E, typename V >
void example(V const& v, E const& e) {
  substitution< E, V > s;         // substitution
 
  std::cout << s(x) << std::endl; // prints x
 
  s[v] = e;
 
  std::cout << s(x) << std::endl; // prints e
}

Returns: expression assignment for variable v, effect

Definition at line 140 of file substitutions.h.

Member Data Documentation

◆ m_map

map_type mcrl2::pbes_system::propositional_variable_substitution::m_map

protected

Definition at line 43 of file substitutions.h.

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

pbes/include/mcrl2/pbes/substitutions.h

Classes

Public Types

Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ expression_type

◆ iterator

◆ map_type

◆ variable_type

Constructor & Destructor Documentation

◆ propositional_variable_substitution() [1/3]

◆ propositional_variable_substitution() [2/3]

◆ propositional_variable_substitution() [3/3]

Member Function Documentation

◆ begin() [1/2]

◆ begin() [2/2]

◆ empty()

◆ end() [1/2]

◆ end() [2/2]

◆ erase()

◆ find() [1/2]

◆ find() [2/2]

◆ operator()()

◆ operator[]()

Member Data Documentation

◆ m_map