spot 2.11.5.dev
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
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 unsigned pos = size();
486 if (other.size() != pos)
487 return false;
488 while (pos > 0)
489 {
490 auto op = (*this)[pos - 1].sub.op;
491 auto sz = (*this)[pos - 1].sub.size;
492 if (other[pos - 1].sub.op != op ||
493 other[pos - 1].sub.size != sz)
494 return false;
495 switch (op)
496 {
497 case acc_cond::acc_op::And:
498 case acc_cond::acc_op::Or:
499 --pos;
500 break;
501 case acc_cond::acc_op::Inf:
502 case acc_cond::acc_op::InfNeg:
503 case acc_cond::acc_op::Fin:
504 case acc_cond::acc_op::FinNeg:
505 pos -= 2;
506 if (other[pos].mark != (*this)[pos].mark)
507 return false;
508 break;
509 }
510 }
511 return true;
512 };
513
514 bool operator<(const acc_code& other) const
515 {
516 unsigned pos = size();
517 auto osize = other.size();
518 if (pos < osize)
519 return true;
520 if (pos > osize)
521 return false;
522 while (pos > 0)
523 {
524 auto op = (*this)[pos - 1].sub.op;
525 auto oop = other[pos - 1].sub.op;
526 if (op < oop)
527 return true;
528 if (op > oop)
529 return false;
530 auto sz = (*this)[pos - 1].sub.size;
531 auto osz = other[pos - 1].sub.size;
532 if (sz < osz)
533 return true;
534 if (sz > osz)
535 return false;
536 switch (op)
537 {
538 case acc_cond::acc_op::And:
539 case acc_cond::acc_op::Or:
540 --pos;
541 break;
542 case acc_cond::acc_op::Inf:
543 case acc_cond::acc_op::InfNeg:
544 case acc_cond::acc_op::Fin:
545 case acc_cond::acc_op::FinNeg:
546 {
547 pos -= 2;
548 auto m = (*this)[pos].mark;
549 auto om = other[pos].mark;
550 if (m < om)
551 return true;
552 if (m > om)
553 return false;
554 break;
555 }
556 }
557 }
558 return false;
559 }
560
561 bool operator>(const acc_code& other) const
562 {
563 return other < *this;
564 }
565
566 bool operator<=(const acc_code& other) const
567 {
568 return !(other < *this);
569 }
570
571 bool operator>=(const acc_code& other) const
572 {
573 return !(*this < other);
574 }
575
576 bool operator!=(const acc_code& other) const
577 {
578 return !(*this == other);
579 }
580
585 bool is_t() const
586 {
587 // We store "t" as an empty condition, or as Inf({}).
588 unsigned s = size();
589 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
590 && !((*this)[s - 2].mark));
591 }
592
599 bool is_f() const
600 {
601 // We store "f" as Fin({}).
602 unsigned s = size();
603 return s > 1
604 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
605 }
606
613 static acc_code f()
614 {
615 acc_code res;
616 res.resize(2);
617 res[0].mark = {};
618 res[1].sub.op = acc_op::Fin;
619 res[1].sub.size = 1;
620 return res;
621 }
622
627 static acc_code t()
628 {
629 return {};
630 }
631
640 {
641 acc_code res;
642 res.resize(2);
643 res[0].mark = m;
644 res[1].sub.op = acc_op::Fin;
645 res[1].sub.size = 1;
646 return res;
647 }
648
649 static acc_code fin(std::initializer_list<unsigned> vals)
650 {
651 return fin(mark_t(vals));
652 }
654
672 {
673 acc_code res;
674 res.resize(2);
675 res[0].mark = m;
676 res[1].sub.op = acc_op::FinNeg;
677 res[1].sub.size = 1;
678 return res;
679 }
680
681 static acc_code fin_neg(std::initializer_list<unsigned> vals)
682 {
683 return fin_neg(mark_t(vals));
684 }
686
696 {
697 acc_code res;
698 res.resize(2);
699 res[0].mark = m;
700 res[1].sub.op = acc_op::Inf;
701 res[1].sub.size = 1;
702 return res;
703 }
704
705 static acc_code inf(std::initializer_list<unsigned> vals)
706 {
707 return inf(mark_t(vals));
708 }
710
728 {
729 acc_code res;
730 res.resize(2);
731 res[0].mark = m;
732 res[1].sub.op = acc_op::InfNeg;
733 res[1].sub.size = 1;
734 return res;
735 }
736
737 static acc_code inf_neg(std::initializer_list<unsigned> vals)
738 {
739 return inf_neg(mark_t(vals));
740 }
742
747 {
748 return inf({0});
749 }
750
755 {
756 return fin({0});
757 }
758
764 static acc_code generalized_buchi(unsigned n)
765 {
766 if (n == 0)
767 return inf({});
768 acc_cond::mark_t m = mark_t::all();
769 m >>= mark_t::max_accsets() - n;
770 return inf(m);
771 }
772
779 {
780 if (n == 0)
781 return fin({});
782 acc_cond::mark_t m = mark_t::all();
783 m >>= mark_t::max_accsets() - n;
784 return fin(m);
785 }
786
791 static acc_code rabin(unsigned n)
792 {
793 acc_cond::acc_code res = f();
794 while (n > 0)
795 {
796 res |= inf({2*n - 1}) & fin({2*n - 2});
797 --n;
798 }
799 return res;
800 }
801
806 static acc_code streett(unsigned n)
807 {
808 acc_cond::acc_code res = t();
809 while (n > 0)
810 {
811 res &= inf({2*n - 1}) | fin({2*n - 2});
812 --n;
813 }
814 return res;
815 }
816
829 template<class Iterator>
830 static acc_code generalized_rabin(Iterator begin, Iterator end)
831 {
832 acc_cond::acc_code res = f();
833 unsigned n = 0;
834 for (Iterator i = begin; i != end; ++i)
835 {
836 unsigned f = n++;
837 acc_cond::mark_t m = {};
838 for (unsigned ni = *i; ni > 0; --ni)
839 m.set(n++);
840 auto pair = inf(m) & fin({f});
841 std::swap(pair, res);
842 res |= std::move(pair);
843 }
844 return res;
845 }
846
854 static acc_code parity(bool is_max, bool is_odd, unsigned sets);
855 static acc_code parity_max(bool is_odd, unsigned sets)
856 {
857 return parity(true, is_odd, sets);
858 }
859 static acc_code parity_max_odd(unsigned sets)
860 {
861 return parity_max(true, sets);
862 }
863 static acc_code parity_max_even(unsigned sets)
864 {
865 return parity_max(false, sets);
866 }
867 static acc_code parity_min(bool is_odd, unsigned sets)
868 {
869 return parity(false, is_odd, sets);
870 }
871 static acc_code parity_min_odd(unsigned sets)
872 {
873 return parity_min(true, sets);
874 }
875 static acc_code parity_min_even(unsigned sets)
876 {
877 return parity_min(false, sets);
878 }
880
897 static acc_code random(unsigned n, double reuse = 0.0);
898
901 {
902 if (is_t() || r.is_f())
903 {
904 *this = r;
905 return *this;
906 }
907 if (is_f() || r.is_t())
908 return *this;
909 unsigned s = size() - 1;
910 unsigned rs = r.size() - 1;
911 // We want to group all Inf(x) operators:
912 // Inf(a) & Inf(b) = Inf(a & b)
913 if (((*this)[s].sub.op == acc_op::Inf
914 && r[rs].sub.op == acc_op::Inf)
915 || ((*this)[s].sub.op == acc_op::InfNeg
916 && r[rs].sub.op == acc_op::InfNeg))
917 {
918 (*this)[s - 1].mark |= r[rs - 1].mark;
919 return *this;
920 }
921
922 // In the more complex scenarios, left and right may both
923 // be conjunctions, and Inf(x) might be a member of each
924 // side. Find it if it exists.
925 // left_inf points to the left Inf mark if any.
926 // right_inf points to the right Inf mark if any.
927 acc_word* left_inf = nullptr;
928 if ((*this)[s].sub.op == acc_op::And)
929 {
930 auto start = &(*this)[s] - (*this)[s].sub.size;
931 auto pos = &(*this)[s] - 1;
932 pop_back();
933 while (pos > start)
934 {
935 if (pos->sub.op == acc_op::Inf)
936 {
937 left_inf = pos - 1;
938 break;
939 }
940 pos -= pos->sub.size + 1;
941 }
942 }
943 else if ((*this)[s].sub.op == acc_op::Inf)
944 {
945 left_inf = &(*this)[s - 1];
946 }
947
948 const acc_word* right_inf = nullptr;
949 auto right_end = &r.back();
950 if (right_end->sub.op == acc_op::And)
951 {
952 auto start = &r[0];
953 auto pos = --right_end;
954 while (pos > start)
955 {
956 if (pos->sub.op == acc_op::Inf)
957 {
958 right_inf = pos - 1;
959 break;
960 }
961 pos -= pos->sub.size + 1;
962 }
963 }
964 else if (right_end->sub.op == acc_op::Inf)
965 {
966 right_inf = right_end - 1;
967 }
968
969 acc_cond::mark_t carry = {};
970 if (left_inf && right_inf)
971 {
972 carry = left_inf->mark;
973 auto pos = left_inf - &(*this)[0];
974 erase(begin() + pos, begin() + pos + 2);
975 }
976 auto sz = size();
977 insert(end(), &r[0], right_end + 1);
978 if (carry)
979 (*this)[sz + (right_inf - &r[0])].mark |= carry;
980
981 acc_word w;
982 w.sub.op = acc_op::And;
983 w.sub.size = size();
984 emplace_back(w);
985 return *this;
986 }
987
990 {
991 acc_code res = *this;
992 res &= r;
993 return res;
994 }
995
996#ifndef SWIG
999 {
1000 acc_code res = *this;
1001 res &= r;
1002 return res;
1003 }
1004#endif // SWIG
1005
1008 {
1009 if (is_t() || r.is_f())
1010 return *this;
1011 if (is_f() || r.is_t())
1012 {
1013 *this = r;
1014 return *this;
1015 }
1016 unsigned s = size() - 1;
1017 unsigned rs = r.size() - 1;
1018 // Fin(a) | Fin(b) = Fin(a | b)
1019 if (((*this)[s].sub.op == acc_op::Fin
1020 && r[rs].sub.op == acc_op::Fin)
1021 || ((*this)[s].sub.op == acc_op::FinNeg
1022 && r[rs].sub.op == acc_op::FinNeg))
1023 {
1024 (*this)[s - 1].mark |= r[rs - 1].mark;
1025 return *this;
1026 }
1027
1028 // In the more complex scenarios, left and right may both
1029 // be disjunctions, and Fin(x) might be a member of each
1030 // side. Find it if it exists.
1031 // left_inf points to the left Inf mark if any.
1032 // right_inf points to the right Inf mark if any.
1033 acc_word* left_fin = nullptr;
1034 if ((*this)[s].sub.op == acc_op::Or)
1035 {
1036 auto start = &(*this)[s] - (*this)[s].sub.size;
1037 auto pos = &(*this)[s] - 1;
1038 pop_back();
1039 while (pos > start)
1040 {
1041 if (pos->sub.op == acc_op::Fin)
1042 {
1043 left_fin = pos - 1;
1044 break;
1045 }
1046 pos -= pos->sub.size + 1;
1047 }
1048 }
1049 else if ((*this)[s].sub.op == acc_op::Fin)
1050 {
1051 left_fin = &(*this)[s - 1];
1052 }
1053
1054 const acc_word* right_fin = nullptr;
1055 auto right_end = &r.back();
1056 if (right_end->sub.op == acc_op::Or)
1057 {
1058 auto start = &r[0];
1059 auto pos = --right_end;
1060 while (pos > start)
1061 {
1062 if (pos->sub.op == acc_op::Fin)
1063 {
1064 right_fin = pos - 1;
1065 break;
1066 }
1067 pos -= pos->sub.size + 1;
1068 }
1069 }
1070 else if (right_end->sub.op == acc_op::Fin)
1071 {
1072 right_fin = right_end - 1;
1073 }
1074
1075 acc_cond::mark_t carry = {};
1076 if (left_fin && right_fin)
1077 {
1078 carry = left_fin->mark;
1079 auto pos = (left_fin - &(*this)[0]);
1080 this->erase(begin() + pos, begin() + pos + 2);
1081 }
1082 auto sz = size();
1083 insert(end(), &r[0], right_end + 1);
1084 if (carry)
1085 (*this)[sz + (right_fin - &r[0])].mark |= carry;
1086 acc_word w;
1087 w.sub.op = acc_op::Or;
1088 w.sub.size = size();
1089 emplace_back(w);
1090 return *this;
1091 }
1092
1093#ifndef SWIG
1096 {
1097 acc_code res = *this;
1098 res |= r;
1099 return res;
1100 }
1101#endif // SWIG
1102
1105 {
1106 acc_code res = *this;
1107 res |= r;
1108 return res;
1109 }
1110
1116 acc_code& operator<<=(unsigned sets)
1117 {
1118 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1119 report_too_many_sets();
1120 if (empty())
1121 return *this;
1122 unsigned pos = size();
1123 do
1124 {
1125 switch ((*this)[pos - 1].sub.op)
1126 {
1127 case acc_cond::acc_op::And:
1128 case acc_cond::acc_op::Or:
1129 --pos;
1130 break;
1131 case acc_cond::acc_op::Inf:
1132 case acc_cond::acc_op::InfNeg:
1133 case acc_cond::acc_op::Fin:
1134 case acc_cond::acc_op::FinNeg:
1135 pos -= 2;
1136 (*this)[pos].mark <<= sets;
1137 break;
1138 }
1139 }
1140 while (pos > 0);
1141 return *this;
1142 }
1143
1147 acc_code operator<<(unsigned sets) const
1148 {
1149 acc_code res = *this;
1150 res <<= sets;
1151 return res;
1152 }
1153
1160 bool is_dnf() const;
1161
1168 bool is_cnf() const;
1169
1181
1189
1194 bdd to_bdd(const bdd* map) const;
1195
1204 std::vector<acc_code> top_disjuncts() const;
1205
1214 std::vector<acc_code> top_conjuncts() const;
1215
1227
1242
1256
1269
1274 int fin_one() const;
1275
1296 std::pair<int, acc_code> fin_one_extract() const;
1297
1316 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1318 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1321
1334 std::vector<std::vector<int>>
1335 missing(mark_t inf, bool accepting) const;
1336
1339 bool accepting(mark_t inf) const;
1340
1346 bool inf_satisfiable(mark_t inf) const;
1347
1360 mark_t always_present) const;
1361
1372 std::vector<unsigned> symmetries() const;
1373
1387 acc_code remove(acc_cond::mark_t rem, bool missing) const;
1388
1393 acc_code strip(acc_cond::mark_t rem, bool missing) const;
1396
1399
1411 std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1413
1421
1423 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1424
1429 std::ostream&
1430 to_html(std::ostream& os,
1431 std::function<void(std::ostream&, int)>
1432 set_printer = nullptr) const;
1433
1438 std::ostream&
1439 to_text(std::ostream& os,
1440 std::function<void(std::ostream&, int)>
1441 set_printer = nullptr) const;
1442
1447 std::ostream&
1448 to_latex(std::ostream& os,
1449 std::function<void(std::ostream&, int)>
1450 set_printer = nullptr) const;
1451
1474 acc_code(const char* input);
1475
1480 {
1481 }
1482
1484 acc_code(const acc_word* other)
1485 : std::vector<acc_word>(other - other->sub.size, other + 1)
1486 {
1487 }
1488
1490 SPOT_API
1491 friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1492 };
1493
1501 acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1502 : num_(0U), all_({}), code_(code)
1503 {
1504 add_sets(n_sets);
1505 uses_fin_acceptance_ = check_fin_acceptance();
1506 }
1507
1512 acc_cond(const acc_code& code)
1513 : num_(0U), all_({}), code_(code)
1514 {
1515 add_sets(code.used_sets().max_set());
1516 uses_fin_acceptance_ = check_fin_acceptance();
1517 }
1518
1521 : num_(o.num_), all_(o.all_), code_(o.code_),
1522 uses_fin_acceptance_(o.uses_fin_acceptance_)
1523 {
1524 }
1525
1528 {
1529 num_ = o.num_;
1530 all_ = o.all_;
1531 code_ = o.code_;
1532 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1533 return *this;
1534 }
1535
1536 ~acc_cond()
1537 {
1538 }
1539
1543 void set_acceptance(const acc_code& code)
1544 {
1545 code_ = code;
1546 uses_fin_acceptance_ = check_fin_acceptance();
1547 }
1548
1551 {
1552 return code_;
1553 }
1554
1557 {
1558 return code_;
1559 }
1560
1561 bool operator==(const acc_cond& other) const
1562 {
1563 return other.num_sets() == num_ && other.get_acceptance() == code_;
1564 }
1565
1566 bool operator!=(const acc_cond& other) const
1567 {
1568 return !(*this == other);
1569 }
1570
1573 {
1574 return uses_fin_acceptance_;
1575 }
1576
1578 bool is_t() const
1579 {
1580 return code_.is_t();
1581 }
1582
1587 bool is_all() const
1588 {
1589 return num_ == 0 && is_t();
1590 }
1591
1593 bool is_f() const
1594 {
1595 return code_.is_f();
1596 }
1597
1602 bool is_none() const
1603 {
1604 return num_ == 0 && is_f();
1605 }
1606
1611 bool is_buchi() const
1612 {
1613 unsigned s = code_.size();
1614 return num_ == 1 &&
1615 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1616 }
1617
1622 bool is_co_buchi() const
1623 {
1624 return num_ == 1 && is_generalized_co_buchi();
1625 }
1626
1630 {
1631 set_acceptance(inf(all_sets()));
1632 }
1633
1637 {
1638 set_acceptance(fin(all_sets()));
1639 }
1640
1646 {
1647 unsigned s = code_.size();
1648 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1649 && code_[0].mark == all_sets());
1650 }
1651
1657 {
1658 unsigned s = code_.size();
1659 return (s == 2 &&
1660 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1661 }
1662
1674 int is_rabin() const;
1675
1687 int is_streett() const;
1688
1698 struct SPOT_API rs_pair
1699 {
1700#ifndef SWIG
1701 rs_pair() = default;
1702 rs_pair(const rs_pair&) = default;
1703 rs_pair& operator=(const rs_pair&) = default;
1704#endif
1705
1706 rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1707 fin(fin),
1708 inf(inf)
1709 {}
1710 acc_cond::mark_t fin;
1711 acc_cond::mark_t inf;
1712
1713 bool operator==(rs_pair o) const
1714 {
1715 return fin == o.fin && inf == o.inf;
1716 }
1717 bool operator!=(rs_pair o) const
1718 {
1719 return fin != o.fin || inf != o.inf;
1720 }
1721 bool operator<(rs_pair o) const
1722 {
1723 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1724 }
1725 bool operator<=(rs_pair o) const
1726 {
1727 return !(o < *this);
1728 }
1729 bool operator>(rs_pair o) const
1730 {
1731 return o < *this;
1732 }
1733 bool operator>=(rs_pair o) const
1734 {
1735 return !(*this < o);
1736 }
1737 };
1748 bool is_streett_like(std::vector<rs_pair>& pairs) const;
1749
1760 bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1761
1771 bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1772
1785 bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1786
1796 bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1797
1798
1801 bool is_parity() const
1802 {
1803 bool max;
1804 bool odd;
1805 return is_parity(max, odd);
1806 }
1807
1816 {
1817 return acc_cond(num_, code_.unit_propagation());
1818 }
1819
1820 // Return (true, m) if there exist some acceptance mark m that
1821 // does not satisfy the acceptance condition. Return (false, 0U)
1822 // otherwise.
1823 std::pair<bool, acc_cond::mark_t> unsat_mark() const
1824 {
1825 return sat_unsat_mark(false);
1826 }
1827 // Return (true, m) if there exist some acceptance mark m that
1828 // does satisfy the acceptance condition. Return (false, 0U)
1829 // otherwise.
1830 std::pair<bool, acc_cond::mark_t> sat_mark() const
1831 {
1832 return sat_unsat_mark(true);
1833 }
1834
1835 protected:
1836 bool check_fin_acceptance() const;
1837 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1838
1839 public:
1848 static acc_code inf(mark_t mark)
1849 {
1850 return acc_code::inf(mark);
1851 }
1852
1853 static acc_code inf(std::initializer_list<unsigned> vals)
1854 {
1855 return inf(mark_t(vals.begin(), vals.end()));
1856 }
1858
1876 {
1877 return acc_code::inf_neg(mark);
1878 }
1879
1880 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1881 {
1882 return inf_neg(mark_t(vals.begin(), vals.end()));
1883 }
1885
1893 static acc_code fin(mark_t mark)
1894 {
1895 return acc_code::fin(mark);
1896 }
1897
1898 static acc_code fin(std::initializer_list<unsigned> vals)
1899 {
1900 return fin(mark_t(vals.begin(), vals.end()));
1901 }
1903
1921 {
1922 return acc_code::fin_neg(mark);
1923 }
1924
1925 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1926 {
1927 return fin_neg(mark_t(vals.begin(), vals.end()));
1928 }
1930
1935 unsigned add_sets(unsigned num)
1936 {
1937 if (num == 0)
1938 return -1U;
1939 unsigned j = num_;
1940 num += j;
1941 if (num > mark_t::max_accsets())
1942 report_too_many_sets();
1943 // Make sure we do not update if we raised an exception.
1944 num_ = num;
1945 all_ = all_sets_();
1946 return j;
1947 }
1948
1953 unsigned add_set()
1954 {
1955 return add_sets(1);
1956 }
1957
1959 mark_t mark(unsigned u) const
1960 {
1961 SPOT_ASSERT(u < num_sets());
1962 return mark_t({u});
1963 }
1964
1969 mark_t comp(const mark_t& l) const
1970 {
1971 return all_ ^ l;
1972 }
1973
1976 {
1977 return all_;
1978 }
1979
1982 bool accepting(mark_t inf) const
1983 {
1984 return code_.accepting(inf);
1985 }
1986
1992 bool inf_satisfiable(mark_t inf) const
1993 {
1994 return code_.inf_satisfiable(inf);
1995 }
1996
2008 trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
2009 {
2010 return code_.maybe_accepting(infinitely_often, always_present);
2011 }
2012
2027
2028 // Deprecated since Spot 2.8
2029 SPOT_DEPRECATED("Use operator<< instead.")
2030 std::ostream& format(std::ostream& os, mark_t m) const
2031 {
2032 if (!m)
2033 return os;
2034 return os << m;
2035 }
2036
2037 // Deprecated since Spot 2.8
2038 SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2039 std::string format(mark_t m) const
2040 {
2041 std::ostringstream os;
2042 if (m)
2043 os << m;
2044 return os.str();
2045 }
2046
2048 unsigned num_sets() const
2049 {
2050 return num_;
2051 }
2052
2060 template<class iterator>
2061 mark_t useless(iterator begin, iterator end) const
2062 {
2063 mark_t u = {}; // The set of useless sets
2064 for (unsigned x = 0; x < num_; ++x)
2065 {
2066 // Skip sets that are already known to be useless.
2067 if (u.has(x))
2068 continue;
2069 auto all = comp(u | mark_t({x}));
2070 // Iterate over all mark_t, and keep track of
2071 // set numbers that always appear with x.
2072 for (iterator y = begin; y != end; ++y)
2073 {
2074 const mark_t& v = *y;
2075 if (v.has(x))
2076 {
2077 all &= v;
2078 if (!all)
2079 break;
2080 }
2081 }
2082 u |= all;
2083 }
2084 return u;
2085 }
2086
2100 acc_cond remove(mark_t rem, bool missing) const
2101 {
2102 return {num_sets(), code_.remove(rem, missing)};
2103 }
2104
2109 acc_cond strip(mark_t rem, bool missing) const
2110 {
2111 return
2112 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2113 }
2114
2117 {
2118 return {num_sets(), code_.force_inf(m)};
2119 }
2120
2124 {
2125 return {num_sets(), code_.remove(all_sets() - rem, true)};
2126 }
2127
2139 std::string name(const char* fmt = "alo") const;
2140
2155 {
2156 return code_.fin_unit();
2157 }
2158
2172 {
2173 return code_.mafins();
2174 }
2175
2188 {
2189 return code_.inf_unit();
2190 }
2191
2196 int fin_one() const
2197 {
2198 return code_.fin_one();
2199 }
2200
2221 std::pair<int, acc_cond> fin_one_extract() const
2222 {
2223 auto [f, c] = code_.fin_one_extract();
2224 return {f, {num_sets(), std::move(c)}};
2225 }
2226
2245 std::tuple<int, acc_cond, acc_cond>
2247 {
2248 auto [f, l, r] = code_.fin_unit_one_split();
2249 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2250 }
2251 std::tuple<int, acc_cond, acc_cond>
2253 {
2254 auto [f, l, r] = code_.fin_unit_one_split_improved();
2255 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2256 }
2258
2267 std::vector<acc_cond> top_disjuncts() const;
2268
2277 std::vector<acc_cond> top_conjuncts() const;
2278
2279 protected:
2280 mark_t all_sets_() const
2281 {
2282 return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2283 }
2284
2285 unsigned num_;
2286 mark_t all_;
2287 acc_code code_;
2288 bool uses_fin_acceptance_ = false;
2289
2290 };
2291
2293 typedef std::vector<acc_cond::rs_pair> rs_pairs;
2294
2295 // Creates view of pairs 'p' with restriction only to marks in 'm'
2296 explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2297 : pairs_(p), view_marks_(m) {}
2298
2299 // Creates view of pairs without restriction to marks
2300 explicit rs_pairs_view(const rs_pairs& p)
2302
2303 acc_cond::mark_t infs() const
2304 {
2305 return do_view([&](const acc_cond::rs_pair& p)
2306 {
2307 return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2308 });
2309 }
2310
2311 acc_cond::mark_t fins() const
2312 {
2313 return do_view([&](const acc_cond::rs_pair& p)
2314 {
2315 return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2316 });
2317 }
2318
2319 acc_cond::mark_t fins_alone() const
2320 {
2321 return do_view([&](const acc_cond::rs_pair& p)
2322 {
2323 return !visible(p.inf) && visible(p.fin) ? p.fin
2324 : acc_cond::mark_t({});
2325 });
2326 }
2327
2328 acc_cond::mark_t infs_alone() const
2329 {
2330 return do_view([&](const acc_cond::rs_pair& p)
2331 {
2332 return !visible(p.fin) && visible(p.inf) ? p.inf
2333 : acc_cond::mark_t({});
2334 });
2335 }
2336
2337 acc_cond::mark_t paired_with_fin(unsigned mark) const
2338 {
2339 acc_cond::mark_t res = {};
2340 for (const auto& p: pairs_)
2341 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2342 res |= p.inf;
2343 return res;
2344 }
2345
2346 const rs_pairs& pairs() const
2347 {
2348 return pairs_;
2349 }
2350
2351 private:
2352 template<typename filter>
2353 acc_cond::mark_t do_view(const filter& filt) const
2354 {
2355 acc_cond::mark_t res = {};
2356 for (const auto& p: pairs_)
2357 res |= filt(p);
2358 return res;
2359 }
2360
2361 bool visible(const acc_cond::mark_t& v) const
2362 {
2363 return !!(view_marks_ & v);
2364 }
2365
2366 const rs_pairs& pairs_;
2367 acc_cond::mark_t view_marks_;
2368 };
2369
2370
2371 SPOT_API
2372 std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2373
2375
2376 namespace internal
2377 {
2378 class SPOT_API mark_iterator
2379 {
2380 public:
2381 typedef unsigned value_type;
2382 typedef const value_type& reference;
2383 typedef const value_type* pointer;
2384 typedef std::ptrdiff_t difference_type;
2385 typedef std::forward_iterator_tag iterator_category;
2386
2387 mark_iterator() noexcept
2388 : m_({})
2389 {
2390 }
2391
2393 : m_(m)
2394 {
2395 }
2396
2397 bool operator==(mark_iterator m) const
2398 {
2399 return m_ == m.m_;
2400 }
2401
2402 bool operator!=(mark_iterator m) const
2403 {
2404 return m_ != m.m_;
2405 }
2406
2407 value_type operator*() const
2408 {
2409 SPOT_ASSERT(m_);
2410 return m_.min_set() - 1;
2411 }
2412
2413 mark_iterator& operator++()
2414 {
2415 m_.clear(this->operator*());
2416 return *this;
2417 }
2418
2419 mark_iterator operator++(int)
2420 {
2421 mark_iterator it = *this;
2422 ++(*this);
2423 return it;
2424 }
2425 private:
2427 };
2428
2429 class SPOT_API mark_container
2430 {
2431 public:
2433 : m_(m)
2434 {
2435 }
2436
2437 mark_iterator begin() const
2438 {
2439 return {m_};
2440 }
2441 mark_iterator end() const
2442 {
2443 return {};
2444 }
2445 private:
2447 };
2448 }
2449
2451 {
2452 return {*this};
2453 }
2454}
2455
2456namespace std
2457{
2458 template<>
2459 struct hash<spot::acc_cond::mark_t>
2460 {
2461 size_t operator()(spot::acc_cond::mark_t m) const noexcept
2462 {
2463 return m.hash();
2464 }
2465 };
2466}
An acceptance condition.
Definition: acc.hh:62
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1550
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:1992
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1975
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1920
mark_t mafins() const
Find a Fin(i) that is mandatory.
Definition: acc.hh:2171
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1875
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1815
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1636
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:2221
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1893
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1622
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition: acc.hh:1982
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1848
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1645
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1925
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1853
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1953
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:1959
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1629
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2116
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2100
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:1501
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1935
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:1801
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1578
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:1969
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1527
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1556
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1898
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1656
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:2252
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:2123
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:2008
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:1602
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1543
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:1587
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2109
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2196
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:2061
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:2154
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:1512
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1520
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1880
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:1611
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:2246
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition: acc.hh:2187
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1572
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1593
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2048
Definition: bitset.hh:39
Definition: acc.hh:2430
Definition: acc.hh:2379
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
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
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:855
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:695
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:998
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:737
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:1104
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:1095
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:649
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:989
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:705
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:875
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:1116
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:599
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:764
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:871
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1484
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:863
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:613
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:859
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:585
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1147
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:791
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1479
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:754
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:727
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:681
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition: acc.hh:900
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:806
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:627
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:671
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:867
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:639
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1007
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:746
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:778
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:830
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:2450
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:1699
Definition: acc.hh:41
Definition: acc.hh:2292
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.4