#include <enumerate_quantifiers_rewriter.h>

Inheritance diagram for mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >:

Public Types
using	super = data_expression_builder< enumerate_quantifiers_builder< DataRewriter, MutableSubstitution > >

using	self = enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >

using	enumerator_element = data::enumerator_list_element< data_expression >

Public Types inherited from mcrl2::data::add_data_expressions< Builder, Derived >
using	super = Builder< Derived >

Public Member Functions
	enumerate_quantifiers_builder (const DataRewriter &R, MutableSubstitution &sigma, const data::data_specification &dataspec, data::enumerator_identifier_generator &id_generator, bool enumerate_infinite_sorts=true)
	Constructor.

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 (data_expression &result, const data::variable_list &v, const data_expression &phi)

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

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

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

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

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

void	operator() (data_expression &result, const data_expression &x, MutableSubstitution &sigma)

Public Member Functions inherited from mcrl2::data::add_data_expressions< Builder, Derived >
template<class T >
void	apply (T &result, const data::variable &x)

template<class T >
void	apply (T &result, const data::function_symbol &x)

template<class T >
void	apply (T &result, const data::application &x)

template<class T >
void	apply (T &result, const data::where_clause &x)

template<class T >
void	apply (T &result, const data::machine_number &x)

template<class T >
void	apply (T &result, const data::untyped_identifier &x)

template<class T >
void	apply (T &result, const data::assignment &x)

template<class T >
void	apply (T &result, const data::untyped_identifier_assignment &x)

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

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

template<class T >
void	apply (T &result, const data::lambda &x)

template<class T >
void	apply (T &result, const data::set_comprehension &x)

template<class T >
void	apply (T &result, const data::bag_comprehension &x)

template<class T >
void	apply (T &result, const data::untyped_set_or_bag_comprehension &x)

template<class T >
void	apply (T &result, const data::data_equation &x)

template<class T >
void	apply (T &result, const data::untyped_data_parameter &x)

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

template<class T >
void	apply (T &result, const data::assignment_expression &x)

template<class T >
void	apply (T &result, const data::abstraction &x)

Public Attributes
const DataRewriter &	m_R

MutableSubstitution &	m_sigma

const data::data_specification &	m_dataspec

bool	m_enumerate_infinite_sorts
	If false, only quantifier variables over finite sort are enumerated.

data::enumerator_algorithm< self >	E
	The enumerator.

Detailed Description

template<typename DataRewriter, IsSubstitution MutableSubstitution>
struct mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >

Definition at line 29 of file enumerate_quantifiers_rewriter.h.

Member Typedef Documentation

◆ enumerator_element

template<typename DataRewriter , IsSubstitution MutableSubstitution>

using mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::enumerator_element = data::enumerator_list_element<data_expression>

Definition at line 33 of file enumerate_quantifiers_rewriter.h.

◆ self

template<typename DataRewriter , IsSubstitution MutableSubstitution>

using mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::self = enumerate_quantifiers_builder<DataRewriter, MutableSubstitution>

Definition at line 32 of file enumerate_quantifiers_rewriter.h.

◆ super

template<typename DataRewriter , IsSubstitution MutableSubstitution>

using mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::super = data_expression_builder<enumerate_quantifiers_builder<DataRewriter, MutableSubstitution> >

Definition at line 31 of file enumerate_quantifiers_rewriter.h.

Constructor & Destructor Documentation

◆ enumerate_quantifiers_builder()

template<typename DataRewriter , IsSubstitution MutableSubstitution>

mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::enumerate_quantifiers_builder	(	const DataRewriter &	R,
		MutableSubstitution &	sigma,
		const data::data_specification &	dataspec,
		data::enumerator_identifier_generator &	id_generator,
		bool	enumerate_infinite_sorts = `true`
	)

inline

Constructor.

Parameters

R	A data rewriter.
sigma	A mutable substitution.
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 57 of file enumerate_quantifiers_rewriter.h.

Member Function Documentation

◆ apply() [1/4]

template<typename DataRewriter , IsSubstitution MutableSubstitution>

template<atermpp::IsATerm T>

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

inline

Definition at line 171 of file enumerate_quantifiers_rewriter.h.

◆ apply() [2/4]

template<typename DataRewriter , IsSubstitution MutableSubstitution>

template<atermpp::IsATerm T>

void mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::apply	(	T &	result,
		const data::lambda &	x
	)

inline

Definition at line 209 of file enumerate_quantifiers_rewriter.h.

◆ apply() [3/4]

template<typename DataRewriter , IsSubstitution MutableSubstitution>

template<atermpp::IsATerm T>

void mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::apply	(	T &	result,
		const data::variable &	x
	)

inline

Definition at line 218 of file enumerate_quantifiers_rewriter.h.

◆ apply() [4/4]

template<typename DataRewriter , IsSubstitution MutableSubstitution>

template<class T >

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

inline

Definition at line 134 of file enumerate_quantifiers_rewriter.h.

◆ enumerate_exists()

template<typename DataRewriter , IsSubstitution MutableSubstitution>

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

inline

Definition at line 113 of file enumerate_quantifiers_rewriter.h.

◆ enumerate_forall()

template<typename DataRewriter , IsSubstitution MutableSubstitution>

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

inline

Definition at line 93 of file enumerate_quantifiers_rewriter.h.

◆ operator()()

template<typename DataRewriter , IsSubstitution MutableSubstitution>

void mcrl2::data::detail::enumerate_quantifiers_builder< DataRewriter, MutableSubstitution >::operator()	(	data_expression &	result,
		const data_expression &	x,
		MutableSubstitution &	sigma
	)

inline

Definition at line 224 of file enumerate_quantifiers_rewriter.h.

◆ redo_substitution()

template<typename DataRewriter , IsSubstitution MutableSubstitution>

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

inline

Definition at line 81 of file enumerate_quantifiers_rewriter.h.

◆ undo_substitution()

template<typename DataRewriter , IsSubstitution MutableSubstitution>

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