mcrl2::data::enumerator_list_element

Include file:

#include "mcrl2/data/enumerator.h

class mcrl2::data::enumerator_list_element

The default element for the todo list of the enumerator.

Public types

type mcrl2::data::enumerator_list_element::expression_type

typedef for Expression

Protected attributes

Expression mcrl2::data::enumerator_list_element::phi

data::variable_list mcrl2::data::enumerator_list_element::v

Public member functions

enumerator_list_element() = default

Default constructor.

enumerator_list_element(data::variable_list v_, const Expression &phi_)

Constructs the element (v, phi)

enumerator_list_element(data::variable_list v_, const Expression &phi_, const enumerator_list_element&)

Constructs the element (v, phi)

enumerator_list_element(data::variable_list v_, const Expression &phi_, const enumerator_list_element&, const data::variable&, const data::data_expression&)

Constructs the element (v, phi)

Expression &expression()

const Expression &expression() const

void invalidate()

Invalidates the element, by giving phi an undefined value.

bool is_solution() const

bool is_valid() const

Returns true if the element is valid. If it becomes false, this is used to signal that the enumeration has been aborted.

void mark(atermpp::term_mark_stack &todo) const

The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.

void set(const data::variable_list &v_, const Expression &phi_)

Set the variables and the condition explicitly.

Parameters:

• v_ The variable list.
• phi_ The condition.

void set(const data::variable_list &v_, const Expression &phi_, const enumerator_list_element&)

Set the variables and the condition explicitly.

Parameters:

• v_ The variable list.
• phi_ The condition.

Other arguments than the first two are ignored.

void set(const data::variable_list &v_, const Expression &phi_, const enumerator_list_element&, const data::variable&, const data::data_expression&)

Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

Parameters:

• v_ The variable list.
• phi_ The condition.

Other arguments than the first two are ignored.

const data::variable_list &variables() const