mcrl2::pbes_system::pbes_constelm_algorithm::vertex

Include file:

#include "mcrl2/pbes/constelm.h

class mcrl2::pbes_system::pbes_constelm_algorithm::vertex

Represents a vertex of the dependency graph.

Protected attributes

constraint_map mcrl2::pbes_system::pbes_constelm_algorithm::vertex::m_constraints

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

qvar_list mcrl2::pbes_system::pbes_constelm_algorithm::vertex::m_qvars

The list of quantified variables that occur in the constraints.

propositional_variable mcrl2::pbes_system::pbes_constelm_algorithm::vertex::m_variable

The propositional variable that corresponds to the vertex.

bool mcrl2::pbes_system::pbes_constelm_algorithm::vertex::m_visited

Indicates whether this vertex has been visited at least once.

Protected member functions

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.

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

bool is_constant(const data::variable &v) const

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.

Public member functions

std::vector<std::size_t> constant_parameter_indices() const

Returns the indices of the constant parameters of this vertex.

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

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”).

const qvar_list &quantified_variables() const

std::string to_string() const

Returns a string representation of the vertex.

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.

const propositional_variable &variable() const

The propositional variable that corresponds to the vertex.

vertex() = default

Constructor.

vertex(propositional_variable x)

Constructor.

Parameters:

• x A propositional variable declaration