12#ifndef MCRL2_DATA_REWRITER_H
13#define MCRL2_DATA_REWRITER_H
27template <
typename Term >
86#ifdef MCRL2_ENABLE_MULTITHREADING
100 return specification;
105 explicit rewriter(
const std::shared_ptr<detail::Rewriter>& r) :
109#ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
110 mutable std::size_t rewrite_calls = 0;
131 template <
typename EquationSelector >
168 template <
typename SubstitutionFunction>
175 sigma_with_iterator[free_variable] =
sigma(free_variable);
177 return (*
this)(d, sigma_with_iterator);
185 template <
typename SubstitutionFunction>
192 sigma_with_iterator[free_variable] =
sigma(free_variable);
194 (*this)(result, d, sigma_with_iterator);
207 (*this)(result, d,
sigma);
220#ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
223#ifdef MCRL2_PRINT_REWRITE_STEPS
227#ifdef MCRL2_PRINT_REWRITE_STEPS
234#ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
235 std::cout <<
"number of data rewrite calls: " << rewrite_calls << std::endl;
Rewriter class for the mCRL2 Library. It only works for terms of type data_expression and data_expres...
basic_rewriter(const data_specification &d, const strategy s=jitty)
Constructor.
basic_rewriter(const data_specification &d, const used_data_equation_selector &equation_selector, const strategy s=jitty)
Constructor.
Term term_type
The type for expressions manipulated by the rewriter.
basic_rewriter(const std::shared_ptr< detail::Rewriter > &r)
Constructor.
basic_rewriter(const basic_rewriter &other)=default
Copy Constructor.
rewrite_strategy strategy
The rewrite strategies of the rewriter.
basic_rewriter & operator=(const basic_rewriter &other)=default
Assignment operator.
std::shared_ptr< detail::Rewriter > m_rewriter
The wrapped Rewriter.
data::mutable_indexed_substitution substitution_type
The type for the substitution that is used internally.
Generic substitution function.
Rewriter that operates on data expressions.
rewriter(const std::shared_ptr< detail::Rewriter > &r)
Constructor for internal use.
static const data_specification & default_specification()
Default specification used if no specification is specified at construction.
void operator()(data_expression &result, const data_expression &d, substitution_type &sigma) const
Rewrites the data expression d, and on the fly applies a substitution function to data variables.
void thread_initialise()
Initialises this rewriter with thread dependent information.
data_expression operator()(const data_expression &d, substitution_type &sigma) const
Rewrites the data expression d, and on the fly applies a substitution function to data variables.
rewriter(const data_specification &d, const EquationSelector &selector, const strategy s=jitty)
Constructor.
static substitution_type & empty_substitution()
rewriter clone()
Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared...
rewriter(const rewriter &r)=default
Constructor.
rewriter(const data_specification &d=rewriter::default_specification(), const strategy s=jitty)
Constructor.
void operator()(data_expression &result, const data_expression &d, const SubstitutionFunction &sigma) const
Rewrites the data expression d, and on the fly applies a substitution function. to data variables.
data_expression operator()(const data_expression &d, const SubstitutionFunction &sigma) const
Rewrites the data expression d, and on the fly applies a substitution function. to data variables.
basic_rewriter< data_expression >::substitution_type substitution_type
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
Component for selecting a subset of equations that are actually used in an encompassing specification...
Contains term traits for data_expression.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
variable_list free_variables(const data_expression &x)
rewrite_strategy
The strategy of the rewriter.
std::set< data::variable > find_free_variables(const data::data_expression &x)
static constexpr bool GlobalThreadSafe
Enables thread safety for the whole toolset.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...