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

* spot/tl/formula.cc: Fix two fixmes.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2019-06-21 22:01:42 +02:00
parent dc34862d3b
commit c830b5db25
1 changed files with 27 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

65
spot/tl/formula.cc
View file

@ -254,46 +254,35 @@ namespace spot
// //
// When we construct a formula such as Multop(Op,X,Multop(Op,Y,Z)) // When we construct a formula such as Multop(Op,X,Multop(Op,Y,Z))
// we will want to inline it as Multop(Op,X,Y,Z). // we will want to inline it as Multop(Op,X,Y,Z).
{ //
vec inlined; // At the same time, it's possible that vec contains some null
vec::iterator i = v.begin(); // pointers we should remove. We can do it in the same loop.
while (i != v.end()) //
{ // It is simpler to construct a separate vector to do that, but that's
// Some simplification routines erase terms using null // only needed if we have nested multops or null poiners.
// pointers that we must ignore. if (std::find_if(v.begin(), v.end(),
if ((*i) == nullptr) [o](const fnode* f) { return f == nullptr || f->is(o); })
{ != v.end())
// FIXME: For commutative operators we should replace {
// the pointer by the first non-null value at the end vec inlined;
// of the array instead of calling erase. for (const fnode* f: v)
i = v.erase(i); {
if (f == nullptr)
continue; continue;
} if (f->is(o))
if ((*i)->is(o)) {
{ unsigned ps = f->size();
unsigned ps = (*i)->size(); for (unsigned n = 0; n < ps; ++n)
for (unsigned n = 0; n < ps; ++n) inlined.emplace_back(f->nth(n)->clone());
inlined.emplace_back((*i)->nth(n)->clone()); f->destroy();
(*i)->destroy(); }
// FIXME: Do not use erase. See previous FIXME. else
i = v.erase(i); {
continue; inlined.emplace_back(f);
} }
// All operators except "Concat" and "Fusion" are }
// commutative, so we just keep a list of the inlined
// arguments that should later be added to the vector.
// For concat we have to keep track of the order of
// all the arguments.
if (o == op::Concat || o == op::Fusion)
inlined.emplace_back(*i);
++i;
}
if (o == op::Concat || o == op::Fusion)
v.swap(inlined); v.swap(inlined);
else }
v.insert(v.end(), inlined.begin(), inlined.end());
}
if (o != op::Concat && o != op::Fusion) if (o != op::Concat && o != op::Fusion)
std::sort(v.begin(), v.end(), formula_ptr_less_than_bool_first()); std::sort(v.begin(), v.end(), formula_ptr_less_than_bool_first());