mCRL2
Loading...
Searching...
No Matches
mutable_map_substitution.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp, 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_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
13#define MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
14
17
18namespace mcrl2 {
19
20namespace data {
21
32template <typename AssociativeContainer = std::map<variable,data_expression> >
34{
35protected:
36 AssociativeContainer m_map;
37
38public:
39 typedef typename AssociativeContainer::key_type variable_type;
40 typedef typename AssociativeContainer::mapped_type expression_type;
41 typedef typename AssociativeContainer::const_iterator const_iterator;
42 typedef typename AssociativeContainer::iterator iterator;
45
48 {
49 typename AssociativeContainer::key_type m_variable;
50 AssociativeContainer& m_map;
51
56 assignment(typename AssociativeContainer::key_type v, AssociativeContainer& m) :
57 m_variable(v), m_map(m)
58 { }
59
60 template <typename AssignableToExpression>
61 assignment& operator=(AssignableToExpression const& e)
62 {
63 mCRL2log(log::trace) << "Setting " << m_variable << " := " << e << std::endl;
64 if (e != m_variable)
65 {
66 m_map[m_variable] = e;
67 }
68 else
69 {
70 m_map.erase(m_variable);
71 }
72 return *this;
73 }
74 };
75
77
78 explicit mutable_map_substitution(const AssociativeContainer& m)
79 : m_map(m)
80 {}
81
82 template <typename VariableContainer, typename ExpressionContainer>
83 mutable_map_substitution(VariableContainer const& variables, ExpressionContainer const& expressions)
84 {
85 assert(variables.size() == expressions.size());
86 auto j = expressions.begin();
87 for (auto i = variables.begin(); i != variables.end(); ++i, ++j)
88 {
89 m_map[*i] = *j;
90 }
91 }
92
94 {
95 auto i = m_map.find(v);
96 if (i == m_map.end())
97 {
98 return v;
99 }
100 else
101 {
102 return i->second;
103 }
104 }
105
107 {
108 return assignment(v, this->m_map);
109 }
110
113 void clear()
114 {
115 m_map.clear();
116 }
117
118 template <typename Substitution>
119 bool operator==(const Substitution&) const
120 {
121 return false;
122 }
123
127 {
128 return m_map.begin();
129 }
130
134 {
135 return m_map.end();
136 }
137
141 {
142 return this->m_map.begin();
143 }
144
148 {
149 return this->m_map.end();
150 }
151
153 bool empty() const
154 {
155 return m_map.empty();
156 }
157
158 std::string to_string() const
159 {
160 std::stringstream result;
161 result << "[";
162 for (auto i = begin(); i != end(); ++i)
163 {
164 result << (i == begin() ? "" : "; ") << i->first << ":" << i->first.sort() << " := " << i->second;
165 }
166 result << "]";
167 return result.str();
168 }
169
172 {
173 return this->m_map.find(v);
174 }
175
178 {
179 return m_map.find(v);
180 }
181};
182
184template <typename VariableContainer, typename ExpressionContainer, typename MapContainer>
185mutable_map_substitution<MapContainer>
186make_mutable_map_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
187{
189}
190
191template <typename VariableContainer, typename ExpressionContainer>
192mutable_map_substitution<std::map<typename VariableContainer::value_type, typename ExpressionContainer::value_type> >
193make_mutable_map_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
194{
196}
197
198template <typename AssociativeContainer>
200{
201 return out << sigma.to_string();
202}
203
204std::set<data::variable> substitution_variables(const mutable_map_substitution<>& sigma);
205
206template <typename AssociativeContainer>
208{
209 for (auto i = sigma.begin(); i != sigma.end(); ++i)
210 {
211 if (!is_simple_substitution(i->first, i->second))
212 {
213 return false;
214 }
215 }
216 return true;
217}
218
219} // namespace data
220
221} // namespace mcrl2
222
223#endif // MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
AssociativeContainer::key_type variable_type
bool operator==(const Substitution &) const
AssociativeContainer::const_iterator const_iterator
const_iterator find(variable_type const &v) const
Returns an iterator that references the expression associated with v or is equal to m_map....
void clear()
Resets the substitution by letting every variable yield itself. Cf. clear() of a map.
const_iterator begin() const
Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become prot...
mutable_map_substitution(const AssociativeContainer &m)
mutable_map_substitution(VariableContainer const &variables, ExpressionContainer const &expressions)
expression_type operator()(const variable_type &v) const
AssociativeContainer::mapped_type expression_type
const_iterator end() const
Returns an iterator pointing past the end of the sequence of assignments TODO: should become protecte...
bool empty() const
Returns true if the substitution is empty.
iterator end()
Returns an iterator pointing past the end of the sequence of assignments TODO: should become protecte...
assignment operator[](variable_type const &v)
iterator find(variable_type const &v)
Returns an iterator that references the expression associated with v or is equal to m_map....
iterator begin()
Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become prot...
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::set< data::variable > substitution_variables(const Substitution &)
Returns the variables appearing in the right hand sides of the substitution.
Definition replace.h:161
bool is_simple_substitution(const Substitution &)
Returns true if the substitution sigma satisfies the property that FV(sigma(x)) is included in {x} fo...
mutable_map_substitution< MapContainer > make_mutable_map_substitution(const VariableContainer &vc, const ExpressionContainer &ec)
Utility function for creating a mutable_map_substitution.
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Wrapper class for internal storage and substitution updates using operator()
assignment(typename AssociativeContainer::key_type v, AssociativeContainer &m)
Constructor.
assignment & operator=(AssignableToExpression const &e)
add your file description here.