mCRL2
Loading...
Searching...
No Matches
enumerator.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_DATA_ENUMERATOR_H
13#define MCRL2_DATA_ENUMERATOR_H
14
15#include <boost/iterator/iterator_facade.hpp>
18#include "mcrl2/data/rewriter.h"
21
22namespace mcrl2
23{
24
25namespace data
26{
27
28namespace detail
29{
30
31inline
32data_expression make_set_(std::size_t function_index, const sort_expression& element_sort, const data_expression_vector& set_elements)
33{
34 data_expression result = sort_fset::empty(element_sort);
35 for (const auto & set_element : set_elements)
36 {
37 if (function_index % 2 == 1)
38 {
39 result=sort_fset::insert(element_sort, set_element, result);
40 }
41 function_index = function_index / 2;
42 }
43 return result;
44}
45
46inline
47data_expression make_if_expression_(std::size_t& function_index,
48 const std::size_t argument_index,
49 const std::vector<data_expression_vector>& data_domain_expressions,
50 const data_expression_vector& codomain_expressions,
51 const variable_vector& parameters)
52{
53 if (argument_index == data_domain_expressions.size())
54 {
55 std::size_t result_expression_index = function_index % codomain_expressions.size();
56 function_index = function_index / codomain_expressions.size();
57 return codomain_expressions[result_expression_index];
58 }
59
60 data_expression result;
61 const data_expression_vector& current_enumerated_elements = data_domain_expressions[argument_index];
62 for (auto i = current_enumerated_elements.rbegin(); i != current_enumerated_elements.rend(); ++i)
63 {
64 if (i == current_enumerated_elements.rbegin())
65 {
66 result = make_if_expression_(function_index, argument_index + 1, data_domain_expressions, codomain_expressions, parameters);
67 }
68 else
69 {
70 const data_expression lhs = make_if_expression_(function_index, argument_index + 1, data_domain_expressions, codomain_expressions, parameters);
71 if (lhs != result) // Optimize: if the lhs and rhs are equal, return the rhs.
72 {
73 result = if_(equal_to(parameters[argument_index], *i), lhs, result);
74 }
75 }
76 }
77 return result;
78}
79
81template <class Rewriter, class MutableSubstitution>
83 const data_specification& dataspec,
84 Rewriter datar, MutableSubstitution& sigma,
87{
88 // TODO: This routine would really benefit from caching the calculated set of elements, as the same set is often generated
89 // over and over again.
90 data_expression_vector all_element_expressions = enumerate_expressions(sort.element_sort(), dataspec, datar, id_generator);
91 if (all_element_expressions.size() >= 32) // If there are at least 2^32 functions, then enumerating them makes little sense.
92 {
93 return false;
94 }
95 if (all_element_expressions.size() > 16) // If there are more than 2^16 functions, provide a warning.
96 {
97 mCRL2log(log::warning) << "Generate 2^" << all_element_expressions.size() << " sets to enumerate sort " << sort << "\n";
98 }
99 const std::size_t number_of_sets = utilities::power_size_t(2, all_element_expressions.size());
100 for (std::size_t i = 0; i < number_of_sets; ++i)
101 {
102 result.push_back(datar(make_set_(i, sort.element_sort(), all_element_expressions), sigma));
103 }
104 return true;
105}
106
108template <class Rewriter>
111 const data::data_specification& dataspec,
112 Rewriter datar,
114 variable_list& function_parameter_list
115 )
116{
117 data_expression_vector codomain_expressions = enumerate_expressions(sort.codomain(), dataspec, datar, id_generator);
118 std::vector<data_expression_vector> domain_expressions;
119 std::size_t total_domain_size = 1;
120 variable_vector function_parameters;
121
122 for (const sort_expression& s: sort.domain())
123 {
124 domain_expressions.push_back(enumerate_expressions(s, dataspec, datar, id_generator));
125 total_domain_size = total_domain_size * domain_expressions.back().size();
126 function_parameters.emplace_back(id_generator(), s);
127 }
128
129 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.
130 {
131 return false;
132 }
133
134 if (total_domain_size * utilities::ceil_log2(codomain_expressions.size()) > 16) // If there are more than 2^16 functions, provide a warning.
135 {
136 mCRL2log(log::warning) << "Generate " << codomain_expressions.size() << "^" << total_domain_size << " functions to enumerate sort " << sort << "\n";
137 }
138
139 function_parameter_list = variable_list(function_parameters.begin(), function_parameters.end());
140
141 const std::size_t number_of_functions = utilities::power_size_t(codomain_expressions.size(), total_domain_size);
142
143 if (number_of_functions == 1)
144 {
145 result.push_back(abstraction(lambda_binder(), function_parameter_list, codomain_expressions.front()));
146 }
147 else
148 {
149 for (std::size_t i = 0; i < number_of_functions; ++i)
150 {
151 std::size_t function_index = i; // function_index is changed in make_if_expression. A copy is therefore required.
152 result.push_back(abstraction(lambda_binder(), function_parameter_list, make_if_expression_(function_index, 0, domain_expressions, codomain_expressions, function_parameters)));
153 }
154 }
155 return true;
156}
157
158template <typename Rewriter>
159bool is_enumerable(const data_specification& dataspec,
160 const Rewriter& rewr,
161 const sort_expression& sort,
162 std::list<sort_expression>& parents)
163{
164 assert(sort == normalize_sorts(sort,dataspec));
165 if (sort_bag::is_bag(sort) || sort_fbag::is_fbag(sort))
166 {
167 return false;
168 }
169 else if (is_function_sort(sort))
170 {
171 const function_sort& func = atermpp::down_cast<function_sort>(sort);
173 data_expression_vector expr_vec;
174 variable_list var_list;
175 return dataspec.is_certainly_finite(func) &&
176 detail::compute_finite_function_sorts(func, id_gen, dataspec, rewr, expr_vec, var_list);
177 }
178 else if (sort_set::is_set(sort) || sort_fset::is_fset(sort))
179 {
181 data_expression_vector expr_vec;
183 return dataspec.is_certainly_finite(atermpp::down_cast<container_sort>(sort).element_sort()) &&
184 (!sort_fset::is_fset(sort) || detail::compute_finite_set_elements(atermpp::down_cast<container_sort>(sort), dataspec, rewr, mut_sub, expr_vec, id_gen));
185 }
186 else
187 {
188 const function_symbol_vector& constructors = dataspec.constructors(sort, true);
189 if (constructors.empty())
190 {
191 return false;
192 }
193 else
194 {
195 if (std::find(parents.begin(), parents.end(), sort) != parents.end())
196 {
197 return true;
198 }
199 parents.push_back(sort);
200 bool result = std::all_of(constructors.begin(), constructors.end(), [&](const function_symbol& constructor)
201 {
202 return !is_function_sort(constructor.sort()) ||
203 std::all_of(atermpp::down_cast<function_sort>(constructor.sort()).domain().begin(), atermpp::down_cast<function_sort>(constructor.sort()).domain().end(),
204 [&](const sort_expression& arg_sort){ return is_enumerable(dataspec, rewr, arg_sort, parents); });
205 });
206 parents.pop_back();
207 return result;
208 }
209 }
210}
211
212} // namespace detail
213
216{
217 explicit enumerator_error(const std::string& message): mcrl2::runtime_error(message)
218 {}
219};
220
221template <typename Rewriter>
222static bool is_enumerable(const data_specification& dataspec, const Rewriter& rewr, const sort_expression& sort)
223{
224 std::list<sort_expression> parentstack;
225 return detail::is_enumerable(dataspec, rewr, sort, parentstack);
226}
227
229template <typename Expression = data::data_expression>
231{
232 protected:
234 Expression phi;
235
236 public:
237 typedef Expression expression_type;
238
241
244 : v(std::move(v_)), phi(phi_)
245 {}
246
249 const Expression& phi_,
251 )
252 : v(std::move(v_)), phi(phi_)
253 {}
254
257 const Expression& phi_,
259 const data::variable&,
261 )
262 : v(std::move(v_)), phi(phi_)
263 {}
264
266 {
267 return v;
268 }
269
270 const Expression& expression() const
271 {
272 return phi;
273 }
274
275 Expression& expression()
276 {
277 return phi;
278 }
279
280 bool is_solution() const
281 {
282 return v.empty();
283 }
284
287 {
288 phi = data::undefined_data_expression();
289 }
290
293 bool is_valid() const
294 {
295 return phi != data::undefined_data_expression();
296 }
297
303 {
304 mark_term(v,todo);
305 mark_term(phi,todo);
306 }
307
311 void set(const data::variable_list& v_, const Expression& phi_)
312 {
313 v=v_;
314 phi=phi_;
315 }
316
321 void set(const data::variable_list& v_, const Expression& phi_,const enumerator_list_element&)
322 {
323 v=v_;
324 phi=phi_;
325 }
326
332 void set(const data::variable_list& v_,
333 const Expression& phi_,
335 const data::variable&,
337 {
338 v=v_;
339 phi=phi_;
340 }
341
342};
343
346template <typename Expression = data::data_expression>
348{
349 protected:
352
353 public:
354 typedef Expression expression_type;
355
358
361 : enumerator_list_element<Expression>(v, phi)
362 {}
363
366 const Expression& phi,
368 )
369 : enumerator_list_element<Expression>(v, phi),
370 m_variables(elem.m_variables),
371 m_expressions(elem.m_expressions)
372 {
373 }
374
377 const data::variable_list& v,
378 const Expression& phi,
380 const data::variable& d,
381 const data::data_expression& e
382 )
383 : enumerator_list_element<Expression>(v, phi),
384 m_variables(elem.m_variables),
385 m_expressions(elem.m_expressions)
386 {
387 m_variables.push_front(d);
388 m_expressions.push_front(e);
389 }
390
392 template <typename VariableList, typename MutableSubstitution, typename Rewriter>
393 void add_assignments(const VariableList& v, MutableSubstitution& result, const Rewriter& rewriter) const
394 {
395 data::enumerator_substitution sigma(m_variables, m_expressions);
396 sigma.revert();
397 for (const data::variable& v_i: v)
398 {
399 result[v_i] = rewriter(sigma(v_i));
400 }
401 }
402
404 template <typename VariableList, typename MutableSubstitution>
405 void remove_assignments(const VariableList& v, MutableSubstitution& result) const
406 {
407 for (const data::variable& v_i: v)
408 {
409 result[v_i] = v_i;
410 }
411 }
412
415 template <typename VariableList, typename Rewriter>
416 data::data_expression_list assign_expressions(const VariableList& v, const Rewriter& rewriter) const
417 {
418 data::enumerator_substitution sigma(m_variables, m_expressions);
419 sigma.revert();
420 return data_expression_list(v.begin(), v.end(), [&](const data::variable& v_i) { return rewriter(sigma(v_i)); });
421 }
422
424 {
425 return data::enumerator_substitution(m_variables, m_expressions);
426 }
427
432 void mark(std::stack<std::reference_wrapper<atermpp::detail::_aterm>>& todo) const
433 {
434 mark_term(*atermpp::detail::address(m_variables), todo);
435 mark_term(*atermpp::detail::address(m_expressions), todo);
436 static_cast<enumerator_list_element<Expression>>(*this).mark(todo);
437 }
438
442 const Expression& phi,
444 const data::variable& d,
445 const data::data_expression& e)
446 {
448 m_variables=elem.m_variables;
449 m_expressions=elem.m_expressions;
450 m_variables.push_front(d);
451 m_expressions.push_front(e);
452 }
453
457 const Expression& phi,
459 {
461 m_variables=elem.m_variables;
462 m_expressions=elem.m_expressions;
463 }
464};
465
466template <typename Expression>
467std::ostream& operator<<(std::ostream& out, const enumerator_list_element<Expression>& p)
468{
469 out << "{ [";
470 const auto& variables = p.variables();
471 for (auto i = variables.begin(); i != variables.end(); ++i)
472 {
473 if (i != variables.begin())
474 {
475 out << ", ";
476 }
477 out << *i << ": " << i->sort();
478 }
479 return out << "], " << p.expression() << " }";
480}
481
482template <typename Expression>
483std::ostream& operator<<(std::ostream& out, const enumerator_list_element_with_substitution<Expression>& p)
484{
485 out << "{ [";
486 const auto& variables = p.variables();
487 for (auto i = variables.begin(); i != variables.end(); ++i)
488 {
489 if (i != variables.begin())
490 {
491 out << ", ";
492 }
493 out << *i << ": " << i->sort();
494 }
495 return out << "], " << p.expression() << ", " << p.sigma() << " }";
496}
497
499template <typename EnumeratorListElement>
501{
502 protected:
504 EnumeratorListElement m_enumerator_element_cache; // This element is used to temporarily store
505 // information, which is more efficient than
506 // declaring such a variable on the stack
507 // as its protection using a protection set
508 // is expensive.
509
510 public:
511 // The following variables are used for local store, to prevent the
512 // variables to be inserted and removed continuously in a protection set.
513 typename EnumeratorListElement::expression_type scratch_expression;
516
517 typedef EnumeratorListElement value_type;
519
521 enumerator_queue() = default;
522
524 explicit enumerator_queue(const EnumeratorListElement& value)
525 : P({value})
526 { }
527
528 void push_back(const EnumeratorListElement& x)
529 {
530#ifdef MCRL2_LOG_ENUMERATOR
531 std::cout << "push_back " << x << std::endl;
532#endif
533 P.push_back(x);
534 }
535
536 template <class... Args>
537 void emplace_back(Args&&... args)
538 {
539#ifdef MCRL2_LOG_ENUMERATOR
540 std::cout << "emplace_back " << EnumeratorListElement(args...) << std::endl;
541#endif
542 P.emplace_back(std::forward<Args>(args)...);
543 }
544
545 bool empty() const
546 {
547 return P.empty();
548 }
549
550 void clear()
551 {
552 P.clear();
553 }
554
556 {
557 return P.size();
558 }
559
560 const EnumeratorListElement& front() const
561 {
562 return P.front();
563 }
564
565 EnumeratorListElement& front()
566 {
567 return P.front();
568 }
569
570 const EnumeratorListElement& back() const
571 {
572 return P.back();
573 }
574
575 EnumeratorListElement& back()
576 {
577 return P.back();
578 }
579
581 {
582 P.pop_front();
583 }
584
585 void pop_back()
586 {
587 P.pop_back();
588 }
589
590 template <class... Args>
591 const EnumeratorListElement& enumerator_element_cache(const Args&... args)
592 {
593 m_enumerator_element_cache.set(args...);
594 return m_enumerator_element_cache;
595 }
596};
597
599template <typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>
601{
602 protected:
603 // A rewriter
604 const Rewriter& R;
605
608
609 // Needed for enumerate_expressions
610 const DataRewriter& r;
611
612 // A name generator
614
616 std::size_t m_max_count;
617
620
621#ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
622 mutable std::size_t rewrite_calls = 0;
623#endif
624
625 std::string print(const data::variable& x) const
626 {
627 std::ostringstream out;
628 out << x << ": " << x.sort();
629 return out.str();
630 }
631
632 template <typename Expression, typename MutableSubstitution>
633 inline
634 Expression rewrite(const Expression& phi, MutableSubstitution& sigma) const
635 {
636#ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
637 rewrite_calls++;
638#endif
639 return const_cast<Rewriter&>(R)(phi, sigma);
640 }
641
642 template <typename Expression, typename MutableSubstitution>
643 inline
644 void rewrite(Expression& result, const Expression& phi, MutableSubstitution& sigma) const
645 {
646#ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
647 rewrite_calls++;
648#endif
649 const_cast<Rewriter&>(R)(result, phi, sigma);
650 }
651
652 public:
653 enumerator_algorithm(const Rewriter& R_,
654 const data::data_specification& dataspec_,
655 const DataRewriter& datar_,
656 enumerator_identifier_generator& id_generator_,
657 bool accept_solutions_with_variables,
658 std::size_t max_count = (std::numeric_limits<std::size_t>::max)()
659 )
660 : R(R_),
661 dataspec(dataspec_),
662 r(datar_),
663 id_generator(id_generator_),
664 m_max_count(max_count),
665 m_accept_solutions_with_variables(accept_solutions_with_variables)
666 {}
667
669
671 {
672#ifdef MCRL2_ENUMERATOR_COUNT_REWRITE_CALLS
673 std::cout << "number of enumerator rewrite calls: " << rewrite_calls << std::endl;
674#endif
675 }
676
678 {
679 id_generator.clear();
680 }
681
682 template <typename T>
684 {
685 bool operator()(const T&) { return false; }
686 };
687
701 template <typename EnumeratorListElement,
702 typename MutableSubstitution,
703 typename ReportSolution,
704 typename Reject = always_false<typename EnumeratorListElement::expression_type>,
705 typename Accept = always_false<typename EnumeratorListElement::expression_type>
706 >
708 MutableSubstitution& sigma,
709 ReportSolution report_solution,
710 Reject reject = Reject(),
711 Accept accept = Accept()
712 ) const
713 {
714 assert(!P.empty());
715 const EnumeratorListElement& p = P.front();
716
717 auto add_element = [&](const data::variable_list& variables,
718 const typename EnumeratorListElement::expression_type& phi,
719 const data::variable& v,
720 const data::data_expression& e
721 ) -> bool
722 {
724 if (reject(P.scratch_expression))
725 {
726 return false;
727 }
728 if ((accept(P.scratch_expression) && m_accept_solutions_with_variables) || variables.empty())
729 {
730 // EnumeratorListElement q(variables, phi1, p, v, e);
731 // return report_solution(q);
732 return report_solution(P.enumerator_element_cache(variables, P.scratch_expression, p, v, e));
733 }
734 P.emplace_back(variables, P.scratch_expression, p, v, e);
735 return false;
736 };
737
738 auto add_element_with_variables = [&](const data::variable_list& variables,
739 const data::variable_list& added_variables,
740 const typename EnumeratorListElement::expression_type& phi,
741 const data::variable& v,
742 const data::data_expression& e
743 ) -> bool
744 {
746 if (reject(P.scratch_expression))
747 {
748 return false;
749 }
750 bool added_variables_empty = added_variables.empty() || (P.scratch_expression == phi && m_accept_solutions_with_variables);
751 if ((accept(P.scratch_expression) && m_accept_solutions_with_variables) || (variables.empty() && added_variables_empty))
752 {
753 // EnumeratorListElement q(variables + added_variables, phi1, p, v, e);
754 return report_solution(P.enumerator_element_cache(variables + added_variables, P.scratch_expression, p, v, e));
755 }
756 if (added_variables_empty)
757 {
758 P.emplace_back(variables, P.scratch_expression, p, v, e);
759 }
760 else
761 {
762 P.emplace_back(variables + added_variables, P.scratch_expression, p, v, e);
763 }
764 return false;
765 };
766
767 const data::variable_list& v = p.variables();
768 const auto& phi = p.expression();
769
770 if (v.empty())
771 {
773 if (reject(P.scratch_expression))
774 {
775 return false;
776 }
777 // EnumeratorListElement q(v, phi1, p);
778 return report_solution(P.enumerator_element_cache(v, P.scratch_expression, p));
779 }
780
781 const auto& v1 = v.front();
782 const auto& v_tail = v.tail();
783 const auto& v1_sort = v1.sort();
784
785 if (reject(phi))
786 {
787 // skip
788 }
789 else if (data::is_function_sort(v1_sort))
790 {
791 const function_sort& function = atermpp::down_cast<function_sort>(v1_sort);
792 if (dataspec.is_certainly_finite(function))
793 {
794 data_expression_vector function_sorts;
795 variable_list function_parameter_list;
796 bool result = detail::compute_finite_function_sorts(function, id_generator, dataspec, r, function_sorts, function_parameter_list);
797 if (!result)
798 {
799 throw mcrl2::runtime_error("Sort " + data::pp(v1_sort) + " has too many elements to enumerate.");
800 }
801
802 for (const data_expression& f: function_sorts)
803 {
804 sigma[v1] = f;
805 if (add_element(v_tail, phi, v1, f))
806 {
807 sigma[v1] = v1;
808 return true;
809 }
810 }
811 }
812 else
813 {
814 throw mcrl2::runtime_error("Cannot enumerate elements of function sort " + data::pp(v1_sort) + ".");
815 }
816 }
817 else if (sort_set::is_set(v1_sort))
818 {
819 const sort_expression& element_sort = atermpp::down_cast<container_sort>(v1_sort).element_sort();
820 if (dataspec.is_certainly_finite(element_sort))
821 {
822 const data_expression lambda_term = abstraction(lambda_binder(), { variable(id_generator(), element_sort) }, sort_bool::false_());
823 const variable fset_variable(id_generator(), sort_fset::fset(element_sort));
824 data_expression e = sort_set::constructor(element_sort, lambda_term, fset_variable);
825 sigma[v1] = e;
826 if (add_element_with_variables(v_tail, { fset_variable }, phi, v1, e))
827 {
828 sigma[v1] = v1;
829 return true;
830 }
831 }
832 else
833 {
834 throw mcrl2::runtime_error("Cannot enumerate elements of set sort " + data::pp(v1_sort) + ".");
835 }
836 }
837 else if (sort_fset::is_fset(v1_sort))
838 {
839 const auto& fset = atermpp::down_cast<container_sort>(v1_sort);
840 if (dataspec.is_certainly_finite(fset.element_sort()))
841 {
842 data_expression_vector set_elements;
843 bool result = detail::compute_finite_set_elements(fset, dataspec, r, sigma, set_elements, id_generator);
844 if (!result)
845 {
846 throw mcrl2::runtime_error("Finite set sort " + data::pp(v1_sort) + " has too many elements to enumerate.");
847 }
848
849 for (const data_expression& e: set_elements)
850 {
851 sigma[v1] = e;
852 if (add_element(v_tail, phi, v1, e))
853 {
854 sigma[v1] = v1;
855 return true;
856 }
857 }
858 }
859 else
860 {
861 throw mcrl2::runtime_error("Cannot enumerate elements of finite set sort " + data::pp(v1_sort) + ".");
862 }
863 }
864 else if (sort_bag::is_bag(v1_sort))
865 {
866 throw mcrl2::runtime_error("Cannot enumerate elements of bag sort " + data::pp(v1_sort) + ".");
867 }
868 else if (sort_fbag::is_fbag(v1_sort))
869 {
870 throw mcrl2::runtime_error("Cannot enumerate elements of finite bag sort " + data::pp(v1_sort) + ".");
871 }
872 else
873 {
874 const function_symbol_vector& C = dataspec.constructors(v1_sort);
875 if (!C.empty())
876 {
877 for (const function_symbol& c: C)
878 {
879 if (data::is_function_sort(c.sort()))
880 {
881 const sort_expression_list& domain = atermpp::down_cast<data::function_sort>(c.sort()).domain();
883 domain.begin(),
884 domain.end(),
885 [&](const data::sort_expression& s) { return data::variable(id_generator(), s); });
886 // data_expression cy = r(application(c, y.begin(), y.end()));
887 // below sigma is not used, but it prevents generating a dummy sigma.
890 if (add_element_with_variables(v_tail, P.scratch_variable_list, phi, v1, P.scratch_data_expression))
891 {
892 sigma[v1] = v1;
893 return true;
894 }
895 }
896 else
897 {
898 // const data_expression e1 = r(c);
899 r(P.scratch_data_expression,c,sigma); // sigma is not used, but in this way no dummy sigma needs to be created.
901 if (add_element(v_tail, phi, v1, P.scratch_data_expression))
902 {
903 sigma[v1] = v1;
904 return true;
905 }
906 }
907 }
908 }
909 else
910 {
911 throw mcrl2::runtime_error("Cannot enumerate elements of sort " + data::pp(v1_sort) + " without constructors.");
912 }
913 }
914 sigma[v1] = v1;
915 return false;
916 }
917
930 template <typename EnumeratorListElement,
931 typename MutableSubstitution,
932 typename ReportSolution,
933 typename Reject = always_false<typename EnumeratorListElement::expression_type>,
934 typename Accept = always_false<typename EnumeratorListElement::expression_type>
935 >
937 MutableSubstitution& sigma,
938 ReportSolution report_solution,
939 Reject reject = Reject(),
940 Accept accept = Accept()
941 ) const
942 {
943 std::size_t count = 0;
944 while (!P.empty())
945 {
946 if (count++ >= m_max_count)
947 {
948 break;
949 }
950 if (enumerate_front(P, sigma, report_solution, reject, accept))
951 {
952 break;
953 }
954 P.pop_front();
955 }
956 return count;
957 }
958
971 template <typename EnumeratorListElement,
972 typename MutableSubstitution,
973 typename ReportSolution,
974 typename Reject = always_false<typename EnumeratorListElement::expression_type>,
975 typename Accept = always_false<typename EnumeratorListElement::expression_type>
976 >
977 std::size_t enumerate(const EnumeratorListElement& p,
978 MutableSubstitution& sigma,
979 ReportSolution report_solution,
980 Reject reject = Reject(),
981 Accept accept = Accept()
982 ) const
983 {
985 return enumerate_all(P, sigma, report_solution, reject, accept);
986 }
987
1000 template <typename EnumeratorListElement,
1001 typename MutableSubstitution,
1002 typename ReportSolution,
1003 typename Reject = always_false<typename EnumeratorListElement::expression_type>,
1004 typename Accept = always_false<typename EnumeratorListElement::expression_type>
1005 >
1006 std::size_t enumerate(const variable_list& vars,
1007 const typename EnumeratorListElement::expression_type& cond,
1008 MutableSubstitution& sigma,
1009 ReportSolution report_solution,
1010 Reject reject = Reject(),
1011 Accept accept = Accept()
1012 ) const
1013 {
1015 P.emplace_back(vars, cond);
1016 return enumerate_all(P, sigma, report_solution, reject, accept);
1017 }
1018
1019 std::size_t max_count() const
1020 {
1021 return m_max_count;
1022 }
1023};
1024
1031template <class Rewriter>
1033 const data_specification& dataspec,
1034 const Rewriter& rewr,
1035 enumerator_identifier_generator& id_generator)
1036{
1037 typedef typename Rewriter::term_type term_type;
1039 assert(dataspec.is_certainly_finite(s));
1040
1041 bool accept_solutions_with_variables = false;
1042 enumerator_algorithm<Rewriter, Rewriter> E(rewr, dataspec, rewr, id_generator, accept_solutions_with_variables);
1045 const variable v("@var@", s);
1046 const variable_list v_list{ v };
1047 E.template enumerate<enumerator_element>(
1048 v_list,
1049 sort_bool::true_(),
1050 sigma,
1051 [&](const enumerator_element& p)
1052 {
1053 p.add_assignments(v_list, sigma, rewr);
1054 result.push_back(sigma(v));
1055 return false;
1056 }
1057 );
1058 return result;
1059}
1060
1066template <class Rewriter>
1068 const data_specification& dataspec,
1069 const Rewriter& rewr)
1070{
1072 return enumerate_expressions(s, dataspec, rewr, id_generator);
1073}
1074
1075} // namespace data
1076
1077} // namespace mcrl2
1078
1079#endif // MCRL2_DATA_ENUMERATOR_H
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
A deque class in which aterms can be stored.
Definition deque.h:34
void pop_back()
Definition deque.h:202
std::size_t size() const
Definition deque.h:239
reference emplace_back(Args &&... args)
Definition deque.h:196
void clear() noexcept
Definition deque.h:126
void push_back(const T &value)
Definition deque.h:183
super::size_type size_type
Definition deque.h:45
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
An abstraction expression.
Definition abstraction.h:26
An application of a data expression to a number of arguments.
\brief A container sort
const sort_expression & element_sort() const
bool is_certainly_finite(const sort_expression &s) const
Checks whether a sort is certainly finite.
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
Rewriter interface class.
Definition rewrite.h:42
An enumerator algorithm that generates solutions of a condition.
Definition enumerator.h:601
void rewrite(Expression &result, const Expression &phi, MutableSubstitution &sigma) const
Definition enumerator.h:644
enumerator_identifier_generator & id_generator
Definition enumerator.h:613
std::size_t m_max_count
max_count The enumeration is aborted after max_count iterations
Definition enumerator.h:616
std::size_t enumerate(const EnumeratorListElement &p, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
Enumerates the element p. Solutions are reported using the callback function report_solution....
Definition enumerator.h:977
enumerator_algorithm(const enumerator_algorithm< Rewriter, DataRewriter > &)=delete
std::size_t enumerate(const variable_list &vars, const typename EnumeratorListElement::expression_type &cond, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
Enumerates the variables v for condition c. Solutions are reported using the callback function report...
bool enumerate_front(enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
Enumerates the front element of the todo list P. The enumeration is interrupted when report_solution ...
Definition enumerator.h:707
std::string print(const data::variable &x) const
Definition enumerator.h:625
bool m_accept_solutions_with_variables
If true, solutions with a non-empty list of variables may be reported.
Definition enumerator.h:619
const data::data_specification & dataspec
A data specification.
Definition enumerator.h:607
std::size_t enumerate_all(enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
Enumerates until P is empty. Solutions are reported using the callback function report_solution....
Definition enumerator.h:936
enumerator_algorithm(const Rewriter &R_, const data::data_specification &dataspec_, const DataRewriter &datar_, enumerator_identifier_generator &id_generator_, bool accept_solutions_with_variables, std::size_t max_count=(std::numeric_limits< std::size_t >::max)())
Definition enumerator.h:653
Expression rewrite(const Expression &phi, MutableSubstitution &sigma) const
Definition enumerator.h:634
An element for the todo list of the enumerator that collects the substitution corresponding to the ex...
Definition enumerator.h:348
enumerator_list_element_with_substitution(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem, const data::variable &d, const data::data_expression &e)
Constructs the element (v, phi, e.sigma[v := x])
Definition enumerator.h:376
data::data_expression_list assign_expressions(const VariableList &v, const Rewriter &rewriter) const
Returns the right hand sides corresponding to the variables v.
Definition enumerator.h:416
enumerator_list_element_with_substitution(const data::variable_list &v, const Expression &phi)
Constructs the element (v, phi, [])
Definition enumerator.h:360
void remove_assignments(const VariableList &v, MutableSubstitution &result) const
Removes the assignments corresponding with this element from the substitution result.
Definition enumerator.h:405
void set(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem, const data::variable &d, const data::data_expression &e)
Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
Definition enumerator.h:441
void add_assignments(const VariableList &v, MutableSubstitution &result, const Rewriter &rewriter) const
Adds the assignments that correspond with this element to the substitution result.
Definition enumerator.h:393
void set(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem)
Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
Definition enumerator.h:456
void mark(std::stack< std::reference_wrapper< atermpp::detail::_aterm > > &todo) const
The following function is needed to mark the aterms in this class, when elements of this class are us...
Definition enumerator.h:432
data::enumerator_substitution sigma() const
Definition enumerator.h:423
enumerator_list_element_with_substitution(const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem)
Constructs the element (v, phi, e.sigma[v := x])
Definition enumerator.h:365
enumerator_list_element_with_substitution()=default
Default constructor.
The default element for the todo list of the enumerator.
Definition enumerator.h:231
enumerator_list_element(data::variable_list v_, const Expression &phi_, const enumerator_list_element &, const data::variable &, const data::data_expression &)
Constructs the element (v, phi)
Definition enumerator.h:256
void set(const data::variable_list &v_, const Expression &phi_)
Set the variables and the condition explicitly.
Definition enumerator.h:311
enumerator_list_element(data::variable_list v_, const Expression &phi_)
Constructs the element (v, phi)
Definition enumerator.h:243
enumerator_list_element(data::variable_list v_, const Expression &phi_, const enumerator_list_element &)
Constructs the element (v, phi)
Definition enumerator.h:248
bool is_valid() const
Returns true if the element is valid. If it becomes false, this is used to signal that the enumeratio...
Definition enumerator.h:293
void set(const data::variable_list &v_, const Expression &phi_, const enumerator_list_element &, const data::variable &, const data::data_expression &)
Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
Definition enumerator.h:332
enumerator_list_element()=default
Default constructor.
void mark(atermpp::term_mark_stack &todo) const
The following function is needed to mark the aterms in this class, when elements of this class are us...
Definition enumerator.h:302
void set(const data::variable_list &v_, const Expression &phi_, const enumerator_list_element &)
Set the variables and the condition explicitly.
Definition enumerator.h:321
void invalidate()
Invalidates the element, by giving phi an undefined value.
Definition enumerator.h:286
const data::variable_list & variables() const
Definition enumerator.h:265
const Expression & expression() const
Definition enumerator.h:270
Contains the enumerator queue.
Definition enumerator.h:501
atermpp::deque< EnumeratorListElement > P
Definition enumerator.h:503
atermpp::deque< EnumeratorListElement >::size_type size() const
Definition enumerator.h:555
enumerator_queue()=default
Default constructor.
const EnumeratorListElement & enumerator_element_cache(const Args &... args)
Definition enumerator.h:591
atermpp::deque< EnumeratorListElement >::size_type size_type
Definition enumerator.h:518
EnumeratorListElement::expression_type scratch_expression
Definition enumerator.h:513
variable_list scratch_variable_list
Definition enumerator.h:515
const EnumeratorListElement & back() const
Definition enumerator.h:570
void push_back(const EnumeratorListElement &x)
Definition enumerator.h:528
void emplace_back(Args &&... args)
Definition enumerator.h:537
EnumeratorListElement m_enumerator_element_cache
Definition enumerator.h:504
EnumeratorListElement & back()
Definition enumerator.h:575
EnumeratorListElement & front()
Definition enumerator.h:565
enumerator_queue(const EnumeratorListElement &value)
Initializes the enumerator queue with the given value.
Definition enumerator.h:524
EnumeratorListElement value_type
Definition enumerator.h:517
data_expression scratch_data_expression
Definition enumerator.h:514
const EnumeratorListElement & front() const
Definition enumerator.h:560
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
\brief Binder for lambda abstraction
Rewriter that operates on data expressions.
Definition rewriter.h:81
\brief A sort expression
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
The class rewriter.
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
static void rewrite(data_expression &result, const data_expression &t, RewriterCompilingJitty *this_rewriter)
@ func
Definition linearise.cpp:77
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
_aterm * address(const unprotected_aterm_core &t)
Definition aterm_core.h:239
void make_term_list(term_list< Term > &target)
Make an empty list and put it in target;.
Definition aterm_list.h:314
std::stack< std::reference_wrapper< detail::_aterm > > term_mark_stack
data_expression make_if_expression_(std::size_t &function_index, const std::size_t argument_index, const std::vector< data_expression_vector > &data_domain_expressions, const data_expression_vector &codomain_expressions, const variable_vector &parameters)
Definition enumerator.h:47
bool is_enumerable(const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort, std::list< sort_expression > &parents)
Definition enumerator.h:159
data_expression make_set_(std::size_t function_index, const sort_expression &element_sort, const data_expression_vector &set_elements)
Definition enumerator.h:32
bool compute_finite_function_sorts(const function_sort &sort, enumerator_identifier_generator &id_generator, const data::data_specification &dataspec, Rewriter datar, data_expression_vector &result, variable_list &function_parameter_list)
Computes the elements of a finite function sort, and puts them in result. If there are too many eleme...
Definition enumerator.h:109
bool compute_finite_set_elements(const container_sort &sort, const data_specification &dataspec, Rewriter datar, MutableSubstitution &sigma, data_expression_vector &result, enumerator_identifier_generator &id_generator)
Computes the elements of a finite set sort, and puts them in result. If there are too many elements,...
Definition enumerator.h:82
bool is_bag(const sort_expression &e)
Recogniser for sort expression Bag(s)
Definition bag1.h:55
bool is_fbag(const sort_expression &e)
Recogniser for sort expression FBag(s)
Definition fbag1.h:54
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:107
bool is_fset(const sort_expression &e)
Recogniser for sort expression FSet(s)
Definition fset1.h:52
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
bool is_set(const sort_expression &e)
Recogniser for sort expression Set(s)
Definition set1.h:53
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
data_expression_vector enumerate_expressions(const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr, enumerator_identifier_generator &id_generator)
Returns a vector with all expressions of sort s.
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
atermpp::term_list< variable > variable_list
\brief list of variables
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
@ warning
Definition logger.h:32
std::size_t power_size_t(const std::size_t n_in, const std::size_t m_in)
Definition math.h:42
std::size_t ceil_log2(std::size_t n)
Definition math.h:28
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
Enumerator exception.
Definition enumerator.h:216
enumerator_error(const std::string &message)
Definition enumerator.h:217
Substitution that stores the assignments as a sequence of variables and a sequence of expressions....