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/data/enumerator_with_iterator.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_ENUMERATOR_WITH_ITERATOR_H
13 : #define MCRL2_DATA_ENUMERATOR_WITH_ITERATOR_H
14 :
15 : #include "mcrl2/atermpp/detail/aterm_configuration.h"
16 : #include "mcrl2/data/enumerator.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace data {
21 :
22 : struct is_not_false
23 : {
24 1715 : bool operator()(const data_expression& x) const
25 : {
26 1715 : return !sort_bool::is_false_function_symbol(x);
27 : }
28 : };
29 :
30 : struct is_not_true
31 : {
32 : bool operator()(const data_expression& x) const
33 : {
34 : return !sort_bool::is_true_function_symbol(x);
35 : }
36 : };
37 :
38 : /// \brief An enumerator algorithm that generates solutions of a condition.
39 : template <typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>
40 : class enumerator_algorithm_without_callback: public enumerator_algorithm<Rewriter, DataRewriter>
41 : {
42 : protected:
43 : typedef enumerator_algorithm<Rewriter, DataRewriter> super;
44 : using super::r;
45 : using super::R;
46 : using super::dataspec;
47 : using super::id_generator;
48 : using super::m_max_count;
49 : using super::rewrite;
50 :
51 : /// \brief throw_exceptions If true, an exception is thrown when the enumeration is aborted.
52 : bool m_throw_exceptions;
53 :
54 : template <typename EnumeratorListElement>
55 1 : void cannot_enumerate(EnumeratorListElement& e, const std::string& msg) const
56 : {
57 1 : e.invalidate();
58 1 : if (m_throw_exceptions)
59 : {
60 1 : throw mcrl2::runtime_error(msg);
61 : }
62 0 : }
63 :
64 : // add element without additional variables
65 : template <typename EnumeratorListElement, typename MutableSubstitution, typename Filter, typename Expression>
66 23815 : void add_element(enumerator_queue<EnumeratorListElement>& P,
67 : MutableSubstitution& sigma,
68 : Filter accept,
69 : const data::variable_list& variables,
70 : const Expression& phi,
71 : const EnumeratorListElement& p,
72 : const data::variable& v,
73 : const data::data_expression& e) const
74 : {
75 23815 : auto phi1 = rewrite(phi, sigma);
76 23815 : if (accept(phi1))
77 : {
78 16473 : P.push_back(EnumeratorListElement(variables, phi1, p, v, e));
79 : }
80 23815 : }
81 :
82 : // add element with additional variables
83 : template <typename EnumeratorListElement, typename MutableSubstitution, typename Filter, typename Expression>
84 1001 : void add_element(enumerator_queue<EnumeratorListElement>& P,
85 : MutableSubstitution& sigma,
86 : Filter accept,
87 : const data::variable_list& variables,
88 : const data::variable_list& added_variables,
89 : const Expression& phi,
90 : const EnumeratorListElement& p,
91 : const data::variable& v,
92 : const data::data_expression& e) const
93 : {
94 1001 : auto phi1 = rewrite(phi, sigma);
95 1001 : if (accept(phi1))
96 : {
97 : // Additional variables are put at the end of the list!
98 999 : P.push_back(EnumeratorListElement(variables + added_variables, phi1, p, v, e));
99 : }
100 1001 : }
101 :
102 : // specialization for enumerator_list_element; in this case we are not interested in the substitutions,
103 : // and this allows an optimization
104 : template <typename MutableSubstitution, typename Filter, typename Expression>
105 10916 : void add_element(enumerator_queue<enumerator_list_element<Expression>>& P,
106 : MutableSubstitution& sigma,
107 : Filter accept,
108 : const data::variable_list& variables,
109 : const data::variable_list& added_variables,
110 : const Expression& phi,
111 : const enumerator_list_element<Expression>& p,
112 : const data::variable& v,
113 : const data::data_expression& e) const
114 : {
115 10916 : auto phi1 = rewrite(phi, sigma);
116 10916 : if (accept(phi1))
117 : {
118 10910 : if (phi1 == phi)
119 : {
120 : // Discard the added_variables, since we know they do not appear in phi1
121 545 : P.push_back(enumerator_list_element<Expression>(variables, phi1, p, v, e));
122 : }
123 : else
124 : {
125 : // Additional variables are put at the end of the list!
126 10365 : P.push_back(enumerator_list_element<Expression>(variables + added_variables, phi1, p, v, e));
127 : }
128 : //mCRL2log(log::debug) << " <add-element> " << P.back() << " with assignment " << v << " := " << e << std::endl;
129 : }
130 10916 : }
131 :
132 : public:
133 606 : enumerator_algorithm_without_callback(const Rewriter& R,
134 : const data::data_specification& dataspec,
135 : const DataRewriter& r,
136 : enumerator_identifier_generator& id_generator,
137 : std::size_t max_count = (std::numeric_limits<std::size_t>::max)(),
138 : bool throw_exceptions = false
139 : )
140 606 : : super(R, dataspec, r, id_generator, false, max_count), m_throw_exceptions(throw_exceptions)
141 606 : {}
142 :
143 : enumerator_algorithm_without_callback(const enumerator_algorithm<Rewriter, DataRewriter>&) = delete;
144 :
145 : template <typename T>
146 : struct always_false
147 : {
148 : bool operator()(const T&) { return false; }
149 : };
150 :
151 : /// \brief Enumerates the front element of the todo list P.
152 : /// \param P The todo list of the algorithm.
153 : /// \param sigma A mutable substitution that is applied by the rewriter.
154 : /// \param accept Elements p for which accept(p) is false are discarded.
155 : /// \pre !P.empty()
156 : template <typename EnumeratorListElement, typename MutableSubstitution, typename Filter>
157 17828 : void step(enumerator_queue<EnumeratorListElement>& P, MutableSubstitution& sigma, Filter accept) const
158 : {
159 17828 : assert(!P.empty());
160 :
161 17828 : auto p = P.front();
162 17828 : const auto& v = p.variables();
163 17828 : const auto& phi = p.expression();
164 : //mCRL2log(log::debug) << " <process-element> " << p << std::endl;
165 17828 : P.pop_front();
166 :
167 17828 : const auto& v1 = v.front();
168 17828 : const auto& v_tail = v.tail();
169 17828 : const auto& v1_sort = v1.sort();
170 :
171 17828 : if (data::is_function_sort(v1_sort))
172 : {
173 1 : const function_sort& function = atermpp::down_cast<function_sort>(v1_sort);
174 1 : if (dataspec.is_certainly_finite(function))
175 : {
176 1 : data_expression_vector function_sorts;
177 1 : variable_list function_parameter_list;
178 1 : bool result = detail::compute_finite_function_sorts(function, id_generator, dataspec, r, function_sorts, function_parameter_list);
179 1 : if (!result)
180 : {
181 0 : cannot_enumerate(p, "Sort " + data::pp(v1_sort) + " has too many elements to enumerate.");
182 : }
183 :
184 1 : data_expression sigma_v1 = sigma(v1);
185 5 : for (const data_expression& f: function_sorts)
186 : {
187 4 : sigma[v1] = f;
188 4 : add_element(P, sigma, accept, v_tail, phi, p, v1, f);
189 : }
190 1 : sigma[v1] = sigma_v1;
191 1 : }
192 : else
193 : {
194 0 : cannot_enumerate(p, "Cannot enumerate elements of function sort " + data::pp(v1_sort) + ".");
195 : }
196 : }
197 17827 : else if (sort_set::is_set(v1_sort))
198 : {
199 1 : const sort_expression& element_sort = atermpp::down_cast<container_sort>(v1_sort).element_sort();
200 1 : if (dataspec.is_certainly_finite(element_sort))
201 : {
202 4 : const data_expression lambda_term = abstraction(lambda_binder(), { variable(id_generator(), element_sort) }, sort_bool::false_());
203 2 : const variable fset_variable(id_generator(), sort_fset::fset(element_sort));
204 1 : data_expression e = sort_set::constructor(element_sort, lambda_term, fset_variable);
205 1 : data_expression sigma_v1 = sigma(v1);
206 1 : sigma[v1] = e;
207 2 : add_element(P, sigma, accept, v_tail, { fset_variable }, phi, p, v1, e);
208 1 : sigma[v1] = sigma_v1;
209 1 : }
210 : else
211 : {
212 0 : cannot_enumerate(p, "Cannot enumerate elements of set sort " + data::pp(v1_sort) + ".");
213 0 : return;
214 : }
215 : }
216 17826 : else if (sort_fset::is_fset(v1_sort))
217 : {
218 1 : const auto& fset = atermpp::down_cast<container_sort>(v1_sort);
219 1 : if (dataspec.is_certainly_finite(fset.element_sort()))
220 : {
221 1 : data_expression_vector set_elements;
222 1 : bool result = detail::compute_finite_set_elements(fset, dataspec, r, sigma, set_elements, id_generator);
223 1 : if (!result)
224 : {
225 0 : cannot_enumerate(p, "Finite set sort " + data::pp(v1_sort) + " has too many elements to enumerate.");
226 : }
227 :
228 1 : data_expression sigma_v1 = sigma(v1);
229 5 : for (const data_expression& e: set_elements)
230 : {
231 4 : sigma[v1] = e;
232 4 : add_element(P, sigma, accept, v_tail, phi, p, v1, e);
233 : }
234 1 : sigma[v1] = sigma_v1;
235 1 : }
236 : else
237 : {
238 0 : cannot_enumerate(p, "Cannot enumerate elements of finite set sort " + data::pp(v1_sort) + ".");
239 0 : return;
240 : }
241 : }
242 17825 : else if (sort_bag::is_bag(v1_sort))
243 : {
244 0 : cannot_enumerate(p, "Cannot enumerate elements of bag sort " + data::pp(v1_sort) + ".");
245 0 : return;
246 : }
247 17825 : else if (sort_fbag::is_fbag(v1_sort))
248 : {
249 0 : cannot_enumerate(p, "Cannot enumerate elements of finite bag sort " + data::pp(v1_sort) + ".");
250 0 : return;
251 : }
252 : else
253 : {
254 17825 : const function_symbol_vector& C = dataspec.constructors(v1_sort);
255 17825 : if (!C.empty())
256 : {
257 53547 : for (const function_symbol& c: C)
258 : {
259 35723 : if (data::is_function_sort(c.sort()))
260 : {
261 11916 : auto const& domain = atermpp::down_cast<data::function_sort>(c.sort()).domain();
262 34901 : data::variable_list y(domain.begin(), domain.end(), [&](const data::sort_expression& s) { return data::variable(id_generator(), s); });
263 : // TODO: We want to apply datar without the substitution sigma, but that is currently an inefficient operation of data::rewriter.
264 11916 : data_expression cy = r(application(c, y.begin(), y.end()), sigma);
265 11916 : sigma[v1] = cy;
266 11916 : add_element(P, sigma, accept, v_tail, y, phi, p, v1, cy);
267 11916 : sigma[v1] = v1;
268 11916 : }
269 : else
270 : {
271 : // TODO: We want to apply r without the substitution sigma, but that is currently an inefficient operation of data::rewriter.
272 23807 : const auto e1 = r(c, sigma);
273 23807 : sigma[v1] = e1;
274 23807 : add_element(P, sigma, accept, v_tail, phi, p, v1, e1);
275 23807 : sigma[v1] = v1;
276 23807 : }
277 : }
278 : }
279 : else
280 : {
281 4 : cannot_enumerate(p, "Cannot enumerate elements of sort " + data::pp(v1_sort) + " without constructors.");
282 0 : return;
283 : }
284 : }
285 17828 : }
286 :
287 : /// \brief Enumerates the front elements of the todo list P until a solution
288 : /// has been found, or until P is empty.
289 : /// \param P The todo list of the algorithm.
290 : /// \param sigma A substitution.
291 : /// \param accept Elements p for which accept(p) is false are discarded.
292 : /// \return The number of elements that have been processed
293 : /// \post Either P.empty() or P.front().is_solution()
294 : template <typename EnumeratorListElement, typename MutableSubstitution, typename Filter>
295 2307 : std::size_t next(enumerator_queue<EnumeratorListElement>& P, MutableSubstitution& sigma, Filter accept) const
296 : {
297 2307 : std::size_t count = 0;
298 20134 : while (!P.empty())
299 : {
300 20077 : if (count++ >= m_max_count)
301 : {
302 149 : break;
303 : }
304 19928 : if (P.front().is_solution())
305 : {
306 2100 : break;
307 : }
308 : else
309 : {
310 17828 : step(P, sigma, accept);
311 : }
312 : }
313 2306 : return count;
314 : }
315 :
316 149 : bool throw_exceptions() const
317 : {
318 149 : return m_throw_exceptions;
319 : }
320 : };
321 :
322 : /// \brief An enumerator algorithm with an iterator interface.
323 : template <typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<> >
324 : class enumerator_algorithm_with_iterator: public enumerator_algorithm_without_callback<Rewriter, DataRewriter>
325 : {
326 : protected:
327 : Filter m_accept;
328 :
329 : public:
330 : typedef enumerator_algorithm_without_callback<Rewriter, DataRewriter> super;
331 : using super::rewrite;
332 :
333 : /// \brief A class to enumerate solutions for terms.
334 : /// \details Solutions are presented as data_expression_lists of the same length as
335 : /// the list of variables for which a solution is sought.
336 : class iterator: public boost::iterator_facade<iterator, const EnumeratorListElement, boost::forward_traversal_tag>
337 : {
338 : protected:
339 : enumerator_algorithm_with_iterator<Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution>* E;
340 : MutableSubstitution* sigma;
341 : enumerator_queue<EnumeratorListElement>* P;
342 : Filter accept;
343 : std::size_t count;
344 :
345 11 : static enumerator_queue<EnumeratorListElement>& default_deque()
346 : {
347 : #ifdef MCRL2_ENABLE_MULTITHREADING
348 : static_assert(mcrl2::utilities::detail::GlobalThreadSafe);
349 11 : thread_local enumerator_queue<EnumeratorListElement> result; // Changed this static variable to thread local,
350 : // as it could be the cause of a thread conflict.
351 : #else
352 : static_assert(!mcrl2::utilities::detail::GlobalThreadSafe);
353 : static enumerator_queue<EnumeratorListElement> result; // Changed this static variable to thread local,
354 : #endif
355 11 : return result;
356 : }
357 :
358 : public:
359 607 : iterator(enumerator_algorithm_with_iterator<Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution>* E_,
360 : enumerator_queue<EnumeratorListElement>* P_,
361 : MutableSubstitution* sigma_,
362 : Filter accept_ = Filter()
363 : )
364 607 : : E(E_), sigma(sigma_), P(P_), accept(accept_), count(0)
365 : {
366 607 : count += E->next(*P, *sigma, accept);
367 606 : }
368 :
369 11 : explicit iterator(Filter accept_ = Filter())
370 11 : : E(nullptr), sigma(nullptr), P(&default_deque()), accept(accept_), count(0)
371 11 : { }
372 :
373 : protected:
374 : friend class boost::iterator_core_access;
375 :
376 1700 : void increment()
377 : {
378 1700 : assert(!P->empty());
379 1700 : P->pop_front();
380 1700 : count += E->next(*P, *sigma, accept);
381 1700 : if (count >= E->max_count())
382 : {
383 149 : if (E->throw_exceptions())
384 : {
385 149 : std::ostringstream out;
386 149 : out << "enumeration was aborted, since it did not complete within " << E->max_count() << " iterations";
387 149 : throw mcrl2::runtime_error(out.str());
388 149 : }
389 : else
390 : {
391 0 : P->clear();
392 0 : return;
393 : }
394 : }
395 : }
396 :
397 2181 : bool equal(iterator const& other) const
398 : {
399 2181 : return P->size() == other.P->size();
400 : }
401 :
402 2099 : const EnumeratorListElement& dereference() const
403 : {
404 2099 : assert(!P->empty());
405 2099 : return P->front();
406 : }
407 : };
408 :
409 606 : enumerator_algorithm_with_iterator(
410 : const Rewriter& R,
411 : const data::data_specification& dataspec,
412 : const DataRewriter& datar,
413 : enumerator_identifier_generator& id_generator,
414 : std::size_t max_count = (std::numeric_limits<std::size_t>::max)(),
415 : bool throw_exceptions = false,
416 : const Filter& f = Filter())
417 : : super(R, dataspec, datar, id_generator, max_count, throw_exceptions)
418 606 : , m_accept(f)
419 606 : {}
420 :
421 : /// \brief Returns an iterator that enumerates solutions for variables that satisfy a condition
422 : /// \param sigma A mutable substitution that is applied by the rewriter contained in E
423 : /// \param P The condition that is solved, together with the list of variables
424 : /// Otherwise an invalidated enumerator element is returned when it is dereferenced.
425 608 : iterator begin(MutableSubstitution& sigma, enumerator_queue<EnumeratorListElement>& P)
426 : {
427 608 : assert(P.size() == 1);
428 608 : auto& p = P.front();
429 608 : p.expression() = rewrite(p.expression(), sigma);
430 608 : if (m_accept(p.expression()))
431 : {
432 607 : return iterator(const_cast<enumerator_algorithm_with_iterator<Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution>*>(this), &P, &sigma, m_accept);
433 : }
434 : else
435 : {
436 1 : return end();
437 : }
438 : }
439 :
440 2182 : const iterator& end()
441 : {
442 : #ifdef MCRL2_ENABLE_MULTITHREADING
443 : static_assert(mcrl2::utilities::detail::GlobalThreadSafe);
444 2182 : thread_local iterator result(m_accept);
445 : #else
446 : static_assert(!mcrl2::utilities::detail::GlobalThreadSafe);
447 : static iterator result(m_accept);
448 : #endif
449 2182 : return result;
450 : }
451 : };
452 :
453 : } // namespace data
454 :
455 : } // namespace mcrl2
456 :
457 : #endif // MCRL2_DATA_ENUMERATOR_WITH_ITERATOR_H
|
