diff --git a/spot/tests/acc.cc b/spot/tests/acc.cc index a32cbb046..f1aa8270e 100644 --- a/spot/tests/acc.cc +++ b/spot/tests/acc.cc @@ -91,11 +91,11 @@ int main() ac3.set_generalized_buchi(); std::cout << ac.num_sets() << " + " << ac2.num_sets() << " = " << ac3.num_sets() << '\n'; - auto m5 = ac3.join(ac, m2, ac2, m3); + auto m5 = m2 | (m3 << ac.num_sets()); check(ac3, m5); - auto m6 = ac3.join(ac, ac.comp(m2 & m3), ac2, m3); + auto m6 = ac.comp(m2 & m3) | (m3 << ac.num_sets()); check(ac3, m6); - auto m7 = ac3.join(ac, ac.comp(m2 & m3), ac2, ac2.all_sets()); + auto m7 = ac.comp(m2 & m3) | (ac.all_sets() << ac.num_sets()); check(ac3, m7); const char* comma = ""; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 97f9f8c93..39cb17420 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -167,23 +167,23 @@ namespace spot return id ^ r.id; } - mark_t operator<<(int i) const + mark_t operator<<(unsigned i) const { return id << i; } - mark_t& operator<<=(int i) + mark_t& operator<<=(unsigned i) { id <<= i; return *this; } - mark_t operator>>(int i) const + mark_t operator>>(unsigned i) const { return id >> i; } - mark_t& operator>>=(int i) + mark_t& operator>>=(unsigned i) { id >>= i; return *this; @@ -1072,15 +1072,8 @@ namespace spot mark_t mark(unsigned u) const { - return mark_(u); - } - - mark_t join(const acc_cond& la, mark_t lm, - const acc_cond& ra, mark_t rm) const - { - assert(la.num_sets() + ra.num_sets() == num_sets()); - (void)ra; - return lm.id | (rm.id << la.num_sets()); + assert(u < num_sets()); + return 1U << u; } mark_t comp(mark_t l) const @@ -1151,12 +1144,6 @@ namespace spot } protected: - mark_t::value_t mark_(unsigned u) const - { - assert(u < num_sets()); - return 1U << u; - } - mark_t::value_t all_sets_() const { if (num_ == 0) diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index 4f3f8da46..5bf1018b2 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -203,12 +203,8 @@ namespace spot acc_cond::mark_t acc() const { - return - prod_->acc().join(prod_->left_acc(), - left_->acc(), - prod_->right_acc(), - right_->acc()); - } + return left_->acc() | (right_->acc() << prod_->left_acc().num_sets()); + } protected: bdd current_cond_; diff --git a/spot/twaalgos/compsusp.cc b/spot/twaalgos/compsusp.cc index f530fbf35..3edd37f43 100644 --- a/spot/twaalgos/compsusp.cc +++ b/spot/twaalgos/compsusp.cc @@ -168,11 +168,10 @@ namespace spot dict->register_all_variables_of(right, res); dict->unregister_variable(bdd_var(v), res); - const acc_cond& la = left->acc(); - const acc_cond& ra = right->acc(); - res->set_generalized_buchi(la.num_sets() + ra.num_sets()); + unsigned lsets = left->num_sets(); + res->set_generalized_buchi(lsets + right->num_sets()); - acc_cond::mark_t radd = ra.all_sets(); + acc_cond::mark_t radd = right->acc().all_sets(); pair_map seen; pair_queue todo; @@ -246,9 +245,7 @@ namespace spot todo.push_back(d); } - acc_cond::mark_t a = - res->acc().join(la, li->acc(), - ra, racc); + acc_cond::mark_t a = li->acc() | (racc << lsets); res->new_edge(src, dest, bdd_exist(cond, v), a); if (ri) diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index 738ba9347..b0a37bc46 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -96,8 +96,7 @@ namespace spot continue; auto dst = new_state(l.dst, r.dst); res->new_edge(top.second, dst, cond, - res->acc().join(left->acc(), l.acc, - right->acc(), r.acc)); + l.acc | (r.acc << left_num)); // If right is deterministic, we can abort immediately! } } diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 27d47e90c..a9d5ac824 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -63,7 +63,7 @@ namespace spot // Let f=[F₁,F₂,...] and i=[I₁,I₂,...] be bitvectors where bit // Fᵢ (resp. Iᵢ) indicates that Fᵢ (resp. Iᵢ) has been visited // in the SCC. - acc_cond::mark_t f = (sets << 1) & inf_pairs; + acc_cond::mark_t f = (sets << 1U) & inf_pairs; acc_cond::mark_t i = sets & inf_pairs; // If we have i&!f = [0,0,...] that means that the cycle formed // by the entire SCC is not accepting. However that does not @@ -168,7 +168,7 @@ namespace spot acc_cond::mark_t inf; std::tie(inf, fin) = aut->get_acceptance().used_inf_fin_sets(); assert(inf == (inf_pairs | inf_alone)); - assert(fin == ((inf_pairs >> 1) | fin_alone)); + assert(fin == ((inf_pairs >> 1U) | fin_alone)); #endif ba_final_states.resize(aut->num_states(), false); ba_type = true; // until proven otherwise @@ -254,7 +254,7 @@ namespace spot // and for all Inf sets that have no matching Fin // sets in this SCC. acc_cond::mark_t sccsets = si.acc(n); - acc_cond::mark_t f = (sccsets << 1) & inf_pairs; + acc_cond::mark_t f = (sccsets << 1U) & inf_pairs; acc_cond::mark_t i = sccsets & (inf_pairs | inf_alone); i -= f; for (auto s: states) @@ -264,7 +264,7 @@ namespace spot res->new_acc_edge(s, t.dst, t.cond, acc); } - auto rem = sccsets & ((inf_pairs >> 1) | fin_alone); + auto rem = sccsets & ((inf_pairs >> 1U) | fin_alone); assert(rem != 0U); auto sets = rem.sets(); @@ -347,7 +347,7 @@ namespace spot o2 != acc_cond::acc_op::Inf || m1.count() != 1 || m2.count() != 1 || - m2 != (m1 << 1)) + m2 != (m1 << 1U)) return nullptr; inf_pairs |= m2; } diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 025c2e532..91e45a01a 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -126,7 +126,7 @@ namespace spot acc_cond::mark_t inf; acc_cond::mark_t fin; std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets(); - assert((inf >> 1) == fin); + assert((inf >> 1U) == fin); scc_info si(in); @@ -139,8 +139,8 @@ namespace spot auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9} auto acc_fin = acc & fin; // {0, 2, 4,6} auto acc_inf = acc & inf; // { 1, 3, 7,9} - auto fin_wo_inf = acc_fin - (acc_inf >> 1); // {4} - auto inf_wo_fin = acc_inf - (acc_fin << 1); // {9} + auto fin_wo_inf = acc_fin - (acc_inf >> 1U); // {4} + auto inf_wo_fin = acc_inf - (acc_fin << 1U); // {9} sccfi.emplace_back(fin_wo_inf, inf_wo_fin, acc_fin == 0U); } @@ -199,7 +199,7 @@ namespace spot continue; // For any Fin set we see, we want to see the // corresponding Inf set. - pend |= (t.acc & fin) << 1; + pend |= (t.acc & fin) << 1U; pend -= t.acc & inf; // Label this transition with all non-pending // inf sets. The strip will shift everything @@ -212,7 +212,7 @@ namespace spot auto a = in->state_acc_sets(t.dst); if (a & scc_fin_wo_inf) continue; - pend |= (a & fin) << 1; + pend |= (a & fin) << 1U; pend -= a & inf; } pend |= scc_inf_wo_fin; @@ -250,7 +250,7 @@ namespace spot auto a = in->state_acc_sets(t.dst); if (a & scc_fin_wo_inf) continue; - pend = (a & fin) << 1; + pend = (a & fin) << 1U; pend -= a & inf; } st2gba_state d(t.dst, pend | scc_inf_wo_fin);