#include <equality_one_point_substitution.h>

Public Member Functions
void	apply_sigma ()

bool	find_constant_assignments ()

bool	find_assignment ()

void	build_equality_map (const std::map< data::variable, std::set< data::data_expression > > &equalities_, bool check_vars, const data::variable_list &vars=data::variable_list())

	one_point_rule_substitution_algorithm (const std::map< data::variable, std::set< data::data_expression > > &equalities_)

	one_point_rule_substitution_algorithm (const std::map< data::variable, std::set< data::data_expression > > &equalities_, const data::variable_list &quantifier_variables)

data::mutable_map_substitution	run (bool find_all_assignments=true)

std::pair< data::mutable_map_substitution<>, std::vector< data::variable > >	run (const data::variable_list &quantifier_variables, bool find_all_assignments=true)

Public Attributes
std::map< data::variable, std::vector< data::data_expression > >	equalities

data::mutable_map_substitution	sigma

std::set< data::variable >	sigma_lhs_variables

data::set_identifier_generator	id_generator

Detailed Description

Definition at line 24 of file equality_one_point_substitution.h.

Constructor & Destructor Documentation

◆ one_point_rule_substitution_algorithm() [1/2]

mcrl2::data::detail::one_point_rule_substitution_algorithm::one_point_rule_substitution_algorithm ( const std::map< data::variable, std::set< data::data_expression > > & equalities_ )

inline

Definition at line 138 of file equality_one_point_substitution.h.

◆ one_point_rule_substitution_algorithm() [2/2]

mcrl2::data::detail::one_point_rule_substitution_algorithm::one_point_rule_substitution_algorithm	(	const std::map< data::variable, std::set< data::data_expression > > &	equalities_,
		const data::variable_list &	quantifier_variables
	)

inline

Definition at line 143 of file equality_one_point_substitution.h.

Member Function Documentation

◆ apply_sigma()

void mcrl2::data::detail::one_point_rule_substitution_algorithm::apply_sigma ( )

inline

Definition at line 32 of file equality_one_point_substitution.h.

◆ build_equality_map()

void mcrl2::data::detail::one_point_rule_substitution_algorithm::build_equality_map	(	const std::map< data::variable, std::set< data::data_expression > > &	equalities_,
		bool	check_vars,
		const data::variable_list &	vars = `data::variable_list()`
	)

inline

Definition at line 114 of file equality_one_point_substitution.h.

◆ find_assignment()

bool mcrl2::data::detail::one_point_rule_substitution_algorithm::find_assignment ( )

inline

Definition at line 75 of file equality_one_point_substitution.h.

◆ find_constant_assignments()

bool mcrl2::data::detail::one_point_rule_substitution_algorithm::find_constant_assignments ( )

inline

Definition at line 45 of file equality_one_point_substitution.h.

◆ run() [1/2]

data::mutable_map_substitution mcrl2::data::detail::one_point_rule_substitution_algorithm::run ( bool find_all_assignments = true )

inline

Definition at line 148 of file equality_one_point_substitution.h.

◆ run() [2/2]

std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > mcrl2::data::detail::one_point_rule_substitution_algorithm::run	(	const data::variable_list &	quantifier_variables,
		bool	find_all_assignments = `true`
	)