23 #include <unordered_map> 26 #include <spot/tl/defaultenv.hh> 27 #include <spot/misc/trival.hh> 41 typedef unsigned value_t;
46 mark_t(value_t
id) noexcept
51 template<
class iterator>
52 mark_t(
const iterator& begin,
const iterator& end) noexcept
55 for (iterator i = begin; i != end; ++i)
59 mark_t(std::initializer_list<unsigned> vals) noexcept
60 :
mark_t(vals.begin(), vals.end())
64 bool operator==(
unsigned o)
const 70 bool operator!=(
unsigned 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 bool operator>=(
mark_t o)
const 106 explicit operator bool()
const 111 bool has(
unsigned u)
const 113 return id & (1
U << u);
121 void clear(
unsigned u)
175 mark_t operator<<(
unsigned i)
const 180 mark_t& operator<<=(
unsigned i)
186 mark_t operator>>(
unsigned i)
const 191 mark_t& operator>>=(
unsigned i)
211 auto rm = (~yv) & (yv - 1);
213 auto lm = ~(yv ^ (yv - 1));
214 xv = ((xv & lm) >> 1) | (xv & rm);
220 bool subset(
mark_t m)
const 222 return this->strip(m) == 0
U;
225 bool proper_subset(
mark_t m)
const 227 return *
this != m && this->subset(m);
231 unsigned count()
const 234 return __builtin_popcount(
id);
250 unsigned max_set()
const 253 return (
id == 0) ? 0 : (
sizeof(unsigned) * 8 - __builtin_clz(
id));
269 unsigned min_set()
const 274 return __builtin_ctz(
id) + 1;
294 mark_t& remove_some(
unsigned n)
301 template<
class iterator>
302 void fill(iterator here)
const 319 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
323 enum class acc_op : unsigned short
324 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
335 struct SPOT_API
acc_code:
public std::vector<acc_word>
337 bool operator==(
const acc_code& other)
const 339 unsigned pos = size();
340 if (other.size() != pos)
344 auto op = (*this)[pos - 1].sub.op;
345 auto sz = (*this)[pos - 1].sub.size;
346 if (other[pos - 1].sub.op !=
op ||
347 other[pos - 1].sub.size != sz)
351 case acc_cond::acc_op::And:
352 case acc_cond::acc_op::Or:
355 case acc_cond::acc_op::Inf:
356 case acc_cond::acc_op::InfNeg:
357 case acc_cond::acc_op::Fin:
358 case acc_cond::acc_op::FinNeg:
360 if (other[pos].mark != (*
this)[pos].mark)
368 bool operator<(
const acc_code& other)
const 370 unsigned pos = size();
371 auto osize = other.size();
378 auto op = (*this)[pos - 1].sub.op;
379 auto oop = other[pos - 1].sub.op;
384 auto sz = (*this)[pos - 1].sub.size;
385 auto osz = other[pos - 1].sub.size;
392 case acc_cond::acc_op::And:
393 case acc_cond::acc_op::Or:
396 case acc_cond::acc_op::Inf:
397 case acc_cond::acc_op::InfNeg:
398 case acc_cond::acc_op::Fin:
399 case acc_cond::acc_op::FinNeg:
402 auto m = (*this)[pos].mark;
403 auto om = other[pos].mark;
415 bool operator>(
const acc_code& other)
const 417 return other < *
this;
420 bool operator<=(
const acc_code& other)
const 422 return !(other < *
this);
425 bool operator>=(
const acc_code& other)
const 427 return !(*
this < other);
430 bool operator!=(
const acc_code& other)
const 432 return !(*
this == other);
438 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
439 && (*this)[s - 2].mark == 0
U);
446 && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0
U;
454 res[1].sub.op = acc_op::Fin;
469 res[1].sub.op = acc_op::Fin;
474 static acc_code fin(std::initializer_list<unsigned> vals)
484 res[1].sub.op = acc_op::FinNeg;
489 static acc_code fin_neg(std::initializer_list<unsigned> vals)
491 return fin_neg(
mark_t(vals));
499 res[1].sub.op = acc_op::Inf;
504 static acc_code inf(std::initializer_list<unsigned> vals)
514 res[1].sub.op = acc_op::InfNeg;
519 static acc_code inf_neg(std::initializer_list<unsigned> vals)
521 return inf_neg(
mark_t(vals));
534 static acc_code generalized_buchi(
unsigned n)
537 if (n == 8 *
sizeof(mark_t::value_t))
542 static acc_code generalized_co_buchi(
unsigned n)
545 if (n == 8 *
sizeof(mark_t::value_t))
556 res |= inf({2*n - 1}) & fin({2*n - 2});
568 res &= inf({2*n - 1}) | fin({2*n - 2});
574 template<
class Iterator>
575 static acc_code generalized_rabin(Iterator begin, Iterator end)
579 for (Iterator i = begin; i != end; ++i)
583 for (
unsigned ni = *i; ni > 0; --ni)
585 auto pair = inf(m) & fin({f});
586 std::swap(pair, res);
587 res |= std::move(pair);
592 static acc_code parity(
bool max,
bool odd,
unsigned sets);
597 static acc_code random(
unsigned n,
double reuse = 0.0);
601 if (is_t() || r.is_f())
606 if (is_f() || r.is_t())
608 unsigned s = size() - 1;
609 unsigned rs = r.size() - 1;
612 if (((*
this)[s].sub.op == acc_op::Inf
613 && r[rs].sub.op == acc_op::Inf)
614 || ((*
this)[s].sub.op == acc_op::InfNeg
615 && r[rs].sub.op == acc_op::InfNeg))
617 (*this)[s - 1].mark |= r[rs - 1].mark;
629 auto start = &(*this)[s] - (*this)[s].sub.size;
630 auto pos = &(*this)[s] - 1;
634 if (pos->sub.op == acc_op::Inf)
639 pos -= pos->sub.size + 1;
642 else if ((*
this)[s].sub.op == acc_op::Inf)
644 left_inf = &(*this)[s - 1];
647 const acc_word* right_inf =
nullptr;
648 auto right_end = &r.back();
652 auto pos = --right_end;
655 if (pos->sub.op == acc_op::Inf)
660 pos -= pos->sub.size + 1;
663 else if (right_end->sub.op == acc_op::Inf)
665 right_inf = right_end - 1;
669 if (left_inf && right_inf)
671 carry = left_inf->mark;
672 auto pos = left_inf - &(*this)[0];
673 erase(begin() + pos, begin() + pos + 2);
676 insert(end(), &r[0], right_end + 1);
678 (*this)[sz + (right_inf - &r[0])].mark |= carry;
703 if (is_t() || r.is_f())
705 if (is_f() || r.is_t())
710 unsigned s = size() - 1;
711 unsigned rs = r.size() - 1;
713 if (((*
this)[s].sub.op == acc_op::Fin
714 && r[rs].sub.op == acc_op::Fin)
715 || ((*
this)[s].sub.op == acc_op::FinNeg
716 && r[rs].sub.op == acc_op::FinNeg))
718 (*this)[s - 1].mark |= r[rs - 1].mark;
730 auto start = &(*this)[s] - (*this)[s].sub.size;
731 auto pos = &(*this)[s] - 1;
735 if (pos->sub.op == acc_op::Fin)
740 pos -= pos->sub.size + 1;
743 else if ((*
this)[s].sub.op == acc_op::Fin)
745 left_fin = &(*this)[s - 1];
748 const acc_word* right_fin =
nullptr;
749 auto right_end = &r.back();
753 auto pos = --right_end;
756 if (pos->sub.op == acc_op::Fin)
761 pos -= pos->sub.size + 1;
764 else if (right_end->sub.op == acc_op::Fin)
766 right_fin = right_end - 1;
770 if (left_fin && right_fin)
772 carry = left_fin->mark;
773 auto pos = (left_fin - &(*this)[0]);
774 this->erase(begin() + pos, begin() + pos + 2);
777 insert(end(), &r[0], right_end + 1);
779 (*this)[sz + (right_fin - &r[0])].mark |= carry;
801 acc_code& operator<<=(
unsigned sets)
805 unsigned pos = size();
808 switch ((*
this)[pos - 1].sub.op)
810 case acc_cond::acc_op::And:
811 case acc_cond::acc_op::Or:
814 case acc_cond::acc_op::Inf:
815 case acc_cond::acc_op::InfNeg:
816 case acc_cond::acc_op::Fin:
817 case acc_cond::acc_op::FinNeg:
819 (*this)[pos].mark.id <<= sets;
827 acc_code operator<<(
unsigned sets)
const 847 std::vector<std::vector<int>>
848 missing(
mark_t inf,
bool accepting)
const;
850 bool accepting(
mark_t inf)
const;
852 bool inf_satisfiable(
mark_t inf)
const;
855 mark_t always_present)
const;
879 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets()
const;
884 to_html(std::ostream& os,
885 std::function<
void(std::ostream&,
int)>
886 set_printer =
nullptr)
const;
891 to_text(std::ostream& os,
892 std::function<
void(std::ostream&,
int)>
893 set_printer =
nullptr)
const;
898 to_latex(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);
940 : num_(0
U), all_(0
U), code_(code)
943 uses_fin_acceptance_ = check_fin_acceptance();
947 : num_(0
U), all_(0
U), code_(code)
949 add_sets(code.used_sets().max_set());
950 uses_fin_acceptance_ = check_fin_acceptance();
954 : num_(o.num_), all_(o.all_), code_(o.code_),
955 uses_fin_acceptance_(o.uses_fin_acceptance_)
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 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;
1070 bool operator==(
rs_pair o)
const 1072 return fin == o.fin && inf == o.inf;
1074 bool operator!=(
rs_pair o)
const 1076 return fin != o.fin || inf != o.inf;
1078 bool operator<(
rs_pair o)
const 1080 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1082 bool operator<=(
rs_pair o)
const 1084 return !(o < *
this);
1086 bool operator>(
rs_pair o)
const 1090 bool operator>=(
rs_pair o)
const 1092 return !(*
this < o);
1105 bool is_streett_like(std::vector<rs_pair>& pairs)
const;
1117 bool is_rabin_like(std::vector<rs_pair>& pairs)
const;
1120 bool is_generalized_rabin(std::vector<unsigned>& pairs)
const;
1127 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1128 bool is_parity()
const 1132 return is_parity(max, odd);
1138 std::pair<bool, acc_cond::mark_t> unsat_mark()
const;
1141 bool check_fin_acceptance()
const;
1146 return acc_code::inf(mark);
1149 static acc_code inf(std::initializer_list<unsigned> vals)
1151 return inf(
mark_t(vals.begin(), vals.end()));
1156 return acc_code::inf_neg(mark);
1159 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1161 return inf_neg(
mark_t(vals.begin(), vals.end()));
1166 return acc_code::fin(mark);
1169 static acc_code fin(std::initializer_list<unsigned> vals)
1171 return fin(
mark_t(vals.begin(), vals.end()));
1176 return acc_code::fin_neg(mark);
1179 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1181 return fin_neg(
mark_t(vals.begin(), vals.end()));
1184 unsigned add_sets(
unsigned num)
1190 if (num_ > 8 *
sizeof(mark_t::id))
1191 throw std::runtime_error(
"Too many acceptance sets used.");
1201 mark_t mark(
unsigned u)
const 1203 SPOT_ASSERT(u < num_sets());
1217 bool accepting(
mark_t inf)
const 1219 return code_.accepting(inf);
1222 bool inf_satisfiable(
mark_t inf)
const 1224 return code_.inf_satisfiable(inf);
1229 return code_.maybe_accepting(infinitely_often, always_present);
1234 std::ostream& format(std::ostream& os,
mark_t m)
const 1242 std::string format(
mark_t m)
const 1244 std::ostringstream os;
1249 unsigned num_sets()
const 1254 template<
class iterator>
1255 mark_t useless(iterator begin, iterator end)
const 1257 mark_t::value_t u = 0
U;
1258 for (
unsigned x = 0; x < num_; ++x)
1263 unsigned all = all_ ^ (u | (1 << x));
1264 for (iterator y = begin; y != end; ++y)
1294 return {num_sets(), code_.remove(rem, missing)};
1301 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1308 return {num_sets(), code_.remove(all_sets() - rem,
true)};
1312 mark_t::value_t all_sets_()
const 1316 return -1
U >> (8 *
sizeof(mark_t::value_t) - num_);
1320 mark_t::value_t all_;
1322 bool uses_fin_acceptance_ =
false;
1327 typedef std::vector<acc_cond::rs_pair> rs_pairs;
1331 : pairs_(p), view_marks_(m) {}
1341 return visible(p.inf) ? p.inf : 0
U;
1349 return visible(p.fin) ? p.fin : 0
U;
1357 return !visible(p.inf) && visible(p.fin) ? p.fin : 0
U;
1365 return !visible(p.fin) && visible(p.inf) ? p.inf : 0
U;
1372 for (
const auto& p: pairs_)
1374 if (visible(p.fin) && visible(p.inf))
1376 if (p.fin.has(mark))
1378 if (p.inf.has(mark))
1385 const rs_pairs& pairs()
const 1391 template<
typename filter>
1395 for (
const auto& p: pairs_)
1402 return (view_marks_ & v) != 0;
1405 const rs_pairs& pairs_;
1411 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
1418 typedef unsigned value_type;
1419 typedef const value_type& reference;
1420 typedef const value_type* pointer;
1421 typedef std::ptrdiff_t difference_type;
1422 typedef std::forward_iterator_tag iterator_category;
1444 value_type operator*()
const 1447 return m_.min_set() - 1;
1496 struct hash<
spot::acc_cond::mark_t>
1500 std::hash<decltype(m.id)> h;
Definition: automata.hh:26
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1058
Definition: formula.hh:1678
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:930
op
Operator types.
Definition: formula.hh:62