#include <enumerate_quantifiers_rewriter.h>

Inheritance diagram for mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >:

Public Types
using	super = simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >

using	self = enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >

using	enumerator_element = data::enumerator_list_element< pbes_expression >

Public Types inherited from mcrl2::pbes_system::detail::simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >
using	super = add_data_rewriter< pbes_system::detail::simplify_builder, Derived, DataRewriter, MutableSubstitution >

using	substitution_administration_type = data::detail::substitution_updater_with_an_identifier_generator< MutableSubstitution, data::enumerator_identifier_generator >

Public Types inherited from mcrl2::pbes_system::detail::add_data_rewriter< pbes_system::detail::simplify_builder, Derived, DataRewriter, MutableSubstitution >
using	super = pbes_system::detail::simplify_builder< Derived >

Public Member Functions
	enumerate_quantifiers_builder (const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, enumerate_quantifiers_mode enum_mode=enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter)
	Constructor.

Derived &	derived ()

atermpp::vector< data::data_expression >	undo_substitution (const data::variable_list &variables)

void	redo_substitution (const data::variable_list &v, const atermpp::vector< data::data_expression > &undo)

void	enumerate_forall (pbes_expression &result, const data::variable_list &v, const pbes_expression &phi)

void	enumerate_exists (pbes_expression &result, const data::variable_list &v, const pbes_expression &phi)

template<class T >
void	apply (T &result, const forall &x)

template<class T >
void	apply (T &result, const exists &x)

template<atermpp::IsATerm T>
void	apply (T &result, const data::data_expression &x)

pbes_expression	operator() (const pbes_expression &x, MutableSubstitution &)

void	operator() (pbes_expression &result, const pbes_expression &x, MutableSubstitution &)

template<class T >
void	apply (T &result, const propositional_variable_instantiation &x)

template<class T >
void	apply (T &result, const forall &x)

template<class T >
void	apply (T &result, const exists &x)

Public Member Functions inherited from mcrl2::pbes_system::detail::simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >
	simplify_data_rewriter_builder (const DataRewriter &R, MutableSubstitution &sigma)

	simplify_data_rewriter_builder (const DataRewriter &R, MutableSubstitution &sigma, const PbesSubstitution &sigma_pbes)

MutableSubstitution &	substitution ()

template<class T , typename SubstitutionType >
void	apply_substitution (T &result, const propositional_variable_instantiation &x, const SubstitutionType &sigma)

template<class T >
void	apply_substitution (T &, const propositional_variable_instantiation &, const no_substitution &)
	Overload to have a trivial function in case the substitution is no_substitution.

template<class T >
void	apply (T &result, const propositional_variable_instantiation &x)

template<class T >
void	apply (T &result, const forall &x)

template<class T >
void	apply (T &result, const exists &x)

Public Member Functions inherited from mcrl2::pbes_system::detail::add_data_rewriter< pbes_system::detail::simplify_builder, Derived, DataRewriter, MutableSubstitution >
	add_data_rewriter (const DataRewriter &R_, MutableSubstitution &sigma_)

void	apply (T &result, const data::data_expression &x)

void	apply (T &result, const propositional_variable_instantiation &x)

Public Attributes
const data::data_specification &	m_dataspec

enumerate_quantifiers_mode	m_enum_mode
	If false, only quantifier variables over finite sorts are enumerated.

data::enumerator_identifier_generator &	m_id_generator
	identifier generator

data::enumerator_algorithm< self >	E
	The enumerator.

Public Attributes inherited from mcrl2::pbes_system::detail::simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >
substitution_administration_type	substitution_administration

const PbesSubstitution &	m_sigma_pbes

Public Attributes inherited from mcrl2::pbes_system::detail::add_data_rewriter< pbes_system::detail::simplify_builder, Derived, DataRewriter, MutableSubstitution >
const DataRewriter &	R

MutableSubstitution &	sigma

Detailed Description

template<typename Derived, typename DataRewriter, typename MutableSubstitution, typename PbesSubstitution>
struct mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >

Parameters

MutableSubstitution This must be a MapSubstitution.

Definition at line 33 of file enumerate_quantifiers_rewriter.h.

Member Typedef Documentation

◆ enumerator_element

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

using mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::enumerator_element = data::enumerator_list_element<pbes_expression>

Definition at line 37 of file enumerate_quantifiers_rewriter.h.

◆ self

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

using mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::self = enumerate_quantifiers_builder<Derived, DataRewriter, MutableSubstitution, PbesSubstitution>

Definition at line 36 of file enumerate_quantifiers_rewriter.h.

◆ super

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

using mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::super = simplify_data_rewriter_builder<Derived, DataRewriter, MutableSubstitution, PbesSubstitution>

Definition at line 35 of file enumerate_quantifiers_rewriter.h.

Constructor & Destructor Documentation

◆ enumerate_quantifiers_builder()

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::enumerate_quantifiers_builder	(	const DataRewriter &	R,
		MutableSubstitution &	sigma,
		const PbesSubstitution &	sigma_pbes,
		const data::data_specification &	dataspec,
		data::enumerator_identifier_generator &	id_generator,
		enumerate_quantifiers_mode	enum_mode = `enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter`
	)

inline

Constructor.

Parameters

R	A data rewriter.
sigma	A mutable substitution.
sigma_pbes	A substitution for pbes variables.
dataspec	A data specification.
id_generator	A generator to generate fresh variable names.
enumerate_infinite_sorts	If true, quantifier variables of infinite sort are enumerated as well.

Definition at line 66 of file enumerate_quantifiers_rewriter.h.

Member Function Documentation

◆ apply() [1/6]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

template<atermpp::IsATerm T>

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::apply	(	T &	result,
		const data::data_expression &	x
	)

inline

Definition at line 244 of file enumerate_quantifiers_rewriter.h.

◆ apply() [2/6]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

template<class T >

void mcrl2::pbes_system::detail::simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::apply	(	T &	result,
		const exists &	x
	)

inline

Definition at line 257 of file simplify_rewriter.h.

◆ apply() [3/6]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

template<class T >

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::apply	(	T &	result,
		const exists &	x
	)

inline

Definition at line 198 of file enumerate_quantifiers_rewriter.h.

◆ apply() [4/6]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

template<class T >

void mcrl2::pbes_system::detail::simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::apply	(	T &	result,
		const forall &	x
	)

inline

Definition at line 248 of file simplify_rewriter.h.

◆ apply() [5/6]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

template<class T >

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::apply	(	T &	result,
		const forall &	x
	)

inline

Definition at line 152 of file enumerate_quantifiers_rewriter.h.

◆ apply() [6/6]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

template<class T >

void mcrl2::pbes_system::detail::simplify_data_rewriter_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::apply	(	T &	result,
		const propositional_variable_instantiation &	x
	)

inline

Definition at line 241 of file simplify_rewriter.h.

◆ derived()

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

Derived & mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::derived ( )

inline

Definition at line 83 of file enumerate_quantifiers_rewriter.h.

◆ enumerate_exists()

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::enumerate_exists	(	pbes_expression &	result,
		const data::variable_list &	v,
		const pbes_expression &	phi
	)

inline

Definition at line 131 of file enumerate_quantifiers_rewriter.h.

◆ enumerate_forall()

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::enumerate_forall	(	pbes_expression &	result,
		const data::variable_list &	v,
		const pbes_expression &	phi
	)

inline

Definition at line 111 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [1/2]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

pbes_expression mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::operator()	(	const pbes_expression &	x,
		MutableSubstitution &
	)

inline

Definition at line 260 of file enumerate_quantifiers_rewriter.h.

◆ operator()() [2/2]

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::operator()	(	pbes_expression &	result,
		const pbes_expression &	x,
		MutableSubstitution &
	)

inline

Definition at line 269 of file enumerate_quantifiers_rewriter.h.

◆ redo_substitution()

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

void mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::redo_substitution	(	const data::variable_list &	v,
		const atermpp::vector< data::data_expression > &	undo
	)

inline

Definition at line 99 of file enumerate_quantifiers_rewriter.h.

◆ undo_substitution()

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

atermpp::vector< data::data_expression > mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::undo_substitution ( const data::variable_list & variables )

inline

Definition at line 88 of file enumerate_quantifiers_rewriter.h.

Member Data Documentation

◆ E

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

data::enumerator_algorithm<self> mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::E

The enumerator.

Definition at line 57 of file enumerate_quantifiers_rewriter.h.

◆ m_dataspec

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

const data::data_specification& mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::m_dataspec

Definition at line 48 of file enumerate_quantifiers_rewriter.h.

◆ m_enum_mode

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

enumerate_quantifiers_mode mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::m_enum_mode

If false, only quantifier variables over finite sorts are enumerated.

Definition at line 51 of file enumerate_quantifiers_rewriter.h.

◆ m_id_generator

template<typename Derived , typename DataRewriter , typename MutableSubstitution , typename PbesSubstitution >

data::enumerator_identifier_generator& mcrl2::pbes_system::detail::enumerate_quantifiers_builder< Derived, DataRewriter, MutableSubstitution, PbesSubstitution >::m_id_generator

identifier generator

Definition at line 54 of file enumerate_quantifiers_rewriter.h.

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

pbes/include/mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ enumerator_element

◆ self

◆ super

Constructor & Destructor Documentation

◆ enumerate_quantifiers_builder()

Member Function Documentation

◆ apply() [1/6]

◆ apply() [2/6]

◆ apply() [3/6]

◆ apply() [4/6]

◆ apply() [5/6]

◆ apply() [6/6]

◆ derived()

◆ enumerate_exists()

◆ enumerate_forall()

◆ operator()() [1/2]

◆ operator()() [2/2]

◆ redo_substitution()

◆ undo_substitution()

Member Data Documentation

◆ E

◆ m_dataspec

◆ m_enum_mode

◆ m_id_generator