Represents a vertex of the dependency graph. More...

#include <constelm.h>

Public Member Functions
	vertex ()=default
	Constructor.

	vertex (propositional_variable x)
	Constructor.

const propositional_variable &	variable () const
	The propositional variable that corresponds to the vertex.

const qvar_list &	quantified_variables () const

const constraint_map &	constraints () const
	Maps data variables to data expressions. If the right hand side is a data variable, it means that it represents NaC ("not a constant").

std::vector< std::size_t >	constant_parameter_indices () const
	Returns the indices of the constant parameters of this vertex.

std::string	to_string () const
	Returns a string representation of the vertex.

bool	update (const qvar_list &qvars, const data::data_expression_list &e, const constraint_map &e_constraints, const DataRewriter &datar)
	Assign new values to the parameters of this vertex, and update the constraints accordingly. The new values have a number of constraints.

Protected Member Functions
bool	is_constant (const data::variable &v) const
	Returns true if the parameter v has been assigned a constant expression.

bool	bound_in_quantifiers (const qvar_list &qvars, const data::data_expression &e)
	Returns true iff all free variables in e are bound in qvars.

void	fix_constraints (std::vector< data::data_expression > deleted_constraints)
	Weaken the constraints so they satisfy.

Protected Attributes
propositional_variable	m_variable
	The propositional variable that corresponds to the vertex.

qvar_list	m_qvars
	The list of quantified variables that occur in the constraints.

constraint_map	m_constraints
	Maps data variables to data expressions. If a parameter is not.

bool	m_visited = false
	Indicates whether this vertex has been visited at least once.

Detailed Description

template<typename DataRewriter, typename PresRewriter>
class mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex

Represents a vertex of the dependency graph.

Definition at line 528 of file constelm.h.

Constructor & Destructor Documentation

◆ vertex() [1/2]

template<typename DataRewriter , typename PresRewriter >

mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::vertex ( )

default

Constructor.

◆ vertex() [2/2]

template<typename DataRewriter , typename PresRewriter >

mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::vertex ( propositional_variable x )

inline

Constructor.

Parameters

x	A propositional variable declaration

Definition at line 606 of file constelm.h.

Member Function Documentation

◆ bound_in_quantifiers()

template<typename DataRewriter , typename PresRewriter >

bool mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::bound_in_quantifiers	(	const qvar_list &	qvars,
		const data::data_expression &	e
	)

inlineprotected

Returns true iff all free variables in e are bound in qvars.

Definition at line 554 of file constelm.h.

◆ constant_parameter_indices()

template<typename DataRewriter , typename PresRewriter >

std::vector< std::size_t > mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::constant_parameter_indices ( ) const

inline

Returns the indices of the constant parameters of this vertex.

Returns: The indices of the constant parameters of this vertex.

Definition at line 630 of file constelm.h.

◆ constraints()

template<typename DataRewriter , typename PresRewriter >

const constraint_map & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::constraints ( ) const

inline

Maps data variables to data expressions. If the right hand side is a data variable, it means that it represents NaC ("not a constant").

Definition at line 623 of file constelm.h.

◆ fix_constraints()

template<typename DataRewriter , typename PresRewriter >

void mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::fix_constraints ( std::vector< data::data_expression > deleted_constraints )

inlineprotected

Weaken the constraints so they satisfy.

vars(m_constraints[d]) subset vars(m_qvars); and
vars(deleted_constraints) intersection vars(m_qvars) = {}

Definition at line 566 of file constelm.h.

◆ is_constant()

template<typename DataRewriter , typename PresRewriter >

bool mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::is_constant ( const data::variable & v ) const

inlineprotected

Returns true if the parameter v has been assigned a constant expression.

Parameters

v	A parameter of this->variable()

Returns: True if the data parameter v has been assigned a constant expression.

Definition at line 547 of file constelm.h.

◆ quantified_variables()

template<typename DataRewriter , typename PresRewriter >

const qvar_list & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::quantified_variables ( ) const

inline

Definition at line 616 of file constelm.h.

◆ to_string()

template<typename DataRewriter , typename PresRewriter >

std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::to_string ( ) const

inline

Returns a string representation of the vertex.

Returns: A string representation of the vertex.

Definition at line 647 of file constelm.h.

◆ update()

template<typename DataRewriter , typename PresRewriter >

bool mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::update	(	const qvar_list &	qvars,
		const data::data_expression_list &	e,
		const constraint_map &	e_constraints,
		const DataRewriter &	datar
	)

inline

Assign new values to the parameters of this vertex, and update the constraints accordingly. The new values have a number of constraints.

Definition at line 664 of file constelm.h.

◆ variable()

template<typename DataRewriter , typename PresRewriter >

const propositional_variable & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::variable ( ) const

inline

The propositional variable that corresponds to the vertex.

Definition at line 611 of file constelm.h.

Member Data Documentation

◆ m_constraints

template<typename DataRewriter , typename PresRewriter >

constraint_map mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::m_constraints

protected

Maps data variables to data expressions. If a parameter is not.

Definition at line 539 of file constelm.h.

◆ m_qvars

template<typename DataRewriter , typename PresRewriter >

qvar_list mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::m_qvars

protected

The list of quantified variables that occur in the constraints.

Definition at line 535 of file constelm.h.

◆ m_variable

template<typename DataRewriter , typename PresRewriter >

propositional_variable mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::m_variable

protected

The propositional variable that corresponds to the vertex.

Definition at line 532 of file constelm.h.

◆ m_visited

template<typename DataRewriter , typename PresRewriter >

bool mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex::m_visited = false

protected

Indicates whether this vertex has been visited at least once.

Definition at line 542 of file constelm.h.

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

pres/include/mcrl2/pres/constelm.h

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ vertex() [1/2]

◆ vertex() [2/2]

Member Function Documentation

◆ bound_in_quantifiers()

◆ constant_parameter_indices()

◆ constraints()

◆ fix_constraints()

◆ is_constant()

◆ quantified_variables()

◆ to_string()

◆ update()

◆ variable()

Member Data Documentation

◆ m_constraints

◆ m_qvars

◆ m_variable

◆ m_visited