spot 2.11.6.dev
Loading...
Searching...
No Matches
acc.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement
3// de l'Epita.
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <functional>
23#include <sstream>
24#include <vector>
25#include <iostream>
26#include <algorithm>
27#include <numeric>
28#include <bddx.h>
29#include <tuple>
30#include <spot/misc/_config.h>
31#include <spot/misc/bitset.hh>
32#include <spot/misc/trival.hh>
33
34namespace spot
35{
36 namespace internal
37 {
38 class mark_container;
39
40 template<bool>
41 struct _32acc {};
42 template<>
43 struct _32acc<true>
44 {
45 SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
46 typedef unsigned value_t;
47 };
48 }
49
52
61 class SPOT_API acc_cond
62 {
63#ifndef SWIG
64 private:
65 [[noreturn]] static void report_too_many_sets();
66#endif
67 public:
68
83 struct mark_t :
84 public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
85 {
86 private:
87 // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
88 typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
89 _value_t id;
90
91 mark_t(_value_t id) noexcept
92 : id(id)
93 {
94 }
95
96 public:
98 mark_t() = default;
99
100#ifndef SWIG
102 template<class iterator>
103 mark_t(const iterator& begin, const iterator& end)
104 : mark_t(_value_t::zero())
105 {
106 for (iterator i = begin; i != end; ++i)
107 if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
108 set(*i);
109 else
110 report_too_many_sets();
111 }
112
114 mark_t(std::initializer_list<unsigned> vals)
115 : mark_t(vals.begin(), vals.end())
116 {
117 }
118
119 SPOT_DEPRECATED("use brace initialization instead")
120 mark_t(unsigned i)
121 {
122 unsigned j = 0;
123 while (i)
124 {
125 if (i & 1U)
126 this->set(j);
127 ++j;
128 i >>= 1;
129 }
130 }
131#endif
132
138 constexpr static unsigned max_accsets()
139 {
140 return SPOT_MAX_ACCSETS;
141 }
142
148 static mark_t all()
149 {
150 return mark_t(_value_t::mone());
151 }
152
153 size_t hash() const noexcept
154 {
155 std::hash<decltype(id)> h;
156 return h(id);
157 }
158
159 SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
160 bool operator==(unsigned o) const
161 {
162 SPOT_ASSERT(o == 0U);
163 (void)o;
164 return !id;
165 }
166
167 SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
168 bool operator!=(unsigned o) const
169 {
170 SPOT_ASSERT(o == 0U);
171 (void)o;
172 return !!id;
173 }
174
175 bool operator==(mark_t o) const
176 {
177 return id == o.id;
178 }
179
180 bool operator!=(mark_t o) const
181 {
182 return id != o.id;
183 }
184
185 bool operator<(mark_t o) const
186 {
187 return id < o.id;
188 }
189
190 bool operator<=(mark_t o) const
191 {
192 return id <= o.id;
193 }
194
195 bool operator>(mark_t o) const
196 {
197 return id > o.id;
198 }
199
200 bool operator>=(mark_t o) const
201 {
202 return id >= o.id;
203 }
204
205 explicit operator bool() const
206 {
207 return !!id;
208 }
209
210 bool has(unsigned u) const
211 {
212 return !!this->operator&(mark_t({0}) << u);
213 }
214
215 void set(unsigned u)
216 {
217 id.set(u);
218 }
219
220 void clear(unsigned u)
221 {
222 id.clear(u);
223 }
224
225 mark_t& operator&=(mark_t r)
226 {
227 id &= r.id;
228 return *this;
229 }
230
231 mark_t& operator|=(mark_t r)
232 {
233 id |= r.id;
234 return *this;
235 }
236
237 mark_t& operator-=(mark_t r)
238 {
239 id &= ~r.id;
240 return *this;
241 }
242
243 mark_t& operator^=(mark_t r)
244 {
245 id ^= r.id;
246 return *this;
247 }
248
249 mark_t operator&(mark_t r) const
250 {
251 return id & r.id;
252 }
253
254 mark_t operator|(mark_t r) const
255 {
256 return id | r.id;
257 }
258
259 mark_t operator-(mark_t r) const
260 {
261 return id & ~r.id;
262 }
263
264 mark_t operator~() const
265 {
266 return ~id;
267 }
268
269 mark_t operator^(mark_t r) const
270 {
271 return id ^ r.id;
272 }
273
274#if SPOT_DEBUG || defined(SWIGPYTHON)
275# define SPOT_WRAP_OP(ins) \
276 try \
277 { \
278 ins; \
279 } \
280 catch (const std::runtime_error& e) \
281 { \
282 report_too_many_sets(); \
283 }
284#else
285# define SPOT_WRAP_OP(ins) ins;
286#endif
287 mark_t operator<<(unsigned i) const
288 {
289 SPOT_WRAP_OP(return id << i);
290 }
291
292 mark_t& operator<<=(unsigned i)
293 {
294 SPOT_WRAP_OP(id <<= i; return *this);
295 }
296
297 mark_t operator>>(unsigned i) const
298 {
299 SPOT_WRAP_OP(return id >> i);
300 }
301
302 mark_t& operator>>=(unsigned i)
303 {
304 SPOT_WRAP_OP(id >>= i; return *this);
305 }
306#undef SPOT_WRAP_OP
307
308 mark_t strip(mark_t y) const
309 {
310 // strip every bit of id that is marked in y
311 // 100101110100.strip(
312 // 001011001000)
313 // == 10 1 11 100
314 // == 10111100
315
316 auto xv = id; // 100101110100
317 auto yv = y.id; // 001011001000
318
319 while (yv && xv)
320 {
321 // Mask for everything after the last 1 in y
322 auto rm = (~yv) & (yv - 1); // 000000000111
323 // Mask for everything before the last 1 in y
324 auto lm = ~(yv ^ (yv - 1)); // 111111110000
325 xv = ((xv & lm) >> 1) | (xv & rm);
326 yv = (yv & lm) >> 1;
327 }
328 return xv;
329 }
330
333 bool subset(mark_t m) const
334 {
335 return !((*this) - m);
336 }
337
340 bool proper_subset(mark_t m) const
341 {
342 return *this != m && this->subset(m);
343 }
344
346 unsigned count() const
347 {
348 return id.count();
349 }
350
355 unsigned max_set() const
356 {
357 if (id)
358 return id.highest()+1;
359 else
360 return 0;
361 }
362
367 unsigned min_set() const
368 {
369 if (id)
370 return id.lowest()+1;
371 else
372 return 0;
373 }
374
380 {
381 return id & -id;
382 }
383
385 bool is_singleton() const
386 {
387#if __GNUC__
388 /* With GCC and Clang, count() is implemented using popcount. */
389 return count() == 1;
390#else
391 return id && !(id & (id - 1));
392#endif
393 }
394
396 bool has_many() const
397 {
398#if __GNUC__
399 /* With GCC and Clang, count() is implemented using popcount. */
400 return count() > 1;
401#else
402 return !!(id & (id - 1));
403#endif
404 }
405
409 mark_t& remove_some(unsigned n)
410 {
411 while (n--)
412 id &= id - 1;
413 return *this;
414 }
415
417 template<class iterator>
418 void fill(iterator here) const
419 {
420 auto a = *this;
421 unsigned level = 0;
422 while (a)
423 {
424 if (a.has(0))
425 *here++ = level;
426 ++level;
427 a >>= 1;
428 }
429 }
430
432 spot::internal::mark_container sets() const;
433
434 SPOT_API
435 friend std::ostream& operator<<(std::ostream& os, mark_t m);
436
437 std::string as_string() const
438 {
439 std::ostringstream os;
440 os << *this;
441 return os.str();
442 }
443 };
444
446 enum class acc_op : unsigned short
447 { Inf, Fin, InfNeg, FinNeg, And, Or };
448
457 {
458 mark_t mark;
459 struct {
460 acc_op op; // Operator
461 unsigned short size; // Size of the subtree (number of acc_word),
462 // not counting this node.
463 } sub;
464 };
465
478 struct SPOT_API acc_code: public std::vector<acc_word>
479 {
481 unit_propagation();
482
483 bool operator==(const acc_code& other) const
484 {
485 // We have two ways to represent t, unfortunately.
486 if (is_t() && other.is_t())
487 return true;
488 unsigned pos = size();
489 if (other.size() != pos)
490 return false;
491 while (pos > 0)
492 {
493 auto op = (*this)[pos - 1].sub.op;
494 auto sz = (*this)[pos - 1].sub.size;
495 if (other[pos - 1].sub.op != op ||
496 other[pos - 1].sub.size != sz)
497 return false;
498 switch (op)
499 {
500 case acc_cond::acc_op::And:
501 case acc_cond::acc_op::Or:
502 --pos;
503 break;
504 case acc_cond::acc_op::Inf:
505 case acc_cond::acc_op::InfNeg:
506 case acc_cond::acc_op::Fin:
507 case acc_cond::acc_op::FinNeg:
508 pos -= 2;
509 if (other[pos].mark != (*this)[pos].mark)
510 return false;
511 break;
512 }
513 }
514 return true;
515 };
516
517 bool operator<(const acc_code& other) const
518 {
519 // We have two ways to represent t, unfortunately.
520 if (is_t() && other.is_t())
521 return false;
522 unsigned pos = size();
523 auto osize = other.size();
524 if (pos < osize)
525 return true;
526 if (pos > osize)
527 return false;
528 while (pos > 0)
529 {
530 auto op = (*this)[pos - 1].sub.op;
531 auto oop = other[pos - 1].sub.op;
532 if (op < oop)
533 return true;
534 if (op > oop)
535 return false;
536 auto sz = (*this)[pos - 1].sub.size;
537 auto osz = other[pos - 1].sub.size;
538 if (sz < osz)
539 return true;
540 if (sz > osz)
541 return false;
542 switch (op)
543 {
544 case acc_cond::acc_op::And:
545 case acc_cond::acc_op::Or:
546 --pos;
547 break;
548 case acc_cond::acc_op::Inf:
549 case acc_cond::acc_op::InfNeg:
550 case acc_cond::acc_op::Fin:
551 case acc_cond::acc_op::FinNeg:
552 {
553 pos -= 2;
554 auto m = (*this)[pos].mark;
555 auto om = other[pos].mark;
556 if (m < om)
557 return true;
558 if (m > om)
559 return false;
560 break;
561 }
562 }
563 }
564 return false;
565 }
566
567 bool operator>(const acc_code& other) const
568 {
569 return other < *this;
570 }
571
572 bool operator<=(const acc_code& other) const
573 {
574 return !(other < *this);
575 }
576
577 bool operator>=(const acc_code& other) const
578 {
579 return !(*this < other);
580 }
581
582 bool operator!=(const acc_code& other) const
583 {
584 return !(*this == other);
585 }
586
591 bool is_t() const
592 {
593 // We store "t" as an empty condition, or as Inf({}).
594 unsigned s = size();
595 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
596 && !((*this)[s - 2].mark));
597 }
598
605 bool is_f() const
606 {
607 // We store "f" as Fin({}).
608 unsigned s = size();
609 return s > 1
610 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
611 }
612
619 static acc_code f()
620 {
621 acc_code res;
622 res.resize(2);
623 res[0].mark = {};
624 res[1].sub.op = acc_op::Fin;
625 res[1].sub.size = 1;
626 return res;
627 }
628
633 static acc_code t()
634 {
635 return {};
636 }
637
646 {
647 acc_code res;
648 res.resize(2);
649 res[0].mark = m;
650 res[1].sub.op = acc_op::Fin;
651 res[1].sub.size = 1;
652 return res;
653 }
654
655 static acc_code fin(std::initializer_list<unsigned> vals)
656 {
657 return fin(mark_t(vals));
658 }
660
678 {
679 acc_code res;
680 res.resize(2);
681 res[0].mark = m;
682 res[1].sub.op = acc_op::FinNeg;
683 res[1].sub.size = 1;
684 return res;
685 }
686
687 static acc_code fin_neg(std::initializer_list<unsigned> vals)
688 {
689 return fin_neg(mark_t(vals));
690 }
692
702 {
703 acc_code res;
704 res.resize(2);
705 res[0].mark = m;
706 res[1].sub.op = acc_op::Inf;
707 res[1].sub.size = 1;
708 return res;
709 }
710
711 static acc_code inf(std::initializer_list<unsigned> vals)
712 {
713 return inf(mark_t(vals));
714 }
716
734 {
735 acc_code res;
736 res.resize(2);
737 res[0].mark = m;
738 res[1].sub.op = acc_op::InfNeg;
739 res[1].sub.size = 1;
740 return res;
741 }
742
743 static acc_code inf_neg(std::initializer_list<unsigned> vals)
744 {
745 return inf_neg(mark_t(vals));
746 }
748
753 {
754 return inf({0});
755 }
756
761 {
762 return fin({0});
763 }
764
770 static acc_code generalized_buchi(unsigned n)
771 {
772 if (n == 0)
773 return inf({});
774 acc_cond::mark_t m = mark_t::all();
775 m >>= mark_t::max_accsets() - n;
776 return inf(m);
777 }
778
785 {
786 if (n == 0)
787 return fin({});
788 acc_cond::mark_t m = mark_t::all();
789 m >>= mark_t::max_accsets() - n;
790 return fin(m);
791 }
792
797 static acc_code rabin(unsigned n)
798 {
799 acc_cond::acc_code res = f();
800 while (n > 0)
801 {
802 res |= inf({2*n - 1}) & fin({2*n - 2});
803 --n;
804 }
805 return res;
806 }
807
812 static acc_code streett(unsigned n)
813 {
814 acc_cond::acc_code res = t();
815 while (n > 0)
816 {
817 res &= inf({2*n - 1}) | fin({2*n - 2});
818 --n;
819 }
820 return res;
821 }
822
835 template<class Iterator>
836 static acc_code generalized_rabin(Iterator begin, Iterator end)
837 {
838 acc_cond::acc_code res = f();
839 unsigned n = 0;
840 for (Iterator i = begin; i != end; ++i)
841 {
842 unsigned f = n++;
843 acc_cond::mark_t m = {};
844 for (unsigned ni = *i; ni > 0; --ni)
845 m.set(n++);
846 auto pair = inf(m) & fin({f});
847 std::swap(pair, res);
848 res |= std::move(pair);
849 }
850 return res;
851 }
852
860 static acc_code parity(bool is_max, bool is_odd, unsigned sets);
861 static acc_code parity_max(bool is_odd, unsigned sets)
862 {
863 return parity(true, is_odd, sets);
864 }
865 static acc_code parity_max_odd(unsigned sets)
866 {
867 return parity_max(true, sets);
868 }
869 static acc_code parity_max_even(unsigned sets)
870 {
871 return parity_max(false, sets);
872 }
873 static acc_code parity_min(bool is_odd, unsigned sets)
874 {
875 return parity(false, is_odd, sets);
876 }
877 static acc_code parity_min_odd(unsigned sets)
878 {
879 return parity_min(true, sets);
880 }
881 static acc_code parity_min_even(unsigned sets)
882 {
883 return parity_min(false, sets);
884 }
886
903 static acc_code random(unsigned n, double reuse = 0.0);
904
907 {
908 if (is_t() || r.is_f())
909 {
910 *this = r;
911 return *this;
912 }
913 if (is_f() || r.is_t())
914 return *this;
915 unsigned s = size() - 1;
916 unsigned rs = r.size() - 1;
917 // We want to group all Inf(x) operators:
918 // Inf(a) & Inf(b) = Inf(a & b)
919 if (((*this)[s].sub.op == acc_op::Inf
920 && r[rs].sub.op == acc_op::Inf)
921 || ((*this)[s].sub.op == acc_op::InfNeg
922 && r[rs].sub.op == acc_op::InfNeg))
923 {
924 (*this)[s - 1].mark |= r[rs - 1].mark;
925 return *this;
926 }
927
928 // In the more complex scenarios, left and right may both
929 // be conjunctions, and Inf(x) might be a member of each
930 // side. Find it if it exists.
931 // left_inf points to the left Inf mark if any.
932 // right_inf points to the right Inf mark if any.
933 acc_word* left_inf = nullptr;
934 if ((*this)[s].sub.op == acc_op::And)
935 {
936 auto start = &(*this)[s] - (*this)[s].sub.size;
937 auto pos = &(*this)[s] - 1;
938 pop_back();
939 while (pos > start)
940 {
941 if (pos->sub.op == acc_op::Inf)
942 {
943 left_inf = pos - 1;
944 break;
945 }
946 pos -= pos->sub.size + 1;
947 }
948 }
949 else if ((*this)[s].sub.op == acc_op::Inf)
950 {
951 left_inf = &(*this)[s - 1];
952 }
953
954 const acc_word* right_inf = nullptr;
955 auto right_end = &r.back();
956 if (right_end->sub.op == acc_op::And)
957 {
958 auto start = &r[0];
959 auto pos = --right_end;
960 while (pos > start)
961 {
962 if (pos->sub.op == acc_op::Inf)
963 {
964 right_inf = pos - 1;
965 break;
966 }
967 pos -= pos->sub.size + 1;
968 }
969 }
970 else if (right_end->sub.op == acc_op::Inf)
971 {
972 right_inf = right_end - 1;
973 }
974
975 acc_cond::mark_t carry = {};
976 if (left_inf && right_inf)
977 {
978 carry = left_inf->mark;
979 auto pos = left_inf - &(*this)[0];
980 erase(begin() + pos, begin() + pos + 2);
981 }
982 auto sz = size();
983 insert(end(), &r[0], right_end + 1);
984 if (carry)
985 (*this)[sz + (right_inf - &r[0])].mark |= carry;
986
987 acc_word w;
988 w.sub.op = acc_op::And;
989 w.sub.size = size();
990 emplace_back(w);
991 return *this;
992 }
993
996 {
997 acc_code res = *this;
998 res &= r;
999 return res;
1000 }
1001
1002#ifndef SWIG
1005 {
1006 acc_code res = *this;
1007 res &= r;
1008 return res;
1009 }
1010#endif // SWIG
1011
1014 {
1015 if (is_t() || r.is_f())
1016 return *this;
1017 if (is_f() || r.is_t())
1018 {
1019 *this = r;
1020 return *this;
1021 }
1022 unsigned s = size() - 1;
1023 unsigned rs = r.size() - 1;
1024 // Fin(a) | Fin(b) = Fin(a | b)
1025 if (((*this)[s].sub.op == acc_op::Fin
1026 && r[rs].sub.op == acc_op::Fin)
1027 || ((*this)[s].sub.op == acc_op::FinNeg
1028 && r[rs].sub.op == acc_op::FinNeg))
1029 {
1030 (*this)[s - 1].mark |= r[rs - 1].mark;
1031 return *this;
1032 }
1033
1034 // In the more complex scenarios, left and right may both
1035 // be disjunctions, and Fin(x) might be a member of each
1036 // side. Find it if it exists.
1037 // left_inf points to the left Inf mark if any.
1038 // right_inf points to the right Inf mark if any.
1039 acc_word* left_fin = nullptr;
1040 if ((*this)[s].sub.op == acc_op::Or)
1041 {
1042 auto start = &(*this)[s] - (*this)[s].sub.size;
1043 auto pos = &(*this)[s] - 1;
1044 pop_back();
1045 while (pos > start)
1046 {
1047 if (pos->sub.op == acc_op::Fin)
1048 {
1049 left_fin = pos - 1;
1050 break;
1051 }
1052 pos -= pos->sub.size + 1;
1053 }
1054 }
1055 else if ((*this)[s].sub.op == acc_op::Fin)
1056 {
1057 left_fin = &(*this)[s - 1];
1058 }
1059
1060 const acc_word* right_fin = nullptr;
1061 auto right_end = &r.back();
1062 if (right_end->sub.op == acc_op::Or)
1063 {
1064 auto start = &r[0];
1065 auto pos = --right_end;
1066 while (pos > start)
1067 {
1068 if (pos->sub.op == acc_op::Fin)
1069 {
1070 right_fin = pos - 1;
1071 break;
1072 }
1073 pos -= pos->sub.size + 1;
1074 }
1075 }
1076 else if (right_end->sub.op == acc_op::Fin)
1077 {
1078 right_fin = right_end - 1;
1079 }
1080
1081 acc_cond::mark_t carry = {};
1082 if (left_fin && right_fin)
1083 {
1084 carry = left_fin->mark;
1085 auto pos = (left_fin - &(*this)[0]);
1086 this->erase(begin() + pos, begin() + pos + 2);
1087 }
1088 auto sz = size();
1089 insert(end(), &r[0], right_end + 1);
1090 if (carry)
1091 (*this)[sz + (right_fin - &r[0])].mark |= carry;
1092 acc_word w;
1093 w.sub.op = acc_op::Or;
1094 w.sub.size = size();
1095 emplace_back(w);
1096 return *this;
1097 }
1098
1099#ifndef SWIG
1102 {
1103 acc_code res = *this;
1104 res |= r;
1105 return res;
1106 }
1107#endif // SWIG
1108
1111 {
1112 acc_code res = *this;
1113 res |= r;
1114 return res;
1115 }
1116
1122 acc_code& operator<<=(unsigned sets)
1123 {
1124 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1125 report_too_many_sets();
1126 if (empty())
1127 return *this;
1128 unsigned pos = size();
1129 do
1130 {
1131 switch ((*this)[pos - 1].sub.op)
1132 {
1133 case acc_cond::acc_op::And:
1134 case acc_cond::acc_op::Or:
1135 --pos;
1136 break;
1137 case acc_cond::acc_op::Inf:
1138 case acc_cond::acc_op::InfNeg:
1139 case acc_cond::acc_op::Fin:
1140 case acc_cond::acc_op::FinNeg:
1141 pos -= 2;
1142 (*this)[pos].mark <<= sets;
1143 break;
1144 }
1145 }
1146 while (pos > 0);
1147 return *this;
1148 }
1149
1153 acc_code operator<<(unsigned sets) const
1154 {
1155 acc_code res = *this;
1156 res <<= sets;
1157 return res;
1158 }
1159
1166 bool is_dnf() const;
1167
1174 bool is_cnf() const;
1175
1187
1195
1200 bdd to_bdd(const bdd* map) const;
1201
1210 std::vector<acc_code> top_disjuncts() const;
1211
1220 std::vector<acc_code> top_conjuncts() const;
1221
1233
1248
1262
1275
1280 int fin_one() const;
1281
1302 std::pair<int, acc_code> fin_one_extract() const;
1303
1322 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1324 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1327
1340 std::vector<std::vector<int>>
1341 missing(mark_t inf, bool accepting) const;
1342
1345 bool accepting(mark_t inf) const;
1346
1352 bool inf_satisfiable(mark_t inf) const;
1353
1366 mark_t always_present) const;
1367
1378 std::vector<unsigned> symmetries() const;
1379
1393 acc_code remove(acc_cond::mark_t rem, bool missing) const;
1394
1399 acc_code strip(acc_cond::mark_t rem, bool missing) const;
1402
1405
1417 std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1419
1427
1429 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1430
1435 std::ostream&
1436 to_html(std::ostream& os,
1437 std::function<void(std::ostream&, int)>
1438 set_printer = nullptr) const;
1439
1444 std::ostream&
1445 to_text(std::ostream& os,
1446 std::function<void(std::ostream&, int)>
1447 set_printer = nullptr) const;
1448
1453 std::ostream&
1454 to_latex(std::ostream& os,
1455 std::function<void(std::ostream&, int)>
1456 set_printer = nullptr) const;
1457
1480 acc_code(const char* input);
1481
1486 {
1487 }
1488
1490 acc_code(const acc_word* other)
1491 : std::vector<acc_word>(other - other->sub.size, other + 1)
1492 {
1493 }
1494
1496 SPOT_API
1497 friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1498 };
1499
1507 acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1508 : num_(0U), all_({}), code_(code)
1509 {
1510 add_sets(n_sets);
1511 uses_fin_acceptance_ = check_fin_acceptance();
1512 }
1513
1518 acc_cond(const acc_code& code)
1519 : num_(0U), all_({}), code_(code)
1520 {
1521 add_sets(code.used_sets().max_set());
1522 uses_fin_acceptance_ = check_fin_acceptance();
1523 }
1524
1527 : num_(o.num_), all_(o.all_), code_(o.code_),
1528 uses_fin_acceptance_(o.uses_fin_acceptance_)
1529 {
1530 }
1531
1534 {
1535 num_ = o.num_;
1536 all_ = o.all_;
1537 code_ = o.code_;
1538 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1539 return *this;
1540 }
1541
1542 ~acc_cond()
1543 {
1544 }
1545
1549 void set_acceptance(const acc_code& code)
1550 {
1551 code_ = code;
1552 uses_fin_acceptance_ = check_fin_acceptance();
1553 }
1554
1557 {
1558 return code_;
1559 }
1560
1563 {
1564 return code_;
1565 }
1566
1567 bool operator==(const acc_cond& other) const
1568 {
1569 if (other.num_sets() != num_)
1570 return false;
1571 const acc_code& ocode = other.get_acceptance();
1572 // We have two ways to represent t, unfortunately.
1573 return (ocode == code_ || (ocode.is_t() && code_.is_t()));
1574 }
1575
1576 bool operator!=(const acc_cond& other) const
1577 {
1578 return !(*this == other);
1579 }
1580
1583 {
1584 return uses_fin_acceptance_;
1585 }
1586
1588 bool is_t() const
1589 {
1590 return code_.is_t();
1591 }
1592
1597 bool is_all() const
1598 {
1599 return num_ == 0 && is_t();
1600 }
1601
1603 bool is_f() const
1604 {
1605 return code_.is_f();
1606 }
1607
1612 bool is_none() const
1613 {
1614 return num_ == 0 && is_f();
1615 }
1616
1621 bool is_buchi() const
1622 {
1623 unsigned s = code_.size();
1624 return num_ == 1 &&
1625 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1626 }
1627
1632 bool is_co_buchi() const
1633 {
1634 return num_ == 1 && is_generalized_co_buchi();
1635 }
1636
1640 {
1641 set_acceptance(inf(all_sets()));
1642 }
1643
1647 {
1648 set_acceptance(fin(all_sets()));
1649 }
1650
1656 {
1657 unsigned s = code_.size();
1658 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1659 && code_[0].mark == all_sets());
1660 }
1661
1667 {
1668 unsigned s = code_.size();
1669 return (s == 2 &&
1670 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1671 }
1672
1684 int is_rabin() const;
1685
1697 int is_streett() const;
1698
1708 struct SPOT_API rs_pair
1709 {
1710#ifndef SWIG
1711 rs_pair() = default;
1712 rs_pair(const rs_pair&) = default;
1713 rs_pair& operator=(const rs_pair&) = default;
1714#endif
1715
1716 rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1717 fin(fin),
1718 inf(inf)
1719 {}
1720 acc_cond::mark_t fin;
1721 acc_cond::mark_t inf;
1722
1723 bool operator==(rs_pair o) const
1724 {
1725 return fin == o.fin && inf == o.inf;
1726 }
1727 bool operator!=(rs_pair o) const
1728 {
1729 return fin != o.fin || inf != o.inf;
1730 }
1731 bool operator<(rs_pair o) const
1732 {
1733 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1734 }
1735 bool operator<=(rs_pair o) const
1736 {
1737 return !(o < *this);
1738 }
1739 bool operator>(rs_pair o) const
1740 {
1741 return o < *this;
1742 }
1743 bool operator>=(rs_pair o) const
1744 {
1745 return !(*this < o);
1746 }
1747 };
1758 bool is_streett_like(std::vector<rs_pair>& pairs) const;
1759
1770 bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1771
1781 bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1782
1795 bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1796
1806 bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1807
1808
1811 bool is_parity() const
1812 {
1813 bool max;
1814 bool odd;
1815 return is_parity(max, odd);
1816 }
1817
1826 {
1827 return acc_cond(num_, code_.unit_propagation());
1828 }
1829
1830 // Return (true, m) if there exist some acceptance mark m that
1831 // does not satisfy the acceptance condition. Return (false, 0U)
1832 // otherwise.
1833 std::pair<bool, acc_cond::mark_t> unsat_mark() const
1834 {
1835 return sat_unsat_mark(false);
1836 }
1837 // Return (true, m) if there exist some acceptance mark m that
1838 // does satisfy the acceptance condition. Return (false, 0U)
1839 // otherwise.
1840 std::pair<bool, acc_cond::mark_t> sat_mark() const
1841 {
1842 return sat_unsat_mark(true);
1843 }
1844
1845 protected:
1846 bool check_fin_acceptance() const;
1847 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1848
1849 public:
1858 static acc_code inf(mark_t mark)
1859 {
1860 return acc_code::inf(mark);
1861 }
1862
1863 static acc_code inf(std::initializer_list<unsigned> vals)
1864 {
1865 return inf(mark_t(vals.begin(), vals.end()));
1866 }
1868
1886 {
1887 return acc_code::inf_neg(mark);
1888 }
1889
1890 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1891 {
1892 return inf_neg(mark_t(vals.begin(), vals.end()));
1893 }
1895
1903 static acc_code fin(mark_t mark)
1904 {
1905 return acc_code::fin(mark);
1906 }
1907
1908 static acc_code fin(std::initializer_list<unsigned> vals)
1909 {
1910 return fin(mark_t(vals.begin(), vals.end()));
1911 }
1913
1931 {
1932 return acc_code::fin_neg(mark);
1933 }
1934
1935 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1936 {
1937 return fin_neg(mark_t(vals.begin(), vals.end()));
1938 }
1940
1945 unsigned add_sets(unsigned num)
1946 {
1947 if (num == 0)
1948 return -1U;
1949 unsigned j = num_;
1950 num += j;
1951 if (num > mark_t::max_accsets())
1952 report_too_many_sets();
1953 // Make sure we do not update if we raised an exception.
1954 num_ = num;
1955 all_ = all_sets_();
1956 return j;
1957 }
1958
1963 unsigned add_set()
1964 {
1965 return add_sets(1);
1966 }
1967
1969 mark_t mark(unsigned u) const
1970 {
1971 SPOT_ASSERT(u < num_sets());
1972 return mark_t({u});
1973 }
1974
1979 mark_t comp(const mark_t& l) const
1980 {
1981 return all_ ^ l;
1982 }
1983
1986 {
1987 return all_;
1988 }
1989
1992 bool accepting(mark_t inf) const
1993 {
1994 return code_.accepting(inf);
1995 }
1996
2002 bool inf_satisfiable(mark_t inf) const
2003 {
2004 return code_.inf_satisfiable(inf);
2005 }
2006
2018 trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
2019 {
2020 return code_.maybe_accepting(infinitely_often, always_present);
2021 }
2022
2037
2038 // Deprecated since Spot 2.8
2039 SPOT_DEPRECATED("Use operator<< instead.")
2040 std::ostream& format(std::ostream& os, mark_t m) const
2041 {
2042 if (!m)
2043 return os;
2044 return os << m;
2045 }
2046
2047 // Deprecated since Spot 2.8
2048 SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2049 std::string format(mark_t m) const
2050 {
2051 std::ostringstream os;
2052 if (m)
2053 os << m;
2054 return os.str();
2055 }
2056
2058 unsigned num_sets() const
2059 {
2060 return num_;
2061 }
2062
2070 template<class iterator>
2071 mark_t useless(iterator begin, iterator end) const
2072 {
2073 mark_t u = {}; // The set of useless sets
2074 for (unsigned x = 0; x < num_; ++x)
2075 {
2076 // Skip sets that are already known to be useless.
2077 if (u.has(x))
2078 continue;
2079 auto all = comp(u | mark_t({x}));
2080 // Iterate over all mark_t, and keep track of
2081 // set numbers that always appear with x.
2082 for (iterator y = begin; y != end; ++y)
2083 {
2084 const mark_t& v = *y;
2085 if (v.has(x))
2086 {
2087 all &= v;
2088 if (!all)
2089 break;
2090 }
2091 }
2092 u |= all;
2093 }
2094 return u;
2095 }
2096
2110 acc_cond remove(mark_t rem, bool missing) const
2111 {
2112 return {num_sets(), code_.remove(rem, missing)};
2113 }
2114
2119 acc_cond strip(mark_t rem, bool missing) const
2120 {
2121 return
2122 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2123 }
2124
2127 {
2128 return {num_sets(), code_.force_inf(m)};
2129 }
2130
2134 {
2135 return {num_sets(), code_.remove(all_sets() - rem, true)};
2136 }
2137
2149 std::string name(const char* fmt = "alo") const;
2150
2165 {
2166 return code_.fin_unit();
2167 }
2168
2182 {
2183 return code_.mafins();
2184 }
2185
2198 {
2199 return code_.inf_unit();
2200 }
2201
2206 int fin_one() const
2207 {
2208 return code_.fin_one();
2209 }
2210
2231 std::pair<int, acc_cond> fin_one_extract() const
2232 {
2233 auto [f, c] = code_.fin_one_extract();
2234 return {f, {num_sets(), std::move(c)}};
2235 }
2236
2255 std::tuple<int, acc_cond, acc_cond>
2257 {
2258 auto [f, l, r] = code_.fin_unit_one_split();
2259 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2260 }
2261 std::tuple<int, acc_cond, acc_cond>
2263 {
2264 auto [f, l, r] = code_.fin_unit_one_split_improved();
2265 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2266 }
2268
2277 std::vector<acc_cond> top_disjuncts() const;
2278
2287 std::vector<acc_cond> top_conjuncts() const;
2288
2289 protected:
2290 mark_t all_sets_() const
2291 {
2292 return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2293 }
2294
2295 unsigned num_;
2296 mark_t all_;
2297 acc_code code_;
2298 bool uses_fin_acceptance_ = false;
2299
2300 };
2301
2303 typedef std::vector<acc_cond::rs_pair> rs_pairs;
2304
2305 // Creates view of pairs 'p' with restriction only to marks in 'm'
2306 explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2307 : pairs_(p), view_marks_(m) {}
2308
2309 // Creates view of pairs without restriction to marks
2310 explicit rs_pairs_view(const rs_pairs& p)
2312
2313 acc_cond::mark_t infs() const
2314 {
2315 return do_view([&](const acc_cond::rs_pair& p)
2316 {
2317 return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2318 });
2319 }
2320
2321 acc_cond::mark_t fins() const
2322 {
2323 return do_view([&](const acc_cond::rs_pair& p)
2324 {
2325 return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2326 });
2327 }
2328
2329 acc_cond::mark_t fins_alone() const
2330 {
2331 return do_view([&](const acc_cond::rs_pair& p)
2332 {
2333 return !visible(p.inf) && visible(p.fin) ? p.fin
2334 : acc_cond::mark_t({});
2335 });
2336 }
2337
2338 acc_cond::mark_t infs_alone() const
2339 {
2340 return do_view([&](const acc_cond::rs_pair& p)
2341 {
2342 return !visible(p.fin) && visible(p.inf) ? p.inf
2343 : acc_cond::mark_t({});
2344 });
2345 }
2346
2347 acc_cond::mark_t paired_with_fin(unsigned mark) const
2348 {
2349 acc_cond::mark_t res = {};
2350 for (const auto& p: pairs_)
2351 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2352 res |= p.inf;
2353 return res;
2354 }
2355
2356 const rs_pairs& pairs() const
2357 {
2358 return pairs_;
2359 }
2360
2361 private:
2362 template<typename filter>
2363 acc_cond::mark_t do_view(const filter& filt) const
2364 {
2365 acc_cond::mark_t res = {};
2366 for (const auto& p: pairs_)
2367 res |= filt(p);
2368 return res;
2369 }
2370
2371 bool visible(const acc_cond::mark_t& v) const
2372 {
2373 return !!(view_marks_ & v);
2374 }
2375
2376 const rs_pairs& pairs_;
2377 acc_cond::mark_t view_marks_;
2378 };
2379
2380
2381 SPOT_API
2382 std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2383
2385
2386 namespace internal
2387 {
2388 class SPOT_API mark_iterator
2389 {
2390 public:
2391 typedef unsigned value_type;
2392 typedef const value_type& reference;
2393 typedef const value_type* pointer;
2394 typedef std::ptrdiff_t difference_type;
2395 typedef std::forward_iterator_tag iterator_category;
2396
2397 mark_iterator() noexcept
2398 : m_({})
2399 {
2400 }
2401
2402 mark_iterator(acc_cond::mark_t m) noexcept
2403 : m_(m)
2404 {
2405 }
2406
2407 bool operator==(mark_iterator m) const
2408 {
2409 return m_ == m.m_;
2410 }
2411
2412 bool operator!=(mark_iterator m) const
2413 {
2414 return m_ != m.m_;
2415 }
2416
2417 value_type operator*() const
2418 {
2419 SPOT_ASSERT(m_);
2420 return m_.min_set() - 1;
2421 }
2422
2423 mark_iterator& operator++()
2424 {
2425 m_.clear(this->operator*());
2426 return *this;
2427 }
2428
2429 mark_iterator operator++(int)
2430 {
2431 mark_iterator it = *this;
2432 ++(*this);
2433 return it;
2434 }
2435 private:
2436 acc_cond::mark_t m_;
2437 };
2438
2439 class SPOT_API mark_container
2440 {
2441 public:
2442 mark_container(spot::acc_cond::mark_t m) noexcept
2443 : m_(m)
2444 {
2445 }
2446
2447 mark_iterator begin() const
2448 {
2449 return {m_};
2450 }
2451 mark_iterator end() const
2452 {
2453 return {};
2454 }
2455 private:
2457 };
2458 }
2459
2460 inline spot::internal::mark_container acc_cond::mark_t::sets() const
2461 {
2462 return {*this};
2463 }
2464}
2465
2466namespace std
2467{
2468 template<>
2469 struct hash<spot::acc_cond::mark_t>
2470 {
2471 size_t operator()(spot::acc_cond::mark_t m) const noexcept
2472 {
2473 return m.hash();
2474 }
2475 };
2476}
An acceptance condition.
Definition acc.hh:62
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition acc.hh:1556
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
Definition acc.hh:2002
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition acc.hh:1985
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition acc.hh:1930
mark_t mafins() const
Find a Fin(i) that is mandatory.
Definition acc.hh:2181
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition acc.hh:1885
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition acc.hh:1825
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition acc.hh:1646
std::pair< int, acc_cond > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it ...
Definition acc.hh:2231
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition acc.hh:1903
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition acc.hh:1632
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition acc.hh:1992
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition acc.hh:1858
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition acc.hh:1655
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition acc.hh:1935
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition acc.hh:1863
unsigned add_set()
Add a single set to the acceptance condition.
Definition acc.hh:1963
bool is_parity(bool &max, bool &odd, bool equiv=false) const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
std::vector< acc_cond > top_disjuncts() const
Return the top-level disjuncts.
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition acc.hh:1969
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition acc.hh:1639
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition acc.hh:2126
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition acc.hh:2110
acc_op
Operators for acceptance formulas.
Definition acc.hh:447
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition acc.hh:1507
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition acc.hh:1945
bool is_parity() const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
Definition acc.hh:1811
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition acc.hh:1588
bool is_generalized_rabin(std::vector< unsigned > &pairs) const
Is the acceptance condition generalized-Rabin?
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition acc.hh:1979
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition acc.hh:1533
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition acc.hh:1562
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition acc.hh:1908
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition acc.hh:1666
std::tuple< int, acc_cond, acc_cond > fin_unit_one_split_improved() const
Split an acceptance condition, trying to select one unit-Fin.
Definition acc.hh:2262
acc_cond restrict_to(mark_t rem) const
Restrict an acceptance condition to a subset of set numbers that are occurring at some point.
Definition acc.hh:2133
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition acc.hh:2018
std::string name(const char *fmt="alo") const
Return the name of this acceptance condition, in the specified format.
bool is_none() const
Whether the acceptance condition is "none".
Definition acc.hh:1612
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition acc.hh:1549
int is_rabin() const
Check if the acceptance condition matches the Rabin acceptance of the HOA format.
bool is_rabin_like(std::vector< rs_pair > &pairs) const
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_p...
mark_t accepting_sets(mark_t inf) const
Return an accepting subset of inf.
bool is_all() const
Whether the acceptance condition is "all".
Definition acc.hh:1597
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition acc.hh:2119
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition acc.hh:2206
mark_t useless(iterator begin, iterator end) const
Compute useless acceptance sets given a list of mark_t that occur in an SCC.
Definition acc.hh:2071
int is_streett() const
Check if the acceptance condition matches the Streett acceptance of the HOA format.
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition acc.hh:2164
bool is_generalized_streett(std::vector< unsigned > &pairs) const
Is the acceptance condition generalized-Streett?
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition acc.hh:1518
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition acc.hh:1526
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition acc.hh:1890
bool is_streett_like(std::vector< rs_pair > &pairs) const
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<...
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition acc.hh:1621
std::vector< acc_cond > top_conjuncts() const
Return the top-level conjuncts.
std::tuple< int, acc_cond, acc_cond > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
Definition acc.hh:2256
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition acc.hh:2197
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition acc.hh:1582
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition acc.hh:1603
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition acc.hh:2058
Definition bitset.hh:39
A class implementing Kleene's three-valued logic.
Definition trival.hh:34
op
Operator types.
Definition formula.hh:79
@ Or
(omega-Rational) Or
@ U
until
@ And
(omega-Rational) And
Definition automata.hh:27
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition mc.hh:131
An acceptance formula.
Definition acc.hh:479
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition acc.hh:861
std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
std::vector< std::vector< int > > missing(mark_t inf, bool accepting) const
Help closing accepting or rejecting cycle.
mark_t mafins() const
Find a Fin(i) that is mandatory.
friend std::ostream & operator<<(std::ostream &os, const acc_code &code)
prints the acceptance formula as text
std::ostream & to_html(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as HTML.
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition acc.hh:701
acc_code to_cnf() const
Convert the acceptance formula into disjunctive normal form.
acc_code operator&(acc_code &&r) const
Conjunct the current condition with r.
Definition acc.hh:1004
acc_code force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition acc.hh:743
std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > useless_colors_patterns() const
Find patterns of useless colors.
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition acc.hh:1110
std::vector< acc_code > top_conjuncts() const
Return the top-level conjuncts.
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition acc.hh:1101
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition acc.hh:655
bool is_dnf() const
Whether the acceptance formula is in disjunctive normal form.
std::vector< acc_code > top_disjuncts() const
Return the top-level disjuncts.
acc_code operator&(const acc_code &r) const
Conjunct the current condition with r.
Definition acc.hh:995
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition acc.hh:711
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition acc.hh:881
static acc_code parity(bool is_max, bool is_odd, unsigned sets)
Build a parity acceptance condition.
mark_t used_once_sets() const
Return the sets that appears only once in the acceptance.
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition acc.hh:1122
bool is_f() const
Is this the "false" acceptance condition?
Definition acc.hh:605
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition acc.hh:770
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition acc.hh:877
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition acc.hh:1490
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
static acc_code parity_max_even(unsigned sets)
Build a parity acceptance condition.
Definition acc.hh:869
static acc_code f()
Construct the "false" acceptance condition.
Definition acc.hh:619
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
static acc_code parity_max_odd(unsigned sets)
Build a parity acceptance condition.
Definition acc.hh:865
std::ostream & to_latex(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as LaTeX.
std::pair< int, acc_code > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it ...
bool is_t() const
Is this the "true" acceptance condition?
Definition acc.hh:591
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition acc.hh:1153
static acc_code random(unsigned n, double reuse=0.0)
Build a random acceptance condition.
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition acc.hh:797
acc_code()
Build an empty acceptance formula.
Definition acc.hh:1485
std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > fin_unit_one_split_improved() const
Split an acceptance condition, trying to select one unit-Fin.
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition acc.hh:760
acc_code complement() const
Complement an acceptance formula.
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition acc.hh:733
bdd to_bdd(const bdd *map) const
Convert the acceptance formula into a BDD.
std::ostream & to_text(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as text.
int fin_one() const
Return one acceptance set i that appears as Fin(i) in the condition.
acc_cond::mark_t used_sets() const
Return the set of sets appearing in the condition.
std::pair< acc_cond::mark_t, acc_cond::mark_t > used_inf_fin_sets() const
Return the sets used as Inf or Fin in the acceptance condition.
acc_code strip(acc_cond::mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
acc_code(const char *input)
Construct an acc_code from a string.
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition acc.hh:687
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition acc.hh:906
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition acc.hh:812
static acc_code t()
Construct the "true" acceptance condition.
Definition acc.hh:633
std::vector< unsigned > symmetries() const
compute the symmetry class of the acceptance sets.
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition acc.hh:677
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition acc.hh:873
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition acc.hh:645
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition acc.hh:1013
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
bool is_cnf() const
Whether the acceptance formula is in conjunctive normal form.
static acc_code buchi()
Build a Büchi acceptance condition.
Definition acc.hh:752
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition acc.hh:784
acc_code remove(acc_cond::mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
acc_code to_dnf() const
Convert the acceptance formula into disjunctive normal form.
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition acc.hh:836
An acceptance mark.
Definition acc.hh:85
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition acc.hh:138
bool is_singleton() const
Whether the mark contains only one bit set.
Definition acc.hh:385
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition acc.hh:379
unsigned max_set() const
The number of the highest set used plus one.
Definition acc.hh:355
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition acc.hh:409
static mark_t all()
A mark_t with all bits set to one.
Definition acc.hh:148
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition acc.hh:2460
bool proper_subset(mark_t m) const
Whether the set of bits represented by *this is a proper subset of those represented by m.
Definition acc.hh:340
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition acc.hh:103
unsigned count() const
Number of bits sets.
Definition acc.hh:346
mark_t()=default
Initialize an empty mark_t.
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition acc.hh:114
bool has_many() const
Whether the mark contains at least two bits set.
Definition acc.hh:396
unsigned min_set() const
The number of the lowest set used plus one.
Definition acc.hh:367
bool subset(mark_t m) const
Whether the set of bits represented by *this is a subset of those represented by m.
Definition acc.hh:333
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition acc.hh:418
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition acc.hh:1709
Definition acc.hh:41
Definition acc.hh:2302
A "node" in an acceptance formulas.
Definition acc.hh:457

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.8