Line data Source code
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 : //
9 : /// \file mcrl2/modal_formula/detail/state_formula_name_clash_resolver.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_RESOLVE_NAME_CLASHES_H
13 : #define MCRL2_MODAL_FORMULA_RESOLVE_NAME_CLASHES_H
14 :
15 : #include "mcrl2/modal_formula/builder.h"
16 : #include "mcrl2/utilities/detail/container_utility.h"
17 :
18 : namespace mcrl2::state_formulas {
19 :
20 : namespace detail
21 : {
22 :
23 : template <typename Derived>
24 : class state_variable_name_clash_resolver: public state_formulas::state_formula_builder<Derived>
25 : {
26 : public:
27 : typedef state_formulas::state_formula_builder<Derived> super;
28 :
29 : using super::enter;
30 : using super::leave;
31 : using super::apply;
32 :
33 : typedef std::map<core::identifier_string, std::vector<core::identifier_string> > name_map;
34 :
35 : /// \brief The stack of names.
36 : name_map m_names;
37 :
38 : /// \brief Generator for fresh variable names.
39 : utilities::number_postfix_generator m_generator;
40 :
41 : /// \brief Pops the name of the stack
42 16 : void pop(const core::identifier_string& name)
43 : {
44 16 : m_names[name].pop_back();
45 16 : }
46 :
47 : /// \brief Pushes name on the stack.
48 16 : void push(const core::identifier_string& name)
49 : {
50 16 : std::vector<core::identifier_string>& names = m_names[name];
51 16 : if (names.empty())
52 : {
53 8 : names.push_back(name);
54 : }
55 : else
56 : {
57 8 : names.push_back(m_generator(std::string(name) + "_"));
58 : }
59 16 : }
60 :
61 14 : void enter(const mu& x)
62 : {
63 14 : push(x.name());
64 14 : }
65 :
66 14 : void leave(const mu& x)
67 : {
68 14 : pop(x.name());
69 14 : }
70 :
71 2 : void enter(const nu& x)
72 : {
73 2 : push(x.name());
74 2 : }
75 :
76 2 : void leave(const nu& x)
77 : {
78 2 : pop(x.name());
79 2 : }
80 :
81 : // Rename variable
82 : template <class T>
83 14 : void apply(T& result, const mu& x)
84 : {
85 14 : enter(x);
86 : // N.B. If the two lines below are replace by
87 : // state_formula result = mu(m_names[x.name()].back(), x.assignments(), (*this)(x.operand()));
88 : // a memory error occurs with the clang and intel compilers!
89 14 : core::identifier_string name = m_names[x.name()].back();
90 14 : state_formula f;
91 14 : apply(f, x.operand());
92 14 : result = mu(name, x.assignments(), f);
93 14 : leave(x);
94 14 : }
95 :
96 : // Rename variable
97 : template <class T>
98 2 : void apply(T& result, const nu& x)
99 : {
100 2 : enter(x);
101 : // N.B. If the two lines below are replace by
102 : // state_formula result = nu(m_names[x.name()].back(), x.assignments(), (*this)(x.operand()));
103 : // a memory error occurs with the clang and intel compilers!
104 2 : core::identifier_string name = m_names[x.name()].back();
105 2 : state_formula f;
106 2 : apply(f, x.operand());
107 2 : result = nu(name, x.assignments(), f);
108 2 : leave(x);
109 2 : }
110 :
111 : // Rename variable
112 : template <class T>
113 13 : void apply(T& result, const variable& x)
114 : {
115 13 : result = variable(m_names[x.name()].back(), x.arguments());
116 13 : }
117 : };
118 :
119 : class state_formula_data_variable_name_clash_resolver: public state_formulas::data_expression_builder<state_formula_data_variable_name_clash_resolver>
120 : {
121 : public:
122 : typedef state_formulas::data_expression_builder<state_formula_data_variable_name_clash_resolver> super;
123 :
124 : using super::enter;
125 : using super::leave;
126 : using super::apply;
127 :
128 : data::set_identifier_generator& generator;
129 : std::multiset<data::variable> bound_variables;
130 : std::map<data::variable, std::vector<data::variable>> substitutions;
131 :
132 0 : explicit state_formula_data_variable_name_clash_resolver(data::set_identifier_generator& generator_)
133 0 : : generator(generator_)
134 0 : {}
135 :
136 0 : void insert(const data::variable& v)
137 : {
138 0 : if (utilities::detail::contains(bound_variables, v))
139 : {
140 0 : substitutions[v].push_back(data::variable(generator(v.name()), v.sort()));
141 : }
142 0 : bound_variables.insert(v);
143 0 : }
144 :
145 0 : void erase(const data::variable& v)
146 : {
147 : // Remove one variable, which must exist. Do not use bound_variables.erase(v) as it removes all variables v.
148 0 : std::multiset<data::variable>::const_iterator var_iter=bound_variables.find(v);
149 0 : assert(var_iter!=bound_variables.end());
150 0 : bound_variables.erase(var_iter);
151 :
152 0 : auto i = substitutions.find(v);
153 0 : if (i != substitutions.end())
154 : {
155 0 : i->second.pop_back();
156 0 : if (i->second.empty())
157 : {
158 0 : substitutions.erase(i);
159 : }
160 : }
161 0 : }
162 :
163 0 : data::assignment_list apply_assignments(const data::assignment_list& x)
164 : {
165 0 : auto sigma = [&](const data::variable& v) -> data::data_expression
166 : {
167 0 : auto i = substitutions.find(v);
168 0 : if (i == substitutions.end())
169 : {
170 0 : return v;
171 : }
172 0 : return i->second.back();
173 0 : };
174 :
175 0 : return data::assignment_list(x.begin(), x.end(), [&](const data::assignment& a)
176 : {
177 0 : return data::assignment(atermpp::down_cast<data::variable>(sigma(a.lhs())), data::replace_free_variables(a.rhs(), sigma));
178 : }
179 0 : );
180 : }
181 :
182 0 : data::variable_list apply_variables(const data::variable_list& x)
183 : {
184 0 : auto sigma = [&](const data::variable& v) -> data::data_expression
185 : {
186 0 : auto i = substitutions.find(v);
187 0 : if (i == substitutions.end())
188 : {
189 0 : return v;
190 : }
191 0 : return i->second.back();
192 0 : };
193 :
194 0 : return data::variable_list(x.begin(), x.end(), [&](const data::variable& v)
195 : {
196 0 : return atermpp::down_cast<data::variable>(sigma(v));
197 : }
198 0 : );
199 : }
200 :
201 : template <class T>
202 0 : void apply(T& result, const mu& x)
203 : {
204 0 : for (const data::assignment& a: x.assignments())
205 : {
206 0 : insert(a.lhs());
207 : }
208 0 : apply(result, x.operand());
209 0 : result = mu(x.name(), apply_assignments(x.assignments()), result);
210 0 : for (const data::assignment& a: x.assignments())
211 : {
212 0 : erase(a.lhs());
213 : }
214 0 : }
215 :
216 : template <class T>
217 0 : void apply(T& result, const nu& x)
218 : {
219 0 : for (const data::assignment& a: x.assignments())
220 : {
221 0 : insert(a.lhs());
222 : }
223 0 : apply(result, x.operand());
224 0 : result = nu(x.name(), apply_assignments(x.assignments()), result);
225 0 : for (const data::assignment& a: x.assignments())
226 : {
227 0 : erase(a.lhs());
228 : }
229 0 : }
230 :
231 : template <class T>
232 0 : void apply(T& result, const forall& x)
233 : {
234 0 : for (const data::variable& v: x.variables())
235 : {
236 0 : insert(v);
237 : }
238 0 : apply(result,x.body());
239 0 : result = forall(apply_variables(x.variables()), result);
240 0 : for (const data::variable& v: x.variables())
241 : {
242 0 : erase(v);
243 : }
244 0 : }
245 :
246 : template <class T>
247 0 : void apply(T& result, const exists& x)
248 : {
249 0 : for (const data::variable& v: x.variables())
250 : {
251 0 : insert(v);
252 : }
253 0 : apply(result, x.body());
254 0 : result = exists(apply_variables(x.variables()), result);
255 0 : for (const data::variable& v: x.variables())
256 : {
257 0 : erase(v);
258 : }
259 0 : }
260 :
261 : template <class T>
262 0 : void apply(T& result, const action_formulas::forall& x)
263 : {
264 0 : for (const data::variable& v: x.variables())
265 : {
266 0 : insert(v);
267 : }
268 0 : action_formulas::action_formula body;
269 0 : apply(body, x.body());
270 0 : result = action_formulas::forall(apply_variables(x.variables()), body);
271 0 : for (const data::variable& v: x.variables())
272 : {
273 0 : erase(v);
274 : }
275 0 : }
276 :
277 : template <class T>
278 0 : void apply(T& result, const action_formulas::exists& x)
279 : {
280 0 : for (const data::variable& v: x.variables())
281 : {
282 0 : insert(v);
283 : }
284 0 : action_formulas::action_formula body;
285 0 : apply(body, x.body());
286 0 : result = action_formulas::exists(apply_variables(x.variables()), body);
287 0 : for (const data::variable& v: x.variables())
288 : {
289 0 : erase(v);
290 : }
291 0 : }
292 :
293 : template <class T>
294 0 : void apply(T& result, const data::data_expression& x)
295 : {
296 0 : auto sigma = [&](const data::variable& v) -> data::data_expression
297 : {
298 0 : auto i = substitutions.find(v);
299 0 : if (i == substitutions.end())
300 : {
301 0 : return v;
302 : }
303 0 : return i->second.back();
304 : };
305 :
306 0 : result=data::replace_free_variables(x, sigma);
307 0 : }
308 : };
309 :
310 : } // namespace detail
311 :
312 : /// \brief Resolves name clashes in state variables of formula x
313 : inline
314 8 : state_formula resolve_state_variable_name_clashes(const state_formula& x)
315 : {
316 8 : state_formula result;
317 8 : core::make_apply_builder<detail::state_variable_name_clash_resolver>().apply(result, x);
318 8 : return result;
319 0 : }
320 :
321 : /// \brief Resolves name clashes in data variables of formula x
322 : inline
323 0 : state_formula resolve_state_formula_data_variable_name_clashes(const state_formula& x, const std::set<core::identifier_string>& context_ids = std::set<core::identifier_string>())
324 : {
325 0 : data::set_identifier_generator generator;
326 0 : generator.add_identifiers(state_formulas::find_identifiers(x));
327 0 : generator.add_identifiers(context_ids);
328 0 : detail::state_formula_data_variable_name_clash_resolver f(generator);
329 0 : state_formula result;
330 0 : f.apply(result, x);
331 0 : return result;
332 0 : }
333 :
334 : } // namespace mcrl2::state_formulas
335 :
336 : #endif // MCRL2_MODAL_FORMULA_RESOLVE_NAME_CLASHES_H
|
