mCRL2
Loading...
Searching...
No Matches
rewriter.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_DATA_REWRITER_H
13#define MCRL2_DATA_REWRITER_H
14
18
19namespace mcrl2
20{
21
22namespace data
23{
24
27template < typename Term >
29{
30 public:
33
34 protected:
36 std::shared_ptr<detail::Rewriter> m_rewriter;
37
38 public:
39
41 typedef Term term_type;
42
45
46 protected:
47
50 explicit basic_rewriter(const std::shared_ptr<detail::Rewriter>& r) :
51 m_rewriter(r)
52 {}
53
55 basic_rewriter(const basic_rewriter& other)=default;
56
58 basic_rewriter& operator=(const basic_rewriter& other)=default;
59
63 explicit basic_rewriter(const data_specification& d, const strategy s = jitty) :
64 m_rewriter(detail::createRewriter(d, used_data_equation_selector(d), static_cast< rewrite_strategy >(s)))
65 { }
66
68 basic_rewriter(const data_specification& d, const used_data_equation_selector& equation_selector, const strategy s = jitty) :
69 m_rewriter(detail::createRewriter(d, equation_selector, static_cast< rewrite_strategy >(s)))
70 {}
71
72};
73
75//
79
80class rewriter: public basic_rewriter<data_expression>
81{
82 protected:
83 // cache the empty substitution, since it is expensive to construct
85 {
86#ifdef MCRL2_ENABLE_MULTITHREADING
88 thread_local substitution_type result;
89#else
91 static substitution_type result;
92#endif
93 return result;
94 }
95
98 {
99 static data_specification specification;
100 return specification;
101 }
102
105 explicit rewriter(const std::shared_ptr<detail::Rewriter>& r) :
107 {}
108
109#ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
110 mutable std::size_t rewrite_calls = 0;
111#endif
112
113 public:
115
118 rewriter(const rewriter& r) = default;
119
125 { }
126
131 template < typename EquationSelector >
132 rewriter(const data_specification& d, const EquationSelector& selector, const strategy s = jitty) :
133 basic_rewriter<data_expression>(d, selector, s)
134 {
135 }
136
141 {
142 return rewriter(m_rewriter->clone());
143 }
144
151 {
152 m_rewriter->thread_initialise();
153 }
154
159 {
160 return (*this)(d, empty_substitution());
161 }
162
168 template <typename SubstitutionFunction>
169 data_expression operator()(const data_expression& d, const SubstitutionFunction& sigma) const
170 {
171 substitution_type sigma_with_iterator;
172 std::set<variable> free_variables = data::find_free_variables(d);
173 for(const variable& free_variable: free_variables)
174 {
175 sigma_with_iterator[free_variable] = sigma(free_variable);
176 }
177 return (*this)(d, sigma_with_iterator);
178 }
179
185 template <typename SubstitutionFunction>
186 void operator()(data_expression& result, const data_expression& d, const SubstitutionFunction& sigma) const
187 {
188 substitution_type sigma_with_iterator;
189 std::set<variable> free_variables = data::find_free_variables(d);
190 for(const variable& free_variable: free_variables)
191 {
192 sigma_with_iterator[free_variable] = sigma(free_variable);
193 }
194 (*this)(result, d, sigma_with_iterator);
195 }
196
202 // Added bij JFG, to avoid the use of find_free_variables in the function operator() with
203 // an arbitrary SubstitionFunction, as this is prohibitively costly.
205 {
206 data_expression result;
207 (*this)(result, d, sigma);
208 return result;
209 }
210
216 // Added bij JFG, to avoid the use of find_free_variables in the function operator() with
217 // an arbitrary SubstitionFunction, as this is prohibitively costly.
219 {
220#ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
221 rewrite_calls++;
222#endif
223#ifdef MCRL2_PRINT_REWRITE_STEPS
224 mCRL2log(log::debug) << "REWRITE " << d << "\n";
225#endif
226 m_rewriter->rewrite(result,d,sigma);
227#ifdef MCRL2_PRINT_REWRITE_STEPS
228 mCRL2log(log::debug) << " ------------> " << result << std::endl;
229#endif
230 }
231
233 {
234#ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
235 std::cout << "number of data rewrite calls: " << rewrite_calls << std::endl;
236#endif
237 }
238};
239
240} // namespace data
241
242} // namespace mcrl2
243
244#endif // MCRL2_DATA_REWRITER_H
Rewriter class for the mCRL2 Library. It only works for terms of type data_expression and data_expres...
Definition rewriter.h:29
basic_rewriter(const data_specification &d, const strategy s=jitty)
Constructor.
Definition rewriter.h:63
basic_rewriter(const data_specification &d, const used_data_equation_selector &equation_selector, const strategy s=jitty)
Constructor.
Definition rewriter.h:68
Term term_type
The type for expressions manipulated by the rewriter.
Definition rewriter.h:41
basic_rewriter(const std::shared_ptr< detail::Rewriter > &r)
Constructor.
Definition rewriter.h:50
basic_rewriter(const basic_rewriter &other)=default
Copy Constructor.
rewrite_strategy strategy
The rewrite strategies of the rewriter.
Definition rewriter.h:44
basic_rewriter & operator=(const basic_rewriter &other)=default
Assignment operator.
std::shared_ptr< detail::Rewriter > m_rewriter
The wrapped Rewriter.
Definition rewriter.h:36
data::mutable_indexed_substitution substitution_type
The type for the substitution that is used internally.
Definition rewriter.h:32
Rewriter that operates on data expressions.
Definition rewriter.h:81
rewriter(const std::shared_ptr< detail::Rewriter > &r)
Constructor for internal use.
Definition rewriter.h:105
static const data_specification & default_specification()
Default specification used if no specification is specified at construction.
Definition rewriter.h:97
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.
Definition rewriter.h:218
void thread_initialise()
Initialises this rewriter with thread dependent information.
Definition rewriter.h:150
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.
Definition rewriter.h:204
rewriter(const data_specification &d, const EquationSelector &selector, const strategy s=jitty)
Constructor.
Definition rewriter.h:132
static substitution_type & empty_substitution()
Definition rewriter.h:84
rewriter clone()
Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared...
Definition rewriter.h:140
rewriter(const rewriter &r)=default
Constructor.
rewriter(const data_specification &d=rewriter::default_specification(), const strategy s=jitty)
Constructor.
Definition rewriter.h:123
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.
Definition rewriter.h:186
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.
Definition rewriter.h:169
basic_rewriter< data_expression >::substitution_type substitution_type
Definition rewriter.h:114
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
Definition rewriter.h:158
Component for selecting a subset of equations that are actually used in an encompassing specification...
Definition selection.h:37
\brief A data variable
Definition variable.h:28
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.
Definition logger.h:391
variable_list free_variables(const data_expression &x)
Definition data.cpp:195
rewrite_strategy
The strategy of the rewriter.
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
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...
Definition indexed_set.h:72