Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING.
3 : //
4 : // Distributed under the Boost Software License, Version 1.0.
5 : // (See accompanying file LICENSE_1_0.txt or copy at
6 : // http://www.boost.org/LICENSE_1_0.txt)
7 : //
8 : /// \file mcrl2/pbes/remove_parameters.h
9 : /// \brief Functions for removing insignificant parameters from pbes types.
10 :
11 : #ifndef MCRL2_PBES_REMOVE_PARAMETERS_H
12 : #define MCRL2_PBES_REMOVE_PARAMETERS_H
13 :
14 : #include "mcrl2/pbes/builder.h"
15 :
16 : namespace mcrl2
17 : {
18 :
19 : namespace pbes_system
20 : {
21 :
22 : /// \cond INTERNAL_DOCS
23 : namespace detail
24 : {
25 :
26 : /// \brief Removes elements with indices in a given sequence from the sequence l
27 : /// \param l A sequence of terms
28 : /// \param to_be_removed A sorted sequence of integers
29 : /// \return The removal result
30 : template <typename Term>
31 58 : atermpp::term_list<Term> remove_elements(const atermpp::term_list<Term>& l, const std::vector<std::size_t>& to_be_removed)
32 : {
33 58 : assert(std::is_sorted(to_be_removed.begin(), to_be_removed.end()));
34 58 : std::size_t index = 0;
35 58 : std::vector<Term> result;
36 58 : auto j = to_be_removed.begin();
37 306 : for (auto i = l.begin(); i != l.end(); ++i, ++index)
38 : {
39 248 : if (j != to_be_removed.end() && index == *j)
40 : {
41 123 : ++j;
42 : }
43 : else
44 : {
45 125 : result.push_back(*i);
46 : }
47 : }
48 116 : return atermpp::term_list<Term>(result.begin(),result.end());
49 58 : }
50 :
51 : template <typename Derived>
52 : struct remove_parameters_builder: public pbes_system::pbes_expression_builder<Derived>
53 : {
54 : typedef pbes_system::pbes_expression_builder<Derived> super;
55 : using super::enter;
56 : using super::leave;
57 : using super::update;
58 : using super::apply;
59 :
60 : const std::vector<std::size_t>& to_be_removed;
61 :
62 58 : remove_parameters_builder(const std::vector<std::size_t>& to_be_removed_)
63 58 : : to_be_removed(to_be_removed_)
64 58 : {}
65 :
66 : template <class T>
67 17 : void apply(T& result, const propositional_variable& x)
68 : {
69 17 : make_propositional_variable(result, x.name(), detail::remove_elements(x.parameters(), to_be_removed));
70 17 : }
71 :
72 : template <class T>
73 41 : void apply(T& result, const propositional_variable_instantiation& x)
74 : {
75 41 : make_propositional_variable_instantiation(result, x.name(), detail::remove_elements(x.parameters(), to_be_removed));
76 41 : }
77 :
78 : void update(pbes_equation& x)
79 : {
80 : propositional_variable variable;
81 : static_cast<Derived&>(*this).apply(variable, x.variable());
82 : x.variable() = variable;
83 : pbes_expression formula;
84 : static_cast<Derived&>(*this).apply(formula, x.formula());
85 : x.formula() = formula;
86 : }
87 :
88 : void update(pbes& x)
89 : {
90 : static_cast<Derived&>(*this).update(x.equations());
91 : propositional_variable_instantiation initial_state;
92 : static_cast<Derived&>(*this).apply(initial_state, x.initial_state());
93 : x.initial_state() = initial_state;
94 : static_cast<Derived&>(*this).update(x.global_variables());
95 : }
96 : };
97 :
98 :
99 : } // namespace detail
100 : /// \endcond
101 :
102 : /// \brief Removes parameters from propositional variable instantiations in a pbes expression
103 : /// \param x A PBES library object that derives from atermpp::aterm_appl
104 : /// \param to_be_removed The indices of parameters that are to be removed
105 : /// \return The expression \p x with parameters removed according to the mapping \p to_be_removed
106 : template <typename T>
107 58 : T remove_parameters(const T& x,
108 : const std::vector<std::size_t>& to_be_removed,
109 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
110 : )
111 : {
112 58 : T result;
113 58 : core::make_apply_builder_arg1<detail::remove_parameters_builder>(to_be_removed).apply(result, x);
114 58 : return result;
115 0 : }
116 :
117 : /// \brief Removes parameters from propositional variable instantiations in a pbes expression
118 : /// \param x A PBES library object that does not derive from atermpp::aterm_appl
119 : /// \param to_be_removed The indices of parameters that are to be removed
120 : /// \return The expression \p x with parameters removed according to the mapping \p to_be_removed
121 : template <typename T>
122 : void remove_parameters(T& x,
123 : const std::vector<std::size_t>& to_be_removed,
124 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
125 : )
126 : {
127 : core::make_apply_builder_arg1<detail::remove_parameters_builder>(to_be_removed).update(x);
128 : }
129 :
130 : /// \cond INTERNAL_DOCS
131 : namespace detail
132 : {
133 :
134 : template <typename Derived>
135 : struct map_based_remove_parameters_builder: public pbes_expression_builder<Derived>
136 : {
137 : typedef pbes_expression_builder<Derived> super;
138 : using super::enter;
139 : using super::leave;
140 : using super::update;
141 : using super::apply;
142 :
143 : const std::map<core::identifier_string, std::vector<std::size_t> >& to_be_removed;
144 :
145 23 : map_based_remove_parameters_builder(const std::map<core::identifier_string, std::vector<std::size_t> >& to_be_removed_)
146 23 : : to_be_removed(to_be_removed_)
147 23 : {}
148 :
149 : // to prevent default operator() being called
150 : template <class T>
151 35 : void apply(T& result, const data::data_expression& x)
152 : {
153 35 : result = x;
154 35 : }
155 :
156 : template <class T>
157 35 : void apply(T& result, const propositional_variable& x)
158 : {
159 35 : auto i = to_be_removed.find(x.name());
160 35 : if (i == to_be_removed.end())
161 : {
162 19 : result = x;
163 19 : return;
164 : }
165 16 : result = remove_parameters(x, i->second);
166 : }
167 :
168 : template <class T>
169 78 : void apply(T& result, const propositional_variable_instantiation& x)
170 : {
171 78 : auto i = to_be_removed.find(x.name());
172 78 : if (i == to_be_removed.end())
173 : {
174 38 : result = x;
175 : }
176 : else
177 : {
178 40 : result = remove_parameters(x, i->second);
179 : }
180 78 : }
181 :
182 35 : void update(pbes_equation& x)
183 : {
184 35 : propositional_variable variable;
185 35 : static_cast<Derived&>(*this).apply(variable, x.variable());
186 35 : x.variable() = variable;
187 35 : pbes_expression formula;
188 35 : static_cast<Derived&>(*this).apply(formula, x.formula());
189 35 : x.formula() = formula;
190 35 : }
191 :
192 22 : void update(pbes& x)
193 : {
194 22 : static_cast<Derived&>(*this).update(x.equations());
195 22 : propositional_variable_instantiation initial_state;
196 22 : static_cast<Derived&>(*this).apply(initial_state, x.initial_state());
197 22 : x.initial_state() = initial_state;
198 22 : }
199 : };
200 : } // namespace detail
201 : /// \endcond
202 :
203 : /// \brief Removes parameters from propositional variable instantiations in a pbes expression
204 : /// \param x A PBES library object that derives from atermpp::aterm_appl
205 : /// \param to_be_removed A mapping that maps propositional variable names to indices of parameters that are removed
206 : /// \return The expression \p x with parameters removed according to the mapping \p to_be_removed
207 : template <typename T>
208 1 : T remove_parameters(const T& x,
209 : const std::map<core::identifier_string, std::vector<std::size_t> >& to_be_removed,
210 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
211 : )
212 : {
213 1 : T result;
214 1 : core::make_apply_builder_arg1<detail::map_based_remove_parameters_builder>(to_be_removed).apply(result, x);
215 1 : return result;
216 0 : }
217 :
218 : /// \brief Removes parameters from propositional variable instantiations in a pbes expression
219 : /// \param x A PBES library object that does not derive from atermpp::aterm_appl
220 : /// \param to_be_removed A mapping that maps propositional variable names to a sorted vector of parameter indices that
221 : /// need to be removed
222 : /// \return The expression \p x with parameters removed according to the mapping \p to_be_removed
223 : template <typename T>
224 22 : void remove_parameters(T& x,
225 : const std::map<core::identifier_string, std::vector<std::size_t> >& to_be_removed,
226 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
227 : )
228 : {
229 22 : core::make_apply_builder_arg1<detail::map_based_remove_parameters_builder>(to_be_removed).update(x);
230 22 : }
231 :
232 : /// \cond INTERNAL_DOCS
233 : namespace detail
234 : {
235 :
236 : template <typename Derived>
237 : struct set_based_remove_parameters_builder: public pbes_expression_builder<Derived>
238 : {
239 : typedef pbes_expression_builder<Derived> super;
240 : using super::enter;
241 : using super::leave;
242 : using super::update;
243 : using super::apply;
244 :
245 : const std::set<data::variable>& to_be_removed;
246 :
247 0 : set_based_remove_parameters_builder(const std::set<data::variable>& to_be_removed_)
248 0 : : to_be_removed(to_be_removed_)
249 0 : {}
250 :
251 0 : void remove_parameters(std::set<data::variable>& x) const
252 : {
253 0 : for (auto i = to_be_removed.begin(); i != to_be_removed.end(); ++i)
254 : {
255 0 : x.erase(*i);
256 : }
257 0 : }
258 :
259 0 : void apply_(data::variable_list& result, const data::variable_list& l) const
260 : {
261 : using utilities::detail::contains;
262 :
263 0 : std::vector<data::variable> result_vec;
264 0 : for (const data::variable& v: l)
265 : {
266 0 : if (!contains(to_be_removed, v))
267 : {
268 0 : result_vec.push_back(v);
269 : }
270 : }
271 0 : result = data::variable_list(result_vec.begin(), result_vec.end());
272 0 : }
273 :
274 : template <class T>
275 : void apply(T& result, const data::assignment_list& l) const
276 : {
277 : using utilities::detail::contains;
278 : std::vector<data::assignment> a(l.begin(), l.end());
279 : a.erase(std::remove_if(a.begin(), a.end(), [&](const data::assignment& y) { return contains(to_be_removed, y.lhs()); }), a.end());
280 : result = data::assignment_list(a.begin(), a.end());
281 : }
282 :
283 : template <class T>
284 0 : void apply(T& result, const propositional_variable& x)
285 : {
286 0 : data::variable_list vars;
287 0 : static_cast<Derived&>(*this).apply_(vars, x.parameters()); // Underscore is nasty trick to select the correct apply.
288 0 : make_propositional_variable(result, x.name(), vars);
289 0 : }
290 :
291 0 : void update(pbes_equation& x)
292 : {
293 0 : propositional_variable variable;
294 0 : static_cast<Derived&>(*this).apply(variable, x.variable());
295 0 : x.variable() = variable;
296 0 : pbes_expression formula;
297 0 : static_cast<Derived&>(*this).apply(formula, x.formula());
298 0 : x.formula() = formula;
299 0 : }
300 :
301 0 : void update(pbes& x)
302 : {
303 0 : static_cast<Derived&>(*this).update(x.equations());
304 0 : propositional_variable_instantiation initial_state;
305 0 : static_cast<Derived&>(*this).apply(initial_state, x.initial_state());
306 0 : x.initial_state() = initial_state;
307 0 : remove_parameters(x.global_variables());
308 0 : }
309 : };
310 : } // namespace detail
311 : /// \endcond
312 :
313 : /// \brief Removes parameters from propositional variable instantiations in a pbes expression
314 : /// \param x A PBES library object that derives from atermpp::aterm_appl
315 : /// \param to_be_removed A set of parameters that are to be removed
316 : /// \return The expression \p x with parameters removed according to the mapping \p to_be_removed
317 : template <typename T>
318 : T remove_parameters(const T& x,
319 : const std::set<data::variable>& to_be_removed,
320 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = 0
321 : )
322 : {
323 : T result;
324 : core::make_apply_builder_arg1<detail::set_based_remove_parameters_builder>(to_be_removed).apply(result, x);
325 : return result;
326 : }
327 :
328 : /// \brief Removes parameters from propositional variable instantiations in a pbes expression
329 : /// \param x A PBES library object that does not derive from atermpp::aterm_appl
330 : /// \param to_be_removed A set of parameters that are to be removed
331 : /// \return The expression \p x with parameters removed according to the mapping \p to_be_removed
332 : template <typename T>
333 0 : void remove_parameters(T& x,
334 : const std::set<data::variable>& to_be_removed,
335 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
336 : )
337 : {
338 0 : core::make_apply_builder_arg1<detail::set_based_remove_parameters_builder>(to_be_removed).update(x);
339 0 : }
340 :
341 :
342 : /// \cond INTERNAL_DOCS
343 : // used in pbes.h
344 : inline
345 : void remove_pbes_parameters(pbes& x,
346 : const std::set<data::variable>& to_be_removed
347 : )
348 : {
349 : remove_parameters(x, to_be_removed);
350 : }
351 : /// \endcond
352 :
353 : } // namespace pbes_system
354 :
355 : } // namespace mcrl2
356 :
357 : #endif // MCRL2_PBES_REMOVE_PARAMETERS_H
|
