Line data Source code
1 : // Author(s): Wieger Wesselink, Jan Friso Groote
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.h
10 : /// \brief The class enumerator.
11 :
12 : #ifndef MCRL2_DATA_ENUMERATOR_H
13 : #define MCRL2_DATA_ENUMERATOR_H
14 :
15 : #include <boost/iterator/iterator_facade.hpp>
16 : #include "mcrl2/atermpp/standard_containers/deque.h"
17 : #include "mcrl2/core/detail/print_utility.h"
18 : #include "mcrl2/data/detail/enumerator_iteration_limit.h"
19 : #include "mcrl2/data/rewriter.h"
20 : #include "mcrl2/data/substitutions/enumerator_substitution.h"
21 : #include "mcrl2/utilities/math.h"
22 :
23 : namespace mcrl2
24 : {
25 :
26 : namespace data
27 : {
28 :
29 : namespace detail
30 : {
31 :
32 : inline
33 292 : data_expression make_set_(std::size_t function_index, const sort_expression& element_sort, const data_expression_vector& set_elements)
34 : {
35 292 : data_expression result = sort_fset::empty(element_sort);
36 1260 : for (const auto & set_element : set_elements)
37 : {
38 968 : if (function_index % 2 == 1)
39 : {
40 484 : result=sort_fset::insert(element_sort, set_element, result);
41 : }
42 968 : function_index = function_index / 2;
43 : }
44 292 : return result;
45 0 : }
46 :
47 : inline
48 23280 : data_expression make_if_expression_(std::size_t& function_index,
49 : const std::size_t argument_index,
50 : const std::vector<data_expression_vector>& data_domain_expressions,
51 : const data_expression_vector& codomain_expressions,
52 : const variable_vector& parameters)
53 : {
54 23280 : if (argument_index == data_domain_expressions.size())
55 : {
56 12448 : std::size_t result_expression_index = function_index % codomain_expressions.size();
57 12448 : function_index = function_index / codomain_expressions.size();
58 12448 : return codomain_expressions[result_expression_index];
59 : }
60 :
61 10832 : data_expression result;
62 10832 : const data_expression_vector& current_enumerated_elements = data_domain_expressions[argument_index];
63 32496 : for (auto i = current_enumerated_elements.rbegin(); i != current_enumerated_elements.rend(); ++i)
64 : {
65 21664 : if (i == current_enumerated_elements.rbegin())
66 : {
67 10832 : result = make_if_expression_(function_index, argument_index + 1, data_domain_expressions, codomain_expressions, parameters);
68 : }
69 : else
70 : {
71 10832 : const data_expression lhs = make_if_expression_(function_index, argument_index + 1, data_domain_expressions, codomain_expressions, parameters);
72 10832 : if (lhs != result) // Optimize: if the lhs and rhs are equal, return the rhs.
73 : {
74 6856 : result = if_(equal_to(parameters[argument_index], *i), lhs, result);
75 : }
76 10832 : }
77 : }
78 10832 : return result;
79 10832 : }
80 :
81 : /// \brief Computes the elements of a finite set sort, and puts them in result. If there are too many elements, false is returned.
82 : template <class Rewriter, class MutableSubstitution>
83 37 : bool compute_finite_set_elements(const container_sort& sort,
84 : const data_specification& dataspec,
85 : Rewriter datar, MutableSubstitution& sigma,
86 : data_expression_vector& result,
87 : enumerator_identifier_generator& id_generator)
88 : {
89 : // TODO: This routine would really benefit from caching the calculated set of elements, as the same set is often generated
90 : // over and over again.
91 37 : data_expression_vector all_element_expressions = enumerate_expressions(sort.element_sort(), dataspec, datar, id_generator);
92 37 : if (all_element_expressions.size() >= 32) // If there are at least 2^32 functions, then enumerating them makes little sense.
93 : {
94 0 : return false;
95 : }
96 37 : if (all_element_expressions.size() > 16) // If there are more than 2^16 functions, provide a warning.
97 : {
98 0 : mCRL2log(log::warning) << "Generate 2^" << all_element_expressions.size() << " sets to enumerate sort " << sort << "\n";
99 : }
100 37 : const std::size_t number_of_sets = utilities::power_size_t(2, all_element_expressions.size());
101 329 : for (std::size_t i = 0; i < number_of_sets; ++i)
102 : {
103 292 : result.push_back(datar(make_set_(i, sort.element_sort(), all_element_expressions), sigma));
104 : }
105 37 : return true;
106 37 : }
107 :
108 : /// \brief Computes the elements of a finite function sort, and puts them in result. If there are too many elements, false is returned.
109 : template <class Rewriter>
110 26 : bool compute_finite_function_sorts(const function_sort& sort,
111 : enumerator_identifier_generator& id_generator,
112 : const data::data_specification& dataspec,
113 : Rewriter datar,
114 : data_expression_vector& result,
115 : variable_list& function_parameter_list
116 : )
117 : {
118 26 : data_expression_vector codomain_expressions = enumerate_expressions(sort.codomain(), dataspec, datar, id_generator);
119 26 : std::vector<data_expression_vector> domain_expressions;
120 26 : std::size_t total_domain_size = 1;
121 26 : variable_vector function_parameters;
122 :
123 90 : for (const sort_expression& s: sort.domain())
124 : {
125 38 : domain_expressions.push_back(enumerate_expressions(s, dataspec, datar, id_generator));
126 38 : total_domain_size = total_domain_size * domain_expressions.back().size();
127 38 : function_parameters.emplace_back(id_generator(), s);
128 : }
129 :
130 26 : if (total_domain_size * utilities::ceil_log2(codomain_expressions.size()) >= 32) // If there are at least 2^32 functions, then enumerating them makes little sense.
131 : {
132 0 : return false;
133 : }
134 :
135 26 : if (total_domain_size * utilities::ceil_log2(codomain_expressions.size()) > 16) // If there are more than 2^16 functions, provide a warning.
136 : {
137 0 : mCRL2log(log::warning) << "Generate " << codomain_expressions.size() << "^" << total_domain_size << " functions to enumerate sort " << sort << "\n";
138 : }
139 :
140 26 : function_parameter_list = variable_list(function_parameters.begin(), function_parameters.end());
141 :
142 26 : const std::size_t number_of_functions = utilities::power_size_t(codomain_expressions.size(), total_domain_size);
143 :
144 26 : if (number_of_functions == 1)
145 : {
146 0 : result.push_back(abstraction(lambda_binder(), function_parameter_list, codomain_expressions.front()));
147 : }
148 : else
149 : {
150 1642 : for (std::size_t i = 0; i < number_of_functions; ++i)
151 : {
152 1616 : std::size_t function_index = i; // function_index is changed in make_if_expression. A copy is therefore required.
153 1616 : result.push_back(abstraction(lambda_binder(), function_parameter_list, make_if_expression_(function_index, 0, domain_expressions, codomain_expressions, function_parameters)));
154 : }
155 : }
156 26 : return true;
157 26 : }
158 :
159 : template <typename Rewriter>
160 2750 : bool is_enumerable(const data_specification& dataspec,
161 : const Rewriter& rewr,
162 : const sort_expression& sort,
163 : std::list<sort_expression>& parents)
164 : {
165 2750 : assert(sort == normalize_sorts(sort,dataspec));
166 2750 : if (sort_bag::is_bag(sort) || sort_fbag::is_fbag(sort))
167 : {
168 0 : return false;
169 : }
170 2750 : else if (is_function_sort(sort))
171 : {
172 1 : const function_sort& func = atermpp::down_cast<function_sort>(sort);
173 2 : enumerator_identifier_generator id_gen;
174 1 : data_expression_vector expr_vec;
175 1 : variable_list var_list;
176 2 : return dataspec.is_certainly_finite(func) &&
177 1 : detail::compute_finite_function_sorts(func, id_gen, dataspec, rewr, expr_vec, var_list);
178 1 : }
179 2749 : else if (sort_set::is_set(sort) || sort_fset::is_fset(sort))
180 : {
181 0 : enumerator_identifier_generator id_gen;
182 0 : data_expression_vector expr_vec;
183 0 : mutable_indexed_substitution<> mut_sub;
184 0 : return dataspec.is_certainly_finite(atermpp::down_cast<container_sort>(sort).element_sort()) &&
185 0 : (!sort_fset::is_fset(sort) || detail::compute_finite_set_elements(atermpp::down_cast<container_sort>(sort), dataspec, rewr, mut_sub, expr_vec, id_gen));
186 0 : }
187 : else
188 : {
189 2749 : const function_symbol_vector& constructors = dataspec.constructors(sort, true);
190 2749 : if (constructors.empty())
191 : {
192 4 : return false;
193 : }
194 : else
195 : {
196 2745 : if (std::find(parents.begin(), parents.end(), sort) != parents.end())
197 : {
198 369 : return true;
199 : }
200 2376 : parents.push_back(sort);
201 2376 : bool result = std::all_of(constructors.begin(), constructors.end(), [&](const function_symbol& constructor)
202 : {
203 5471 : return !is_function_sort(constructor.sort()) ||
204 724 : std::all_of(atermpp::down_cast<function_sort>(constructor.sort()).domain().begin(), atermpp::down_cast<function_sort>(constructor.sort()).domain().end(),
205 5840 : [&](const sort_expression& arg_sort){ return is_enumerable(dataspec, rewr, arg_sort, parents); });
206 : });
207 2376 : parents.pop_back();
208 2376 : return result;
209 : }
210 : }
211 : }
212 :
213 : } // namespace detail
214 :
215 : /// \brief Enumerator exception
216 : struct enumerator_error: public mcrl2::runtime_error
217 : {
218 0 : explicit enumerator_error(const std::string& message): mcrl2::runtime_error(message)
219 0 : {}
220 : };
221 :
222 : template <typename Rewriter>
223 1657 : static bool is_enumerable(const data_specification& dataspec, const Rewriter& rewr, const sort_expression& sort)
224 : {
225 1657 : std::list<sort_expression> parentstack;
226 3314 : return detail::is_enumerable(dataspec, rewr, sort, parentstack);
227 1657 : }
228 :
229 : /// \brief The default element for the todo list of the enumerator
230 : template <typename Expression = data::data_expression>
231 : class enumerator_list_element
232 : {
233 : protected:
234 : data::variable_list v;
235 : Expression phi;
236 :
237 : public:
238 : typedef Expression expression_type;
239 :
240 : /// \brief Default constructor
241 2804 : enumerator_list_element() = default;
242 :
243 : /// \brief Constructs the element (v, phi)
244 4623 : enumerator_list_element(data::variable_list v_, const Expression& phi_)
245 4623 : : v(std::move(v_)), phi(phi_)
246 4623 : {}
247 :
248 : /// \brief Constructs the element (v, phi)
249 : enumerator_list_element(data::variable_list v_,
250 : const Expression& phi_,
251 : const enumerator_list_element&
252 : )
253 : : v(std::move(v_)), phi(phi_)
254 : {}
255 :
256 : /// \brief Constructs the element (v, phi)
257 26774 : enumerator_list_element(data::variable_list v_,
258 : const Expression& phi_,
259 : const enumerator_list_element&,
260 : const data::variable&,
261 : const data::data_expression&
262 : )
263 26774 : : v(std::move(v_)), phi(phi_)
264 26774 : {}
265 :
266 20234 : const data::variable_list& variables() const
267 : {
268 20234 : return v;
269 : }
270 :
271 8465 : const Expression& expression() const
272 : {
273 8465 : return phi;
274 : }
275 :
276 19652 : Expression& expression()
277 : {
278 19652 : return phi;
279 : }
280 :
281 19928 : bool is_solution() const
282 : {
283 19928 : return v.empty();
284 : }
285 :
286 : /// \brief Invalidates the element, by giving phi an undefined value
287 1 : void invalidate()
288 : {
289 1 : phi = data::undefined_data_expression();
290 1 : }
291 :
292 : /// \brief Returns true if the element is valid. If it becomes false, this is used to signal that
293 : /// the enumeration has been aborted.
294 123 : bool is_valid() const
295 : {
296 123 : return phi != data::undefined_data_expression();
297 : }
298 :
299 : /// \brief The following function is needed to mark the aterms in this class,
300 : /// when elements of this class are used in an atermpp standard container.
301 : /// When garbage collection of aterms is taking place this function is
302 : /// called for all elements of this class in the atermpp container.
303 218 : void mark(atermpp::term_mark_stack& todo) const
304 : {
305 218 : mark_term(v,todo);
306 218 : mark_term(phi,todo);
307 218 : }
308 :
309 : /// \brief Set the variables and the condition explicitly.
310 : /// \param v_ The variable list.
311 : /// \param phi_ The condition.
312 2738 : void set(const data::variable_list& v_, const Expression& phi_)
313 : {
314 2738 : v=v_;
315 2738 : phi=phi_;
316 2738 : }
317 :
318 : /// \brief Set the variables and the condition explicitly.
319 : /// \param v_ The variable list.
320 : /// \param phi_ The condition.
321 : /// \details Other arguments than the first two are ignored.
322 0 : void set(const data::variable_list& v_, const Expression& phi_,const enumerator_list_element&)
323 : {
324 0 : v=v_;
325 0 : phi=phi_;
326 0 : }
327 :
328 : /// \brief Set the variable ands and the expression explicitly
329 : /// as the element (v, phi, e.sigma[v := x]).
330 : /// \param v_ The variable list.
331 : /// \param phi_ The condition.
332 : /// \details Other arguments than the first two are ignored.
333 1989 : void set(const data::variable_list& v_,
334 : const Expression& phi_,
335 : const enumerator_list_element&,
336 : const data::variable&,
337 : const data::data_expression&)
338 : {
339 1989 : v=v_;
340 1989 : phi=phi_;
341 1989 : }
342 :
343 : };
344 :
345 : /// \brief An element for the todo list of the enumerator that collects the substitution
346 : /// corresponding to the expression phi
347 : template <typename Expression = data::data_expression>
348 : class enumerator_list_element_with_substitution: public enumerator_list_element<Expression>
349 : {
350 : protected:
351 : data::variable_list m_variables;
352 : data::data_expression_list m_expressions;
353 :
354 : public:
355 : typedef Expression expression_type;
356 :
357 : /// \brief Default constructor
358 1147 : enumerator_list_element_with_substitution() = default;
359 :
360 : /// \brief Constructs the element (v, phi, [])
361 1147 : enumerator_list_element_with_substitution(const data::variable_list& v, const Expression& phi)
362 1147 : : enumerator_list_element<Expression>(v, phi)
363 1147 : {}
364 :
365 : /// \brief Constructs the element (v, phi, e.sigma[v := x])
366 : enumerator_list_element_with_substitution(const data::variable_list& v,
367 : const Expression& phi,
368 : const enumerator_list_element_with_substitution<Expression>& elem
369 : )
370 : : enumerator_list_element<Expression>(v, phi),
371 : m_variables(elem.m_variables),
372 : m_expressions(elem.m_expressions)
373 : {
374 : }
375 :
376 : /// \brief Constructs the element (v, phi, e.sigma[v := x])
377 1828 : enumerator_list_element_with_substitution(
378 : const data::variable_list& v,
379 : const Expression& phi,
380 : const enumerator_list_element_with_substitution<Expression>& elem,
381 : const data::variable& d,
382 : const data::data_expression& e
383 : )
384 : : enumerator_list_element<Expression>(v, phi),
385 1828 : m_variables(elem.m_variables),
386 1828 : m_expressions(elem.m_expressions)
387 : {
388 1828 : m_variables.push_front(d);
389 1828 : m_expressions.push_front(e);
390 1828 : }
391 :
392 : /// \brief Adds the assignments that correspond with this element to the substitution result.
393 : template <typename VariableList, typename MutableSubstitution, typename Rewriter>
394 2967 : void add_assignments(const VariableList& v, MutableSubstitution& result, const Rewriter& rewriter) const
395 : {
396 5934 : data::enumerator_substitution sigma(m_variables, m_expressions);
397 2967 : sigma.revert();
398 8922 : for (const data::variable& v_i: v)
399 : {
400 2988 : result[v_i] = rewriter(sigma(v_i));
401 : }
402 2967 : }
403 :
404 : /// \brief Removes the assignments corresponding with this element from the substitution result.
405 : template <typename VariableList, typename MutableSubstitution>
406 : void remove_assignments(const VariableList& v, MutableSubstitution& result) const
407 : {
408 : for (const data::variable& v_i: v)
409 : {
410 : result[v_i] = v_i;
411 : }
412 : }
413 :
414 : /// \brief Returns the right hand sides corresponding to the variables v
415 : /// \pre variables in v must be contained in variables()
416 : template <typename VariableList, typename Rewriter>
417 0 : data::data_expression_list assign_expressions(const VariableList& v, const Rewriter& rewriter) const
418 : {
419 0 : data::enumerator_substitution sigma(m_variables, m_expressions);
420 0 : sigma.revert();
421 0 : return data_expression_list(v.begin(), v.end(), [&](const data::variable& v_i) { return rewriter(sigma(v_i)); });
422 0 : }
423 :
424 : data::enumerator_substitution sigma() const
425 : {
426 : return data::enumerator_substitution(m_variables, m_expressions);
427 : }
428 :
429 : /// \brief The following function is needed to mark the aterms in this class,
430 : /// when elements of this class are used in an atermpp standard container.
431 : /// When garbage collection of aterms is taking place this function is
432 : /// called for all elements of this class in the atermpp container.
433 0 : void mark(std::stack<std::reference_wrapper<atermpp::detail::_aterm>>& todo) const
434 : {
435 0 : mark_term(*atermpp::detail::address(m_variables), todo);
436 0 : mark_term(*atermpp::detail::address(m_expressions), todo);
437 0 : static_cast<enumerator_list_element<Expression>>(*this).mark(todo);
438 0 : }
439 :
440 : /// \brief Set the variable ands and the expression explicitly
441 : /// as the element (v, phi, e.sigma[v := x]).
442 2719 : void set(const data::variable_list& v,
443 : const Expression& phi,
444 : const enumerator_list_element_with_substitution<Expression>& elem,
445 : const data::variable& d,
446 : const data::data_expression& e)
447 : {
448 2719 : enumerator_list_element<Expression>::set(v, phi);
449 2719 : m_variables=elem.m_variables;
450 2719 : m_expressions=elem.m_expressions;
451 2719 : m_variables.push_front(d);
452 2719 : m_expressions.push_front(e);
453 2719 : }
454 :
455 : /// \brief Set the variable ands and the expression explicitly
456 : /// as the element (v, phi, e.sigma[v := x]).
457 19 : void set(const data::variable_list& v,
458 : const Expression& phi,
459 : const enumerator_list_element_with_substitution<Expression>& elem)
460 : {
461 19 : enumerator_list_element<Expression>::set(v, phi);
462 19 : m_variables=elem.m_variables;
463 19 : m_expressions=elem.m_expressions;
464 19 : }
465 : };
466 :
467 : template <typename Expression>
468 : std::ostream& operator<<(std::ostream& out, const enumerator_list_element<Expression>& p)
469 : {
470 : out << "{ [";
471 : const auto& variables = p.variables();
472 : for (auto i = variables.begin(); i != variables.end(); ++i)
473 : {
474 : if (i != variables.begin())
475 : {
476 : out << ", ";
477 : }
478 : out << *i << ": " << i->sort();
479 : }
480 : return out << "], " << p.expression() << " }";
481 : }
482 :
483 : template <typename Expression>
484 : std::ostream& operator<<(std::ostream& out, const enumerator_list_element_with_substitution<Expression>& p)
485 : {
486 : out << "{ [";
487 : const auto& variables = p.variables();
488 : for (auto i = variables.begin(); i != variables.end(); ++i)
489 : {
490 : if (i != variables.begin())
491 : {
492 : out << ", ";
493 : }
494 : out << *i << ": " << i->sort();
495 : }
496 : return out << "], " << p.expression() << ", " << p.sigma() << " }";
497 : }
498 :
499 : /// \brief Contains the enumerator queue.
500 : template <typename EnumeratorListElement>
501 : class enumerator_queue
502 : {
503 : protected:
504 : atermpp::deque<EnumeratorListElement> P;
505 : EnumeratorListElement m_enumerator_element_cache; // This element is used to temporarily store
506 : // information, which is more efficient than
507 : // declaring such a variable on the stack
508 : // as its protection using a protection set
509 : // is expensive.
510 :
511 : public:
512 : // The following variables are used for local store, to prevent the
513 : // variables to be inserted and removed continuously in a protection set.
514 : typename EnumeratorListElement::expression_type scratch_expression;
515 : data_expression scratch_data_expression;
516 : variable_list scratch_variable_list;
517 :
518 : typedef EnumeratorListElement value_type;
519 : typedef typename atermpp::deque<EnumeratorListElement>::size_type size_type;
520 :
521 : /// \brief Default constructor
522 1031 : enumerator_queue() = default;
523 :
524 : /// \brief Initializes the enumerator queue with the given value
525 1773 : explicit enumerator_queue(const EnumeratorListElement& value)
526 3546 : : P({value})
527 1773 : { }
528 :
529 28386 : void push_back(const EnumeratorListElement& x)
530 : {
531 : #ifdef MCRL2_LOG_ENUMERATOR
532 : std::cout << "push_back " << x << std::endl;
533 : #endif
534 28386 : P.push_back(x);
535 28386 : }
536 :
537 : template <class... Args>
538 1238 : void emplace_back(Args&&... args)
539 : {
540 : #ifdef MCRL2_LOG_ENUMERATOR
541 : std::cout << "emplace_back " << EnumeratorListElement(args...) << std::endl;
542 : #endif
543 1238 : P.emplace_back(std::forward<Args>(args)...);
544 1238 : }
545 :
546 48646 : bool empty() const
547 : {
548 48646 : return P.empty();
549 : }
550 :
551 2 : void clear()
552 : {
553 2 : P.clear();
554 2 : }
555 :
556 4970 : typename atermpp::deque<EnumeratorListElement>::size_type size() const
557 : {
558 4970 : return P.size();
559 : }
560 :
561 : const EnumeratorListElement& front() const
562 : {
563 : return P.front();
564 : }
565 :
566 42869 : EnumeratorListElement& front()
567 : {
568 42869 : return P.front();
569 : }
570 :
571 : const EnumeratorListElement& back() const
572 : {
573 : return P.back();
574 : }
575 :
576 : EnumeratorListElement& back()
577 : {
578 : return P.back();
579 : }
580 :
581 21820 : void pop_front()
582 : {
583 21820 : P.pop_front();
584 21820 : }
585 :
586 : void pop_back()
587 : {
588 : P.pop_back();
589 : }
590 :
591 : template <class... Args>
592 4727 : const EnumeratorListElement& enumerator_element_cache(const Args&... args)
593 : {
594 4727 : m_enumerator_element_cache.set(args...);
595 4727 : return m_enumerator_element_cache;
596 : }
597 : };
598 :
599 : /// \brief An enumerator algorithm that generates solutions of a condition.
600 : template <typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>
601 : class enumerator_algorithm
602 : {
603 : protected:
604 : // A rewriter
605 : const Rewriter& R;
606 :
607 : /// \brief A data specification.
608 : const data::data_specification& dataspec;
609 :
610 : // Needed for enumerate_expressions
611 : const DataRewriter& r;
612 :
613 : // A name generator
614 : enumerator_identifier_generator& id_generator;
615 :
616 : /// \brief max_count The enumeration is aborted after max_count iterations
617 : std::size_t m_max_count;
618 :
619 : /// \brief If true, solutions with a non-empty list of variables may be reported.
620 : bool m_accept_solutions_with_variables;
621 :
622 : #ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
623 : mutable std::size_t rewrite_calls = 0;
624 : #endif
625 :
626 : std::string print(const data::variable& x) const
627 : {
628 : std::ostringstream out;
629 : out << x << ": " << x.sort();
630 : return out.str();
631 : }
632 :
633 : template <typename Expression, typename MutableSubstitution>
634 : inline
635 36340 : Expression rewrite(const Expression& phi, MutableSubstitution& sigma) const
636 : {
637 : #ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
638 : rewrite_calls++;
639 : #endif
640 36340 : return const_cast<Rewriter&>(R)(phi, sigma);
641 : }
642 :
643 : template <typename Expression, typename MutableSubstitution>
644 : inline
645 6501 : void rewrite(Expression& result, const Expression& phi, MutableSubstitution& sigma) const
646 : {
647 : #ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
648 : rewrite_calls++;
649 : #endif
650 6501 : const_cast<Rewriter&>(R)(result, phi, sigma);
651 6501 : }
652 :
653 : public:
654 7111 : enumerator_algorithm(const Rewriter& R_,
655 : const data::data_specification& dataspec_,
656 : const DataRewriter& datar_,
657 : enumerator_identifier_generator& id_generator_,
658 : bool accept_solutions_with_variables,
659 : std::size_t max_count = (std::numeric_limits<std::size_t>::max)()
660 : )
661 7111 : : R(R_),
662 7111 : dataspec(dataspec_),
663 7111 : r(datar_),
664 7111 : id_generator(id_generator_),
665 7111 : m_max_count(max_count),
666 7111 : m_accept_solutions_with_variables(accept_solutions_with_variables)
667 7111 : {}
668 :
669 : enumerator_algorithm(const enumerator_algorithm<Rewriter, DataRewriter>&) = delete;
670 :
671 7111 : ~enumerator_algorithm()
672 : {
673 : #ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
674 : std::cout << "number of enumerator rewrite calls: " << rewrite_calls << std::endl;
675 : #endif
676 7111 : }
677 :
678 : void reset_id_generator()
679 : {
680 : id_generator.clear();
681 : }
682 :
683 : template <typename T>
684 : struct always_false
685 : {
686 3460 : bool operator()(const T&) { return false; }
687 : };
688 :
689 : /// \brief Enumerates the front element of the todo list P.
690 : /// The enumeration is interrupted when report_solution returns true for the reported solution.
691 : /// \param P The todo list of the algorithm.
692 : /// \param sigma A mutable substitution that is applied by the rewriter.
693 : /// \param reject Elements p for which reject(p) is true are discarded.
694 : /// \param accept Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.
695 : /// \param report_solution A callback function that is called whenever a solution is found.
696 : /// It takes an enumerator element as argument.
697 : /// If report_solution returns true, the enumeration is interrupted.
698 : /// N.B. If the enumeration is resumed after an interruption, the element p that
699 : /// was interrupted will be enumerated again.
700 : /// \pre !P.empty()
701 : /// \return If the return value is true, enumeration will be interrupted
702 : template <typename EnumeratorListElement,
703 : typename MutableSubstitution,
704 : typename ReportSolution,
705 : typename Reject = always_false<typename EnumeratorListElement::expression_type>,
706 : typename Accept = always_false<typename EnumeratorListElement::expression_type>
707 : >
708 2406 : bool enumerate_front(enumerator_queue<EnumeratorListElement>& P,
709 : MutableSubstitution& sigma,
710 : ReportSolution report_solution,
711 : Reject reject = Reject(),
712 : Accept accept = Accept()
713 : ) const
714 : {
715 2406 : assert(!P.empty());
716 2406 : const EnumeratorListElement& p = P.front();
717 :
718 24751 : auto add_element = [&](const data::variable_list& variables,
719 : const typename EnumeratorListElement::expression_type& phi,
720 : const data::variable& v,
721 : const data::data_expression& e
722 : ) -> bool
723 : {
724 6304 : rewrite(P.scratch_expression, phi, sigma);
725 6304 : if (reject(P.scratch_expression))
726 : {
727 1490 : return false;
728 : }
729 4814 : if ((accept(P.scratch_expression) && m_accept_solutions_with_variables) || variables.empty())
730 : {
731 : // EnumeratorListElement q(variables, phi1, p, v, e);
732 : // return report_solution(q);
733 4704 : return report_solution(P.enumerator_element_cache(variables, P.scratch_expression, p, v, e));
734 : }
735 110 : P.emplace_back(variables, P.scratch_expression, p, v, e);
736 110 : return false;
737 : };
738 :
739 3112 : auto add_element_with_variables = [&](const data::variable_list& variables,
740 : const data::variable_list& added_variables,
741 : const typename EnumeratorListElement::expression_type& phi,
742 : const data::variable& v,
743 : const data::data_expression& e
744 : ) -> bool
745 : {
746 178 : rewrite(P.scratch_expression, phi, sigma);
747 178 : if (reject(P.scratch_expression))
748 : {
749 64 : return false;
750 : }
751 114 : bool added_variables_empty = added_variables.empty() || (P.scratch_expression == phi && m_accept_solutions_with_variables);
752 114 : if ((accept(P.scratch_expression) && m_accept_solutions_with_variables) || (variables.empty() && added_variables_empty))
753 : {
754 : // EnumeratorListElement q(variables + added_variables, phi1, p, v, e);
755 4 : return report_solution(P.enumerator_element_cache(variables + added_variables, P.scratch_expression, p, v, e));
756 : }
757 110 : if (added_variables_empty)
758 : {
759 0 : P.emplace_back(variables, P.scratch_expression, p, v, e);
760 : }
761 : else
762 : {
763 110 : P.emplace_back(variables + added_variables, P.scratch_expression, p, v, e);
764 : }
765 110 : return false;
766 : };
767 :
768 2406 : const data::variable_list& v = p.variables();
769 2406 : const auto& phi = p.expression();
770 :
771 2406 : if (v.empty())
772 : {
773 19 : rewrite(P.scratch_expression, phi, sigma);
774 19 : if (reject(P.scratch_expression))
775 : {
776 0 : return false;
777 : }
778 : // EnumeratorListElement q(v, phi1, p);
779 19 : return report_solution(P.enumerator_element_cache(v, P.scratch_expression, p));
780 : }
781 :
782 2387 : const auto& v1 = v.front();
783 2387 : const auto& v_tail = v.tail();
784 2387 : const auto& v1_sort = v1.sort();
785 :
786 2387 : if (reject(phi))
787 : {
788 : // skip
789 : }
790 2387 : else if (data::is_function_sort(v1_sort))
791 : {
792 24 : const function_sort& function = atermpp::down_cast<function_sort>(v1_sort);
793 24 : if (dataspec.is_certainly_finite(function))
794 : {
795 24 : data_expression_vector function_sorts;
796 24 : variable_list function_parameter_list;
797 24 : bool result = detail::compute_finite_function_sorts(function, id_generator, dataspec, r, function_sorts, function_parameter_list);
798 24 : if (!result)
799 : {
800 0 : throw mcrl2::runtime_error("Sort " + data::pp(v1_sort) + " has too many elements to enumerate.");
801 : }
802 :
803 1632 : for (const data_expression& f: function_sorts)
804 : {
805 1608 : sigma[v1] = f;
806 1608 : if (add_element(v_tail, phi, v1, f))
807 : {
808 0 : sigma[v1] = v1;
809 0 : return true;
810 : }
811 : }
812 24 : }
813 : else
814 : {
815 0 : throw mcrl2::runtime_error("Cannot enumerate elements of function sort " + data::pp(v1_sort) + ".");
816 : }
817 : }
818 2363 : else if (sort_set::is_set(v1_sort))
819 : {
820 12 : const sort_expression& element_sort = atermpp::down_cast<container_sort>(v1_sort).element_sort();
821 12 : if (dataspec.is_certainly_finite(element_sort))
822 : {
823 48 : const data_expression lambda_term = abstraction(lambda_binder(), { variable(id_generator(), element_sort) }, sort_bool::false_());
824 24 : const variable fset_variable(id_generator(), sort_fset::fset(element_sort));
825 12 : data_expression e = sort_set::constructor(element_sort, lambda_term, fset_variable);
826 12 : sigma[v1] = e;
827 24 : if (add_element_with_variables(v_tail, { fset_variable }, phi, v1, e))
828 : {
829 0 : sigma[v1] = v1;
830 0 : return true;
831 : }
832 12 : }
833 : else
834 : {
835 0 : throw mcrl2::runtime_error("Cannot enumerate elements of set sort " + data::pp(v1_sort) + ".");
836 : }
837 : }
838 2351 : else if (sort_fset::is_fset(v1_sort))
839 : {
840 36 : const auto& fset = atermpp::down_cast<container_sort>(v1_sort);
841 36 : if (dataspec.is_certainly_finite(fset.element_sort()))
842 : {
843 36 : data_expression_vector set_elements;
844 36 : bool result = detail::compute_finite_set_elements(fset, dataspec, r, sigma, set_elements, id_generator);
845 36 : if (!result)
846 : {
847 0 : throw mcrl2::runtime_error("Finite set sort " + data::pp(v1_sort) + " has too many elements to enumerate.");
848 : }
849 :
850 324 : for (const data_expression& e: set_elements)
851 : {
852 288 : sigma[v1] = e;
853 288 : if (add_element(v_tail, phi, v1, e))
854 : {
855 0 : sigma[v1] = v1;
856 0 : return true;
857 : }
858 : }
859 36 : }
860 : else
861 : {
862 0 : throw mcrl2::runtime_error("Cannot enumerate elements of finite set sort " + data::pp(v1_sort) + ".");
863 : }
864 : }
865 2315 : else if (sort_bag::is_bag(v1_sort))
866 : {
867 0 : throw mcrl2::runtime_error("Cannot enumerate elements of bag sort " + data::pp(v1_sort) + ".");
868 : }
869 2315 : else if (sort_fbag::is_fbag(v1_sort))
870 : {
871 0 : throw mcrl2::runtime_error("Cannot enumerate elements of finite bag sort " + data::pp(v1_sort) + ".");
872 : }
873 : else
874 : {
875 2315 : const function_symbol_vector& C = dataspec.constructors(v1_sort);
876 2315 : if (!C.empty())
877 : {
878 6775 : for (const function_symbol& c: C)
879 : {
880 4574 : if (data::is_function_sort(c.sort()))
881 : {
882 166 : const sort_expression_list& domain = atermpp::down_cast<data::function_sort>(c.sort()).domain();
883 166 : atermpp::make_term_list(P.scratch_variable_list,
884 : domain.begin(),
885 : domain.end(),
886 300 : [&](const data::sort_expression& s) { return data::variable(id_generator(), s); });
887 : // data_expression cy = r(application(c, y.begin(), y.end()));
888 : // below sigma is not used, but it prevents generating a dummy sigma.
889 166 : r(P.scratch_data_expression, application(c, P.scratch_variable_list.begin(), P.scratch_variable_list.end()),sigma);
890 166 : sigma[v1] = P.scratch_data_expression;
891 166 : if (add_element_with_variables(v_tail, P.scratch_variable_list, phi, v1, P.scratch_data_expression))
892 : {
893 4 : sigma[v1] = v1;
894 113 : return true;
895 : }
896 : }
897 : else
898 : {
899 : // const data_expression e1 = r(c);
900 4408 : r(P.scratch_data_expression,c,sigma); // sigma is not used, but in this way no dummy sigma needs to be created.
901 4408 : sigma[v1] = P.scratch_data_expression;
902 4408 : if (add_element(v_tail, phi, v1, P.scratch_data_expression))
903 : {
904 109 : sigma[v1] = v1;
905 109 : return true;
906 : }
907 : }
908 : }
909 : }
910 : else
911 : {
912 1 : throw mcrl2::runtime_error("Cannot enumerate elements of sort " + data::pp(v1_sort) + " without constructors.");
913 : }
914 : }
915 2273 : sigma[v1] = v1;
916 2273 : return false;
917 : }
918 :
919 : /// \brief Enumerates until P is empty. Solutions are reported using the callback function report_solution.
920 : /// The enumeration is interrupted when report_solution returns true for the reported solution.
921 : /// \param P The todo list of the algorithm.
922 : /// \param sigma A substitution.
923 : /// \param reject Elements p for which reject(p) is true are discarded.
924 : /// \param accept Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.
925 : /// \param report_solution A callback function that is called whenever a solution is found.
926 : /// It takes an enumerator element as argument.
927 : /// If report_solution returns true, the enumeration is interrupted.
928 : /// N.B. If the enumeration is resumed after an interruption, the element p that
929 : /// was interrupted will be enumerated again.
930 : /// \return The number of elements that have been processed
931 : template <typename EnumeratorListElement,
932 : typename MutableSubstitution,
933 : typename ReportSolution,
934 : typename Reject = always_false<typename EnumeratorListElement::expression_type>,
935 : typename Accept = always_false<typename EnumeratorListElement::expression_type>
936 : >
937 2187 : std::size_t enumerate_all(enumerator_queue<EnumeratorListElement>& P,
938 : MutableSubstitution& sigma,
939 : ReportSolution report_solution,
940 : Reject reject = Reject(),
941 : Accept accept = Accept()
942 : ) const
943 : {
944 2187 : std::size_t count = 0;
945 4479 : while (!P.empty())
946 : {
947 2406 : if (count++ >= m_max_count)
948 : {
949 0 : break;
950 : }
951 2406 : if (enumerate_front(P, sigma, report_solution, reject, accept))
952 : {
953 113 : break;
954 : }
955 2292 : P.pop_front();
956 : }
957 2186 : return count;
958 : }
959 :
960 : /// \brief Enumerates the element p. Solutions are reported using the callback function report_solution.
961 : /// The enumeration is interrupted when report_solution returns true for the reported solution.
962 : /// \param p An enumerator element, i.e. an expression with a list of variables.
963 : /// \param sigma A substitution.
964 : /// \param reject Elements p for which reject(p) is true are discarded.
965 : /// \param accept Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.
966 : /// \param report_solution A callback function that is called whenever a solution is found.
967 : /// It takes an enumerator element as argument.
968 : /// If report_solution returns true, the enumeration is interrupted.
969 : /// N.B. If the enumeration is resumed after an interruption, the element p that
970 : /// was interrupted will be enumerated again.
971 : /// \return The number of elements that have been processed
972 : template <typename EnumeratorListElement,
973 : typename MutableSubstitution,
974 : typename ReportSolution,
975 : typename Reject = always_false<typename EnumeratorListElement::expression_type>,
976 : typename Accept = always_false<typename EnumeratorListElement::expression_type>
977 : >
978 1169 : std::size_t enumerate(const EnumeratorListElement& p,
979 : MutableSubstitution& sigma,
980 : ReportSolution report_solution,
981 : Reject reject = Reject(),
982 : Accept accept = Accept()
983 : ) const
984 : {
985 1169 : enumerator_queue<EnumeratorListElement> P(p);
986 2337 : return enumerate_all(P, sigma, report_solution, reject, accept);
987 1169 : }
988 :
989 : /// \brief Enumerates the variables v for condition c. Solutions are reported using the callback function report_solution.
990 : /// The enumeration is interrupted when report_solution returns true for the reported solution.
991 : /// \param p An enumerator element, i.e. an expression with a list of variables.
992 : /// \param sigma A substitution.
993 : /// \param reject Elements p for which reject(p) is true are discarded.
994 : /// \param accept Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.
995 : /// \param report_solution A callback function that is called whenever a solution is found.
996 : /// It takes an enumerator element as argument.
997 : /// If report_solution returns true, the enumeration is interrupted.
998 : /// N.B. If the enumeration is resumed after an interruption, the element p that
999 : /// was interrupted will be enumerated again.
1000 : /// \return The number of elements that have been processed
1001 : template <typename EnumeratorListElement,
1002 : typename MutableSubstitution,
1003 : typename ReportSolution,
1004 : typename Reject = always_false<typename EnumeratorListElement::expression_type>,
1005 : typename Accept = always_false<typename EnumeratorListElement::expression_type>
1006 : >
1007 1018 : std::size_t enumerate(const variable_list& vars,
1008 : const typename EnumeratorListElement::expression_type& cond,
1009 : MutableSubstitution& sigma,
1010 : ReportSolution report_solution,
1011 : Reject reject = Reject(),
1012 : Accept accept = Accept()
1013 : ) const
1014 : {
1015 1018 : enumerator_queue<EnumeratorListElement> P;
1016 1018 : P.emplace_back(vars, cond);
1017 2036 : return enumerate_all(P, sigma, report_solution, reject, accept);
1018 1018 : }
1019 :
1020 1849 : std::size_t max_count() const
1021 : {
1022 1849 : return m_max_count;
1023 : }
1024 : };
1025 :
1026 : /// \brief Returns a vector with all expressions of sort s.
1027 : /// \param s A sort expression.
1028 : /// \param dataspec The data specification defining the terms of sort \a s.
1029 : /// \param rewr A rewriter to be used to simplify terms and conditions.
1030 : /// \param id_generator An identifier generator used to generate new names for variables.
1031 : /// \details It is assumed that the sort s has only a finite number of elements.
1032 : template <class Rewriter>
1033 103 : data_expression_vector enumerate_expressions(const sort_expression& s,
1034 : const data_specification& dataspec,
1035 : const Rewriter& rewr,
1036 : enumerator_identifier_generator& id_generator)
1037 : {
1038 : typedef typename Rewriter::term_type term_type;
1039 : typedef enumerator_list_element_with_substitution<term_type> enumerator_element;
1040 103 : assert(dataspec.is_certainly_finite(s));
1041 :
1042 103 : bool accept_solutions_with_variables = false;
1043 103 : enumerator_algorithm<Rewriter, Rewriter> E(rewr, dataspec, rewr, id_generator, accept_solutions_with_variables);
1044 103 : data_expression_vector result;
1045 103 : mutable_indexed_substitution<> sigma;
1046 206 : const variable v("@var@", s);
1047 206 : const variable_list v_list{ v };
1048 206 : E.template enumerate<enumerator_element>(
1049 : v_list,
1050 103 : sort_bool::true_(),
1051 : sigma,
1052 464 : [&](const enumerator_element& p)
1053 : {
1054 232 : p.add_assignments(v_list, sigma, rewr);
1055 232 : result.push_back(sigma(v));
1056 232 : return false;
1057 : }
1058 : );
1059 206 : return result;
1060 103 : }
1061 :
1062 : /// \brief Returns a vector with all expressions of sort s.
1063 : /// \param s A sort expression.
1064 : /// \param dataspec The data specification defining the terms of sort \a s.
1065 : /// \param rewr A rewriter to be used to simplify terms and conditions.
1066 : /// \details It is assumed that the sort s has only a finite number of elements.
1067 : template <class Rewriter>
1068 2 : data_expression_vector enumerate_expressions(const sort_expression& s,
1069 : const data_specification& dataspec,
1070 : const Rewriter& rewr)
1071 : {
1072 4 : enumerator_identifier_generator id_generator;
1073 4 : return enumerate_expressions(s, dataspec, rewr, id_generator);
1074 2 : }
1075 :
1076 : } // namespace data
1077 :
1078 : } // namespace mcrl2
1079 :
1080 : #endif // MCRL2_DATA_ENUMERATOR_H
|
