mCRL2
Searching...
No Matches
replace_constants_by_variables.h
Go to the documentation of this file.
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
11
12#ifndef MCRL2_DATA_REPLACE_CONSTANTS_BY_VARIABLES_H
13#define MCRL2_DATA_REPLACE_CONSTANTS_BY_VARIABLES_H
14
15#include "mcrl2/data/rewriter.h"
16#include "mcrl2/data/builder.h"
17
18namespace mcrl2 {
19
20namespace data {
21
22namespace detail {
23
27template <template <class> class Builder>
28struct replace_constants_by_variables_builder: public Builder<replace_constants_by_variables_builder<Builder>>
29{
30 typedef Builder<replace_constants_by_variables_builder<Builder>> super;
31 using super::apply;
32 using super::update;
33
35 std::unordered_map<data::data_expression, data::variable> substitutions;
38
40 {
41 return data::find_free_variables(x).empty();
42 }
43
45 : r(r_), sigma(sigma_)
46 {}
47
48 template <class T>
49 void apply(T& result, const data::application& x)
50 {
51 auto i = substitutions.find(x);
52 if (i != substitutions.end())
53 {
54 result = i->second;
55 }
56 else if (is_constant(x))
57 {
58 data::variable v(id_generator("@rewr_var"), x.sort());
59 substitutions[x] = v;
60 sigma[v] = r(x, sigma);
61 result = v;
62 }
63 else
64 {
65 super::apply(result, x);
66 }
67 }
68};
69
70} // namespace detail
71
72} // namespace data
73
74} // namespace mcrl2
75
76#endif // MCRL2_DATA_REPLACE_CONSTANTS_BY_VARIABLES_H
An application of a data expression to a number of arguments.
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
Rewriter that operates on data expressions.
Definition rewriter.h:81
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A data variable
Definition variable.h:28