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

split: Improve performance of split_edges()

Browse source 
* spot/twaalgos/split.cc: Add cache to avoid
  computing multiple split on the same condition.
This commit is contained in:
Jerome Dubois 2021-01-22 20:45:34 +01:00 • committed by Alexandre Duret-Lutz
parent b082df201f
commit ec4deb3219
1 changed files with 22 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

18
spot/twaalgos/split.cc
View file

@ -24,6 +24,7 @@
#include <spot/misc/bddlt.hh> #include <spot/misc/bddlt.hh>
#include <algorithm> #include <algorithm>
#include <map>
namespace spot namespace spot
{ {
@ -39,6 +40,8 @@ namespace spot
internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph()); internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph());
bdd all = aut->ap_vars(); bdd all = aut->ap_vars();
std::map<unsigned, std::pair<unsigned, unsigned>> split_cond;
for (auto& e: aut->edges()) for (auto& e: aut->edges())
{ {
bdd cond = e.cond; bdd cond = e.cond;
@ -50,12 +53,27 @@ namespace spot
auto d = aut->univ_dests(dst); auto d = aut->univ_dests(dst);
dst = uniq.new_univ_dests(d.begin(), d.end()); dst = uniq.new_univ_dests(d.begin(), d.end());
} }
auto& [begin, end] = split_cond[cond.id()];
if (begin == end)
{
begin = aut->num_edges();
while (cond != bddfalse) while (cond != bddfalse)
{ {
bdd cube = bdd_satoneset(cond, all, bddfalse); bdd cube = bdd_satoneset(cond, all, bddfalse);
cond -= cube; cond -= cube;
out->new_edge(e.src, dst, cube, e.acc); out->new_edge(e.src, dst, cube, e.acc);
} }
end = aut->num_edges();
}
else
{
auto& g = aut->get_graph();
for (unsigned i = begin; i < end; ++i)
out->new_edge(e.src, dst, g.edge_storage(i).cond, e.acc);
}
} }
return out; return out;
} }