diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index dfc5eb263..603b5eed6 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -271,7 +271,7 @@ namespace spot bool maximal_accepting_loops_for_scc(const scc_info& si, unsigned scc, const acc_cond& forced_acc, - const std::vector& keep, + const bitvect& keep, std::function callback) { diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index e298925d9..3ffd795b9 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -21,6 +21,7 @@ #include #include +#include namespace spot { @@ -73,13 +74,13 @@ namespace spot /// `si->inner_edges_of(num)` lists the relevant edges. /// /// The search is restricted to a set of edges of the given SCC - /// for which \a keep (an array indexed by edge numbers) is true. + /// for which \a keep (a bitvect indexed by edge numbers) is true. /// /// Returns false iff no accepting loop where found. SPOT_API bool maximal_accepting_loops_for_scc(const scc_info& si, unsigned scc, const acc_cond& forced_acc, - const std::vector& keep, + const bitvect& keep, std::function callback); #endif diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 115763081..c31999c37 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -888,7 +888,7 @@ namespace spot if (auto choice = f(e, e.dst, si->get_filter_data()); choice != edge_filter_choice::keep) return choice; - if (!(*d.keep_)[d.aut_->edge_number(e)] || (d.cut_sets_ & e.acc)) + if (!(*d.keep_).get(d.aut_->edge_number(e)) || (d.cut_sets_ & e.acc)) return edge_filter_choice::cut; return edge_filter_choice::keep; } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index e36359470..2de9a1cb8 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -22,6 +22,7 @@ #include #include #include +#include namespace spot { @@ -792,7 +793,7 @@ namespace spot const_twa_graph_ptr aut_; acc_cond old_acc_; bool restore_old_acc_ = false; - const std::vector* keep_ = nullptr; + const bitvect* keep_ = nullptr; static scc_info::edge_filter_choice filter_scc_and_mark_(const twa_graph::edge_storage_t& e, @@ -833,7 +834,7 @@ namespace spot scc_and_mark_filter(const scc_info& lower_si, unsigned lower_scc, acc_cond::mark_t cut_sets, - const std::vector& keep) + const bitvect& keep) : scc_and_mark_filter(lower_si, lower_scc, cut_sets) { keep_ = &keep; diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index c86c929b5..c58a34e6a 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -20,11 +20,9 @@ #include "config.h" #include #include -#include #include #include #include -#include namespace spot { @@ -380,16 +378,16 @@ namespace spot { if (bitvectors.size() > 2 * n) return; - bitvectors.emplace_back(nedges, false); - bitvectors.emplace_back(nstates, false); + bitvectors.emplace_back(std::unique_ptr(make_bitvect(nedges))); + bitvectors.emplace_back(std::unique_ptr(make_bitvect(nstates))); }; - auto edge_vector = [&] (unsigned n) -> std::vector& + auto edge_vector = [&] (unsigned n) -> bitvect& { - return bitvectors[2 * n]; + return *bitvectors[2 * n]; }; - auto state_vector = [&] (unsigned n) -> std::vector& + auto state_vector = [&] (unsigned n) -> bitvect& { - return bitvectors[2 * n + 1]; + return *bitvectors[2 * n + 1]; }; allocate_vectors_maybe(0); @@ -416,8 +414,8 @@ namespace spot n.scc = scc; for (auto& e: si_->inner_edges_of(scc)) { - n.edges[aut->edge_number(e)] = true; - n.states[e.src] = true; + n.edges.set(aut->edge_number(e)); + n.states.set(e.src); } } @@ -482,11 +480,7 @@ namespace spot n.parent = node; n.level = lvl + 1; n.scc = scc; - bv->foreach_set_index([&](unsigned e) - { - n.edges[e] = true; - n.states[aut->edge_storage(e).src] = true; - }); + n.edges |= *bv; } unsigned after_size = nodes_.size(); unsigned children = after_size - before_size; @@ -534,6 +528,16 @@ namespace spot ++node.level; trees_[scc].max_level = std::max(trees_[scc].max_level, node.level); } + // Compute the set of states hit by each edge vector. + // Skip the first ones, because they are used in the roots of each tree + // and have already been filled. + unsigned nv = bitvectors.size(); + for (unsigned n = 2; n < nv; n += 2) + bitvectors[n]->foreach_set_index([&aut, + &states=*bitvectors[n+1]](unsigned e) + { + states.set(aut->edge_storage(e).src); + }); } unsigned acd::leftmost_branch_(unsigned n, unsigned state) const @@ -546,7 +550,7 @@ namespace spot unsigned child = first_child; do { - if (nodes_[child].states[state]) + if (nodes_[child].states.get(state)) { n = child; goto loop; @@ -567,7 +571,7 @@ namespace spot if (trees_[scc].trivial) // the branch is irrelevant for transiant SCCs return 0; unsigned n = trees_[scc].root; - assert(nodes_[n].states[s]); + assert(nodes_[n].states.get(s)); return leftmost_branch_(n, s); } @@ -582,7 +586,7 @@ namespace spot unsigned child = 0; unsigned dst = aut_->edge_storage(edge).dst; - while (!nodes_[branch].edges[edge]) + while (!nodes_[branch].edges.get(edge)) { unsigned parent = nodes_[branch].parent; if (SPOT_UNLIKELY(branch == parent)) @@ -604,7 +608,7 @@ namespace spot do { child = nodes_[child].next_sibling; - if (nodes_[child].states[dst]) + if (nodes_[child].states.get(dst)) return {leftmost_branch_(child, dst), lvl}; } while (child != start_child); @@ -643,7 +647,7 @@ namespace spot const char* sep = "T: "; for (unsigned n = 1; n <= nedges; ++n) { - bool val = n < nedges && edges[n] + bool val = n < nedges && edges.get(n) && si_->scc_of(aut_->edge_storage(n).dst) == scc; if (val != lastval) { @@ -675,7 +679,7 @@ namespace spot sep = "\nQ: "; for (unsigned n = 0; n <= nstates; ++n) { - bool val = n < nstates && states[n] && si_->scc_of(n) == scc; + bool val = n < nstates && states.get(n) && si_->scc_of(n) == scc; if (val != lastval) { if (lastval) @@ -708,7 +712,7 @@ namespace spot os << " class=\""; const char* sep = ""; for (unsigned n = 0; n < nstates; ++n) - if (states[n] && si_->scc_of(n) == scc) + if (states.get(n) && si_->scc_of(n) == scc) { os << sep << "acdS" << n << '\n'; sep = " "; @@ -746,7 +750,7 @@ namespace spot auto& edges = nodes_[n].edges; unsigned nedges = edges.size(); for (unsigned e = 1; e < nedges; ++e) - if (edges[e] && si_->scc_of(aut_->edge_storage(e).dst) == scc) + if (edges.get(e) && si_->scc_of(aut_->edge_storage(e).dst) == scc) res.push_back(e); return res; } diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index 8222a8335..c4d3563b4 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -21,6 +21,8 @@ #include #include +#include +#include #include #include @@ -285,9 +287,9 @@ namespace spot unsigned first_child = 0; unsigned level; unsigned scc; - std::vector& edges; - std::vector& states; - acd_node(std::vector& e, std::vector& s) noexcept + bitvect& edges; + bitvect& states; + acd_node(bitvect& e, bitvect& s) noexcept : edges(e), states(s) { } @@ -297,7 +299,7 @@ namespace spot std::deque nodes_; // Likewise for bitvectors: this is the support for all edge vectors // and state vectors used in acd_node. - std::deque> bitvectors; + std::deque> bitvectors; // Information about a tree of the ACD. Each tree correspond // to an SCC. struct scc_data