30#include <spot/misc/_config.h>
31#include <spot/misc/bitset.hh>
32#include <spot/misc/trival.hh>
45 SPOT_DEPRECATED(
"mark_t no longer relies on unsigned, stop using value_t")
46 typedef unsigned value_t;
66 has_parity_prefix(
acc_cond& new_acc, std::vector<unsigned>& colors)
const;
70 [[noreturn]]
static void report_too_many_sets();
106 apply_permutation(std::vector<unsigned> permut);
111 template<
class iterator>
112 mark_t(
const iterator& begin,
const iterator& end)
115 for (iterator i = begin; i != end; ++i)
116 if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
119 report_too_many_sets();
123 mark_t(std::initializer_list<unsigned> vals)
124 :
mark_t(vals.begin(), vals.end())
149 return SPOT_MAX_ACCSETS;
159 return mark_t(_value_t::mone());
162 size_t hash() const noexcept
164 std::hash<
decltype(id)> h;
169 bool operator==(
unsigned o)
const
171 SPOT_ASSERT(o == 0U);
177 bool operator!=(
unsigned o)
const
179 SPOT_ASSERT(o == 0U);
184 bool operator==(mark_t o)
const
189 bool operator!=(mark_t o)
const
194 bool operator<(mark_t o)
const
199 bool operator<=(mark_t o)
const
204 bool operator>(mark_t o)
const
209 bool operator>=(mark_t o)
const
214 explicit operator bool()
const
219 bool has(
unsigned u)
const
221 return !!this->operator&(mark_t({0}) << u);
229 void clear(
unsigned u)
234 mark_t& operator&=(mark_t r)
240 mark_t& operator|=(mark_t r)
246 mark_t& operator-=(mark_t r)
252 mark_t& operator^=(mark_t r)
258 mark_t operator&(mark_t r)
const
268 mark_t operator-(mark_t r)
const
273 mark_t operator~()
const
278 mark_t operator^(mark_t r)
const
283#if SPOT_DEBUG || defined(SWIGPYTHON)
284# define SPOT_WRAP_OP(ins) \
289 catch (const std::runtime_error& e) \
291 report_too_many_sets(); \
294# define SPOT_WRAP_OP(ins) ins;
296 mark_t operator<<(
unsigned i)
const
298 SPOT_WRAP_OP(
return id << i);
301 mark_t& operator<<=(
unsigned i)
303 SPOT_WRAP_OP(
id <<= i;
return *
this);
306 mark_t operator>>(
unsigned i)
const
308 SPOT_WRAP_OP(
return id >> i);
311 mark_t& operator>>=(
unsigned i)
313 SPOT_WRAP_OP(
id >>= i;
return *
this);
317 mark_t strip(mark_t y)
const
331 auto rm = (~yv) & (yv - 1);
333 auto lm = ~(yv ^ (yv - 1));
334 xv = ((xv & lm) >> 1) | (xv & rm);
344 return !((*this) - m);
351 return *
this != m && this->subset(m);
367 return id.highest()+1;
379 return id.lowest()+1;
400 return id && !(
id & (
id - 1));
411 return !!(
id & (
id - 1));
426 template<
class iterator>
444 friend std::ostream& operator<<(std::ostream& os,
mark_t m);
446 std::string as_string()
const
448 std::ostringstream os;
456 { Inf, Fin, InfNeg, FinNeg,
And,
Or };
487 struct SPOT_API
acc_code:
public std::vector<acc_word>
493 has_parity_prefix(
acc_cond& new_cond,
494 std::vector<unsigned>& colors)
const;
497 is_parity_max_equiv(std::vector<int>& permut,
501 bool operator==(
const acc_code& other)
const
503 unsigned pos = size();
504 if (other.size() != pos)
508 auto op = (*this)[pos - 1].sub.op;
509 auto sz = (*this)[pos - 1].sub.size;
510 if (other[pos - 1].sub.op !=
op ||
511 other[pos - 1].sub.size != sz)
515 case acc_cond::acc_op::And:
516 case acc_cond::acc_op::Or:
519 case acc_cond::acc_op::Inf:
520 case acc_cond::acc_op::InfNeg:
521 case acc_cond::acc_op::Fin:
522 case acc_cond::acc_op::FinNeg:
524 if (other[pos].mark != (*
this)[pos].mark)
532 bool operator<(
const acc_code& other)
const
534 unsigned pos = size();
535 auto osize = other.size();
542 auto op = (*this)[pos - 1].sub.op;
543 auto oop = other[pos - 1].sub.op;
548 auto sz = (*this)[pos - 1].sub.size;
549 auto osz = other[pos - 1].sub.size;
556 case acc_cond::acc_op::And:
557 case acc_cond::acc_op::Or:
560 case acc_cond::acc_op::Inf:
561 case acc_cond::acc_op::InfNeg:
562 case acc_cond::acc_op::Fin:
563 case acc_cond::acc_op::FinNeg:
566 auto m = (*this)[pos].mark;
567 auto om = other[pos].mark;
579 bool operator>(
const acc_code& other)
const
581 return other < *
this;
584 bool operator<=(
const acc_code& other)
const
586 return !(other < *
this);
589 bool operator>=(
const acc_code& other)
const
591 return !(*
this < other);
594 bool operator!=(
const acc_code& other)
const
596 return !(*
this == other);
607 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
608 && !((*this)[s - 2].mark));
622 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
636 res[1].sub.op = acc_op::Fin;
662 res[1].sub.op = acc_op::Fin;
694 res[1].sub.op = acc_op::FinNeg;
701 return fin_neg(
mark_t(vals));
718 res[1].sub.op = acc_op::Inf;
750 res[1].sub.op = acc_op::InfNeg;
757 return inf_neg(
mark_t(vals));
787 m >>= mark_t::max_accsets() - n;
801 m >>= mark_t::max_accsets() - n;
814 res |= inf({2*n - 1}) & fin({2*n - 2});
829 res &= inf({2*n - 1}) | fin({2*n - 2});
847 template<
class Iterator>
852 for (Iterator i = begin; i != end; ++i)
856 for (
unsigned ni = *i; ni > 0; --ni)
858 auto pair = inf(m) & fin({f});
859 std::swap(pair, res);
860 res |= std::move(pair);
875 return parity(
true, is_odd, sets);
879 return parity_max(
true, sets);
883 return parity_max(
false, sets);
887 return parity(
false, is_odd, sets);
891 return parity_min(
true, sets);
895 return parity_min(
false, sets);
920 if (is_t() || r.
is_f())
925 if (is_f() || r.
is_t())
927 unsigned s = size() - 1;
928 unsigned rs = r.size() - 1;
931 if (((*
this)[s].sub.op == acc_op::Inf
932 && r[rs].sub.op == acc_op::Inf)
933 || ((*
this)[s].sub.op == acc_op::InfNeg
934 && r[rs].sub.op == acc_op::InfNeg))
936 (*this)[s - 1].mark |= r[rs - 1].mark;
946 if ((*
this)[s].sub.op == acc_op::And)
948 auto start = &(*this)[s] - (*this)[s].sub.size;
949 auto pos = &(*this)[s] - 1;
953 if (pos->sub.op == acc_op::Inf)
958 pos -= pos->sub.size + 1;
961 else if ((*
this)[s].sub.op == acc_op::Inf)
963 left_inf = &(*this)[s - 1];
966 const acc_word* right_inf =
nullptr;
967 auto right_end = &r.back();
968 if (right_end->sub.op == acc_op::And)
971 auto pos = --right_end;
974 if (pos->sub.op == acc_op::Inf)
979 pos -= pos->sub.size + 1;
982 else if (right_end->sub.op == acc_op::Inf)
984 right_inf = right_end - 1;
988 if (left_inf && right_inf)
990 carry = left_inf->mark;
991 auto pos = left_inf - &(*this)[0];
992 erase(begin() + pos, begin() + pos + 2);
995 insert(end(), &r[0], right_end + 1);
997 (*this)[sz + (right_inf - &r[0])].mark |= carry;
1000 w.sub.op = acc_op::And;
1001 w.sub.size = size();
1025 if (is_t() || r.
is_f())
1027 if (is_f() || r.
is_t())
1032 unsigned s = size() - 1;
1033 unsigned rs = r.size() - 1;
1035 if (((*
this)[s].sub.op == acc_op::Fin
1036 && r[rs].sub.op == acc_op::Fin)
1037 || ((*
this)[s].sub.op == acc_op::FinNeg
1038 && r[rs].sub.op == acc_op::FinNeg))
1040 (*this)[s - 1].mark |= r[rs - 1].mark;
1050 if ((*
this)[s].sub.op == acc_op::Or)
1052 auto start = &(*this)[s] - (*this)[s].sub.size;
1053 auto pos = &(*this)[s] - 1;
1057 if (pos->sub.op == acc_op::Fin)
1062 pos -= pos->sub.size + 1;
1065 else if ((*
this)[s].sub.op == acc_op::Fin)
1067 left_fin = &(*this)[s - 1];
1070 const acc_word* right_fin =
nullptr;
1071 auto right_end = &r.back();
1072 if (right_end->sub.op == acc_op::Or)
1075 auto pos = --right_end;
1078 if (pos->sub.op == acc_op::Fin)
1080 right_fin = pos - 1;
1083 pos -= pos->sub.size + 1;
1086 else if (right_end->sub.op == acc_op::Fin)
1088 right_fin = right_end - 1;
1092 if (left_fin && right_fin)
1094 carry = left_fin->mark;
1095 auto pos = (left_fin - &(*this)[0]);
1096 this->erase(begin() + pos, begin() + pos + 2);
1099 insert(end(), &r[0], right_end + 1);
1101 (*this)[sz + (right_fin - &r[0])].mark |= carry;
1103 w.sub.op = acc_op::Or;
1104 w.sub.size = size();
1132 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1133 report_too_many_sets();
1136 unsigned pos = size();
1139 switch ((*
this)[pos - 1].sub.op)
1141 case acc_cond::acc_op::And:
1142 case acc_cond::acc_op::Or:
1145 case acc_cond::acc_op::Inf:
1146 case acc_cond::acc_op::InfNeg:
1147 case acc_cond::acc_op::Fin:
1148 case acc_cond::acc_op::FinNeg:
1150 (*this)[pos].mark <<= sets;
1312 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1327 std::vector<std::vector<int>>
1353 mark_t always_present)
const;
1404 std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1424 std::function<
void(std::ostream&,
int)>
1425 set_printer =
nullptr)
const;
1433 std::function<
void(std::ostream&,
int)>
1434 set_printer =
nullptr)
const;
1442 std::function<
void(std::ostream&,
int)>
1443 set_printer =
nullptr)
const;
1478 : std::vector<
acc_word>(other - other->sub.size, other + 1)
1495 : num_(0U), all_({}), code_(code)
1498 uses_fin_acceptance_ = check_fin_acceptance();
1506 : num_(0
U), all_({}), code_(code)
1508 add_sets(code.used_sets().max_set());
1509 uses_fin_acceptance_ = check_fin_acceptance();
1514 : num_(o.num_), all_(o.all_), code_(o.code_),
1515 uses_fin_acceptance_(o.uses_fin_acceptance_)
1525 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1539 uses_fin_acceptance_ = check_fin_acceptance();
1554 bool operator==(
const acc_cond& other)
const
1559 bool operator!=(
const acc_cond& other)
const
1561 return !(*
this == other);
1567 return uses_fin_acceptance_;
1573 return code_.is_t();
1582 return num_ == 0 && is_t();
1588 return code_.is_f();
1597 return num_ == 0 && is_f();
1606 unsigned s = code_.size();
1608 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1617 return num_ == 1 && is_generalized_co_buchi();
1624 set_acceptance(inf(all_sets()));
1631 set_acceptance(fin(all_sets()));
1640 unsigned s = code_.size();
1641 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1642 && code_[0].mark == all_sets());
1651 unsigned s = code_.size();
1653 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1706 bool operator==(
rs_pair o)
const
1708 return fin == o.fin && inf == o.inf;
1710 bool operator!=(
rs_pair o)
const
1712 return fin != o.fin || inf != o.inf;
1714 bool operator<(
rs_pair o)
const
1716 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1718 bool operator<=(
rs_pair o)
const
1720 return !(o < *
this);
1722 bool operator>(
rs_pair o)
const
1726 bool operator>=(
rs_pair o)
const
1728 return !(*
this < o);
1789 bool is_parity(
bool& max,
bool& odd,
bool equiv =
false)
const;
1792 bool is_parity_max_equiv(std::vector<int>& permut,
bool even)
const;
1800 return is_parity(max, odd);
1812 return acc_cond(num_, code_.unit_propagation());
1818 std::pair<bool, acc_cond::mark_t> unsat_mark()
const
1820 return sat_unsat_mark(
false);
1825 std::pair<bool, acc_cond::mark_t> sat_mark()
const
1827 return sat_unsat_mark(
true);
1831 bool check_fin_acceptance()
const;
1832 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(
bool)
const;
1845 return acc_code::inf(mark);
1850 return inf(
mark_t(vals.begin(), vals.end()));
1872 return acc_code::inf_neg(mark);
1877 return inf_neg(
mark_t(vals.begin(), vals.end()));
1890 return acc_code::fin(mark);
1895 return fin(
mark_t(vals.begin(), vals.end()));
1917 return acc_code::fin_neg(mark);
1922 return fin_neg(
mark_t(vals.begin(), vals.end()));
1936 if (num > mark_t::max_accsets())
1937 report_too_many_sets();
1956 SPOT_ASSERT(u < num_sets());
1976 apply_permutation(std::vector<unsigned>permut)
1978 return acc_cond(apply_permutation_aux(permut));
1982 apply_permutation_aux(std::vector<unsigned>permut)
1984 auto conj = top_conjuncts();
1985 auto disj = top_disjuncts();
1987 if (conj.size() > 1)
1989 auto transformed = std::vector<acc_code>();
1990 for (
auto elem : conj)
1991 transformed.push_back(elem.apply_permutation_aux(permut));
1992 std::sort(transformed.begin(), transformed.end());
1993 auto uniq = std::unique(transformed.begin(), transformed.end());
1994 auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
1995 [](acc_code c1, acc_code c2)
2001 else if (disj.size() > 1)
2003 auto transformed = std::vector<acc_code>();
2004 for (
auto elem : disj)
2005 transformed.push_back(elem.apply_permutation_aux(permut));
2006 std::sort(transformed.begin(), transformed.end());
2007 auto uniq = std::unique(transformed.begin(), transformed.end());
2008 auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
2009 [](acc_code c1, acc_code c2)
2017 if (code_.back().sub.op == acc_cond::acc_op::Fin)
2018 return fin(code_[0].mark.apply_permutation(permut));
2019 if (code_.back().sub.op == acc_cond::acc_op::Inf)
2020 return inf(code_[0].mark.apply_permutation(permut));
2030 return code_.accepting(inf);
2040 return code_.inf_satisfiable(inf);
2056 return code_.maybe_accepting(infinitely_often, always_present);
2076 std::ostream& format(std::ostream& os,
mark_t m)
const
2085 std::
string format(mark_t m)
const
2087 std::ostringstream os;
2106 template<
class iterator>
2110 for (
unsigned x = 0; x < num_; ++x)
2115 auto all = comp(u |
mark_t({x}));
2118 for (iterator y = begin; y != end; ++y)
2148 return {num_sets(), code_.
remove(rem, missing)};
2158 { num_sets() - (all_sets() & rem).count(), code_.
strip(rem, missing) };
2164 return {num_sets(), code_.
force_inf(m)};
2171 return {num_sets(), code_.
remove(all_sets() - rem,
true)};
2185 std::string
name(
const char* fmt =
"alo")
const;
2200 return code_.fin_unit();
2216 return code_.inf_unit();
2225 return code_.fin_one();
2250 auto [f, c] = code_.fin_one_extract();
2251 return {f, {num_sets(), std::move(c)}};
2270 std::tuple<int, acc_cond, acc_cond>
2273 auto [f, l, r] = code_.fin_unit_one_split();
2274 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2306 bool uses_fin_acceptance_ =
false;
2311 typedef std::vector<acc_cond::rs_pair> rs_pairs;
2315 : pairs_(p), view_marks_(m) {}
2341 return !visible(p.inf) && visible(p.fin) ? p.fin
2350 return !visible(p.fin) && visible(p.inf) ? p.inf
2358 for (
const auto& p: pairs_)
2359 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2364 const rs_pairs& pairs()
const
2370 template<
typename filter>
2374 for (
const auto& p: pairs_)
2381 return !!(view_marks_ & v);
2384 const rs_pairs& pairs_;
2390 std::ostream& operator<<(std::ostream& os,
const acc_cond& acc);
2399 typedef unsigned value_type;
2400 typedef const value_type& reference;
2401 typedef const value_type* pointer;
2402 typedef std::ptrdiff_t difference_type;
2403 typedef std::forward_iterator_tag iterator_category;
2425 value_type operator*()
const
2428 return m_.min_set() - 1;
2433 m_.clear(this->
operator*());
2474 acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
2477 for (
auto color : sets())
2478 if (color < permut.size())
2479 result.set(permut[color]);
2487 struct hash<
spot::acc_cond::mark_t>
An acceptance condition.
Definition: acc.hh:62
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1543
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:2038
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1970
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1915
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1870
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1810
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1629
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:2248
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1888
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1615
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition: acc.hh:2028
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1843
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1638
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1920
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1848
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1948
bool is_parity(bool &max, bool &odd, bool equiv=false) const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
std::vector< acc_cond > top_disjuncts() const
Return the top-level disjuncts.
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1954
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1622
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2162
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2146
acc_op
Operators for acceptance formulas.
Definition: acc.hh:456
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1494
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1930
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:1796
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1571
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:1964
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1520
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1549
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1893
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1649
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:2169
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:2054
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:1595
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1536
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:1580
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2155
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2223
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:2107
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:2198
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:1505
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1513
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1875
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:1604
std::vector< acc_cond > top_conjuncts() const
Return the top-level conjuncts.
std::tuple< int, acc_cond, acc_cond > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
Definition: acc.hh:2271
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition: acc.hh:2214
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1565
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1586
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2094
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
op
Operator types.
Definition: formula.hh:79
@ And
(omega-Rational) And
Definition: automata.hh:27
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:131
An acceptance formula.
Definition: acc.hh:488
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:873
std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
std::vector< std::vector< int > > missing(mark_t inf, bool accepting) const
Help closing accepting or rejecting cycle.
friend std::ostream & operator<<(std::ostream &os, const acc_code &code)
prints the acceptance formula as text
std::ostream & to_html(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as HTML.
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:713
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:1015
acc_code force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:755
std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > useless_colors_patterns() const
Find patterns of useless colors.
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1118
std::vector< acc_code > top_conjuncts() const
Return the top-level conjuncts.
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1110
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:667
bool is_dnf() const
Whether the acceptance formula is in disjunctive normal form.
std::vector< acc_code > top_disjuncts() const
Return the top-level disjuncts.
acc_code operator&(const acc_code &r) const
Conjunct the current condition with r.
Definition: acc.hh:1007
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:723
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:893
static acc_code parity(bool is_max, bool is_odd, unsigned sets)
Build a parity acceptance condition.
mark_t used_once_sets() const
Return the sets that appears only once in the acceptance.
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1130
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:617
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:782
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:889
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1477
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:881
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:631
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:877
std::ostream & to_latex(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as LaTeX.
std::pair< int, acc_code > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it ...
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:603
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1161
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:809
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1472
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:772
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:745
bdd to_bdd(const bdd *map) const
Convert the acceptance formula into a BDD.
std::ostream & to_text(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as text.
int fin_one() const
Return one acceptance set i that appears as Fin(i) in the condition.
acc_cond::mark_t used_sets() const
Return the set of sets appearing in the condition.
std::pair< acc_cond::mark_t, acc_cond::mark_t > used_inf_fin_sets() const
Return the sets used as Inf or Fin in the acceptance condition.
acc_code strip(acc_cond::mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
acc_code(const char *input)
Construct an acc_code from a string.
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:699
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition: acc.hh:918
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:824
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:645
std::vector< unsigned > symmetries() const
compute the symmetry class of the acceptance sets.
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:689
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:885
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:657
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1023
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:764
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:796
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:848
An acceptance mark.
Definition: acc.hh:90
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:147
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:394
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:388
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:364
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:418
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:157
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2468
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:349
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:112
unsigned count() const
Number of bits sets.
Definition: acc.hh:355
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:123
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:405
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:376
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:342
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:427
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1692
A "node" in an acceptance formulas.
Definition: acc.hh:466