29 #include <spot/misc/_config.h> 30 #include <spot/misc/bitset.hh> 31 #include <spot/misc/trival.hh> 44 SPOT_DEPRECATED(
"mark_t no longer relies on unsigned, stop using value_t")
45 typedef unsigned value_t;
65 has_parity_prefix(
acc_cond& new_acc, std::vector<unsigned>& colors)
const;
69 [[noreturn]]
static void report_too_many_sets();
105 apply_permutation(std::vector<unsigned> permut);
109 template<
class iterator>
111 mark_t(
const iterator& begin,
const iterator& end)
114 for (iterator i = begin; i != end; ++i)
115 if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
118 report_too_many_sets();
122 mark_t(std::initializer_list<unsigned> vals)
123 :
mark_t(vals.begin(), vals.end())
148 return SPOT_MAX_ACCSETS;
158 return mark_t(_value_t::mone());
161 size_t hash()
const noexcept
163 std::hash<decltype(id)> h;
168 bool operator==(
unsigned o)
const 170 SPOT_ASSERT(o == 0
U);
176 bool operator!=(
unsigned o)
const 178 SPOT_ASSERT(o == 0
U);
183 bool operator==(
mark_t o)
const 188 bool operator!=(
mark_t o)
const 193 bool operator<(
mark_t o)
const 198 bool operator<=(
mark_t o)
const 203 bool operator>(
mark_t o)
const 208 bool operator>=(
mark_t o)
const 213 explicit operator bool()
const 218 bool has(
unsigned u)
const 220 return !!this->operator&(
mark_t({0}) << u);
228 void clear(
unsigned u)
282 #if SPOT_DEBUG || defined(SWIGPYTHON) 283 # define SPOT_WRAP_OP(ins) \ 288 catch (const std::runtime_error& e) \ 290 report_too_many_sets(); \ 293 # define SPOT_WRAP_OP(ins) ins; 295 mark_t operator<<(
unsigned i)
const 297 SPOT_WRAP_OP(
return id << i);
300 mark_t& operator<<=(
unsigned i)
302 SPOT_WRAP_OP(
id <<= i;
return *
this);
305 mark_t operator>>(
unsigned i)
const 307 SPOT_WRAP_OP(
return id >> i);
310 mark_t& operator>>=(
unsigned i)
312 SPOT_WRAP_OP(
id >>= i;
return *
this);
330 auto rm = (~yv) & (yv - 1);
332 auto lm = ~(yv ^ (yv - 1));
333 xv = ((xv & lm) >> 1) | (xv & rm);
343 return !((*this) - m);
350 return *
this != m && this->subset(m);
366 return id.highest()+1;
378 return id.lowest()+1;
399 return id && !(
id & (
id - 1));
410 return !!(
id & (
id - 1));
425 template<
class iterator>
443 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
445 std::string as_string()
const 447 std::ostringstream os;
455 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
486 struct SPOT_API
acc_code:
public std::vector<acc_word>
492 has_parity_prefix(
acc_cond& new_cond,
493 std::vector<unsigned>& colors)
const;
496 is_parity_max_equiv(std::vector<int>& permut,
500 bool operator==(
const acc_code& other)
const 502 unsigned pos = size();
503 if (other.size() != pos)
507 auto op = (*this)[pos - 1].sub.op;
508 auto sz = (*this)[pos - 1].sub.size;
509 if (other[pos - 1].sub.op !=
op ||
510 other[pos - 1].sub.size != sz)
514 case acc_cond::acc_op::And:
515 case acc_cond::acc_op::Or:
518 case acc_cond::acc_op::Inf:
519 case acc_cond::acc_op::InfNeg:
520 case acc_cond::acc_op::Fin:
521 case acc_cond::acc_op::FinNeg:
523 if (other[pos].mark != (*
this)[pos].mark)
531 bool operator<(
const acc_code& other)
const 533 unsigned pos = size();
534 auto osize = other.size();
541 auto op = (*this)[pos - 1].sub.op;
542 auto oop = other[pos - 1].sub.op;
547 auto sz = (*this)[pos - 1].sub.size;
548 auto osz = other[pos - 1].sub.size;
555 case acc_cond::acc_op::And:
556 case acc_cond::acc_op::Or:
559 case acc_cond::acc_op::Inf:
560 case acc_cond::acc_op::InfNeg:
561 case acc_cond::acc_op::Fin:
562 case acc_cond::acc_op::FinNeg:
565 auto m = (*this)[pos].mark;
566 auto om = other[pos].mark;
578 bool operator>(
const acc_code& other)
const 580 return other < *
this;
583 bool operator<=(
const acc_code& other)
const 585 return !(other < *
this);
588 bool operator>=(
const acc_code& other)
const 590 return !(*
this < other);
593 bool operator!=(
const acc_code& other)
const 595 return !(*
this == other);
606 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
607 && !((*this)[s - 2].mark));
621 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
635 res[1].sub.op = acc_op::Fin;
661 res[1].sub.op = acc_op::Fin;
693 res[1].sub.op = acc_op::FinNeg;
700 return fin_neg(
mark_t(vals));
717 res[1].sub.op = acc_op::Inf;
749 res[1].sub.op = acc_op::InfNeg;
756 return inf_neg(
mark_t(vals));
786 m >>= mark_t::max_accsets() - n;
800 m >>= mark_t::max_accsets() - n;
813 res |= inf({2*n - 1}) & fin({2*n - 2});
828 res &= inf({2*n - 1}) | fin({2*n - 2});
846 template<
class Iterator>
851 for (Iterator i = begin; i != end; ++i)
855 for (
unsigned ni = *i; ni > 0; --ni)
857 auto pair = inf(m) & fin({f});
858 std::swap(pair, res);
859 res |= std::move(pair);
871 static acc_code parity(
bool is_max,
bool is_odd,
unsigned sets);
874 return parity(
true, is_odd, sets);
878 return parity_max(
true, sets);
882 return parity_max(
false, sets);
886 return parity(
false, is_odd, sets);
890 return parity_min(
true, sets);
894 return parity_min(
false, sets);
914 static acc_code random(
unsigned n,
double reuse = 0.0);
919 if (is_t() || r.
is_f())
924 if (is_f() || r.
is_t())
926 unsigned s = size() - 1;
927 unsigned rs = r.size() - 1;
930 if (((*
this)[s].sub.op == acc_op::Inf
931 && r[rs].sub.op == acc_op::Inf)
932 || ((*
this)[s].sub.op == acc_op::InfNeg
933 && r[rs].sub.op == acc_op::InfNeg))
935 (*this)[s - 1].mark |= r[rs - 1].mark;
947 auto start = &(*this)[s] - (*this)[s].sub.size;
948 auto pos = &(*this)[s] - 1;
952 if (pos->sub.op == acc_op::Inf)
957 pos -= pos->sub.size + 1;
960 else if ((*
this)[s].sub.op == acc_op::Inf)
962 left_inf = &(*this)[s - 1];
965 const acc_word* right_inf =
nullptr;
966 auto right_end = &r.back();
970 auto pos = --right_end;
973 if (pos->sub.op == acc_op::Inf)
978 pos -= pos->sub.size + 1;
981 else if (right_end->sub.op == acc_op::Inf)
983 right_inf = right_end - 1;
987 if (left_inf && right_inf)
989 carry = left_inf->mark;
990 auto pos = left_inf - &(*this)[0];
991 erase(begin() + pos, begin() + pos + 2);
994 insert(end(), &r[0], right_end + 1);
996 (*this)[sz + (right_inf - &r[0])].mark |= carry;
1000 w.sub.size = size();
1024 if (is_t() || r.
is_f())
1026 if (is_f() || r.
is_t())
1031 unsigned s = size() - 1;
1032 unsigned rs = r.size() - 1;
1034 if (((*
this)[s].sub.op == acc_op::Fin
1035 && r[rs].sub.op == acc_op::Fin)
1036 || ((*
this)[s].sub.op == acc_op::FinNeg
1037 && r[rs].sub.op == acc_op::FinNeg))
1039 (*this)[s - 1].mark |= r[rs - 1].mark;
1051 auto start = &(*this)[s] - (*this)[s].sub.size;
1052 auto pos = &(*this)[s] - 1;
1056 if (pos->sub.op == acc_op::Fin)
1061 pos -= pos->sub.size + 1;
1064 else if ((*
this)[s].sub.op == acc_op::Fin)
1066 left_fin = &(*this)[s - 1];
1069 const acc_word* right_fin =
nullptr;
1070 auto right_end = &r.back();
1074 auto pos = --right_end;
1077 if (pos->sub.op == acc_op::Fin)
1079 right_fin = pos - 1;
1082 pos -= pos->sub.size + 1;
1085 else if (right_end->sub.op == acc_op::Fin)
1087 right_fin = right_end - 1;
1091 if (left_fin && right_fin)
1093 carry = left_fin->mark;
1094 auto pos = (left_fin - &(*this)[0]);
1095 this->erase(begin() + pos, begin() + pos + 2);
1098 insert(end(), &r[0], right_end + 1);
1100 (*this)[sz + (right_fin - &r[0])].mark |= carry;
1103 w.sub.size = size();
1131 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1132 report_too_many_sets();
1135 unsigned pos = size();
1138 switch ((*
this)[pos - 1].sub.op)
1140 case acc_cond::acc_op::And:
1141 case acc_cond::acc_op::Or:
1144 case acc_cond::acc_op::Inf:
1145 case acc_cond::acc_op::InfNeg:
1146 case acc_cond::acc_op::Fin:
1147 case acc_cond::acc_op::FinNeg:
1149 (*this)[pos].mark <<= sets;
1173 bool is_dnf()
const;
1181 bool is_cnf()
const;
1212 std::vector<acc_code> top_disjuncts()
const;
1222 std::vector<acc_code> top_conjuncts()
const;
1253 int fin_one()
const;
1267 std::vector<std::vector<int>>
1268 missing(
mark_t inf,
bool accepting)
const;
1272 bool accepting(
mark_t inf)
const;
1279 bool inf_satisfiable(
mark_t inf)
const;
1293 mark_t always_present)
const;
1305 std::vector<unsigned> symmetries()
const;
1339 mark_t used_once_sets()
const;
1342 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets()
const;
1349 to_html(std::ostream& os,
1350 std::function<
void(std::ostream&,
int)>
1351 set_printer =
nullptr)
const;
1358 to_text(std::ostream& os,
1359 std::function<
void(std::ostream&,
int)>
1360 set_printer =
nullptr)
const;
1367 to_latex(std::ostream& os,
1368 std::function<
void(std::ostream&,
int)>
1369 set_printer =
nullptr)
const;
1404 :
std::vector<
acc_word>(other - other->sub.size, other + 1)
1410 friend std::ostream& operator<<(std::ostream& os,
const acc_code& code);
1421 : num_(0
U), all_({}), code_(code)
1424 uses_fin_acceptance_ = check_fin_acceptance();
1432 : num_(0
U), all_({}), code_(code)
1434 add_sets(code.used_sets().max_set());
1435 uses_fin_acceptance_ = check_fin_acceptance();
1440 : num_(o.num_), all_(o.all_), code_(o.code_),
1441 uses_fin_acceptance_(o.uses_fin_acceptance_)
1451 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1465 uses_fin_acceptance_ = check_fin_acceptance();
1480 bool operator==(
const acc_cond& other)
const 1485 bool operator!=(
const acc_cond& other)
const 1487 return !(*
this == other);
1493 return uses_fin_acceptance_;
1499 return code_.is_t();
1508 return num_ == 0 && is_t();
1514 return code_.is_f();
1523 return num_ == 0 && is_f();
1532 unsigned s = code_.size();
1534 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1543 return num_ == 1 && is_generalized_co_buchi();
1550 set_acceptance(inf(all_sets()));
1557 set_acceptance(fin(all_sets()));
1566 unsigned s = code_.size();
1567 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1568 && code_[0].mark == all_sets());
1577 unsigned s = code_.size();
1579 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1593 int is_rabin()
const;
1606 int is_streett()
const;
1631 bool operator==(
rs_pair o)
const 1633 return fin == o.fin && inf == o.inf;
1635 bool operator!=(
rs_pair o)
const 1637 return fin != o.fin || inf != o.inf;
1639 bool operator<(
rs_pair o)
const 1641 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1643 bool operator<=(
rs_pair o)
const 1645 return !(o < *
this);
1647 bool operator>(
rs_pair o)
const 1651 bool operator>=(
rs_pair o)
const 1653 return !(*
this < o);
1666 bool is_streett_like(std::vector<rs_pair>& pairs)
const;
1678 bool is_rabin_like(std::vector<rs_pair>& pairs)
const;
1689 bool is_generalized_rabin(std::vector<unsigned>& pairs)
const;
1703 bool is_generalized_streett(std::vector<unsigned>& pairs)
const;
1714 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1717 bool is_parity_max_equiv(std::vector<int>& permut,
bool even)
const;
1725 return is_parity(max, odd);
1737 return acc_cond(num_, code_.unit_propagation());
1743 std::pair<bool, acc_cond::mark_t> unsat_mark()
const 1745 return sat_unsat_mark(
false);
1750 std::pair<bool, acc_cond::mark_t> sat_mark()
const 1752 return sat_unsat_mark(
true);
1756 bool check_fin_acceptance()
const;
1757 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(
bool)
const;
1770 return acc_code::inf(mark);
1775 return inf(
mark_t(vals.begin(), vals.end()));
1797 return acc_code::inf_neg(mark);
1802 return inf_neg(
mark_t(vals.begin(), vals.end()));
1815 return acc_code::fin(mark);
1820 return fin(
mark_t(vals.begin(), vals.end()));
1842 return acc_code::fin_neg(mark);
1847 return fin_neg(
mark_t(vals.begin(), vals.end()));
1861 if (num > mark_t::max_accsets())
1862 report_too_many_sets();
1881 SPOT_ASSERT(u < num_sets());
1901 apply_permutation(std::vector<unsigned>permut)
1903 return acc_cond(apply_permutation_aux(permut));
1907 apply_permutation_aux(std::vector<unsigned>permut)
1909 auto conj = top_conjuncts();
1910 auto disj = top_disjuncts();
1912 if (conj.size() > 1)
1914 auto transformed = std::vector<acc_code>();
1915 for (
auto elem : conj)
1916 transformed.push_back(elem.apply_permutation_aux(permut));
1917 std::sort(transformed.begin(), transformed.end());
1918 auto uniq = std::unique(transformed.begin(), transformed.end());
1919 auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
1926 else if (disj.size() > 1)
1928 auto transformed = std::vector<acc_code>();
1929 for (
auto elem : disj)
1930 transformed.push_back(elem.apply_permutation_aux(permut));
1931 std::sort(transformed.begin(), transformed.end());
1932 auto uniq = std::unique(transformed.begin(), transformed.end());
1933 auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
1942 if (code_.back().sub.op == acc_cond::acc_op::Fin)
1943 return fin(code_[0].mark.apply_permutation(permut));
1944 if (code_.back().sub.op == acc_cond::acc_op::Inf)
1945 return inf(code_[0].mark.apply_permutation(permut));
1955 return code_.accepting(inf);
1965 return code_.inf_satisfiable(inf);
1981 return code_.maybe_accepting(infinitely_often, always_present);
2001 std::ostream& format(std::ostream& os,
mark_t m)
const 2010 std::string format(
mark_t m)
const 2012 std::ostringstream os;
2031 template<
class iterator>
2035 for (
unsigned x = 0; x < num_; ++x)
2040 auto all = comp(u |
mark_t({x}));
2043 for (iterator y = begin; y != end; ++y)
2073 return {num_sets(), code_.
remove(rem, missing)};
2083 { num_sets() - (all_sets() & rem).count(), code_.
strip(rem, missing) };
2089 return {num_sets(), code_.
force_inf(m)};
2096 return {num_sets(), code_.
remove(all_sets() - rem,
true)};
2110 std::string name(
const char* fmt =
"alo")
const;
2125 return code_.fin_unit();
2134 return code_.fin_one();
2145 std::vector<acc_cond> top_disjuncts()
const;
2155 std::vector<acc_cond> top_conjuncts()
const;
2166 bool uses_fin_acceptance_ =
false;
2171 typedef std::vector<acc_cond::rs_pair> rs_pairs;
2175 : pairs_(p), view_marks_(m) {}
2201 return !visible(p.inf) && visible(p.fin) ? p.fin
2210 return !visible(p.fin) && visible(p.inf) ? p.inf
2218 for (
const auto& p: pairs_)
2219 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2224 const rs_pairs& pairs()
const 2230 template<
typename filter>
2234 for (
const auto& p: pairs_)
2241 return !!(view_marks_ & v);
2244 const rs_pairs& pairs_;
2250 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
2259 typedef unsigned value_type;
2260 typedef const value_type& reference;
2261 typedef const value_type* pointer;
2262 typedef std::ptrdiff_t difference_type;
2263 typedef std::forward_iterator_tag iterator_category;
2285 value_type operator*()
const 2288 return m_.min_set() - 1;
2293 m_.clear(this->
operator*());
2334 acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
2337 for (
auto color : sets())
2338 if (color < permut.size())
2339 result.set(permut[color]);
2347 struct hash<
spot::acc_cond::mark_t>
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:712
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:146
Definition: automata.hh:26
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:375
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:387
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1506
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1895
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2328
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1813
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2087
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1512
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:616
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:1963
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1530
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1855
acc_op
Operators for acceptance formulas.
Definition: acc.hh:454
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1845
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1879
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:363
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1491
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1617
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:426
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1469
static acc_code parity_max_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:876
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:630
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1768
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:111
Definition: bitset.hh:402
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:2094
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:341
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1735
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1818
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:156
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1160
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:823
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1564
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1462
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:348
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1840
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:892
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1109
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1403
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1795
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2071
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:417
static acc_code parity_max_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:880
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1521
An acceptance condition.
Definition: acc.hh:60
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2080
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1446
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1420
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:122
A "node" in an acceptance formulas.
Definition: acc.hh:464
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1022
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:722
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1555
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:666
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2132
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:763
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:872
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1800
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1475
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1541
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1889
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:644
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:884
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:393
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:771
unsigned count() const
Number of bits sets.
Definition: acc.hh:354
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:744
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1398
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1575
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:2123
op
Operator types.
Definition: formula.hh:78
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:1721
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1129
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2019
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1773
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:781
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:888
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1439
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1117
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:808
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1873
An acceptance formula.
Definition: acc.hh:486
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:656
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:847
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:2032
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1431
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition...
Definition: acc.hh:1953
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1497
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:1979
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1548
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:688
An acceptance mark.
Definition: acc.hh:87
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:754
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:698
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:795
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:404
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:602