alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

zlktree: simplify heuristic computation

Browse source 
* spot/twaalgos/zlktree.cc: Here.
* spot/twaalgos/zlktree.hh: Add a way to remove an option.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-30 17:05:18 +02:00
parent 88d0d2e112
commit 2c435c6c11
2 changed files with 19 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

14
spot/twaalgos/zlktree.cc
View file

@ -386,6 +386,10 @@ namespace spot
acc_cond posacc = aut->acc(); acc_cond posacc = aut->acc();
acc_cond negacc(posacc.num_sets(), posacc.get_acceptance().complement()); acc_cond negacc(posacc.num_sets(), posacc.get_acceptance().complement());
if (nstates <= 1)
// The ordering heuristic does not help if we have a single state.
opt_ = opt_ - acd_options::ORDER_HEURISTIC;
// The bitvectors store edge and state-vectors that are shared // The bitvectors store edge and state-vectors that are shared
// among the different trees. // among the different trees.
auto allocate_vectors_maybe = [&](unsigned n) auto allocate_vectors_maybe = [&](unsigned n)
@ -508,19 +512,20 @@ namespace spot
seen_dup->add_common(*seen_src, *seen_dst); seen_dup->add_common(*seen_src, *seen_dst);
*seen_src |= *seen_dst; *seen_src |= *seen_dst;
} }
if (seen_dup->is_fully_clear())
goto skip_sort;
// Now the union in seen_src is not useful anymore. Process // Now the union in seen_src is not useful anymore. Process
// each node again, but consider only the states that are in // each node again, but consider only the states that are in
// seen_dup. // seen_dup.
for (auto& [sz, bv]: out) for (auto& [sz, bv]: out)
{ {
seen_src->clear_all(); // local source of the node seen_src->clear_all(); // local source of the node
bv->foreach_set_index([&aut, &seen_src, &seen_dup](unsigned e) bv->foreach_set_index([&aut, &seen_src](unsigned e)
{ {
unsigned idx = aut->edge_storage(e).src; seen_src->set(aut->edge_storage(e).src);
if (seen_dup->get(idx))
seen_src->set(idx); // store duplicates
}); });
seen_dst->clear_all(); seen_dst->clear_all();
*seen_src &= *seen_dup;
// Count the number of states reached by leaving this node. // Count the number of states reached by leaving this node.
seen_src->foreach_set_index([&aut, bv=bv.get(), seen_src->foreach_set_index([&aut, bv=bv.get(),
&seen_dst](unsigned s) &seen_dst](unsigned s)
@ -536,6 +541,7 @@ namespace spot
[&](auto& p1, auto& p2) { [&](auto& p1, auto& p2) {
return p1.size > p2.size; return p1.size > p2.size;
}); });
skip_sort:;
} }
unsigned before_size = nodes_.size(); unsigned before_size = nodes_.size();

9
spot/twaalgos/zlktree.hh
View file

@ -196,6 +196,15 @@ namespace spot
return static_cast<acd_options>(static_cast<ut>(left) return static_cast<acd_options>(static_cast<ut>(left)
| static_cast<ut>(right)); | static_cast<ut>(right));
} }
inline
acd_options operator-(acd_options left, acd_options right)
{
typedef std::underlying_type_t<acd_options> ut;
return static_cast<acd_options>(static_cast<ut>(left)
& ~static_cast<ut>(right));
}
#endif #endif
/// \ingroup twa_acc_transform /// \ingroup twa_acc_transform