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

expansions: split-off OrRat case

Browse source
This commit is contained in:
Antoine Martin 2022-12-15 10:44:37 +01:00
parent 1240fec39b
commit 3c6929829d
1 changed files with 22 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

35
spot/tl/expansions.cc
View file

@ -305,7 +305,6 @@ namespace spot
}
case op::AndRat:
case op::OrRat:
{
expansion_t res;
for (const auto& sub_f : f)
@ -314,9 +313,6 @@ namespace spot
if (exps.empty())
{
if (f.kind() == op::OrRat)
continue;
// op::AndRat: one of the expansions was empty (the only
// edge was `false`), so the AndRat is empty as
// well
@ -337,15 +333,6 @@ namespace spot
{
if ((l_key & r_key) != bddfalse)
insert_or_merge(new_res, l_key & r_key, formula::multop(f.kind(), {l_val, r_val}));
if (f.is(op::OrRat))
{
if ((l_key & !r_key) != bddfalse)
insert_or_merge(new_res, l_key & !r_key, l_val);
if ((!l_key & r_key) != bddfalse)
insert_or_merge(new_res, !l_key & r_key, r_val);
}
}
}
@ -355,6 +342,28 @@ namespace spot
return res;
}
case op::OrRat:
{
expansion_t res;
for (const auto& sub_f : f)
{
auto exps = expansion(sub_f, d, owner);
if (exps.empty())
continue;
if (res.empty())
{
res = std::move(exps);
continue;
}
for (const auto& [label, dest] : exps)
insert_or_merge(res, label, dest);
}
return res;
}
default:
std::cerr << "unimplemented kind "
<< static_cast<int>(f.kind())