spot  2.12
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <functional>
22 #include <sstream>
23 #include <vector>
24 #include <iostream>
25 #include <algorithm>
26 #include <numeric>
27 #include <bddx.h>
28 #include <tuple>
29 #include <spot/misc/_config.h>
30 #include <spot/misc/bitset.hh>
31 #include <spot/misc/trival.hh>
32 
33 namespace spot
34 {
35  namespace internal
36  {
37  class mark_container;
38 
39  template<bool>
40  struct _32acc {};
41  template<>
42  struct _32acc<true>
43  {
44  SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
45  typedef unsigned value_t;
46  };
47  }
48 
51 
60  class SPOT_API acc_cond
61  {
62 #ifndef SWIG
63  private:
64  [[noreturn]] static void report_too_many_sets();
65 #endif
66  public:
67 
82  struct mark_t :
83  public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
84  {
85  private:
86  // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
87  typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
88  _value_t id;
89 
90  mark_t(_value_t id) noexcept
91  : id(id)
92  {
93  }
94 
95  public:
97  mark_t() = default;
98 
99 #ifndef SWIG
101  template<class iterator>
102  mark_t(const iterator& begin, const iterator& end)
103  : mark_t(_value_t::zero())
104  {
105  for (iterator i = begin; i != end; ++i)
106  if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
107  set(*i);
108  else
109  report_too_many_sets();
110  }
111 
113  mark_t(std::initializer_list<unsigned> vals)
114  : mark_t(vals.begin(), vals.end())
115  {
116  }
117 
118  SPOT_DEPRECATED("use brace initialization instead")
119  mark_t(unsigned i)
120  {
121  unsigned j = 0;
122  while (i)
123  {
124  if (i & 1U)
125  this->set(j);
126  ++j;
127  i >>= 1;
128  }
129  }
130 #endif
131 
137  constexpr static unsigned max_accsets()
138  {
139  return SPOT_MAX_ACCSETS;
140  }
141 
147  static mark_t all()
148  {
149  return mark_t(_value_t::mone());
150  }
151 
152  size_t hash() const noexcept
153  {
154  std::hash<decltype(id)> h;
155  return h(id);
156  }
157 
158  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
159  bool operator==(unsigned o) const
160  {
161  SPOT_ASSERT(o == 0U);
162  (void)o;
163  return !id;
164  }
165 
166  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
167  bool operator!=(unsigned o) const
168  {
169  SPOT_ASSERT(o == 0U);
170  (void)o;
171  return !!id;
172  }
173 
174  bool operator==(mark_t o) const
175  {
176  return id == o.id;
177  }
178 
179  bool operator!=(mark_t o) const
180  {
181  return id != o.id;
182  }
183 
184  bool operator<(mark_t o) const
185  {
186  return id < o.id;
187  }
188 
189  bool operator<=(mark_t o) const
190  {
191  return id <= o.id;
192  }
193 
194  bool operator>(mark_t o) const
195  {
196  return id > o.id;
197  }
198 
199  bool operator>=(mark_t o) const
200  {
201  return id >= o.id;
202  }
203 
204  explicit operator bool() const
205  {
206  return !!id;
207  }
208 
209  bool has(unsigned u) const
210  {
211  return !!this->operator&(mark_t({0}) << u);
212  }
213 
214  void set(unsigned u)
215  {
216  id.set(u);
217  }
218 
219  void clear(unsigned u)
220  {
221  id.clear(u);
222  }
223 
224  mark_t& operator&=(mark_t r)
225  {
226  id &= r.id;
227  return *this;
228  }
229 
230  mark_t& operator|=(mark_t r)
231  {
232  id |= r.id;
233  return *this;
234  }
235 
236  mark_t& operator-=(mark_t r)
237  {
238  id &= ~r.id;
239  return *this;
240  }
241 
242  mark_t& operator^=(mark_t r)
243  {
244  id ^= r.id;
245  return *this;
246  }
247 
248  mark_t operator&(mark_t r) const
249  {
250  return id & r.id;
251  }
252 
253  mark_t operator|(mark_t r) const
254  {
255  return id | r.id;
256  }
257 
258  mark_t operator-(mark_t r) const
259  {
260  return id & ~r.id;
261  }
262 
263  mark_t operator~() const
264  {
265  return ~id;
266  }
267 
268  mark_t operator^(mark_t r) const
269  {
270  return id ^ r.id;
271  }
272 
273 #if SPOT_DEBUG || defined(SWIGPYTHON)
274 # define SPOT_WRAP_OP(ins) \
275  try \
276  { \
277  ins; \
278  } \
279  catch (const std::runtime_error& e) \
280  { \
281  report_too_many_sets(); \
282  }
283 #else
284 # define SPOT_WRAP_OP(ins) ins;
285 #endif
286  mark_t operator<<(unsigned i) const
287  {
288  SPOT_WRAP_OP(return id << i);
289  }
290 
291  mark_t& operator<<=(unsigned i)
292  {
293  SPOT_WRAP_OP(id <<= i; return *this);
294  }
295 
296  mark_t operator>>(unsigned i) const
297  {
298  SPOT_WRAP_OP(return id >> i);
299  }
300 
301  mark_t& operator>>=(unsigned i)
302  {
303  SPOT_WRAP_OP(id >>= i; return *this);
304  }
305 #undef SPOT_WRAP_OP
306 
307  mark_t strip(mark_t y) const
308  {
309  // strip every bit of id that is marked in y
310  // 100101110100.strip(
311  // 001011001000)
312  // == 10 1 11 100
313  // == 10111100
314 
315  auto xv = id; // 100101110100
316  auto yv = y.id; // 001011001000
317 
318  while (yv && xv)
319  {
320  // Mask for everything after the last 1 in y
321  auto rm = (~yv) & (yv - 1); // 000000000111
322  // Mask for everything before the last 1 in y
323  auto lm = ~(yv ^ (yv - 1)); // 111111110000
324  xv = ((xv & lm) >> 1) | (xv & rm);
325  yv = (yv & lm) >> 1;
326  }
327  return xv;
328  }
329 
332  bool subset(mark_t m) const
333  {
334  return !((*this) - m);
335  }
336 
339  bool proper_subset(mark_t m) const
340  {
341  return *this != m && this->subset(m);
342  }
343 
345  unsigned count() const
346  {
347  return id.count();
348  }
349 
354  unsigned max_set() const
355  {
356  if (id)
357  return id.highest()+1;
358  else
359  return 0;
360  }
361 
366  unsigned min_set() const
367  {
368  if (id)
369  return id.lowest()+1;
370  else
371  return 0;
372  }
373 
378  mark_t lowest() const
379  {
380  return id & -id;
381  }
382 
384  bool is_singleton() const
385  {
386 #if __GNUC__
387  /* With GCC and Clang, count() is implemented using popcount. */
388  return count() == 1;
389 #else
390  return id && !(id & (id - 1));
391 #endif
392  }
393 
395  bool has_many() const
396  {
397 #if __GNUC__
398  /* With GCC and Clang, count() is implemented using popcount. */
399  return count() > 1;
400 #else
401  return !!(id & (id - 1));
402 #endif
403  }
404 
408  mark_t& remove_some(unsigned n)
409  {
410  while (n--)
411  id &= id - 1;
412  return *this;
413  }
414 
416  template<class iterator>
417  void fill(iterator here) const
418  {
419  auto a = *this;
420  unsigned level = 0;
421  while (a)
422  {
423  if (a.has(0))
424  *here++ = level;
425  ++level;
426  a >>= 1;
427  }
428  }
429 
431  spot::internal::mark_container sets() const;
432 
433  std::string as_string() const;
434  };
435 
437  enum class acc_op : unsigned short
438  { Inf, Fin, InfNeg, FinNeg, And, Or };
439 
447  union acc_word
448  {
449  mark_t mark;
450  struct {
451  acc_op op; // Operator
452  unsigned short size; // Size of the subtree (number of acc_word),
453  // not counting this node.
454  } sub;
455  };
456 
469  struct SPOT_API acc_code: public std::vector<acc_word>
470  {
471  acc_code
472  unit_propagation();
473 
474  bool operator==(const acc_code& other) const
475  {
476  // We have two ways to represent t, unfortunately.
477  if (is_t() && other.is_t())
478  return true;
479  unsigned pos = size();
480  if (other.size() != pos)
481  return false;
482  while (pos > 0)
483  {
484  auto op = (*this)[pos - 1].sub.op;
485  auto sz = (*this)[pos - 1].sub.size;
486  if (other[pos - 1].sub.op != op ||
487  other[pos - 1].sub.size != sz)
488  return false;
489  switch (op)
490  {
491  case acc_cond::acc_op::And:
492  case acc_cond::acc_op::Or:
493  --pos;
494  break;
495  case acc_cond::acc_op::Inf:
496  case acc_cond::acc_op::InfNeg:
497  case acc_cond::acc_op::Fin:
498  case acc_cond::acc_op::FinNeg:
499  pos -= 2;
500  if (other[pos].mark != (*this)[pos].mark)
501  return false;
502  break;
503  }
504  }
505  return true;
506  };
507 
508  bool operator<(const acc_code& other) const
509  {
510  // We have two ways to represent t, unfortunately.
511  if (is_t() && other.is_t())
512  return false;
513  unsigned pos = size();
514  auto osize = other.size();
515  if (pos < osize)
516  return true;
517  if (pos > osize)
518  return false;
519  while (pos > 0)
520  {
521  auto op = (*this)[pos - 1].sub.op;
522  auto oop = other[pos - 1].sub.op;
523  if (op < oop)
524  return true;
525  if (op > oop)
526  return false;
527  auto sz = (*this)[pos - 1].sub.size;
528  auto osz = other[pos - 1].sub.size;
529  if (sz < osz)
530  return true;
531  if (sz > osz)
532  return false;
533  switch (op)
534  {
535  case acc_cond::acc_op::And:
536  case acc_cond::acc_op::Or:
537  --pos;
538  break;
539  case acc_cond::acc_op::Inf:
540  case acc_cond::acc_op::InfNeg:
541  case acc_cond::acc_op::Fin:
542  case acc_cond::acc_op::FinNeg:
543  {
544  pos -= 2;
545  auto m = (*this)[pos].mark;
546  auto om = other[pos].mark;
547  if (m < om)
548  return true;
549  if (m > om)
550  return false;
551  break;
552  }
553  }
554  }
555  return false;
556  }
557 
558  bool operator>(const acc_code& other) const
559  {
560  return other < *this;
561  }
562 
563  bool operator<=(const acc_code& other) const
564  {
565  return !(other < *this);
566  }
567 
568  bool operator>=(const acc_code& other) const
569  {
570  return !(*this < other);
571  }
572 
573  bool operator!=(const acc_code& other) const
574  {
575  return !(*this == other);
576  }
577 
582  bool is_t() const
583  {
584  // We store "t" as an empty condition, or as Inf({}).
585  unsigned s = size();
586  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
587  && !((*this)[s - 2].mark));
588  }
589 
596  bool is_f() const
597  {
598  // We store "f" as Fin({}).
599  unsigned s = size();
600  return s > 1
601  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
602  }
603 
610  static acc_code f()
611  {
612  acc_code res;
613  res.resize(2);
614  res[0].mark = {};
615  res[1].sub.op = acc_op::Fin;
616  res[1].sub.size = 1;
617  return res;
618  }
619 
624  static acc_code t()
625  {
626  return {};
627  }
628 
636  static acc_code fin(mark_t m)
637  {
638  acc_code res;
639  res.resize(2);
640  res[0].mark = m;
641  res[1].sub.op = acc_op::Fin;
642  res[1].sub.size = 1;
643  return res;
644  }
645 
646  static acc_code fin(std::initializer_list<unsigned> vals)
647  {
648  return fin(mark_t(vals));
649  }
651 
669  {
670  acc_code res;
671  res.resize(2);
672  res[0].mark = m;
673  res[1].sub.op = acc_op::FinNeg;
674  res[1].sub.size = 1;
675  return res;
676  }
677 
678  static acc_code fin_neg(std::initializer_list<unsigned> vals)
679  {
680  return fin_neg(mark_t(vals));
681  }
683 
692  static acc_code inf(mark_t m)
693  {
694  acc_code res;
695  res.resize(2);
696  res[0].mark = m;
697  res[1].sub.op = acc_op::Inf;
698  res[1].sub.size = 1;
699  return res;
700  }
701 
702  static acc_code inf(std::initializer_list<unsigned> vals)
703  {
704  return inf(mark_t(vals));
705  }
707 
725  {
726  acc_code res;
727  res.resize(2);
728  res[0].mark = m;
729  res[1].sub.op = acc_op::InfNeg;
730  res[1].sub.size = 1;
731  return res;
732  }
733 
734  static acc_code inf_neg(std::initializer_list<unsigned> vals)
735  {
736  return inf_neg(mark_t(vals));
737  }
739 
743  static acc_code buchi()
744  {
745  return inf({0});
746  }
747 
751  static acc_code cobuchi()
752  {
753  return fin({0});
754  }
755 
761  static acc_code generalized_buchi(unsigned n)
762  {
763  if (n == 0)
764  return inf({});
765  acc_cond::mark_t m = mark_t::all();
766  m >>= mark_t::max_accsets() - n;
767  return inf(m);
768  }
769 
775  static acc_code generalized_co_buchi(unsigned n)
776  {
777  if (n == 0)
778  return fin({});
779  acc_cond::mark_t m = mark_t::all();
780  m >>= mark_t::max_accsets() - n;
781  return fin(m);
782  }
783 
788  static acc_code rabin(unsigned n)
789  {
790  acc_cond::acc_code res = f();
791  while (n > 0)
792  {
793  res |= inf({2*n - 1}) & fin({2*n - 2});
794  --n;
795  }
796  return res;
797  }
798 
803  static acc_code streett(unsigned n)
804  {
805  acc_cond::acc_code res = t();
806  while (n > 0)
807  {
808  res &= inf({2*n - 1}) | fin({2*n - 2});
809  --n;
810  }
811  return res;
812  }
813 
826  template<class Iterator>
827  static acc_code generalized_rabin(Iterator begin, Iterator end)
828  {
829  acc_cond::acc_code res = f();
830  unsigned n = 0;
831  for (Iterator i = begin; i != end; ++i)
832  {
833  unsigned f = n++;
834  acc_cond::mark_t m = {};
835  for (unsigned ni = *i; ni > 0; --ni)
836  m.set(n++);
837  auto pair = inf(m) & fin({f});
838  std::swap(pair, res);
839  res |= std::move(pair);
840  }
841  return res;
842  }
843 
851  static acc_code parity(bool is_max, bool is_odd, unsigned sets);
852  static acc_code parity_max(bool is_odd, unsigned sets)
853  {
854  return parity(true, is_odd, sets);
855  }
856  static acc_code parity_max_odd(unsigned sets)
857  {
858  return parity_max(true, sets);
859  }
860  static acc_code parity_max_even(unsigned sets)
861  {
862  return parity_max(false, sets);
863  }
864  static acc_code parity_min(bool is_odd, unsigned sets)
865  {
866  return parity(false, is_odd, sets);
867  }
868  static acc_code parity_min_odd(unsigned sets)
869  {
870  return parity_min(true, sets);
871  }
872  static acc_code parity_min_even(unsigned sets)
873  {
874  return parity_min(false, sets);
875  }
877 
894  static acc_code random(unsigned n, double reuse = 0.0);
895 
898  {
899  if (is_t() || r.is_f())
900  {
901  *this = r;
902  return *this;
903  }
904  if (is_f() || r.is_t())
905  return *this;
906  unsigned s = size() - 1;
907  unsigned rs = r.size() - 1;
908  // We want to group all Inf(x) operators:
909  // Inf(a) & Inf(b) = Inf(a & b)
910  if (((*this)[s].sub.op == acc_op::Inf
911  && r[rs].sub.op == acc_op::Inf)
912  || ((*this)[s].sub.op == acc_op::InfNeg
913  && r[rs].sub.op == acc_op::InfNeg))
914  {
915  (*this)[s - 1].mark |= r[rs - 1].mark;
916  return *this;
917  }
918 
919  // In the more complex scenarios, left and right may both
920  // be conjunctions, and Inf(x) might be a member of each
921  // side. Find it if it exists.
922  // left_inf points to the left Inf mark if any.
923  // right_inf points to the right Inf mark if any.
924  acc_word* left_inf = nullptr;
925  if ((*this)[s].sub.op == acc_op::And)
926  {
927  auto start = &(*this)[s] - (*this)[s].sub.size;
928  auto pos = &(*this)[s] - 1;
929  pop_back();
930  while (pos > start)
931  {
932  if (pos->sub.op == acc_op::Inf)
933  {
934  left_inf = pos - 1;
935  break;
936  }
937  pos -= pos->sub.size + 1;
938  }
939  }
940  else if ((*this)[s].sub.op == acc_op::Inf)
941  {
942  left_inf = &(*this)[s - 1];
943  }
944 
945  const acc_word* right_inf = nullptr;
946  auto right_end = &r.back();
947  if (right_end->sub.op == acc_op::And)
948  {
949  auto start = &r[0];
950  auto pos = --right_end;
951  while (pos > start)
952  {
953  if (pos->sub.op == acc_op::Inf)
954  {
955  right_inf = pos - 1;
956  break;
957  }
958  pos -= pos->sub.size + 1;
959  }
960  }
961  else if (right_end->sub.op == acc_op::Inf)
962  {
963  right_inf = right_end - 1;
964  }
965 
966  acc_cond::mark_t carry = {};
967  if (left_inf && right_inf)
968  {
969  carry = left_inf->mark;
970  auto pos = left_inf - &(*this)[0];
971  erase(begin() + pos, begin() + pos + 2);
972  }
973  auto sz = size();
974  insert(end(), &r[0], right_end + 1);
975  if (carry)
976  (*this)[sz + (right_inf - &r[0])].mark |= carry;
977 
978  acc_word w;
979  w.sub.op = acc_op::And;
980  w.sub.size = size();
981  emplace_back(w);
982  return *this;
983  }
984 
986  acc_code operator&(const acc_code& r) const
987  {
988  acc_code res = *this;
989  res &= r;
990  return res;
991  }
992 
993 #ifndef SWIG
996  {
997  acc_code res = *this;
998  res &= r;
999  return res;
1000  }
1001 #endif // SWIG
1002 
1005  {
1006  if (is_t() || r.is_f())
1007  return *this;
1008  if (is_f() || r.is_t())
1009  {
1010  *this = r;
1011  return *this;
1012  }
1013  unsigned s = size() - 1;
1014  unsigned rs = r.size() - 1;
1015  // Fin(a) | Fin(b) = Fin(a | b)
1016  if (((*this)[s].sub.op == acc_op::Fin
1017  && r[rs].sub.op == acc_op::Fin)
1018  || ((*this)[s].sub.op == acc_op::FinNeg
1019  && r[rs].sub.op == acc_op::FinNeg))
1020  {
1021  (*this)[s - 1].mark |= r[rs - 1].mark;
1022  return *this;
1023  }
1024 
1025  // In the more complex scenarios, left and right may both
1026  // be disjunctions, and Fin(x) might be a member of each
1027  // side. Find it if it exists.
1028  // left_inf points to the left Inf mark if any.
1029  // right_inf points to the right Inf mark if any.
1030  acc_word* left_fin = nullptr;
1031  if ((*this)[s].sub.op == acc_op::Or)
1032  {
1033  auto start = &(*this)[s] - (*this)[s].sub.size;
1034  auto pos = &(*this)[s] - 1;
1035  pop_back();
1036  while (pos > start)
1037  {
1038  if (pos->sub.op == acc_op::Fin)
1039  {
1040  left_fin = pos - 1;
1041  break;
1042  }
1043  pos -= pos->sub.size + 1;
1044  }
1045  }
1046  else if ((*this)[s].sub.op == acc_op::Fin)
1047  {
1048  left_fin = &(*this)[s - 1];
1049  }
1050 
1051  const acc_word* right_fin = nullptr;
1052  auto right_end = &r.back();
1053  if (right_end->sub.op == acc_op::Or)
1054  {
1055  auto start = &r[0];
1056  auto pos = --right_end;
1057  while (pos > start)
1058  {
1059  if (pos->sub.op == acc_op::Fin)
1060  {
1061  right_fin = pos - 1;
1062  break;
1063  }
1064  pos -= pos->sub.size + 1;
1065  }
1066  }
1067  else if (right_end->sub.op == acc_op::Fin)
1068  {
1069  right_fin = right_end - 1;
1070  }
1071 
1072  acc_cond::mark_t carry = {};
1073  if (left_fin && right_fin)
1074  {
1075  carry = left_fin->mark;
1076  auto pos = (left_fin - &(*this)[0]);
1077  this->erase(begin() + pos, begin() + pos + 2);
1078  }
1079  auto sz = size();
1080  insert(end(), &r[0], right_end + 1);
1081  if (carry)
1082  (*this)[sz + (right_fin - &r[0])].mark |= carry;
1083  acc_word w;
1084  w.sub.op = acc_op::Or;
1085  w.sub.size = size();
1086  emplace_back(w);
1087  return *this;
1088  }
1089 
1090 #ifndef SWIG
1093  {
1094  acc_code res = *this;
1095  res |= r;
1096  return res;
1097  }
1098 #endif // SWIG
1099 
1101  acc_code operator|(const acc_code& r) const
1102  {
1103  acc_code res = *this;
1104  res |= r;
1105  return res;
1106  }
1107 
1113  acc_code& operator<<=(unsigned sets)
1114  {
1115  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1116  report_too_many_sets();
1117  if (empty())
1118  return *this;
1119  unsigned pos = size();
1120  do
1121  {
1122  switch ((*this)[pos - 1].sub.op)
1123  {
1124  case acc_cond::acc_op::And:
1125  case acc_cond::acc_op::Or:
1126  --pos;
1127  break;
1128  case acc_cond::acc_op::Inf:
1129  case acc_cond::acc_op::InfNeg:
1130  case acc_cond::acc_op::Fin:
1131  case acc_cond::acc_op::FinNeg:
1132  pos -= 2;
1133  (*this)[pos].mark <<= sets;
1134  break;
1135  }
1136  }
1137  while (pos > 0);
1138  return *this;
1139  }
1140 
1144  acc_code operator<<(unsigned sets) const
1145  {
1146  acc_code res = *this;
1147  res <<= sets;
1148  return res;
1149  }
1150 
1157  bool is_dnf() const;
1158 
1165  bool is_cnf() const;
1166 
1177  acc_code to_dnf() const;
1178 
1185  acc_code to_cnf() const;
1186 
1191  bdd to_bdd(const bdd* map) const;
1192 
1201  std::vector<acc_code> top_disjuncts() const;
1202 
1211  std::vector<acc_code> top_conjuncts() const;
1212 
1224 
1238  mark_t fin_unit() const;
1239 
1252  mark_t mafins() const;
1253 
1265  mark_t inf_unit() const;
1266 
1271  int fin_one() const;
1272 
1293  std::pair<int, acc_code> fin_one_extract() const;
1294 
1313  std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1315  std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1318 
1331  std::vector<std::vector<int>>
1332  missing(mark_t inf, bool accepting) const;
1333 
1336  bool accepting(mark_t inf) const;
1337 
1343  bool inf_satisfiable(mark_t inf) const;
1344 
1356  trival maybe_accepting(mark_t infinitely_often,
1357  mark_t always_present) const;
1358 
1369  std::vector<unsigned> symmetries() const;
1370 
1384  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1385 
1390  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1393 
1396 
1408  std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1410 
1418 
1420  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1421 
1426  std::ostream&
1427  to_html(std::ostream& os,
1428  std::function<void(std::ostream&, int)>
1429  set_printer = nullptr) const;
1430 
1435  std::ostream&
1436  to_text(std::ostream& os,
1437  std::function<void(std::ostream&, int)>
1438  set_printer = nullptr) const;
1439 
1444  std::ostream&
1445  to_latex(std::ostream& os,
1446  std::function<void(std::ostream&, int)>
1447  set_printer = nullptr) const;
1448 
1471  acc_code(const char* input);
1472 
1477  {
1478  }
1479 
1481  acc_code(const acc_word* other)
1482  : std::vector<acc_word>(other - other->sub.size, other + 1)
1483  {
1484  }
1485 
1486  };
1487 
1495  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1496  : num_(0U), all_({}), code_(code)
1497  {
1498  add_sets(n_sets);
1499  uses_fin_acceptance_ = check_fin_acceptance();
1500  }
1501 
1506  acc_cond(const acc_code& code)
1507  : num_(0U), all_({}), code_(code)
1508  {
1509  add_sets(code.used_sets().max_set());
1510  uses_fin_acceptance_ = check_fin_acceptance();
1511  }
1512 
1514  acc_cond(const acc_cond& o)
1515  : num_(o.num_), all_(o.all_), code_(o.code_),
1516  uses_fin_acceptance_(o.uses_fin_acceptance_)
1517  {
1518  }
1519 
1522  {
1523  num_ = o.num_;
1524  all_ = o.all_;
1525  code_ = o.code_;
1526  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1527  return *this;
1528  }
1529 
1530  ~acc_cond()
1531  {
1532  }
1533 
1537  void set_acceptance(const acc_code& code)
1538  {
1539  code_ = code;
1540  uses_fin_acceptance_ = check_fin_acceptance();
1541  }
1542 
1544  const acc_code& get_acceptance() const
1545  {
1546  return code_;
1547  }
1548 
1551  {
1552  return code_;
1553  }
1554 
1555  bool operator==(const acc_cond& other) const
1556  {
1557  if (other.num_sets() != num_)
1558  return false;
1559  const acc_code& ocode = other.get_acceptance();
1560  // We have two ways to represent t, unfortunately.
1561  return (ocode == code_ || (ocode.is_t() && code_.is_t()));
1562  }
1563 
1564  bool operator!=(const acc_cond& other) const
1565  {
1566  return !(*this == other);
1567  }
1568 
1570  bool uses_fin_acceptance() const
1571  {
1572  return uses_fin_acceptance_;
1573  }
1574 
1576  bool is_t() const
1577  {
1578  return code_.is_t();
1579  }
1580 
1585  bool is_all() const
1586  {
1587  return num_ == 0 && is_t();
1588  }
1589 
1591  bool is_f() const
1592  {
1593  return code_.is_f();
1594  }
1595 
1600  bool is_none() const
1601  {
1602  return num_ == 0 && is_f();
1603  }
1604 
1609  bool is_buchi() const
1610  {
1611  unsigned s = code_.size();
1612  return num_ == 1 &&
1613  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1614  }
1615 
1620  bool is_co_buchi() const
1621  {
1622  return num_ == 1 && is_generalized_co_buchi();
1623  }
1624 
1628  {
1629  set_acceptance(inf(all_sets()));
1630  }
1631 
1635  {
1636  set_acceptance(fin(all_sets()));
1637  }
1638 
1644  {
1645  unsigned s = code_.size();
1646  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1647  && code_[0].mark == all_sets());
1648  }
1649 
1655  {
1656  unsigned s = code_.size();
1657  return (s == 2 &&
1658  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1659  }
1660 
1672  int is_rabin() const;
1673 
1685  int is_streett() const;
1686 
1696  struct SPOT_API rs_pair
1697  {
1698 #ifndef SWIG
1699  rs_pair() = default;
1700  rs_pair(const rs_pair&) = default;
1701  rs_pair& operator=(const rs_pair&) = default;
1702 #endif
1703 
1704  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1705  fin(fin),
1706  inf(inf)
1707  {}
1708  acc_cond::mark_t fin;
1709  acc_cond::mark_t inf;
1710 
1711  bool operator==(rs_pair o) const
1712  {
1713  return fin == o.fin && inf == o.inf;
1714  }
1715  bool operator!=(rs_pair o) const
1716  {
1717  return fin != o.fin || inf != o.inf;
1718  }
1719  bool operator<(rs_pair o) const
1720  {
1721  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1722  }
1723  bool operator<=(rs_pair o) const
1724  {
1725  return !(o < *this);
1726  }
1727  bool operator>(rs_pair o) const
1728  {
1729  return o < *this;
1730  }
1731  bool operator>=(rs_pair o) const
1732  {
1733  return !(*this < o);
1734  }
1735  };
1746  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1747 
1758  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1759 
1769  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1770 
1783  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1784 
1794  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1795 
1796 
1799  bool is_parity() const
1800  {
1801  bool max;
1802  bool odd;
1803  return is_parity(max, odd);
1804  }
1805 
1814  {
1815  return acc_cond(num_, code_.unit_propagation());
1816  }
1817 
1818  // Return (true, m) if there exist some acceptance mark m that
1819  // does not satisfy the acceptance condition. Return (false, 0U)
1820  // otherwise.
1821  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1822  {
1823  return sat_unsat_mark(false);
1824  }
1825  // Return (true, m) if there exist some acceptance mark m that
1826  // does satisfy the acceptance condition. Return (false, 0U)
1827  // otherwise.
1828  std::pair<bool, acc_cond::mark_t> sat_mark() const
1829  {
1830  return sat_unsat_mark(true);
1831  }
1832 
1833  protected:
1834  bool check_fin_acceptance() const;
1835  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1836 
1837  public:
1846  static acc_code inf(mark_t mark)
1847  {
1848  return acc_code::inf(mark);
1849  }
1850 
1851  static acc_code inf(std::initializer_list<unsigned> vals)
1852  {
1853  return inf(mark_t(vals.begin(), vals.end()));
1854  }
1856 
1873  static acc_code inf_neg(mark_t mark)
1874  {
1875  return acc_code::inf_neg(mark);
1876  }
1877 
1878  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1879  {
1880  return inf_neg(mark_t(vals.begin(), vals.end()));
1881  }
1883 
1891  static acc_code fin(mark_t mark)
1892  {
1893  return acc_code::fin(mark);
1894  }
1895 
1896  static acc_code fin(std::initializer_list<unsigned> vals)
1897  {
1898  return fin(mark_t(vals.begin(), vals.end()));
1899  }
1901 
1918  static acc_code fin_neg(mark_t mark)
1919  {
1920  return acc_code::fin_neg(mark);
1921  }
1922 
1923  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1924  {
1925  return fin_neg(mark_t(vals.begin(), vals.end()));
1926  }
1928 
1933  unsigned add_sets(unsigned num)
1934  {
1935  if (num == 0)
1936  return -1U;
1937  unsigned j = num_;
1938  num += j;
1939  if (num > mark_t::max_accsets())
1940  report_too_many_sets();
1941  // Make sure we do not update if we raised an exception.
1942  num_ = num;
1943  all_ = all_sets_();
1944  return j;
1945  }
1946 
1951  unsigned add_set()
1952  {
1953  return add_sets(1);
1954  }
1955 
1957  mark_t mark(unsigned u) const
1958  {
1959  SPOT_ASSERT(u < num_sets());
1960  return mark_t({u});
1961  }
1962 
1967  mark_t comp(const mark_t& l) const
1968  {
1969  return all_ ^ l;
1970  }
1971 
1974  {
1975  return all_;
1976  }
1977 
1980  bool accepting(mark_t inf) const
1981  {
1982  return code_.accepting(inf);
1983  }
1984 
1990  bool inf_satisfiable(mark_t inf) const
1991  {
1992  return code_.inf_satisfiable(inf);
1993  }
1994 
2006  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
2007  {
2008  return code_.maybe_accepting(infinitely_often, always_present);
2009  }
2010 
2025 
2026  // Deprecated since Spot 2.8
2027  SPOT_DEPRECATED("Use operator<< instead.")
2028  std::ostream& format(std::ostream& os, mark_t m) const;
2029 
2030  // Deprecated since Spot 2.8
2031  SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2032  std::string format(mark_t m) const;
2033 
2035  unsigned num_sets() const
2036  {
2037  return num_;
2038  }
2039 
2047  template<class iterator>
2048  mark_t useless(iterator begin, iterator end) const
2049  {
2050  mark_t u = {}; // The set of useless sets
2051  for (unsigned x = 0; x < num_; ++x)
2052  {
2053  // Skip sets that are already known to be useless.
2054  if (u.has(x))
2055  continue;
2056  auto all = comp(u | mark_t({x}));
2057  // Iterate over all mark_t, and keep track of
2058  // set numbers that always appear with x.
2059  for (iterator y = begin; y != end; ++y)
2060  {
2061  const mark_t& v = *y;
2062  if (v.has(x))
2063  {
2064  all &= v;
2065  if (!all)
2066  break;
2067  }
2068  }
2069  u |= all;
2070  }
2071  return u;
2072  }
2073 
2087  acc_cond remove(mark_t rem, bool missing) const
2088  {
2089  return {num_sets(), code_.remove(rem, missing)};
2090  }
2091 
2096  acc_cond strip(mark_t rem, bool missing) const
2097  {
2098  return
2099  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2100  }
2101 
2104  {
2105  return {num_sets(), code_.force_inf(m)};
2106  }
2107 
2111  {
2112  return {num_sets(), code_.remove(all_sets() - rem, true)};
2113  }
2114 
2126  std::string name(const char* fmt = "alo") const;
2127 
2142  {
2143  return code_.fin_unit();
2144  }
2145 
2158  mark_t mafins() const
2159  {
2160  return code_.mafins();
2161  }
2162 
2175  {
2176  return code_.inf_unit();
2177  }
2178 
2183  int fin_one() const
2184  {
2185  return code_.fin_one();
2186  }
2187 
2208  std::pair<int, acc_cond> fin_one_extract() const
2209  {
2210  auto [f, c] = code_.fin_one_extract();
2211  return {f, {num_sets(), std::move(c)}};
2212  }
2213 
2232  std::tuple<int, acc_cond, acc_cond>
2234  {
2235  auto [f, l, r] = code_.fin_unit_one_split();
2236  return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2237  }
2238  std::tuple<int, acc_cond, acc_cond>
2240  {
2241  auto [f, l, r] = code_.fin_unit_one_split_improved();
2242  return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2243  }
2245 
2254  std::vector<acc_cond> top_disjuncts() const;
2255 
2264  std::vector<acc_cond> top_conjuncts() const;
2265 
2266  protected:
2267  mark_t all_sets_() const
2268  {
2269  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2270  }
2271 
2272  unsigned num_;
2273  mark_t all_;
2274  acc_code code_;
2275  bool uses_fin_acceptance_ = false;
2276 
2277  };
2278 
2279  struct rs_pairs_view {
2280  typedef std::vector<acc_cond::rs_pair> rs_pairs;
2281 
2282  // Creates view of pairs 'p' with restriction only to marks in 'm'
2283  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2284  : pairs_(p), view_marks_(m) {}
2285 
2286  // Creates view of pairs without restriction to marks
2287  explicit rs_pairs_view(const rs_pairs& p)
2289 
2290  acc_cond::mark_t infs() const
2291  {
2292  return do_view([&](const acc_cond::rs_pair& p)
2293  {
2294  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2295  });
2296  }
2297 
2298  acc_cond::mark_t fins() const
2299  {
2300  return do_view([&](const acc_cond::rs_pair& p)
2301  {
2302  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2303  });
2304  }
2305 
2306  acc_cond::mark_t fins_alone() const
2307  {
2308  return do_view([&](const acc_cond::rs_pair& p)
2309  {
2310  return !visible(p.inf) && visible(p.fin) ? p.fin
2311  : acc_cond::mark_t({});
2312  });
2313  }
2314 
2315  acc_cond::mark_t infs_alone() const
2316  {
2317  return do_view([&](const acc_cond::rs_pair& p)
2318  {
2319  return !visible(p.fin) && visible(p.inf) ? p.inf
2320  : acc_cond::mark_t({});
2321  });
2322  }
2323 
2324  acc_cond::mark_t paired_with_fin(unsigned mark) const
2325  {
2326  acc_cond::mark_t res = {};
2327  for (const auto& p: pairs_)
2328  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2329  res |= p.inf;
2330  return res;
2331  }
2332 
2333  const rs_pairs& pairs() const
2334  {
2335  return pairs_;
2336  }
2337 
2338  private:
2339  template<typename filter>
2340  acc_cond::mark_t do_view(const filter& filt) const
2341  {
2342  acc_cond::mark_t res = {};
2343  for (const auto& p: pairs_)
2344  res |= filt(p);
2345  return res;
2346  }
2347 
2348  bool visible(const acc_cond::mark_t& v) const
2349  {
2350  return !!(view_marks_ & v);
2351  }
2352 
2353  const rs_pairs& pairs_;
2354  acc_cond::mark_t view_marks_;
2355  };
2356 
2357 
2358  SPOT_API
2359  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2360 
2361  // The next two operators used to be declared as friend inside the
2362  // acc_cond::mark_t and acc_cond::acc_code, but Swig 4.2.1
2363  // introduced a bug with friend operators. See
2364  // https://github.com/swig/swig/issues/2845
2365 
2366  SPOT_API
2367  std::ostream& operator<<(std::ostream& os, acc_cond::mark_t m);
2368 
2370  SPOT_API
2371  std::ostream& operator<<(std::ostream& os,
2372  const acc_cond::acc_code& code);
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 
2392  mark_iterator(acc_cond::mark_t m) noexcept
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:
2426  acc_cond::mark_t m_;
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 
2456 namespace 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:61
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:1990
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1973
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1918
mark_t mafins() const
Find a Fin(i) that is mandatory.
Definition: acc.hh:2158
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1873
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1813
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1634
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1544
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1891
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1620
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition: acc.hh:1980
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1846
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1643
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1923
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1851
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1951
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...
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1957
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1627
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2103
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2087
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:2233
acc_op
Operators for acceptance formulas.
Definition: acc.hh:438
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1495
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1933
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:1799
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1576
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:1967
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:2239
std::vector< acc_cond > top_conjuncts() const
Return the top-level conjuncts.
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:2208
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1896
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1654
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:2110
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:2006
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:1600
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1537
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:1585
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2096
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2183
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:2048
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:2141
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1550
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:1506
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1514
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1521
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1878
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:1609
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition: acc.hh:2174
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1570
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1591
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2035
std::vector< acc_cond > top_disjuncts() const
Return the top-level disjuncts.
Definition: bitset.hh:38
Definition: acc.hh:2430
Definition: acc.hh:2379
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
op
Operator types.
Definition: formula.hh:78
@ Or
(omega-Rational) Or
@ U
until
@ And
(omega-Rational) And
Definition: automata.hh:26
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:130
An acceptance formula.
Definition: acc.hh:470
std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > useless_colors_patterns() const
Find patterns of useless colors.
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.
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:852
mark_t mafins() const
Find a Fin(i) that is mandatory.
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:692
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:995
acc_code force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
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_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:734
std::vector< acc_code > top_disjuncts() const
Return the top-level disjuncts.
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.
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:1101
std::vector< std::vector< int > > missing(mark_t inf, bool accepting) const
Help closing accepting or rejecting cycle.
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1092
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:646
bool is_dnf() const
Whether the acceptance formula is in disjunctive normal form.
acc_code operator&(const acc_code &r) const
Conjunct the current condition with r.
Definition: acc.hh:986
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:702
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:872
static acc_code parity(bool is_max, bool is_odd, unsigned sets)
Build a parity acceptance 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.
mark_t used_once_sets() const
Return the sets that appears only once in the acceptance.
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:596
std::ostream & to_text(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as text.
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:761
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:868
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1481
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:860
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:610
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:856
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:582
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1144
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:788
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1476
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:751
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:724
bdd to_bdd(const bdd *map) const
Convert the acceptance formula into a BDD.
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.
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:678
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1113
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:803
std::vector< acc_code > top_conjuncts() const
Return the top-level conjuncts.
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:624
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:668
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:864
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 ...
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:636
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:743
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:775
std::vector< unsigned > symmetries() const
compute the symmetry class of the acceptance sets.
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:827
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1004
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition: acc.hh:897
std::ostream & to_latex(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as LaTeX.
An acceptance mark.
Definition: acc.hh:84
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:384
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:378
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:354
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:408
constexpr static unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:137
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:147
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:339
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:102
unsigned count() const
Number of bits sets.
Definition: acc.hh:345
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:113
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:395
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:366
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:332
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:417
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1697
Definition: acc.hh:40
Definition: acc.hh:2279
A "node" in an acceptance formulas.
Definition: acc.hh:448

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.1