From 4993e80706f63ff93cd92692769d9de16f6da03a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 Dec 2015 18:49:11 +0100 Subject: [PATCH] acc: simplify interface using operators * spot/twa/acc.hh, spot/twa/acc.cc: Here. Also remove some redundant functions. * spot/parseaut/parseaut.yy, spot/priv/accmap.hh, spot/tests/acc.cc, spot/tests/twagraph.cc, spot/twa/taatgba.hh, spot/twa/twaproduct.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc, spot/twaalgos/lbtt.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/product.cc, spot/twaalgos/remfin.cc, spot/twaalgos/simulation.cc, spot/twaalgos/tau03opt.cc, spot/twaalgos/weight.cc, spot/twaalgos/weight.hh: Adjust. * NEWS: Mention the changes. --- NEWS | 15 ++++ spot/parseaut/parseaut.yy | 14 ++-- spot/priv/accmap.hh | 6 +- spot/tests/acc.cc | 22 +++--- spot/tests/twagraph.cc | 6 +- spot/twa/acc.cc | 38 +++++----- spot/twa/acc.hh | 134 ++++++++++++++++++----------------- spot/twa/taatgba.hh | 2 +- spot/twa/twaproduct.cc | 5 +- spot/twaalgos/dtwasat.cc | 2 +- spot/twaalgos/hoa.cc | 14 ++-- spot/twaalgos/lbtt.cc | 2 +- spot/twaalgos/ltl2tgba_fm.cc | 2 +- spot/twaalgos/product.cc | 7 +- spot/twaalgos/remfin.cc | 10 +-- spot/twaalgos/simulation.cc | 10 +-- spot/twaalgos/tau03opt.cc | 8 +-- spot/twaalgos/weight.cc | 10 +-- spot/twaalgos/weight.hh | 8 +-- 19 files changed, 161 insertions(+), 154 deletions(-) diff --git a/NEWS b/NEWS index b11ff3322..e45f39182 100644 --- a/NEWS +++ b/NEWS @@ -33,6 +33,21 @@ New in spot 1.99.6a (not yet released) instead of just weak SCCs. This gets rid of some corner cases that used to require ad hoc handling. + * acc_cond::acc_code's methods append_or(), append_and(), and + shift_left() have been replaced by operators |=, &=, <<=, and for + completeness the operators |, &, and << have been added. + + * Several methods have been removed from the acc_cond class because + they were simply redundant with the methods of acc_cond::mark_t, + and more complex to use. + + acc_cond::marks(...) -> use acc_cond::mark_t(...) directly + acc_cond::sets(m) -> use m.sets() + acc_cond::has(m, u) -> use m.has(u) directly + acc_cond::cup(l, r) -> use l | r + acc_cond::cap(l, r) -> use l & r + acc_cond::set_minus(l, r) -> use l - r + Python: * Iterating over the transitions leaving a state (the diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 72c1f1632..907935b26 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -786,13 +786,13 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' } | acceptance-cond '&' acceptance-cond { - $3->append_and(std::move(*$1)); + *$3 &= std::move(*$1); $$ = $3; delete $1; } | acceptance-cond '|' acceptance-cond { - $3->append_or(std::move(*$1)); + *$3 |= std::move(*$1); $$ = $3; delete $1; } @@ -1804,7 +1804,7 @@ fix_acceptance_aux(spot::acc_cond& acc, while (sub < pos) { --pos; - c.append_and(fix_acceptance_aux(acc, in, pos, onlyneg, both, base)); + c &= fix_acceptance_aux(acc, in, pos, onlyneg, both, base); pos -= in[pos].size; } return c; @@ -1818,7 +1818,7 @@ fix_acceptance_aux(spot::acc_cond& acc, while (sub < pos) { --pos; - c.append_or(fix_acceptance_aux(acc, in, pos, onlyneg, both, base)); + c |= fix_acceptance_aux(acc, in, pos, onlyneg, both, base); pos -= in[pos].size; } return c; @@ -1839,7 +1839,7 @@ fix_acceptance_aux(spot::acc_cond& acc, ++base; } if (tmp) - c.append_or(acc.fin(tmp)); + c |= acc.fin(tmp); return c; } case spot::acc_cond::acc_op::InfNeg: @@ -1854,7 +1854,7 @@ fix_acceptance_aux(spot::acc_cond& acc, ++base; } if (tmp) - c.append_and(acc.inf(tmp)); + c &= acc.inf(tmp); return c; } } @@ -1886,7 +1886,7 @@ static void fix_acceptance(result_& r) unsigned base = 0; if (both) { - auto v = acc.sets(both); + auto v = both.sets(); auto vs = v.size(); base = acc.add_sets(vs); for (auto& t: r.h->aut->edge_vector()) diff --git a/spot/priv/accmap.hh b/spot/priv/accmap.hh index b1d2dce95..5340526a2 100644 --- a/spot/priv/accmap.hh +++ b/spot/priv/accmap.hh @@ -64,7 +64,7 @@ namespace spot auto p = map_.find(name); if (p == map_.end()) return std::make_pair(false, 0U); - return std::make_pair(true, aut_->acc().marks({p->second})); + return std::make_pair(true, acc_cond::mark_t({p->second})); } }; @@ -83,7 +83,7 @@ namespace spot std::pair lookup(unsigned n) { if (n < aut_->acc().num_sets()) - return std::make_pair(true, aut_->acc().marks({n})); + return std::make_pair(true, acc_cond::mark_t({n})); else return std::make_pair(false, 0U); } @@ -109,7 +109,7 @@ namespace spot return std::make_pair(true, p->second); if (used_ < aut_->acc().num_sets()) { - auto res = aut_->acc().marks({used_++}); + auto res = acc_cond::mark_t({used_++}); map_[n] = res; return std::make_pair(true, res); } diff --git a/spot/tests/acc.cc b/spot/tests/acc.cc index a019982d6..a32cbb046 100644 --- a/spot/tests/acc.cc +++ b/spot/tests/acc.cc @@ -59,9 +59,9 @@ int main() ac.set_generalized_buchi(); std::cout << ac.get_acceptance() << '\n'; - auto m1 = ac.marks({0, 2}); - auto m2 = ac.marks({0, 3}); - auto m3 = ac.marks({2, 1}); + auto m1 = spot::acc_cond::mark_t({0, 2}); + auto m2 = spot::acc_cond::mark_t({0, 3}); + auto m3 = spot::acc_cond::mark_t({2, 1}); check(ac, m1); check(ac, m2); @@ -128,23 +128,23 @@ int main() auto code1 = ac.inf({0, 1, 3}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; - code1.append_or(ac.fin({2})); + code1 |= ac.fin({2}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; - code1.append_or(ac.fin({0})); + code1 |= ac.fin({0}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; - code1.append_or(ac.fin({})); + code1 |= ac.fin({}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; - code1.append_and(ac.inf({})); + code1 &= ac.inf({}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; auto code2 = code1; - code1.append_and(ac.fin({0, 1})); + code1 &= ac.fin({0, 1}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; - code1.append_and(ac.fin({})); + code1 &= ac.fin({}); std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; - code2.append_or(ac.fin({0, 1})); + code2 |= ac.fin({0, 1}); std::cout << code2.size() << ' ' << code2 << ' ' << code2.is_dnf() << '\n'; auto code3 = ac.inf({0, 1}); - code3.append_and(ac.fin({2, 3})); + code3 &= ac.fin({2, 3}); std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n'; // code3 == (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) diff --git a/spot/tests/twagraph.cc b/spot/tests/twagraph.cc index 36b7b90eb..e7a54b99e 100644 --- a/spot/tests/twagraph.cc +++ b/spot/tests/twagraph.cc @@ -41,9 +41,9 @@ static void f1() tg->new_edge(s1, s2, p1, 0U); tg->new_edge(s1, s3, p2, tg->acc().mark(1)); tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0)); - tg->new_edge(s3, s1, p1 | p2, tg->acc().marks({0, 1})); + tg->new_edge(s3, s1, p1 | p2, spot::acc_cond::mark_t({0, 1})); tg->new_edge(s3, s2, p1 >> p2, 0U); - tg->new_edge(s3, s3, bddtrue, tg->acc().marks({0, 1})); + tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1})); spot::print_dot(std::cout, tg); @@ -63,7 +63,7 @@ static void f1() spot::print_dot(std::cout, tg); } - auto all = tg->acc().marks({0, 1}); + spot::acc_cond::mark_t all({0, 1}); tg->new_edge(s3, s1, p1 | p2, all); tg->new_edge(s3, s2, p1 >> p2, 0U); tg->new_edge(s3, s1, bddtrue, all); diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 5e5ac1e83..e5e229e01 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -538,9 +538,9 @@ namespace spot for (int i = start; i != end; i += inc) { if ((i & 1) == odd) - res.append_or(inf({(unsigned)i})); + res |= inf({(unsigned)i}); else - res.append_and(fin({(unsigned)i})); + res &= fin({(unsigned)i}); } return res; } @@ -577,9 +577,9 @@ namespace spot int p2 = mrand(s); if (drand() < 0.5) - codes[p2].append_or(std::move(codes.back())); + codes[p2] |= std::move(codes.back()); else - codes[p2].append_and(std::move(codes.back())); + codes[p2] &= std::move(codes.back()); codes.pop_back(); } @@ -765,8 +765,7 @@ namespace spot // The strange order here make sure we can smaller set // numbers at the end of the acceptance code, i.e., at // the front of the output. - auto a = fin(s); - a.append_and(std::move(c)); + auto a = fin(s) & std::move(c); std::swap(a, c); } else // Positive variable? -> Inf @@ -775,9 +774,9 @@ namespace spot cube = h; } } - c.append_and(inf(i)); + c &= inf(i); // See comment above for the order. - c.append_or(std::move(rescode)); + c |= std::move(rescode); std::swap(c, rescode); } @@ -838,8 +837,7 @@ namespace spot // The strange order here make sure we can smaller set // numbers at the end of the acceptance code, i.e., at // the front of the output. - auto a = inf(s); - a.append_or(std::move(c)); + auto a = inf(s) | std::move(c); std::swap(a, c); } else // Positive variable? -> Fin @@ -848,9 +846,9 @@ namespace spot cube = h; } } - c.append_or(fin(m)); + c |= fin(m); // See comment above for the order. - c.append_and(std::move(rescode)); + c &= std::move(rescode); std::swap(c, rescode); } return rescode; @@ -1069,8 +1067,7 @@ namespace spot auto res = acc_cond::acc_code::f(); do { - auto tmp = complement_rec(pos); - tmp.append_or(std::move(res)); + auto tmp = complement_rec(pos) | std::move(res); std::swap(tmp, res); pos -= pos->size + 1; } @@ -1083,8 +1080,7 @@ namespace spot auto res = acc_cond::acc_code::t(); do { - auto tmp = complement_rec(pos); - tmp.append_and(std::move(res)); + auto tmp = complement_rec(pos) & std::move(res); std::swap(tmp, res); pos -= pos->size + 1; } @@ -1128,8 +1124,7 @@ namespace spot auto res = acc_cond::acc_code::t(); do { - auto tmp = strip_rec(pos, rem, missing); - tmp.append_and(std::move(res)); + auto tmp = strip_rec(pos, rem, missing) & std::move(res); std::swap(tmp, res); pos -= pos->size + 1; } @@ -1142,8 +1137,7 @@ namespace spot auto res = acc_cond::acc_code::f(); do { - auto tmp = strip_rec(pos, rem, missing); - tmp.append_or(std::move(res)); + auto tmp = strip_rec(pos, rem, missing) | std::move(res); std::swap(tmp, res); pos -= pos->size + 1; } @@ -1313,7 +1307,7 @@ namespace spot // Prepend instead of append, to preserve the input order. auto tmp = parse_term(input); std::swap(tmp, res); - res.append_or(std::move(tmp)); + res |= std::move(tmp); } return res; } @@ -1477,7 +1471,7 @@ namespace spot // Prepend instead of append, to preserve the input order. auto tmp = parse_term(input); std::swap(tmp, res); - res.append_and(std::move(tmp)); + res &= std::move(tmp); } return res; } diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index f3ccf5e09..489dd9dcd 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -512,9 +512,7 @@ namespace spot acc_cond::acc_code res = f(); while (n > 0) { - acc_cond::acc_code pair = inf({2*n - 1}); - pair.append_and(fin({2*n - 2})); - res.append_or(std::move(pair)); + res |= inf({2*n - 1}) & fin({2*n - 2}); --n; } return res; @@ -526,9 +524,7 @@ namespace spot acc_cond::acc_code res = t(); while (n > 0) { - acc_cond::acc_code pair = inf({2*n - 1}); - pair.append_or(fin({2*n - 2})); - res.append_and(std::move(pair)); + res &= inf({2*n - 1}) | fin({2*n - 2}); --n; } return res; @@ -545,9 +541,9 @@ namespace spot acc_cond::mark_t m = 0U; for (unsigned ni = *i; ni > 0; --ni) m.set(n++); - pair.append_and(inf(m)); + pair &= inf(m); std::swap(pair, res); - res.append_or(std::move(pair)); + res |= std::move(pair); } return res; } @@ -559,15 +555,15 @@ namespace spot // acceptance formula. static acc_code random(unsigned n, double reuse = 0.0); - void append_and(acc_code&& r) + acc_code& operator&=(acc_code&& r) { if (is_tt() || r.is_ff()) { *this = std::move(r); - return; + return *this; } if (is_ff() || r.is_tt()) - return; + return *this; unsigned s = size() - 1; unsigned rs = r.size() - 1; // We want to group all Inf(x) operators: @@ -576,7 +572,7 @@ namespace spot || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) { (*this)[s - 1].mark |= r[rs - 1].mark; - return; + return *this; } // In the more complex scenarios, left and right may both @@ -648,17 +644,18 @@ namespace spot w.op = acc_op::And; w.size = size(); push_back(w); + return *this; } - void append_and(const acc_code& r) + acc_code& operator&=(const acc_code& r) { if (is_tt() || r.is_ff()) { *this = r; - return; + return *this; } if (is_ff() || r.is_tt()) - return; + return *this; unsigned s = size() - 1; unsigned rs = r.size() - 1; // Inf(a) & Inf(b) = Inf(a & b) @@ -666,7 +663,7 @@ namespace spot || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) { (*this)[s - 1].mark |= r[rs - 1].mark; - return; + return *this; } // In the more complex scenarios, left and right may both @@ -738,16 +735,31 @@ namespace spot w.op = acc_op::And; w.size = size(); push_back(w); + return *this; } - void append_or(acc_code&& r) + acc_code operator&(acc_code&& r) + { + acc_code res = *this; + res &= r; + return res; + } + + acc_code operator&(const acc_code& r) + { + acc_code res = *this; + res &= r; + return res; + } + + acc_code& operator|=(acc_code&& r) { if (is_tt() || r.is_ff()) - return; + return *this; if (is_ff() || r.is_tt()) { *this = std::move(r); - return; + return *this; } unsigned s = size() - 1; unsigned rs = r.size() - 1; @@ -756,7 +768,7 @@ namespace spot || ((*this)[s].op == acc_op::FinNeg && r[rs].op == acc_op::FinNeg)) { (*this)[s - 1].mark |= r[rs - 1].mark; - return; + return *this; } if ((*this)[s].op == acc_op::Or) pop_back(); @@ -767,12 +779,32 @@ namespace spot w.op = acc_op::Or; w.size = size(); push_back(w); + return *this; } - void shift_left(unsigned sets) + acc_code& operator|=(const acc_code& r) + { + return *this |= acc_code(r); + } + + acc_code operator|(acc_code&& r) + { + acc_code res = *this; + res |= r; + return res; + } + + acc_code operator|(const acc_code& r) + { + acc_code res = *this; + res |= r; + return res; + } + + acc_code& operator<<=(unsigned sets) { if (empty()) - return; + return *this; unsigned pos = size(); do { @@ -792,6 +824,14 @@ namespace spot } } while (pos > 0); + return *this; + } + + acc_code operator<<(unsigned sets) const + { + acc_code res = *this; + res <<= sets; + return res; } bool is_dnf() const; @@ -854,8 +894,8 @@ namespace spot friend std::ostream& operator<<(std::ostream& os, const acc_code& code); }; - acc_cond(unsigned n_sets = 0) - : num_(0U), all_(0U) + acc_cond(unsigned n_sets = 0, acc_code code = {}) + : num_(0U), all_(0U), code_(code) { add_sets(n_sets); } @@ -970,7 +1010,7 @@ namespace spot acc_code inf(std::initializer_list vals) const { - return inf(marks(vals.begin(), vals.end())); + return inf(mark_t(vals.begin(), vals.end())); } acc_code inf_neg(mark_t mark) const @@ -980,7 +1020,7 @@ namespace spot acc_code inf_neg(std::initializer_list vals) const { - return inf_neg(marks(vals.begin(), vals.end())); + return inf_neg(mark_t(vals.begin(), vals.end())); } acc_code fin(mark_t mark) const @@ -990,7 +1030,7 @@ namespace spot acc_code fin(std::initializer_list vals) const { - return fin(marks(vals.begin(), vals.end())); + return fin(mark_t(vals.begin(), vals.end())); } acc_code fin_neg(mark_t mark) const @@ -1000,7 +1040,7 @@ namespace spot acc_code fin_neg(std::initializer_list vals) const { - return fin_neg(marks(vals.begin(), vals.end())); + return fin_neg(mark_t(vals.begin(), vals.end())); } unsigned add_sets(unsigned num) @@ -1025,44 +1065,6 @@ namespace spot return mark_(u); } - template - mark_t marks(const iterator& begin, const iterator& end) const - { - return mark_t(begin, end); - } - - mark_t marks(std::initializer_list vals) const - { - return marks(vals.begin(), vals.end()); - } - - // FIXME: Return some iterable object without building a vector. - std::vector sets(mark_t m) const - { - return m.sets(); - } - - // whether m contains u - bool has(mark_t m, unsigned u) const - { - return m.has(u); - } - - mark_t cup(mark_t l, mark_t r) const - { - return l | r; - } - - mark_t cap(mark_t l, mark_t r) const - { - return l & r; - } - - mark_t set_minus(mark_t l, mark_t r) const - { - return l - r; - } - mark_t join(const acc_cond& la, mark_t lm, const acc_cond& ra, mark_t rm) const { diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh index f31408021..a720c6aac 100644 --- a/spot/twa/taatgba.hh +++ b/spot/twa/taatgba.hh @@ -196,7 +196,7 @@ namespace spot { auto p = acc_map_.emplace(f, 0); if (p.second) - p.first->second = acc_.marks({acc_.add_set()}); + p.first->second = acc_cond::mark_t({acc_.add_set()}); t->acceptance_conditions |= p.first->second; } diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index 19853fa9f..4f3f8da46 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -312,9 +312,8 @@ namespace spot assert(num_sets() == 0); auto left_num = left->num_sets(); - auto right_acc = right->get_acceptance(); - right_acc.shift_left(left_num); - right_acc.append_and(left->get_acceptance()); + auto right_acc = right->get_acceptance() << left_num; + right_acc &= left->get_acceptance(); set_acceptance(left_num + right->num_sets(), right_acc); } diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index e898a9699..ac3c8c7c2 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -996,7 +996,7 @@ namespace spot ta(q2, l, d.cacc.mark(m), q3); int tai = d.transaccid[ta]; - if (d.cacc.has(biga, m)) + if (biga.has(m)) tai = -tai; out << tai << ' '; } diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 0d88e46ff..eaea788af 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -70,16 +70,14 @@ namespace spot } std::ostream& - emit_acc(std::ostream& os, - const const_twa_graph_ptr& aut, - acc_cond::mark_t b) + emit_acc(std::ostream& os, acc_cond::mark_t b) { // FIXME: We could use a cache for this. if (b == 0U) return os; os << " {"; bool notfirst = false; - for (auto v: aut->acc().sets(b)) + for (auto v: b.sets()) { if (notfirst) os << ' '; @@ -492,7 +490,7 @@ namespace spot acc = t.acc; break; } - md.emit_acc(os, aut, acc); + md.emit_acc(os, acc); } os << nl; @@ -503,7 +501,7 @@ namespace spot { os << '[' << md.sup[t.cond] << "] " << t.dst; if (this_acc == Hoa_Acceptance_Transitions) - md.emit_acc(os, aut, t.acc); + md.emit_acc(os, t.acc); os << nl; } } @@ -515,7 +513,7 @@ namespace spot os << t.dst; if (this_acc == Hoa_Acceptance_Transitions) { - md.emit_acc(os, aut, t.acc); + md.emit_acc(os, t.acc); os << nl; } else @@ -561,7 +559,7 @@ namespace spot os << out[i]; if (this_acc != Hoa_Acceptance_States) { - md.emit_acc(os, aut, outm[i]) << nl; + md.emit_acc(os, outm[i]) << nl; ++i; } else diff --git a/spot/twaalgos/lbtt.cc b/spot/twaalgos/lbtt.cc index 21163c09c..c006210c9 100644 --- a/spot/twaalgos/lbtt.cc +++ b/spot/twaalgos/lbtt.cc @@ -98,7 +98,7 @@ namespace spot body_ << out - 1 << ' '; if (!sba_format_) { - for (auto s: aut_->acc().sets(si->acc())) + for (auto s: si->acc().sets()) body_ << s << ' '; body_ << "-1 "; } diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 63cc0a5f4..0bd5d9ee9 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -253,7 +253,7 @@ namespace spot } } while (a != bddtrue); - return acc.marks(t.begin(), t.end()); + return acc_cond::mark_t(t.begin(), t.end()); } int diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index 42e0a5318..16515739c 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -54,12 +54,11 @@ namespace spot res->copy_ap_of(left); res->copy_ap_of(right); auto left_num = left->num_sets(); - auto right_acc = right->get_acceptance(); - right_acc.shift_left(left_num); + auto right_acc = right->get_acceptance() << left_num; if (and_acc) - right_acc.append_and(left->get_acceptance()); + right_acc &= left->get_acceptance(); else - right_acc.append_or(acc_cond::acc_code(left->get_acceptance())); + right_acc |= left->get_acceptance(); res->set_acceptance(left_num + right->num_sets(), right_acc); auto v = new product_states; diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 2e403f04b..9fcac273c 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -445,7 +445,7 @@ namespace spot c.insert(c.end(), w, w + 2); auto p = res.emplace(fin, c); if (!p.second) - p.first->second.append_or(std::move(c)); + p.first->second |= std::move(c); } } return res; @@ -627,7 +627,7 @@ namespace spot trace << "rem[" << i << "] = " << rem[i] << " m = " << m << '\n'; add[i] = m; - code[i].append_and(acc.inf(m)); + code[i] &= acc.inf(m); trace << "code[" << i << "] = " << code[i] << '\n'; } } @@ -636,14 +636,14 @@ namespace spot trace << "We have a true term\n"; unsigned one = acc.add_sets(1); extra_sets += 1; - auto m = acc.marks({one}); + acc_cond::mark_t m({one}); auto c = acc.inf(m); for (unsigned i = 0; i < sz; ++i) { if (!code[i].is_tt()) continue; add[i] = m; - code[i].append_and(c); + code[i] &= std::move(c); c = acc.fin(0U); // Use false for the other terms. trace << "code[" << i << "] = " << code[i] << '\n'; } @@ -653,7 +653,7 @@ namespace spot acc_cond::acc_code new_code = aut->acc().fin(0U); for (auto c: code) - new_code.append_or(std::move(c)); + new_code |= std::move(c); unsigned cs = code.size(); for (unsigned i = 0; i < cs; ++i) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index fc8aae767..99c4ed778 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -168,12 +168,12 @@ namespace spot { // FIXME: Use a cache. bdd res = bddtrue; - for (auto n: a_->acc().sets(m)) + for (auto n: m.sets()) res &= bdd_ithvar(acc_vars + n); return res; } - acc_cond::mark_t bdd_to_mark(const twa_graph_ptr& aut, bdd b) + acc_cond::mark_t bdd_to_mark(bdd b) { // FIXME: Use a cache. std::vector res; @@ -182,7 +182,7 @@ namespace spot res.push_back(bdd_var(b) - acc_vars); b = bdd_high(b); } - return aut->acc().marks(res.begin(), res.end()); + return acc_cond::mark_t(res.begin(), res.end()); } direct_simulation(const const_twa_graph_ptr& in) @@ -575,8 +575,8 @@ namespace spot all_class_var_); // Keep only ones who are acceptance condition. - auto acc = bdd_to_mark(res, bdd_existcomp(cond_acc_dest, - all_proms_)); + auto acc = bdd_to_mark(bdd_existcomp(cond_acc_dest, + all_proms_)); // Keep the other! bdd cond = bdd_existcomp(cond_acc_dest, diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index 91cbdb4eb..2c2a77e6e 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -160,9 +160,9 @@ namespace spot // FIXME: This should be improved. std::vector res; unsigned max = a_->num_sets(); - for (unsigned n = 0; n < max && a_->acc().has(acc, n); ++n) + for (unsigned n = 0; n < max && acc.has(n); ++n) res.push_back(n); - return a_->acc().marks(res.begin(), res.end()); + return acc_cond::mark_t(res.begin(), res.end()); } /// \brief weight of the state on top of the blue stack. @@ -209,7 +209,7 @@ namespace spot { trace << " It is white, go down" << std::endl; if (use_weights) - current_weight.add(a_->acc(), acc); + current_weight.add(acc); inc_states(); h.add_new_state(s_prime, CYAN, current_weight); push(st_blue, s_prime, label, acc); @@ -260,7 +260,7 @@ namespace spot stack_item f_dest(f); pop(st_blue); if (use_weights) - current_weight.sub(a_->acc(), f_dest.acc); + current_weight.sub(f_dest.acc); typename heap::color_ref c_prime = h.get_color_ref(f_dest.s); assert(!c_prime.is_white()); c_prime.set_color(BLUE); diff --git a/spot/twaalgos/weight.cc b/spot/twaalgos/weight.cc index 51bf79142..dfafd9d91 100644 --- a/spot/twaalgos/weight.cc +++ b/spot/twaalgos/weight.cc @@ -31,16 +31,16 @@ namespace spot { } - weight& weight::add(const acc_cond& acc, acc_cond::mark_t a) + weight& weight::add(acc_cond::mark_t a) { - for (auto s: acc.sets(a)) + for (auto s: a.sets()) ++m[s]; return *this; } - weight& weight::sub(const acc_cond& acc, acc_cond::mark_t a) + weight& weight::sub(acc_cond::mark_t a) { - for (auto s: acc.sets(a)) + for (auto s: a.sets()) if (m[s] > 0) --m[s]; return *this; @@ -53,7 +53,7 @@ namespace spot for (unsigned n = 0; n < max; ++n) if (m[n] > w.m[n]) res.push_back(n); - return acc.marks(res.begin(), res.end()); + return acc_cond::mark_t(res.begin(), res.end()); } std::ostream& operator<<(std::ostream& os, const weight& w) diff --git a/spot/twaalgos/weight.hh b/spot/twaalgos/weight.hh index 355ecd5b5..f125dc590 100644 --- a/spot/twaalgos/weight.hh +++ b/spot/twaalgos/weight.hh @@ -37,10 +37,10 @@ namespace spot public: /// Construct a empty vector (all counters set to zero). weight(const acc_cond& acc); - /// Increment by one the counters of each acceptance condition in \a acc. - weight& add(const acc_cond& acc, acc_cond::mark_t a); - /// Decrement by one the counters of each acceptance condition in \a acc. - weight& sub(const acc_cond& acc, acc_cond::mark_t a); + /// Increment by one the counters of each acceptance condition in \a a. + weight& add(acc_cond::mark_t a); + /// Decrement by one the counters of each acceptance condition in \a a. + weight& sub(acc_cond::mark_t a); /// Return the set of each acceptance condition such that its counter is /// strictly greatest than the corresponding counter in w. ///