Replace each constant data application c by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times. More...

#include <replace_constants_by_variables.h>

Inheritance diagram for mcrl2::data::detail::replace_constants_by_variables_builder< Builder >:

Public Types
typedef Builder< replace_constants_by_variables_builder< Builder > >	super

Public Member Functions
bool	is_constant (const data::data_expression &x) const

	replace_constants_by_variables_builder (const data::rewriter &r_, data::mutable_indexed_substitution<> &sigma_)

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

Public Attributes
data::set_identifier_generator	id_generator

std::unordered_map< data::data_expression, data::variable >	substitutions

const data::rewriter &	r

data::mutable_indexed_substitution &	sigma

Detailed Description

template<template< class > class Builder>
struct mcrl2::data::detail::replace_constants_by_variables_builder< Builder >

Replace each constant data application c by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.

Definition at line 28 of file replace_constants_by_variables.h.

Member Typedef Documentation

◆ super

template<template< class > class Builder>

typedef Builder<replace_constants_by_variables_builder<Builder> > mcrl2::data::detail::replace_constants_by_variables_builder< Builder >::super

Definition at line 30 of file replace_constants_by_variables.h.

Constructor & Destructor Documentation

◆ replace_constants_by_variables_builder()

template<template< class > class Builder>

mcrl2::data::detail::replace_constants_by_variables_builder< Builder >::replace_constants_by_variables_builder	(	const data::rewriter &	r_,
		data::mutable_indexed_substitution<> &	sigma_
	)