mcrl2::data::enumerate_quantifiers_rewriter Struct Reference

#include <enumerate_quantifiers_rewriter.h>

Public Types
using	variable_type = data::variable

Public Member Functions
	enumerate_quantifiers_rewriter (const data::rewriter &R, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts=true)
template<IsSubstitution Substitution>
void	operator() (data_expression &result, const data_expression &x, Substitution &sigma) const
template<IsSubstitution Substitution>
data_expression	operator() (const data_expression &x, Substitution &sigma) const

Protected Attributes
const data::rewriter &	m_rewriter
	A data rewriter.
const data::data_specification &	m_dataspec
	A data specification.
bool	m_enumerate_infinite_sorts
	If true, quantifier variables of infinite sort are enumerated.
data::enumerator_identifier_generator &	m_id_generator

Detailed Description

Definition at line 232 of file enumerate_quantifiers_rewriter.h.

Member Typedef Documentation

variable_type

using mcrl2::data::enumerate_quantifiers_rewriter::variable_type = data::variable

Definition at line 247 of file enumerate_quantifiers_rewriter.h.

Constructor & Destructor Documentation

enumerate_quantifiers_rewriter()

mcrl2::data::enumerate_quantifiers_rewriter::enumerate_quantifiers_rewriter ( const data::rewriter &  R, const data::data_specification &  dataspec, data::enumerator_identifier_generator &  id_generator, bool  enumerate_infinite_sorts = true  )

inline

Definition at line 249 of file enumerate_quantifiers_rewriter.h.

Member Function Documentation

operator()() [1/2]

template<IsSubstitution Substitution>

data_expression mcrl2::data::enumerate_quantifiers_rewriter::operator() ( const data_expression &  x, Substitution &  sigma  ) const

inline

Definition at line 266 of file enumerate_quantifiers_rewriter.h.

operator()() [2/2]

template<IsSubstitution Substitution>

void mcrl2::data::enumerate_quantifiers_rewriter::operator() ( data_expression &  result, const data_expression &  x, Substitution &  sigma  ) const

inline

Definition at line 260 of file enumerate_quantifiers_rewriter.h.

Member Data Documentation

m_dataspec

const data::data_specification& mcrl2::data::enumerate_quantifiers_rewriter::m_dataspec

protected

A data specification.

Definition at line 239 of file enumerate_quantifiers_rewriter.h.

m_enumerate_infinite_sorts

bool mcrl2::data::enumerate_quantifiers_rewriter::m_enumerate_infinite_sorts

protected

If true, quantifier variables of infinite sort are enumerated.

Definition at line 242 of file enumerate_quantifiers_rewriter.h.

m_id_generator

data::enumerator_identifier_generator& mcrl2::data::enumerate_quantifiers_rewriter::m_id_generator

protected

Definition at line 244 of file enumerate_quantifiers_rewriter.h.

m_rewriter

const data::rewriter& mcrl2::data::enumerate_quantifiers_rewriter::m_rewriter

protected

A data rewriter.

Definition at line 236 of file enumerate_quantifiers_rewriter.h.

---

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

• data/include/mcrl2/data/rewriters/enumerate_quantifiers_rewriter.h