23 #include <unordered_map>
26 #include <spot/tl/defaultenv.hh>
36 typedef unsigned value_t;
41 mark_t(value_t
id) noexcept
46 template<
class iterator>
47 mark_t(
const iterator& begin,
const iterator& end) noexcept
50 for (iterator i = begin; i != end; ++i)
54 mark_t(std::initializer_list<unsigned> vals) noexcept
55 :
mark_t(vals.begin(), vals.end())
59 bool operator==(
unsigned o)
const
65 bool operator!=(
unsigned o)
const
71 bool operator==(
mark_t o)
const
76 bool operator!=(
mark_t o)
const
81 bool operator<(
mark_t o)
const
86 bool operator<=(
mark_t o)
const
91 bool operator>(
mark_t o)
const
96 bool operator>=(
mark_t o)
const
101 operator bool()
const
106 bool has(
unsigned u)
const
108 return id & (1
U << u);
116 void clear(
unsigned u)
170 mark_t operator<<(
unsigned i)
const
175 mark_t& operator<<=(
unsigned i)
181 mark_t operator>>(
unsigned i)
const
186 mark_t& operator>>=(
unsigned i)
206 auto rm = (~yv) & (yv - 1);
208 auto lm = ~(yv ^ (yv - 1));
209 xv = ((xv & lm) >> 1) | (xv & rm);
216 unsigned count()
const
219 return __builtin_popcount(
id);
235 unsigned max_set()
const
254 mark_t& remove_some(
unsigned n)
261 template<
class iterator>
262 void fill(iterator here)
const
276 std::vector<unsigned> sets()
const
278 std::vector<unsigned> res;
279 fill(std::back_inserter(res));
284 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
288 enum class acc_op : unsigned short
289 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
300 struct SPOT_API
acc_code:
public std::vector<acc_word>
302 bool operator==(
const acc_code& other)
const
304 unsigned pos = size();
305 if (other.size() != pos)
309 auto op = (*this)[pos - 1].sub.op;
310 auto sz = (*this)[pos - 1].sub.size;
311 if (other[pos - 1].sub.op !=
op ||
312 other[pos - 1].sub.size != sz)
316 case acc_cond::acc_op::And:
317 case acc_cond::acc_op::Or:
320 case acc_cond::acc_op::Inf:
321 case acc_cond::acc_op::InfNeg:
322 case acc_cond::acc_op::Fin:
323 case acc_cond::acc_op::FinNeg:
325 if (other[pos].mark != (*
this)[pos].mark)
333 bool operator<(
const acc_code& other)
const
335 unsigned pos = size();
336 auto osize = other.size();
343 auto op = (*this)[pos - 1].sub.op;
344 auto oop = other[pos - 1].sub.op;
349 auto sz = (*this)[pos - 1].sub.size;
350 auto osz = other[pos - 1].sub.size;
357 case acc_cond::acc_op::And:
358 case acc_cond::acc_op::Or:
361 case acc_cond::acc_op::Inf:
362 case acc_cond::acc_op::InfNeg:
363 case acc_cond::acc_op::Fin:
364 case acc_cond::acc_op::FinNeg:
366 auto m = (*this)[pos].mark;
367 auto om = other[pos].mark;
378 bool operator>(
const acc_code& other)
const
380 return other < *
this;
383 bool operator<=(
const acc_code& other)
const
385 return !(other < *
this);
388 bool operator>=(
const acc_code& other)
const
390 return !(*
this < other);
393 bool operator!=(
const acc_code& other)
const
395 return !(*
this == other);
401 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
402 && (*this)[s - 2].mark == 0
U);
409 && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0
U;
417 res[1].sub.op = acc_op::Fin;
432 res[1].sub.op = acc_op::Fin;
437 static acc_code fin(std::initializer_list<unsigned> vals)
447 res[1].sub.op = acc_op::FinNeg;
452 static acc_code fin_neg(std::initializer_list<unsigned> vals)
454 return fin_neg(
mark_t(vals));
462 res[1].sub.op = acc_op::Inf;
467 static acc_code inf(std::initializer_list<unsigned> vals)
477 res[1].sub.op = acc_op::InfNeg;
482 static acc_code inf_neg(std::initializer_list<unsigned> vals)
484 return inf_neg(
mark_t(vals));
497 static acc_code generalized_buchi(
unsigned n)
500 if (n == 8 *
sizeof(mark_t::value_t))
505 static acc_code generalized_co_buchi(
unsigned n)
508 if (n == 8 *
sizeof(mark_t::value_t))
519 res |= inf({2*n - 1}) & fin({2*n - 2});
531 res &= inf({2*n - 1}) | fin({2*n - 2});
537 template<
class Iterator>
538 static acc_code generalized_rabin(Iterator begin, Iterator end)
542 for (Iterator i = begin; i != end; ++i)
546 for (
unsigned ni = *i; ni > 0; --ni)
549 std::swap(pair, res);
550 res |= std::move(pair);
555 static acc_code parity(
bool max,
bool odd,
unsigned sets);
560 static acc_code random(
unsigned n,
double reuse = 0.0);
564 if (is_t() || r.is_f())
566 *
this = std::move(r);
569 if (is_f() || r.is_t())
571 unsigned s = size() - 1;
572 unsigned rs = r.size() - 1;
575 if (((*
this)[s].sub.op == acc_op::Inf
576 && r[rs].sub.op == acc_op::Inf)
577 || ((*
this)[s].sub.op == acc_op::InfNeg
578 && r[rs].sub.op == acc_op::InfNeg))
580 (*this)[s - 1].mark |= r[rs - 1].mark;
592 auto start = &(*this)[s] - (*this)[s].sub.size;
593 auto pos = &(*this)[s] - 1;
597 if (pos->sub.op == acc_op::Inf)
602 pos -= pos->sub.size + 1;
605 else if ((*
this)[s].sub.op == acc_op::Inf)
607 left_inf = &(*this)[s - 1];
611 auto right_end = &r.back();
615 auto pos = --right_end;
618 if (pos->sub.op == acc_op::Inf)
623 pos -= pos->sub.size + 1;
626 else if (right_end->sub.op == acc_op::Inf)
628 right_inf = right_end - 1;
631 if (left_inf && right_inf)
633 left_inf->mark |= right_inf->mark;
634 insert(this->end(), &r[0], right_inf);
635 insert(this->end(), right_inf + 2, right_end + 1);
640 insert(this->begin(), right_inf, right_inf + 2);
641 insert(this->end(), &r[0], right_inf);
642 insert(this->end(), right_inf + 2, right_end + 1);
646 insert(this->end(), &r[0], right_end + 1);
658 if (is_t() || r.is_f())
663 if (is_f() || r.is_t())
665 unsigned s = size() - 1;
666 unsigned rs = r.size() - 1;
668 if (((*
this)[s].sub.op == acc_op::Inf
669 && r[rs].sub.op == acc_op::Inf)
670 || ((*
this)[s].sub.op == acc_op::InfNeg
671 && r[rs].sub.op == acc_op::InfNeg))
673 (*this)[s - 1].mark |= r[rs - 1].mark;
685 auto start = &(*this)[s] - (*this)[s].sub.size;
686 auto pos = &(*this)[s] - 1;
690 if (pos->sub.op == acc_op::Inf)
695 pos -= pos->sub.size + 1;
698 else if ((*
this)[s].sub.op == acc_op::Inf)
700 left_inf = &(*this)[s - 1];
703 const acc_word* right_inf =
nullptr;
704 auto right_end = &r.back();
708 auto pos = --right_end;
711 if (pos->sub.op == acc_op::Inf)
716 pos -= pos->sub.size + 1;
719 else if (right_end->sub.op == acc_op::Inf)
721 right_inf = right_end - 1;
724 if (left_inf && right_inf)
726 left_inf->mark |= right_inf->mark;
727 insert(this->end(), &r[0], right_inf);
728 insert(this->end(), right_inf + 2, right_end + 1);
733 insert(this->begin(), right_inf, right_inf + 2);
734 insert(this->end(), &r[0], right_inf);
735 insert(this->end(), right_inf + 2, right_end + 1);
739 insert(this->end(), &r[0], right_end + 1);
765 if (is_t() || r.is_f())
767 if (is_f() || r.is_t())
769 *
this = std::move(r);
772 unsigned s = size() - 1;
773 unsigned rs = r.size() - 1;
775 if (((*
this)[s].sub.op == acc_op::Fin
776 && r[rs].sub.op == acc_op::Fin)
777 || ((*
this)[s].sub.op == acc_op::FinNeg
778 && r[rs].sub.op == acc_op::FinNeg))
780 (*this)[s - 1].mark |= r[rs - 1].mark;
787 insert(this->end(), r.begin(), r.end());
814 acc_code& operator<<=(
unsigned sets)
818 unsigned pos = size();
821 switch ((*
this)[pos - 1].sub.op)
823 case acc_cond::acc_op::And:
824 case acc_cond::acc_op::Or:
827 case acc_cond::acc_op::Inf:
828 case acc_cond::acc_op::InfNeg:
829 case acc_cond::acc_op::Fin:
830 case acc_cond::acc_op::FinNeg:
832 (*this)[pos].mark.id <<= sets;
840 acc_code operator<<(
unsigned sets)
const
860 std::vector<std::vector<int>>
861 missing(
mark_t inf,
bool accepting)
const;
863 bool accepting(
mark_t inf)
const;
865 bool inf_satisfiable(
mark_t inf)
const;
886 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets()
const;
891 to_html(std::ostream& os,
892 std::function<
void(std::ostream&,
int)>
893 set_printer =
nullptr)
const;
898 to_text(std::ostream& os,
899 std::function<
void(std::ostream&,
int)>
900 set_printer =
nullptr)
const;
936 friend std::ostream& operator<<(std::ostream& os,
const acc_code& code);
939 acc_cond(
unsigned n_sets = 0,
const acc_code& code = {})
940 : num_(0
U), all_(0
U), code_(code)
943 uses_fin_acceptance_ = check_fin_acceptance();
946 acc_cond(
const acc_code& code)
947 : num_(0
U), all_(0
U), code_(code)
949 add_sets(code.used_sets().max_set());
950 uses_fin_acceptance_ = check_fin_acceptance();
953 acc_cond(
const acc_cond& o)
954 : num_(o.num_), all_(o.all_), code_(o.code_),
955 uses_fin_acceptance_(o.uses_fin_acceptance_)
959 acc_cond& operator=(
const acc_cond& o)
964 uses_fin_acceptance_ = o.uses_fin_acceptance_;
972 void set_acceptance(
const acc_code& code)
975 uses_fin_acceptance_ = check_fin_acceptance();
978 const acc_code& get_acceptance()
const
983 acc_code& get_acceptance()
988 bool uses_fin_acceptance()
const
990 return uses_fin_acceptance_;
1000 return num_ == 0 && is_t();
1005 return code_.is_f();
1008 bool is_none()
const
1010 return num_ == 0 && is_f();
1013 bool is_buchi()
const
1015 unsigned s = code_.size();
1017 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1020 bool is_co_buchi()
const
1022 return num_ == 1 && is_generalized_co_buchi();
1025 void set_generalized_buchi()
1027 set_acceptance(inf(all_sets()));
1030 bool is_generalized_buchi()
const
1032 unsigned s = code_.size();
1033 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1034 && code_[0].mark == all_sets());
1037 bool is_generalized_co_buchi()
const
1039 unsigned s = code_.size();
1041 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1045 int is_rabin()
const;
1047 int is_streett()
const;
1050 bool is_generalized_rabin(std::vector<unsigned>& pairs)
const;
1057 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1058 bool is_parity()
const
1062 return is_parity(max, min);
1068 std::pair<bool, acc_cond::mark_t> unsat_mark()
const;
1071 bool check_fin_acceptance()
const;
1074 static acc_code inf(mark_t mark)
1076 return acc_code::inf(mark);
1079 static acc_code inf(std::initializer_list<unsigned> vals)
1081 return inf(mark_t(vals.begin(), vals.end()));
1084 static acc_code inf_neg(mark_t mark)
1086 return acc_code::inf_neg(mark);
1089 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1091 return inf_neg(mark_t(vals.begin(), vals.end()));
1094 static acc_code fin(mark_t mark)
1096 return acc_code::fin(mark);
1099 static acc_code fin(std::initializer_list<unsigned> vals)
1101 return fin(mark_t(vals.begin(), vals.end()));
1104 static acc_code fin_neg(mark_t mark)
1106 return acc_code::fin_neg(mark);
1109 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1111 return fin_neg(mark_t(vals.begin(), vals.end()));
1114 unsigned add_sets(
unsigned num)
1120 if (num_ > 8 *
sizeof(mark_t::id))
1121 throw std::runtime_error(
"Too many acceptance sets used.");
1131 mark_t mark(
unsigned u)
const
1133 SPOT_ASSERT(u < num_sets());
1137 mark_t comp(mark_t l)
const
1142 mark_t all_sets()
const
1147 bool accepting(mark_t inf)
const
1149 return code_.accepting(inf);
1152 bool inf_satisfiable(mark_t inf)
const
1154 return code_.inf_satisfiable(inf);
1157 mark_t accepting_sets(mark_t inf)
const;
1159 std::ostream& format(std::ostream& os, mark_t m)
const
1167 std::string format(mark_t m)
const
1169 std::ostringstream os;
1174 unsigned num_sets()
const
1179 template<
class iterator>
1180 mark_t useless(iterator begin, iterator end)
const
1182 mark_t::value_t u = 0
U;
1183 for (
unsigned x = 0; x < num_; ++x)
1188 unsigned all = all_ ^ (u | (1 << x));
1189 for (iterator y = begin; y != end; ++y)
1205 mark_t::value_t all_sets_()
const
1209 return -1
U >> (8 *
sizeof(mark_t::value_t) - num_);
1213 mark_t::value_t all_;
1215 bool uses_fin_acceptance_ =
false;
1220 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
1226 struct hash<
spot::acc_cond::mark_t>
1230 std::hash<decltype(m.id)> h;
Definition: formula.hh:1671
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:930
op
Operator types.
Definition: formula.hh:62