Prefer emplace_back to push_back
* spot/graph/ngraph.hh, spot/ltsmin/ltsmin.cc, spot/misc/bitvect.hh, spot/misc/intvcomp.cc, spot/misc/satsolver.cc, spot/priv/weight.cc, spot/ta/taexplicit.cc, spot/taalgos/minimize.cc, spot/taalgos/reachiter.cc, spot/tl/exclusive.cc, spot/tl/formula.cc, spot/tl/formula.hh, spot/tl/mark.cc, spot/tl/mutation.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc, spot/tl/simplify.cc, spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/taatgba.hh, spot/twa/twa.hh, spot/twa/twagraph.cc, spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc, spot/twaalgos/compsusp.cc, spot/twaalgos/copy.cc, spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/emptiness.cc, spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc, spot/twaalgos/mask.hh, spot/twaalgos/minimize.cc, spot/twaalgos/powerset.cc, spot/twaalgos/product.cc, spot/twaalgos/randomgraph.cc, spot/twaalgos/reachiter.cc, spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/se05.cc, spot/twaalgos/simulation.cc, spot/twaalgos/stutter.cc, spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc, spot/twaalgos/word.cc, tests/core/bitvect.cc: here.
This commit is contained in:
parent
ef214b2c42
commit
43ec36cda7
54 changed files with 310 additions and 310 deletions
|
|
@ -144,7 +144,7 @@ namespace spot
|
||||||
std::vector<State_Name> d;
|
std::vector<State_Name> d;
|
||||||
d.reserve(dst.size());
|
d.reserve(dst.size());
|
||||||
for (auto n: dst)
|
for (auto n: dst)
|
||||||
d.push_back(get_state(n));
|
d.emplace_back(get_state(n));
|
||||||
return g_.new_edge(get_state(src), d, std::forward<Args>(args)...);
|
return g_.new_edge(get_state(src), d, std::forward<Args>(args)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -156,7 +156,7 @@ namespace spot
|
||||||
std::vector<state> d;
|
std::vector<state> d;
|
||||||
d.reserve(dst.size());
|
d.reserve(dst.size());
|
||||||
for (auto n: dst)
|
for (auto n: dst)
|
||||||
d.push_back(get_state(n));
|
d.emplace_back(get_state(n));
|
||||||
return g_.new_edge(get_state(src), d, std::forward<Args>(args)...);
|
return g_.new_edge(get_state(src), d, std::forward<Args>(args)...);
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
|
||||||
|
|
@ -236,7 +236,7 @@ namespace spot
|
||||||
new(p->allocate()) spins_state(ctx->state_size, p);
|
new(p->allocate()) spins_state(ctx->state_size, p);
|
||||||
memcpy(out->vars, dst, ctx->state_size * sizeof(int));
|
memcpy(out->vars, dst, ctx->state_size * sizeof(int));
|
||||||
out->compute_hash();
|
out->compute_hash();
|
||||||
ctx->transitions.push_back(out);
|
ctx->transitions.emplace_back(out);
|
||||||
}
|
}
|
||||||
|
|
||||||
void transition_callback_compress(void* arg, transition_info_t*, int *dst)
|
void transition_callback_compress(void* arg, transition_info_t*, int *dst)
|
||||||
|
|
@ -252,7 +252,7 @@ namespace spot
|
||||||
spins_compressed_state* out = new(mem) spins_compressed_state(csize, p);
|
spins_compressed_state* out = new(mem) spins_compressed_state(csize, p);
|
||||||
memcpy(out->vars, ctx->compressed, csize * sizeof(int));
|
memcpy(out->vars, ctx->compressed, csize * sizeof(int));
|
||||||
out->compute_hash();
|
out->compute_hash();
|
||||||
ctx->transitions.push_back(out);
|
ctx->transitions.emplace_back(out);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
@ -462,7 +462,7 @@ namespace spot
|
||||||
// Record that X.Y must be equal to Z.
|
// Record that X.Y must be equal to Z.
|
||||||
int v = dict->register_proposition(*ap, d.get());
|
int v = dict->register_proposition(*ap, d.get());
|
||||||
one_prop p = { ni->second.num, OP_EQ, ei->second, v };
|
one_prop p = { ni->second.num, OP_EQ, ei->second, v };
|
||||||
out.push_back(p);
|
out.emplace_back(p);
|
||||||
free(name);
|
free(name);
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
@ -473,7 +473,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
int v = dict->register_proposition(*ap, d);
|
int v = dict->register_proposition(*ap, d);
|
||||||
one_prop p = { var_num, OP_NE, 0, v };
|
one_prop p = { var_num, OP_NE, 0, v };
|
||||||
out.push_back(p);
|
out.emplace_back(p);
|
||||||
free(name);
|
free(name);
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
@ -591,7 +591,7 @@ namespace spot
|
||||||
|
|
||||||
int v = dict->register_proposition(*ap, d);
|
int v = dict->register_proposition(*ap, d);
|
||||||
one_prop p = { var_num, op, val, v };
|
one_prop p = { var_num, op, val, v };
|
||||||
out.push_back(p);
|
out.emplace_back(p);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (errors)
|
if (errors)
|
||||||
|
|
@ -809,7 +809,7 @@ namespace spot
|
||||||
|
|
||||||
// Add a self-loop to dead-states if we care about these.
|
// Add a self-loop to dead-states if we care about these.
|
||||||
if (res != bddfalse)
|
if (res != bddfalse)
|
||||||
cc->transitions.push_back(st->clone());
|
cc->transitions.emplace_back(st->clone());
|
||||||
}
|
}
|
||||||
|
|
||||||
state_condition_last_cc_ = cc;
|
state_condition_last_cc_ = cc;
|
||||||
|
|
@ -861,7 +861,7 @@ namespace spot
|
||||||
|
|
||||||
// Add a self-loop to dead-states if we care about these.
|
// Add a self-loop to dead-states if we care about these.
|
||||||
if (t == 0 && scond != bddfalse)
|
if (t == 0 && scond != bddfalse)
|
||||||
cc->transitions.push_back(st->clone());
|
cc->transitions.emplace_back(st->clone());
|
||||||
}
|
}
|
||||||
|
|
||||||
if (iter_cache_)
|
if (iter_cache_)
|
||||||
|
|
|
||||||
|
|
@ -141,7 +141,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Append one bit.
|
/// Append one bit.
|
||||||
void push_back(bool val)
|
void emplace_back(bool val)
|
||||||
{
|
{
|
||||||
if (size() == capacity())
|
if (size() == capacity())
|
||||||
grow();
|
grow();
|
||||||
|
|
@ -153,7 +153,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Append the lowest \a count bits of \a data.
|
/// \brief Append the lowest \a count bits of \a data.
|
||||||
void push_back(block_t data, unsigned count)
|
void emplace_back(block_t data, unsigned count)
|
||||||
{
|
{
|
||||||
if (size() + count > capacity())
|
if (size() + count > capacity())
|
||||||
grow();
|
grow();
|
||||||
|
|
@ -417,18 +417,18 @@ namespace spot
|
||||||
{
|
{
|
||||||
block_t data = storage_[indexb];
|
block_t data = storage_[indexb];
|
||||||
data >>= bitb;
|
data >>= bitb;
|
||||||
res->push_back(data, count);
|
res->emplace_back(data, count);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
block_t data = storage_[indexb];
|
block_t data = storage_[indexb];
|
||||||
data >>= bitb;
|
data >>= bitb;
|
||||||
res->push_back(data, bpb - bitb);
|
res->emplace_back(data, bpb - bitb);
|
||||||
count -= bpb - bitb;
|
count -= bpb - bitb;
|
||||||
while (count >= bpb)
|
while (count >= bpb)
|
||||||
{
|
{
|
||||||
++indexb;
|
++indexb;
|
||||||
res->push_back(storage_[indexb], bpb);
|
res->emplace_back(storage_[indexb], bpb);
|
||||||
count -= bpb;
|
count -= bpb;
|
||||||
SPOT_ASSERT(indexb != indexe || count == 0);
|
SPOT_ASSERT(indexb != indexe || count == 0);
|
||||||
}
|
}
|
||||||
|
|
@ -437,7 +437,7 @@ namespace spot
|
||||||
++indexb;
|
++indexb;
|
||||||
SPOT_ASSERT(indexb == indexe);
|
SPOT_ASSERT(indexb == indexe);
|
||||||
SPOT_ASSERT(count == end % bpb);
|
SPOT_ASSERT(count == end % bpb);
|
||||||
res->push_back(storage_[indexb], count);
|
res->emplace_back(storage_[indexb], count);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return res;
|
return res;
|
||||||
|
|
|
||||||
|
|
@ -196,7 +196,7 @@ namespace spot
|
||||||
|
|
||||||
void push_data(unsigned int i)
|
void push_data(unsigned int i)
|
||||||
{
|
{
|
||||||
result_->push_back(i);
|
result_->emplace_back(i);
|
||||||
}
|
}
|
||||||
|
|
||||||
const std::vector<unsigned int>*
|
const std::vector<unsigned int>*
|
||||||
|
|
@ -246,7 +246,7 @@ namespace spot
|
||||||
|
|
||||||
void push_data(unsigned int i)
|
void push_data(unsigned int i)
|
||||||
{
|
{
|
||||||
output_.push_back(i);
|
output_.emplace_back(i);
|
||||||
}
|
}
|
||||||
|
|
||||||
bool have_data() const
|
bool have_data() const
|
||||||
|
|
@ -543,7 +543,7 @@ namespace spot
|
||||||
void push_data(int i)
|
void push_data(int i)
|
||||||
{
|
{
|
||||||
prev_ = i;
|
prev_ = i;
|
||||||
result_.push_back(i);
|
result_.emplace_back(i);
|
||||||
--size_;
|
--size_;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -551,7 +551,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
size_ -= i;
|
size_ -= i;
|
||||||
while (i--)
|
while (i--)
|
||||||
result_.push_back(prev_);
|
result_.emplace_back(prev_);
|
||||||
}
|
}
|
||||||
|
|
||||||
bool have_comp_data() const
|
bool have_comp_data() const
|
||||||
|
|
|
||||||
|
|
@ -108,7 +108,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (i == 0)
|
if (i == 0)
|
||||||
goto done;
|
goto done;
|
||||||
sol.push_back(i);
|
sol.emplace_back(i);
|
||||||
}
|
}
|
||||||
if (!in->eof())
|
if (!in->eof())
|
||||||
// If we haven't reached end-of-file, then we just attempted
|
// If we haven't reached end-of-file, then we just attempted
|
||||||
|
|
|
||||||
|
|
@ -52,7 +52,7 @@ namespace spot
|
||||||
std::vector<unsigned> res;
|
std::vector<unsigned> res;
|
||||||
for (unsigned n = 0; n < max; ++n)
|
for (unsigned n = 0; n < max; ++n)
|
||||||
if (m[n] > w.m[n])
|
if (m[n] > w.m[n])
|
||||||
res.push_back(n);
|
res.emplace_back(n);
|
||||||
return acc_cond::mark_t(res.begin(), res.end());
|
return acc_cond::mark_t(res.begin(), res.end());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -158,8 +158,8 @@ namespace spot
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
trans_by_condition->push_back(t);
|
trans_by_condition->emplace_back(t);
|
||||||
transitions_->push_back(t);
|
transitions_->emplace_back(t);
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -266,7 +266,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
hash_set* cI = new hash_set;
|
hash_set* cI = new hash_set;
|
||||||
cI->insert(*i);
|
cI->insert(*i);
|
||||||
done.push_back(cI);
|
done.emplace_back(cI);
|
||||||
|
|
||||||
used_var[set_num] = 1;
|
used_var[set_num] = 1;
|
||||||
free_var.erase(set_num);
|
free_var.erase(set_num);
|
||||||
|
|
@ -284,9 +284,9 @@ namespace spot
|
||||||
used_var[num] = s;
|
used_var[num] = s;
|
||||||
free_var.erase(num);
|
free_var.erase(num);
|
||||||
if (s > 1)
|
if (s > 1)
|
||||||
cur_run.push_back(G);
|
cur_run.emplace_back(G);
|
||||||
else
|
else
|
||||||
done.push_back(G);
|
done.emplace_back(G);
|
||||||
for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i)
|
for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i)
|
||||||
state_set_map[*i] = num;
|
state_set_map[*i] = num;
|
||||||
|
|
||||||
|
|
@ -304,9 +304,9 @@ namespace spot
|
||||||
used_var[num] = s;
|
used_var[num] = s;
|
||||||
free_var.erase(num);
|
free_var.erase(num);
|
||||||
if (s > 1)
|
if (s > 1)
|
||||||
cur_run.push_back(F);
|
cur_run.emplace_back(F);
|
||||||
else
|
else
|
||||||
done.push_back(F);
|
done.emplace_back(F);
|
||||||
for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i)
|
for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i)
|
||||||
state_set_map[*i] = num;
|
state_set_map[*i] = num;
|
||||||
}
|
}
|
||||||
|
|
@ -323,9 +323,9 @@ namespace spot
|
||||||
used_var[num] = s;
|
used_var[num] = s;
|
||||||
free_var.erase(num);
|
free_var.erase(num);
|
||||||
if (s > 1)
|
if (s > 1)
|
||||||
cur_run.push_back(G_F);
|
cur_run.emplace_back(G_F);
|
||||||
else
|
else
|
||||||
done.push_back(G_F);
|
done.emplace_back(G_F);
|
||||||
for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i)
|
for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i)
|
||||||
state_set_map[*i] = num;
|
state_set_map[*i] = num;
|
||||||
}
|
}
|
||||||
|
|
@ -342,9 +342,9 @@ namespace spot
|
||||||
used_var[num] = s;
|
used_var[num] = s;
|
||||||
free_var.erase(num);
|
free_var.erase(num);
|
||||||
if (s > 1)
|
if (s > 1)
|
||||||
cur_run.push_back(S);
|
cur_run.emplace_back(S);
|
||||||
else
|
else
|
||||||
done.push_back(S);
|
done.emplace_back(S);
|
||||||
for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i)
|
for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i)
|
||||||
state_set_map[*i] = num;
|
state_set_map[*i] = num;
|
||||||
}
|
}
|
||||||
|
|
@ -432,7 +432,7 @@ namespace spot
|
||||||
trace
|
trace
|
||||||
<< "set " << format_hash_set(bsi->second, ta_)
|
<< "set " << format_hash_set(bsi->second, ta_)
|
||||||
<< " was not split" << std::endl;
|
<< " was not split" << std::endl;
|
||||||
next_run.push_back(bsi->second);
|
next_run.emplace_back(bsi->second);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -466,14 +466,14 @@ namespace spot
|
||||||
trace
|
trace
|
||||||
<< "set " << format_hash_set(set, ta_)
|
<< "set " << format_hash_set(set, ta_)
|
||||||
<< " is minimal" << std::endl;
|
<< " is minimal" << std::endl;
|
||||||
done.push_back(set);
|
done.emplace_back(set);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
trace
|
trace
|
||||||
<< "set " << format_hash_set(set, ta_)
|
<< "set " << format_hash_set(set, ta_)
|
||||||
<< " should be processed further" << std::endl;
|
<< " should be processed further" << std::endl;
|
||||||
next_run.push_back(set);
|
next_run.emplace_back(set);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -167,7 +167,7 @@ namespace spot
|
||||||
void
|
void
|
||||||
ta_reachable_iterator_breadth_first::add_state(const state* s)
|
ta_reachable_iterator_breadth_first::add_state(const state* s)
|
||||||
{
|
{
|
||||||
todo.push_back(s);
|
todo.emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
const state*
|
const state*
|
||||||
|
|
|
||||||
|
|
@ -104,7 +104,7 @@ namespace spot
|
||||||
|
|
||||||
void exclusive_ap::add_group(std::vector<formula> ap)
|
void exclusive_ap::add_group(std::vector<formula> ap)
|
||||||
{
|
{
|
||||||
groups.push_back(ap);
|
groups.emplace_back(ap);
|
||||||
}
|
}
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
|
|
@ -130,12 +130,12 @@ namespace spot
|
||||||
|
|
||||||
for (auto ap: g)
|
for (auto ap: g)
|
||||||
if (s->find(ap) != s->end())
|
if (s->find(ap) != s->end())
|
||||||
group.push_back(ap);
|
group.emplace_back(ap);
|
||||||
|
|
||||||
unsigned s = group.size();
|
unsigned s = group.size();
|
||||||
for (unsigned j = 0; j < s; ++j)
|
for (unsigned j = 0; j < s; ++j)
|
||||||
for (unsigned k = j + 1; k < s; ++k)
|
for (unsigned k = j + 1; k < s; ++k)
|
||||||
v.push_back(nand(group[j], group[k]));
|
v.emplace_back(nand(group[j], group[k]));
|
||||||
};
|
};
|
||||||
|
|
||||||
delete s;
|
delete s;
|
||||||
|
|
@ -166,7 +166,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
int v = d->has_registered_proposition(ap, aut);
|
int v = d->has_registered_proposition(ap, aut);
|
||||||
if (v >= 0)
|
if (v >= 0)
|
||||||
group.push_back(bdd_nithvar(v));
|
group.emplace_back(bdd_nithvar(v));
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned s = group.size();
|
unsigned s = group.size();
|
||||||
|
|
|
||||||
|
|
@ -105,7 +105,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
if ((*i)->is_boolean())
|
if ((*i)->is_boolean())
|
||||||
{
|
{
|
||||||
b.push_back(*i);
|
b.emplace_back(*i);
|
||||||
i = v.erase(i);
|
i = v.erase(i);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -230,7 +230,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
unsigned ps = (*i)->size();
|
unsigned ps = (*i)->size();
|
||||||
for (unsigned n = 0; n < ps; ++n)
|
for (unsigned n = 0; n < ps; ++n)
|
||||||
inlined.push_back((*i)->nth(n)->clone());
|
inlined.emplace_back((*i)->nth(n)->clone());
|
||||||
(*i)->destroy();
|
(*i)->destroy();
|
||||||
// FIXME: Do not use erase. See previous FIXME.
|
// FIXME: Do not use erase. See previous FIXME.
|
||||||
i = v.erase(i);
|
i = v.erase(i);
|
||||||
|
|
@ -242,7 +242,7 @@ namespace spot
|
||||||
// For concat we have to keep track of the order of
|
// For concat we have to keep track of the order of
|
||||||
// all the arguments.
|
// all the arguments.
|
||||||
if (o == op::Concat || o == op::Fusion)
|
if (o == op::Concat || o == op::Fusion)
|
||||||
inlined.push_back(*i);
|
inlined.emplace_back(*i);
|
||||||
++i;
|
++i;
|
||||||
}
|
}
|
||||||
if (o == op::Concat || o == op::Fusion)
|
if (o == op::Concat || o == op::Fusion)
|
||||||
|
|
@ -470,10 +470,10 @@ namespace spot
|
||||||
i->destroy();
|
i->destroy();
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
tmp.push_back(i);
|
tmp.emplace_back(i);
|
||||||
}
|
}
|
||||||
if (tmp.empty())
|
if (tmp.empty())
|
||||||
tmp.push_back(weak_abs);
|
tmp.emplace_back(weak_abs);
|
||||||
v.swap(tmp);
|
v.swap(tmp);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -1624,7 +1624,7 @@ namespace spot
|
||||||
v.reserve(s - 1);
|
v.reserve(s - 1);
|
||||||
for (unsigned j = 0; j < s; ++j)
|
for (unsigned j = 0; j < s; ++j)
|
||||||
if (i != j)
|
if (i != j)
|
||||||
v.push_back(nth(j)->clone());
|
v.emplace_back(nth(j)->clone());
|
||||||
return multop(o, v);
|
return multop(o, v);
|
||||||
}
|
}
|
||||||
default:
|
default:
|
||||||
|
|
|
||||||
|
|
@ -1018,7 +1018,7 @@ namespace spot
|
||||||
tmp.reserve(l.size());
|
tmp.reserve(l.size());
|
||||||
for (auto f: l)
|
for (auto f: l)
|
||||||
if (f.ptr_)
|
if (f.ptr_)
|
||||||
tmp.push_back(f.ptr_->clone());
|
tmp.emplace_back(f.ptr_->clone());
|
||||||
return formula(fnode::multop(o, std::move(tmp)));
|
return formula(fnode::multop(o, std::move(tmp)));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1029,7 +1029,7 @@ namespace spot
|
||||||
tmp.reserve(l.size());
|
tmp.reserve(l.size());
|
||||||
for (auto f: l)
|
for (auto f: l)
|
||||||
if (f.ptr_)
|
if (f.ptr_)
|
||||||
tmp.push_back(f.to_node_());
|
tmp.emplace_back(f.to_node_());
|
||||||
return formula(fnode::multop(o, std::move(tmp)));
|
return formula(fnode::multop(o, std::move(tmp)));
|
||||||
}
|
}
|
||||||
#endif // !SWIG
|
#endif // !SWIG
|
||||||
|
|
@ -1628,7 +1628,7 @@ namespace spot
|
||||||
std::vector<formula> tmp;
|
std::vector<formula> tmp;
|
||||||
tmp.reserve(size());
|
tmp.reserve(size());
|
||||||
for (auto f: *this)
|
for (auto f: *this)
|
||||||
tmp.push_back(trans(f));
|
tmp.emplace_back(trans(f));
|
||||||
return multop(o, std::move(tmp));
|
return multop(o, std::move(tmp));
|
||||||
}
|
}
|
||||||
case op::Star:
|
case op::Star:
|
||||||
|
|
|
||||||
|
|
@ -137,24 +137,24 @@ namespace spot
|
||||||
if (c.is(op::EConcatMarked))
|
if (c.is(op::EConcatMarked))
|
||||||
{
|
{
|
||||||
empairs.emplace(c[0], c[1]);
|
empairs.emplace(c[0], c[1]);
|
||||||
v.push_back(c.map(recurse));
|
v.emplace_back(c.map(recurse));
|
||||||
}
|
}
|
||||||
else if (c.is(op::EConcat))
|
else if (c.is(op::EConcat))
|
||||||
{
|
{
|
||||||
elist.push_back(c);
|
elist.emplace_back(c);
|
||||||
}
|
}
|
||||||
else if (c.is(op::NegClosureMarked))
|
else if (c.is(op::NegClosureMarked))
|
||||||
{
|
{
|
||||||
nmset.insert(c[0]);
|
nmset.insert(c[0]);
|
||||||
v.push_back(c.map(recurse));
|
v.emplace_back(c.map(recurse));
|
||||||
}
|
}
|
||||||
else if (c.is(op::NegClosure))
|
else if (c.is(op::NegClosure))
|
||||||
{
|
{
|
||||||
nlist.push_back(c);
|
nlist.emplace_back(c);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
v.push_back(c);
|
v.emplace_back(c);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// Keep only the non-marked EConcat for which we
|
// Keep only the non-marked EConcat for which we
|
||||||
|
|
@ -162,12 +162,12 @@ namespace spot
|
||||||
for (auto e: elist)
|
for (auto e: elist)
|
||||||
if (empairs.find(std::make_pair(e[0], e[1]))
|
if (empairs.find(std::make_pair(e[0], e[1]))
|
||||||
== empairs.end())
|
== empairs.end())
|
||||||
v.push_back(e);
|
v.emplace_back(e);
|
||||||
// Keep only the non-marked NegClosure for which we
|
// Keep only the non-marked NegClosure for which we
|
||||||
// have not seen a similar NegClosureMarked.
|
// have not seen a similar NegClosureMarked.
|
||||||
for (auto n: nlist)
|
for (auto n: nlist)
|
||||||
if (nmset.find(n[0]) == nmset.end())
|
if (nmset.find(n[0]) == nmset.end())
|
||||||
v.push_back(n);
|
v.emplace_back(n);
|
||||||
res = formula::And(v);
|
res = formula::And(v);
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
|
|
|
||||||
|
|
@ -116,7 +116,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
vec v1;
|
vec v1;
|
||||||
vec v2;
|
vec v2;
|
||||||
v1.push_back(f[0]);
|
v1.emplace_back(f[0]);
|
||||||
bool reverse = false;
|
bool reverse = false;
|
||||||
int i = 1;
|
int i = 1;
|
||||||
while (i < mos)
|
while (i < mos)
|
||||||
|
|
@ -128,10 +128,10 @@ namespace spot
|
||||||
reverse = true;
|
reverse = true;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
v1.push_back(f[i++]);
|
v1.emplace_back(f[i++]);
|
||||||
}
|
}
|
||||||
for (; i < mos; ++i)
|
for (; i < mos; ++i)
|
||||||
v2.push_back(f[i]);
|
v2.emplace_back(f[i]);
|
||||||
formula first = AndNLM_(v1);
|
formula first = AndNLM_(v1);
|
||||||
formula second = AndNLM_(v2);
|
formula second = AndNLM_(v2);
|
||||||
formula ost = formula::one_star();
|
formula ost = formula::one_star();
|
||||||
|
|
|
||||||
|
|
@ -253,8 +253,8 @@ namespace spot
|
||||||
if (!s.empty())
|
if (!s.empty())
|
||||||
{
|
{
|
||||||
formula top = s.top();
|
formula top = s.top();
|
||||||
in.first->second.push_back(top);
|
in.first->second.emplace_back(top);
|
||||||
g[top].push_back(f);
|
g[top].emplace_back(f);
|
||||||
if (!in.second)
|
if (!in.second)
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
@ -291,10 +291,10 @@ namespace spot
|
||||||
// Note that we only add an edge in one
|
// Note that we only add an edge in one
|
||||||
// direction, because we are building a cycle
|
// direction, because we are building a cycle
|
||||||
// between all children anyway.
|
// between all children anyway.
|
||||||
g[pred].push_back(next);
|
g[pred].emplace_back(next);
|
||||||
pred = next;
|
pred = next;
|
||||||
}
|
}
|
||||||
g[pred].push_back(f[0]);
|
g[pred].emplace_back(f[0]);
|
||||||
}
|
}
|
||||||
s.pop();
|
s.pop();
|
||||||
}
|
}
|
||||||
|
|
@ -436,7 +436,7 @@ namespace spot
|
||||||
if (b && b != f)
|
if (b && b != f)
|
||||||
{
|
{
|
||||||
res.reserve(sz - i + 1);
|
res.reserve(sz - i + 1);
|
||||||
res.push_back(visit(b));
|
res.emplace_back(visit(b));
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -444,7 +444,7 @@ namespace spot
|
||||||
res.reserve(sz);
|
res.reserve(sz);
|
||||||
}
|
}
|
||||||
for (; i < sz; ++i)
|
for (; i < sz; ++i)
|
||||||
res.push_back(visit(f[i]));
|
res.emplace_back(visit(f[i]));
|
||||||
return formula::multop(f.kind(), res);
|
return formula::multop(f.kind(), res);
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
|
||||||
|
|
@ -47,8 +47,8 @@ namespace spot
|
||||||
// First line
|
// First line
|
||||||
std::vector<formula> va1;
|
std::vector<formula> va1;
|
||||||
formula npi = formula::Not(i);
|
formula npi = formula::Not(i);
|
||||||
va1.push_back(i);
|
va1.emplace_back(i);
|
||||||
va1.push_back(formula::U(i, formula::And({npi, c})));
|
va1.emplace_back(formula::U(i, formula::And({npi, c})));
|
||||||
|
|
||||||
for (auto j: aps)
|
for (auto j: aps)
|
||||||
if (j != i)
|
if (j != i)
|
||||||
|
|
@ -56,22 +56,22 @@ namespace spot
|
||||||
// make sure the arguments of OR are created in a
|
// make sure the arguments of OR are created in a
|
||||||
// deterministic order
|
// deterministic order
|
||||||
auto tmp = formula::U(formula::Not(j), npi);
|
auto tmp = formula::U(formula::Not(j), npi);
|
||||||
va1.push_back(formula::Or({formula::U(j, npi), tmp}));
|
va1.emplace_back(formula::Or({formula::U(j, npi), tmp}));
|
||||||
}
|
}
|
||||||
vo.push_back(formula::And(va1));
|
vo.emplace_back(formula::And(va1));
|
||||||
// Second line
|
// Second line
|
||||||
std::vector<formula> va2;
|
std::vector<formula> va2;
|
||||||
va2.push_back(npi);
|
va2.emplace_back(npi);
|
||||||
va2.push_back(formula::U(npi, formula::And({i, c})));
|
va2.emplace_back(formula::U(npi, formula::And({i, c})));
|
||||||
for (auto j: aps)
|
for (auto j: aps)
|
||||||
if (j != i)
|
if (j != i)
|
||||||
{
|
{
|
||||||
// make sure the arguments of OR are created in a
|
// make sure the arguments of OR are created in a
|
||||||
// deterministic order
|
// deterministic order
|
||||||
auto tmp = formula::U(formula::Not(j), i);
|
auto tmp = formula::U(formula::Not(j), i);
|
||||||
va2.push_back(formula::Or({formula::U(j, i), tmp}));
|
va2.emplace_back(formula::Or({formula::U(j, i), tmp}));
|
||||||
}
|
}
|
||||||
vo.push_back(formula::And(va2));
|
vo.emplace_back(formula::And(va2));
|
||||||
}
|
}
|
||||||
// Third line
|
// Third line
|
||||||
std::vector<formula> va3;
|
std::vector<formula> va3;
|
||||||
|
|
@ -80,10 +80,10 @@ namespace spot
|
||||||
// make sure the arguments of OR are created in a
|
// make sure the arguments of OR are created in a
|
||||||
// deterministic order
|
// deterministic order
|
||||||
auto tmp = formula::G(formula::Not(i));
|
auto tmp = formula::G(formula::Not(i));
|
||||||
va3.push_back(formula::Or({formula::G(i), tmp}));
|
va3.emplace_back(formula::Or({formula::G(i), tmp}));
|
||||||
}
|
}
|
||||||
va3.push_back(c);
|
va3.emplace_back(c);
|
||||||
vo.push_back(formula::And(va3));
|
vo.emplace_back(formula::And(va3));
|
||||||
return formula::Or(vo);
|
return formula::Or(vo);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -482,7 +482,7 @@ namespace spot
|
||||||
unsigned mos = f.size();
|
unsigned mos = f.size();
|
||||||
vec v;
|
vec v;
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
for (unsigned i = 0; i < mos; ++i)
|
||||||
v.push_back(rec(f[i], negated));
|
v.emplace_back(rec(f[i], negated));
|
||||||
op on = o;
|
op on = o;
|
||||||
if (negated)
|
if (negated)
|
||||||
on = o == op::Or ? op::And : op::Or;
|
on = o == op::Or ? op::And : op::Or;
|
||||||
|
|
@ -704,7 +704,7 @@ namespace spot
|
||||||
case op::X:
|
case op::X:
|
||||||
if (res_X && !eu)
|
if (res_X && !eu)
|
||||||
{
|
{
|
||||||
res_X->push_back(f[0]);
|
res_X->emplace_back(f[0]);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
|
|
@ -713,13 +713,13 @@ namespace spot
|
||||||
formula c = f[0];
|
formula c = f[0];
|
||||||
if (res_FG && u && c.is(op::G))
|
if (res_FG && u && c.is(op::G))
|
||||||
{
|
{
|
||||||
res_FG->push_back(((split_ & Strip_FG) == Strip_FG
|
res_FG->emplace_back(((split_ & Strip_FG) == Strip_FG
|
||||||
? c[0] : f));
|
? c[0] : f));
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
if (res_F && !eu)
|
if (res_F && !eu)
|
||||||
{
|
{
|
||||||
res_F->push_back(((split_ & Strip_F) == Strip_F
|
res_F->emplace_back(((split_ & Strip_F) == Strip_F
|
||||||
? c : f));
|
? c : f));
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
@ -730,13 +730,13 @@ namespace spot
|
||||||
formula c = f[0];
|
formula c = f[0];
|
||||||
if (res_GF && e && c.is(op::F))
|
if (res_GF && e && c.is(op::F))
|
||||||
{
|
{
|
||||||
res_GF->push_back(((split_ & Strip_GF) == Strip_GF
|
res_GF->emplace_back(((split_ & Strip_GF) == Strip_GF
|
||||||
? c[0] : f));
|
? c[0] : f));
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
if (res_G && !eu)
|
if (res_G && !eu)
|
||||||
{
|
{
|
||||||
res_G->push_back(((split_ & Strip_G) == Strip_G
|
res_G->emplace_back(((split_ & Strip_G) == Strip_G
|
||||||
? c : f));
|
? c : f));
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
@ -746,7 +746,7 @@ namespace spot
|
||||||
case op::W:
|
case op::W:
|
||||||
if (res_U_or_W)
|
if (res_U_or_W)
|
||||||
{
|
{
|
||||||
res_U_or_W->push_back(f);
|
res_U_or_W->emplace_back(f);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
|
|
@ -754,14 +754,14 @@ namespace spot
|
||||||
case op::M:
|
case op::M:
|
||||||
if (res_R_or_M)
|
if (res_R_or_M)
|
||||||
{
|
{
|
||||||
res_R_or_M->push_back(f);
|
res_R_or_M->emplace_back(f);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
if (res_Bool && f.is_boolean())
|
if (res_Bool && f.is_boolean())
|
||||||
{
|
{
|
||||||
res_Bool->push_back(f);
|
res_Bool->emplace_back(f);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
|
|
@ -770,21 +770,21 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (res_EventUniv && e && u)
|
if (res_EventUniv && e && u)
|
||||||
{
|
{
|
||||||
res_EventUniv->push_back(f);
|
res_EventUniv->emplace_back(f);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
if (res_Event && e)
|
if (res_Event && e)
|
||||||
{
|
{
|
||||||
res_Event->push_back(f);
|
res_Event->emplace_back(f);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
if (res_Univ && u)
|
if (res_Univ && u)
|
||||||
{
|
{
|
||||||
res_Univ->push_back(f);
|
res_Univ->emplace_back(f);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
res_other->push_back(f);
|
res_other->emplace_back(f);
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned split_;
|
unsigned split_;
|
||||||
|
|
@ -892,7 +892,7 @@ namespace spot
|
||||||
mospliter s(mospliter::Split_EventUniv, c, c_);
|
mospliter s(mospliter::Split_EventUniv, c, c_);
|
||||||
op oc = c.kind();
|
op oc = c.kind();
|
||||||
s.res_EventUniv->
|
s.res_EventUniv->
|
||||||
push_back(unop_multop(op::X, oc,
|
emplace_back(unop_multop(op::X, oc,
|
||||||
std::move(*s.res_other)));
|
std::move(*s.res_other)));
|
||||||
formula result =
|
formula result =
|
||||||
formula::multop(oc,
|
formula::multop(oc,
|
||||||
|
|
@ -984,10 +984,10 @@ namespace spot
|
||||||
mospliter::Split_EventUniv,
|
mospliter::Split_EventUniv,
|
||||||
c, c_);
|
c, c_);
|
||||||
s.res_EventUniv->
|
s.res_EventUniv->
|
||||||
push_back(unop_multop(op::F, op::And,
|
emplace_back(unop_multop(op::F, op::And,
|
||||||
std::move(*s.res_other)));
|
std::move(*s.res_other)));
|
||||||
s.res_EventUniv->
|
s.res_EventUniv->
|
||||||
push_back(unop_unop_multop(op::F, op::G, op::And,
|
emplace_back(unop_unop_multop(op::F, op::G, op::And,
|
||||||
std::move(*s.res_FG)));
|
std::move(*s.res_FG)));
|
||||||
formula res =
|
formula res =
|
||||||
formula::And(std::move(*s.res_EventUniv));
|
formula::And(std::move(*s.res_EventUniv));
|
||||||
|
|
@ -1059,10 +1059,10 @@ namespace spot
|
||||||
mospliter::Split_EventUniv,
|
mospliter::Split_EventUniv,
|
||||||
c, c_);
|
c, c_);
|
||||||
s.res_EventUniv->
|
s.res_EventUniv->
|
||||||
push_back(unop_multop(op::G, op::Or,
|
emplace_back(unop_multop(op::G, op::Or,
|
||||||
std::move(*s.res_other)));
|
std::move(*s.res_other)));
|
||||||
s.res_EventUniv->
|
s.res_EventUniv->
|
||||||
push_back(unop_unop_multop(op::G, op::F, op::Or,
|
emplace_back(unop_unop_multop(op::G, op::F, op::Or,
|
||||||
std::move(*s.res_GF)));
|
std::move(*s.res_GF)));
|
||||||
formula res =
|
formula res =
|
||||||
formula::Or(std::move(*s.res_EventUniv));
|
formula::Or(std::move(*s.res_EventUniv));
|
||||||
|
|
@ -1126,7 +1126,7 @@ namespace spot
|
||||||
mospliter s(mospliter::Split_EventUniv,
|
mospliter s(mospliter::Split_EventUniv,
|
||||||
c[0], c_);
|
c[0], c_);
|
||||||
s.res_EventUniv->
|
s.res_EventUniv->
|
||||||
push_back(unop_multop(op::F, op::And,
|
emplace_back(unop_multop(op::F, op::And,
|
||||||
std::move(*s.res_other)));
|
std::move(*s.res_other)));
|
||||||
formula res =
|
formula res =
|
||||||
formula::G(formula::And(std::move(*s.res_EventUniv)));
|
formula::G(formula::And(std::move(*s.res_EventUniv)));
|
||||||
|
|
@ -1158,7 +1158,7 @@ namespace spot
|
||||||
unsigned s = c.size();
|
unsigned s = c.size();
|
||||||
vec v;
|
vec v;
|
||||||
for (unsigned n = 0; n < s; ++n)
|
for (unsigned n = 0; n < s; ++n)
|
||||||
v.push_back(formula::unop(o, c[n]));
|
v.emplace_back(formula::unop(o, c[n]));
|
||||||
return recurse(formula::multop(o == op::Closure
|
return recurse(formula::multop(o == op::Closure
|
||||||
? op::Or : op::And, v));
|
? op::Or : op::And, v));
|
||||||
}
|
}
|
||||||
|
|
@ -1175,7 +1175,7 @@ namespace spot
|
||||||
unsigned end = c.size();
|
unsigned end = c.size();
|
||||||
v.reserve(end);
|
v.reserve(end);
|
||||||
for (unsigned i = 0; i < end; ++i)
|
for (unsigned i = 0; i < end; ++i)
|
||||||
v.push_back(formula::unop(o, c[i]));
|
v.emplace_back(formula::unop(o, c[i]));
|
||||||
return recurse(formula::multop(o == op::Closure ?
|
return recurse(formula::multop(o == op::Closure ?
|
||||||
op::Or : op::And, v));
|
op::Or : op::And, v));
|
||||||
}
|
}
|
||||||
|
|
@ -1209,7 +1209,7 @@ namespace spot
|
||||||
vec v;
|
vec v;
|
||||||
v.reserve(s);
|
v.reserve(s);
|
||||||
for (unsigned n = start; n <= end; ++n)
|
for (unsigned n = start; n <= end; ++n)
|
||||||
v.push_back(c[n]);
|
v.emplace_back(c[n]);
|
||||||
tail = formula::Concat(v);
|
tail = formula::Concat(v);
|
||||||
tail = formula::unop(o, tail);
|
tail = formula::unop(o, tail);
|
||||||
}
|
}
|
||||||
|
|
@ -1252,9 +1252,9 @@ namespace spot
|
||||||
unsigned ss = c.size();
|
unsigned ss = c.size();
|
||||||
vec v;
|
vec v;
|
||||||
v.reserve(ss);
|
v.reserve(ss);
|
||||||
v.push_back(formula::Star(sc, 0, max));
|
v.emplace_back(formula::Star(sc, 0, max));
|
||||||
for (unsigned n = 1; n < ss; ++n)
|
for (unsigned n = 1; n < ss; ++n)
|
||||||
v.push_back(c[n]);
|
v.emplace_back(c[n]);
|
||||||
formula tail = formula::Concat(v);
|
formula tail = formula::Concat(v);
|
||||||
tail = // {b[*0..j-i]} or !{b[*0..j-i]}
|
tail = // {b[*0..j-i]} or !{b[*0..j-i]}
|
||||||
formula::unop(o, tail);
|
formula::unop(o, tail);
|
||||||
|
|
@ -1545,7 +1545,7 @@ namespace spot
|
||||||
vec v;
|
vec v;
|
||||||
for (unsigned n = 0; n < s; ++n)
|
for (unsigned n = 0; n < s; ++n)
|
||||||
// {r₁}[]->b
|
// {r₁}[]->b
|
||||||
v.push_back(formula::binop(bindop, a[n], b));
|
v.emplace_back(formula::binop(bindop, a[n], b));
|
||||||
return recurse(formula::multop(op_and, v));
|
return recurse(formula::multop(op_and, v));
|
||||||
}
|
}
|
||||||
return orig;
|
return orig;
|
||||||
|
|
@ -1609,7 +1609,7 @@ namespace spot
|
||||||
formula b2 = formula::Or(std::move(*s.res_other));
|
formula b2 = formula::Or(std::move(*s.res_other));
|
||||||
if (b2 != b)
|
if (b2 != b)
|
||||||
{
|
{
|
||||||
s.res_Event->push_back(formula::binop(o, a, b2));
|
s.res_Event->emplace_back(formula::binop(o, a, b2));
|
||||||
return recurse
|
return recurse
|
||||||
(formula::Or(std::move(*s.res_Event)));
|
(formula::Or(std::move(*s.res_Event)));
|
||||||
}
|
}
|
||||||
|
|
@ -1621,7 +1621,7 @@ namespace spot
|
||||||
formula b2 = formula::And(std::move(*s.res_other));
|
formula b2 = formula::And(std::move(*s.res_other));
|
||||||
if (b2 != b)
|
if (b2 != b)
|
||||||
{
|
{
|
||||||
s.res_EventUniv->push_back(formula::binop(o,
|
s.res_EventUniv->emplace_back(formula::binop(o,
|
||||||
a, b2));
|
a, b2));
|
||||||
return recurse
|
return recurse
|
||||||
(formula::And(std::move(*s.res_EventUniv)));
|
(formula::And(std::move(*s.res_EventUniv)));
|
||||||
|
|
@ -1634,7 +1634,7 @@ namespace spot
|
||||||
formula a2 = formula::And(std::move(*s.res_other));
|
formula a2 = formula::And(std::move(*s.res_other));
|
||||||
if (a2 != a)
|
if (a2 != a)
|
||||||
{
|
{
|
||||||
s.res_EventUniv->push_back(formula::binop(o,
|
s.res_EventUniv->emplace_back(formula::binop(o,
|
||||||
a2, b));
|
a2, b));
|
||||||
return recurse
|
return recurse
|
||||||
(formula::And(std::move(*s.res_EventUniv)));
|
(formula::And(std::move(*s.res_EventUniv)));
|
||||||
|
|
@ -1647,7 +1647,7 @@ namespace spot
|
||||||
formula b2 = formula::And(std::move(*s.res_other));
|
formula b2 = formula::And(std::move(*s.res_other));
|
||||||
if (b2 != b)
|
if (b2 != b)
|
||||||
{
|
{
|
||||||
s.res_Univ->push_back(formula::binop(o, a, b2));
|
s.res_Univ->emplace_back(formula::binop(o, a, b2));
|
||||||
return recurse
|
return recurse
|
||||||
(formula::And(std::move(*s.res_Univ)));
|
(formula::And(std::move(*s.res_Univ)));
|
||||||
}
|
}
|
||||||
|
|
@ -1939,7 +1939,7 @@ namespace spot
|
||||||
vec res;
|
vec res;
|
||||||
res.reserve(mos);
|
res.reserve(mos);
|
||||||
for (auto f: mo)
|
for (auto f: mo)
|
||||||
res.push_back(f);
|
res.emplace_back(f);
|
||||||
op o = mo.kind();
|
op o = mo.kind();
|
||||||
|
|
||||||
// basics reduction do not concern Boolean formulas,
|
// basics reduction do not concern Boolean formulas,
|
||||||
|
|
@ -2093,12 +2093,12 @@ namespace spot
|
||||||
vec xgv;
|
vec xgv;
|
||||||
xgv.reserve(xgs);
|
xgv.reserve(xgs);
|
||||||
for (auto f: xgset)
|
for (auto f: xgset)
|
||||||
xgv.push_back(f);
|
xgv.emplace_back(f);
|
||||||
xv.emplace_back(unop_multop(op::G, op::And, xgv));
|
xv.emplace_back(unop_multop(op::G, op::And, xgv));
|
||||||
}
|
}
|
||||||
for (auto f: xset)
|
for (auto f: xset)
|
||||||
xv.emplace_back(f);
|
xv.emplace_back(f);
|
||||||
res.push_back(unop_multop(op::X, op::And, xv));
|
res.emplace_back(unop_multop(op::X, op::And, xv));
|
||||||
}
|
}
|
||||||
|
|
||||||
// Gather all operands by type.
|
// Gather all operands by type.
|
||||||
|
|
@ -2120,7 +2120,7 @@ namespace spot
|
||||||
// Xa & Xb & f1...fn = X(a & b & f1...fn)
|
// Xa & Xb & f1...fn = X(a & b & f1...fn)
|
||||||
if (!s.res_X->empty() && !opt_.favor_event_univ)
|
if (!s.res_X->empty() && !opt_.favor_event_univ)
|
||||||
{
|
{
|
||||||
s.res_X->push_back(allFG);
|
s.res_X->emplace_back(allFG);
|
||||||
allFG = nullptr;
|
allFG = nullptr;
|
||||||
s.res_X->insert(s.res_X->begin(),
|
s.res_X->insert(s.res_X->begin(),
|
||||||
s.res_EventUniv->begin(),
|
s.res_EventUniv->begin(),
|
||||||
|
|
@ -2143,23 +2143,23 @@ namespace spot
|
||||||
if (f.is(op::G))
|
if (f.is(op::G))
|
||||||
{
|
{
|
||||||
seen_g = true;
|
seen_g = true;
|
||||||
eu.push_back(f[0]);
|
eu.emplace_back(f[0]);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
eu.push_back(f);
|
eu.emplace_back(f);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
s.res_other->push_back(f);
|
s.res_other->emplace_back(f);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (seen_g)
|
if (seen_g)
|
||||||
{
|
{
|
||||||
eu.push_back(allFG);
|
eu.emplace_back(allFG);
|
||||||
allFG = nullptr;
|
allFG = nullptr;
|
||||||
s.res_other->push_back(unop_multop(op::G, op::And,
|
s.res_other->emplace_back(unop_multop(op::G, op::And,
|
||||||
eu));
|
eu));
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -2297,10 +2297,10 @@ namespace spot
|
||||||
for (auto& f: *s.res_G)
|
for (auto& f: *s.res_G)
|
||||||
if (f.is_eventual())
|
if (f.is_eventual())
|
||||||
{
|
{
|
||||||
event.push_back(f);
|
event.emplace_back(f);
|
||||||
f = nullptr; // Remove it from res_G.
|
f = nullptr; // Remove it from res_G.
|
||||||
}
|
}
|
||||||
s.res_X->push_back(unop_multop(op::G, op::And,
|
s.res_X->emplace_back(unop_multop(op::G, op::And,
|
||||||
std::move(event)));
|
std::move(event)));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -2310,9 +2310,9 @@ namespace spot
|
||||||
// Xa & Xb & ... = X(a & b & ...)
|
// Xa & Xb & ... = X(a & b & ...)
|
||||||
formula allX = unop_multop(op::X, op::And,
|
formula allX = unop_multop(op::X, op::And,
|
||||||
std::move(*s.res_X));
|
std::move(*s.res_X));
|
||||||
s.res_other->push_back(allX);
|
s.res_other->emplace_back(allX);
|
||||||
s.res_other->push_back(allG);
|
s.res_other->emplace_back(allG);
|
||||||
s.res_other->push_back(allFG);
|
s.res_other->emplace_back(allFG);
|
||||||
formula r = formula::And(std::move(*s.res_other));
|
formula r = formula::And(std::move(*s.res_other));
|
||||||
// If we altered the formula in some way, process
|
// If we altered the formula in some way, process
|
||||||
// it another time.
|
// it another time.
|
||||||
|
|
@ -2337,13 +2337,13 @@ namespace spot
|
||||||
// = 0 otherwise
|
// = 0 otherwise
|
||||||
if (f.min() > 1 || f.max() < 1)
|
if (f.min() > 1 || f.max() < 1)
|
||||||
return formula::ff();
|
return formula::ff();
|
||||||
ares.push_back(f[0]);
|
ares.emplace_back(f[0]);
|
||||||
f = nullptr;
|
f = nullptr;
|
||||||
break;
|
break;
|
||||||
case op::Fusion:
|
case op::Fusion:
|
||||||
// b && {r1:..:rn} = b && r1 && .. && rn
|
// b && {r1:..:rn} = b && r1 && .. && rn
|
||||||
for (auto ri: f)
|
for (auto ri: f)
|
||||||
ares.push_back(ri);
|
ares.emplace_back(ri);
|
||||||
f = nullptr;
|
f = nullptr;
|
||||||
break;
|
break;
|
||||||
case op::Concat:
|
case op::Concat:
|
||||||
|
|
@ -2368,13 +2368,13 @@ namespace spot
|
||||||
}
|
}
|
||||||
if (nonempty == 1)
|
if (nonempty == 1)
|
||||||
{
|
{
|
||||||
ares.push_back(ri);
|
ares.emplace_back(ri);
|
||||||
}
|
}
|
||||||
else if (nonempty == 0)
|
else if (nonempty == 0)
|
||||||
{
|
{
|
||||||
vec sum;
|
vec sum;
|
||||||
for (auto j: f)
|
for (auto j: f)
|
||||||
sum.push_back(j);
|
sum.emplace_back(j);
|
||||||
ares.emplace_back(formula::OrRat(sum));
|
ares.emplace_back(formula::OrRat(sum));
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -2385,11 +2385,11 @@ namespace spot
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
default:
|
default:
|
||||||
ares.push_back(f);
|
ares.emplace_back(f);
|
||||||
f = nullptr;
|
f = nullptr;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
ares.push_back(b);
|
ares.emplace_back(b);
|
||||||
auto r = formula::AndRat(std::move(ares));
|
auto r = formula::AndRat(std::move(ares));
|
||||||
// If we altered the formula in some way, process
|
// If we altered the formula in some way, process
|
||||||
// it another time.
|
// it another time.
|
||||||
|
|
@ -2419,13 +2419,13 @@ namespace spot
|
||||||
continue;
|
continue;
|
||||||
if (i.is(op::Concat))
|
if (i.is(op::Concat))
|
||||||
{
|
{
|
||||||
head1.push_back(h);
|
head1.emplace_back(h);
|
||||||
tail1.push_back(i.all_but(0));
|
tail1.emplace_back(i.all_but(0));
|
||||||
}
|
}
|
||||||
else // op::Fusion
|
else // op::Fusion
|
||||||
{
|
{
|
||||||
head2.push_back(h);
|
head2.emplace_back(h);
|
||||||
tail2.push_back(i.all_but(0));
|
tail2.emplace_back(i.all_but(0));
|
||||||
}
|
}
|
||||||
i = nullptr;
|
i = nullptr;
|
||||||
}
|
}
|
||||||
|
|
@ -2433,13 +2433,13 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula h = formula::And(std::move(head1));
|
formula h = formula::And(std::move(head1));
|
||||||
formula t = formula::AndRat(std::move(tail1));
|
formula t = formula::AndRat(std::move(tail1));
|
||||||
s.res_other->push_back(formula::Concat({h, t}));
|
s.res_other->emplace_back(formula::Concat({h, t}));
|
||||||
}
|
}
|
||||||
if (!head2.empty())
|
if (!head2.empty())
|
||||||
{
|
{
|
||||||
formula h = formula::And(std::move(head2));
|
formula h = formula::And(std::move(head2));
|
||||||
formula t = formula::AndRat(std::move(tail2));
|
formula t = formula::AndRat(std::move(tail2));
|
||||||
s.res_other->push_back(formula::Fusion({h, t}));
|
s.res_other->emplace_back(formula::Fusion({h, t}));
|
||||||
}
|
}
|
||||||
|
|
||||||
// {r1;b1}&&{r2;b2} = {r1&&r2};{b1∧b2}
|
// {r1;b1}&&{r2;b2} = {r1&&r2};{b1∧b2}
|
||||||
|
|
@ -2462,13 +2462,13 @@ namespace spot
|
||||||
continue;
|
continue;
|
||||||
if (i.is(op::Concat))
|
if (i.is(op::Concat))
|
||||||
{
|
{
|
||||||
tail3.push_back(t);
|
tail3.emplace_back(t);
|
||||||
head3.push_back(i.all_but(s));
|
head3.emplace_back(i.all_but(s));
|
||||||
}
|
}
|
||||||
else // op::Fusion
|
else // op::Fusion
|
||||||
{
|
{
|
||||||
tail4.push_back(t);
|
tail4.emplace_back(t);
|
||||||
head4.push_back(i.all_but(s));
|
head4.emplace_back(i.all_but(s));
|
||||||
}
|
}
|
||||||
i = nullptr;
|
i = nullptr;
|
||||||
}
|
}
|
||||||
|
|
@ -2476,13 +2476,13 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula h = formula::AndRat(std::move(head3));
|
formula h = formula::AndRat(std::move(head3));
|
||||||
formula t = formula::And(std::move(tail3));
|
formula t = formula::And(std::move(tail3));
|
||||||
s.res_other->push_back(formula::Concat({h, t}));
|
s.res_other->emplace_back(formula::Concat({h, t}));
|
||||||
}
|
}
|
||||||
if (!head4.empty())
|
if (!head4.empty())
|
||||||
{
|
{
|
||||||
formula h = formula::AndRat(std::move(head4));
|
formula h = formula::AndRat(std::move(head4));
|
||||||
formula t = formula::And(std::move(tail4));
|
formula t = formula::And(std::move(tail4));
|
||||||
s.res_other->push_back(formula::Fusion({h, t}));
|
s.res_other->emplace_back(formula::Fusion({h, t}));
|
||||||
}
|
}
|
||||||
|
|
||||||
auto r = formula::AndRat(std::move(*s.res_other));
|
auto r = formula::AndRat(std::move(*s.res_other));
|
||||||
|
|
@ -2651,13 +2651,13 @@ namespace spot
|
||||||
vec xfv;
|
vec xfv;
|
||||||
xfv.reserve(xfs);
|
xfv.reserve(xfs);
|
||||||
for (auto f: xfset)
|
for (auto f: xfset)
|
||||||
xfv.push_back(f);
|
xfv.emplace_back(f);
|
||||||
xv.push_back(unop_multop(op::F, op::Or, xfv));
|
xv.emplace_back(unop_multop(op::F, op::Or, xfv));
|
||||||
}
|
}
|
||||||
// Also gather the remaining Xa | X(b|c) as X(b|c).
|
// Also gather the remaining Xa | X(b|c) as X(b|c).
|
||||||
for (auto f: xset)
|
for (auto f: xset)
|
||||||
xv.push_back(f);
|
xv.emplace_back(f);
|
||||||
res.push_back(unop_multop(op::X, op::Or, xv));
|
res.emplace_back(unop_multop(op::X, op::Or, xv));
|
||||||
}
|
}
|
||||||
|
|
||||||
// Gather all operand by type.
|
// Gather all operand by type.
|
||||||
|
|
@ -2679,7 +2679,7 @@ namespace spot
|
||||||
// Xa | Xb | f1...fn = X(a | b | f1...fn)
|
// Xa | Xb | f1...fn = X(a | b | f1...fn)
|
||||||
if (!s.res_X->empty() && !opt_.favor_event_univ)
|
if (!s.res_X->empty() && !opt_.favor_event_univ)
|
||||||
{
|
{
|
||||||
s.res_X->push_back(allGF);
|
s.res_X->emplace_back(allGF);
|
||||||
allGF = nullptr;
|
allGF = nullptr;
|
||||||
s.res_X->insert(s.res_X->end(),
|
s.res_X->insert(s.res_X->end(),
|
||||||
s.res_EventUniv->begin(),
|
s.res_EventUniv->begin(),
|
||||||
|
|
@ -2713,7 +2713,7 @@ namespace spot
|
||||||
// (counting the number of "subtransitions"
|
// (counting the number of "subtransitions"
|
||||||
// or, degeneralizing the automaton amplifies
|
// or, degeneralizing the automaton amplifies
|
||||||
// these differences)
|
// these differences)
|
||||||
s.res_F->push_back(allGF);
|
s.res_F->emplace_back(allGF);
|
||||||
allGF = nullptr;
|
allGF = nullptr;
|
||||||
s.res_F->insert(s.res_F->end(),
|
s.res_F->insert(s.res_F->end(),
|
||||||
s.res_EventUniv->begin(),
|
s.res_EventUniv->begin(),
|
||||||
|
|
@ -2721,7 +2721,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
else if (opt_.favor_event_univ)
|
else if (opt_.favor_event_univ)
|
||||||
{
|
{
|
||||||
s.res_EventUniv->push_back(allGF);
|
s.res_EventUniv->emplace_back(allGF);
|
||||||
allGF = nullptr;
|
allGF = nullptr;
|
||||||
bool seen_f = false;
|
bool seen_f = false;
|
||||||
if (s.res_EventUniv->size() > 1)
|
if (s.res_EventUniv->size() > 1)
|
||||||
|
|
@ -2740,7 +2740,7 @@ namespace spot
|
||||||
formula eu =
|
formula eu =
|
||||||
unop_multop(op::F, op::Or,
|
unop_multop(op::F, op::Or,
|
||||||
std::move(*s.res_EventUniv));
|
std::move(*s.res_EventUniv));
|
||||||
s.res_other->push_back(eu);
|
s.res_other->emplace_back(eu);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (!seen_f)
|
if (!seen_f)
|
||||||
|
|
@ -2882,10 +2882,10 @@ namespace spot
|
||||||
for (auto& f: *s.res_F)
|
for (auto& f: *s.res_F)
|
||||||
if (f.is_universal())
|
if (f.is_universal())
|
||||||
{
|
{
|
||||||
univ.push_back(f);
|
univ.emplace_back(f);
|
||||||
f = nullptr; // Remove it from res_F.
|
f = nullptr; // Remove it from res_F.
|
||||||
}
|
}
|
||||||
s.res_X->push_back(unop_multop(op::F, op::Or,
|
s.res_X->emplace_back(unop_multop(op::F, op::Or,
|
||||||
std::move(univ)));
|
std::move(univ)));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -2895,9 +2895,9 @@ namespace spot
|
||||||
// Xa | Xb | ... = X(a | b | ...)
|
// Xa | Xb | ... = X(a | b | ...)
|
||||||
formula allX = unop_multop(op::X, op::Or,
|
formula allX = unop_multop(op::X, op::Or,
|
||||||
std::move(*s.res_X));
|
std::move(*s.res_X));
|
||||||
s.res_other->push_back(allX);
|
s.res_other->emplace_back(allX);
|
||||||
s.res_other->push_back(allF);
|
s.res_other->emplace_back(allF);
|
||||||
s.res_other->push_back(allGF);
|
s.res_other->emplace_back(allGF);
|
||||||
formula r = formula::Or(std::move(*s.res_other));
|
formula r = formula::Or(std::move(*s.res_other));
|
||||||
// If we altered the formula in some way, process
|
// If we altered the formula in some way, process
|
||||||
// it another time.
|
// it another time.
|
||||||
|
|
@ -2961,16 +2961,16 @@ namespace spot
|
||||||
continue;
|
continue;
|
||||||
if (i.is(op::Concat))
|
if (i.is(op::Concat))
|
||||||
{
|
{
|
||||||
head1.push_back(h);
|
head1.emplace_back(h);
|
||||||
tail1.push_back(i.all_but(0));
|
tail1.emplace_back(i.all_but(0));
|
||||||
}
|
}
|
||||||
else // op::Fusion
|
else // op::Fusion
|
||||||
{
|
{
|
||||||
formula t = i.all_but(0);
|
formula t = i.all_but(0);
|
||||||
if (t.accepts_eword())
|
if (t.accepts_eword())
|
||||||
continue;
|
continue;
|
||||||
head2.push_back(h);
|
head2.emplace_back(h);
|
||||||
tail2.push_back(t);
|
tail2.emplace_back(t);
|
||||||
}
|
}
|
||||||
i = nullptr;
|
i = nullptr;
|
||||||
}
|
}
|
||||||
|
|
@ -2978,13 +2978,13 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula h = formula::And(std::move(head1));
|
formula h = formula::And(std::move(head1));
|
||||||
formula t = formula::AndNLM(std::move(tail1));
|
formula t = formula::AndNLM(std::move(tail1));
|
||||||
s.res_other->push_back(formula::Concat({h, t}));
|
s.res_other->emplace_back(formula::Concat({h, t}));
|
||||||
}
|
}
|
||||||
if (!head2.empty())
|
if (!head2.empty())
|
||||||
{
|
{
|
||||||
formula h = formula::And(std::move(head2));
|
formula h = formula::And(std::move(head2));
|
||||||
formula t = formula::AndNLM(std::move(tail2));
|
formula t = formula::AndNLM(std::move(tail2));
|
||||||
s.res_other->push_back(formula::Fusion({h, t}));
|
s.res_other->emplace_back(formula::Fusion({h, t}));
|
||||||
}
|
}
|
||||||
|
|
||||||
formula r = formula::AndNLM(std::move(*s.res_other));
|
formula r = formula::AndNLM(std::move(*s.res_other));
|
||||||
|
|
|
||||||
|
|
@ -519,7 +519,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
for (auto i: p)
|
for (auto i: p)
|
||||||
pairs.push_back(i.second);
|
pairs.emplace_back(i.second);
|
||||||
return (!(seen_fin & seen_inf)
|
return (!(seen_fin & seen_inf)
|
||||||
&& (seen_fin | seen_inf) == all_sets());
|
&& (seen_fin | seen_inf) == all_sets());
|
||||||
}
|
}
|
||||||
|
|
@ -568,7 +568,7 @@ namespace spot
|
||||||
codes.reserve(n_accs);
|
codes.reserve(n_accs);
|
||||||
for (unsigned i = 0; i < n_accs; ++i)
|
for (unsigned i = 0; i < n_accs; ++i)
|
||||||
{
|
{
|
||||||
codes.push_back(drand() < 0.5 ? inf({i}) : fin({i}));
|
codes.emplace_back(drand() < 0.5 ? inf({i}) : fin({i}));
|
||||||
if (reuse > 0.0 && drand() < reuse)
|
if (reuse > 0.0 && drand() < reuse)
|
||||||
--i;
|
--i;
|
||||||
}
|
}
|
||||||
|
|
@ -664,9 +664,9 @@ namespace spot
|
||||||
std::vector<bdd> r;
|
std::vector<bdd> r;
|
||||||
for (unsigned i = 0; r.size() < umax; ++i)
|
for (unsigned i = 0; r.size() < umax; ++i)
|
||||||
if (used.has(i))
|
if (used.has(i))
|
||||||
r.push_back(bdd_ithvar(base++));
|
r.emplace_back(bdd_ithvar(base++));
|
||||||
else
|
else
|
||||||
r.push_back(bddfalse);
|
r.emplace_back(bddfalse);
|
||||||
return to_bdd_rec(&lhs.back(), &r[0]) == to_bdd_rec(&rhs.back(), &r[0]);
|
return to_bdd_rec(&lhs.back(), &r[0]) == to_bdd_rec(&rhs.back(), &r[0]);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -740,11 +740,11 @@ namespace spot
|
||||||
if (used.has(i))
|
if (used.has(i))
|
||||||
{
|
{
|
||||||
sets[base] = i;
|
sets[base] = i;
|
||||||
r.push_back(bdd_ithvar(base++));
|
r.emplace_back(bdd_ithvar(base++));
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
r.push_back(bddfalse);
|
r.emplace_back(bddfalse);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -812,11 +812,11 @@ namespace spot
|
||||||
if (used.has(i))
|
if (used.has(i))
|
||||||
{
|
{
|
||||||
sets[base] = i;
|
sets[base] = i;
|
||||||
r.push_back(bdd_ithvar(base++));
|
r.emplace_back(bdd_ithvar(base++));
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
r.push_back(bddfalse);
|
r.emplace_back(bddfalse);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -886,11 +886,11 @@ namespace spot
|
||||||
if (used.has(i))
|
if (used.has(i))
|
||||||
{
|
{
|
||||||
sets[base] = i;
|
sets[base] = i;
|
||||||
r.push_back(bdd_ithvar(base++));
|
r.emplace_back(bdd_ithvar(base++));
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
r.push_back(bddfalse);
|
r.emplace_back(bddfalse);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -950,13 +950,13 @@ namespace spot
|
||||||
{
|
{
|
||||||
sets[base] = i;
|
sets[base] = i;
|
||||||
bdd v = bdd_ithvar(base++);
|
bdd v = bdd_ithvar(base++);
|
||||||
r.push_back(v);
|
r.emplace_back(v);
|
||||||
if (inf.has(i))
|
if (inf.has(i))
|
||||||
known &= v;
|
known &= v;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
r.push_back(bddfalse);
|
r.emplace_back(bddfalse);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -984,12 +984,12 @@ namespace spot
|
||||||
bdd h = bdd_high(cube);
|
bdd h = bdd_high(cube);
|
||||||
if (h == bddfalse) // Negative variable
|
if (h == bddfalse) // Negative variable
|
||||||
{
|
{
|
||||||
partial.push_back(s);
|
partial.emplace_back(s);
|
||||||
cube = bdd_low(cube);
|
cube = bdd_low(cube);
|
||||||
}
|
}
|
||||||
else // Positive variable
|
else // Positive variable
|
||||||
{
|
{
|
||||||
partial.push_back(-s - 1);
|
partial.emplace_back(-s - 1);
|
||||||
cube = h;
|
cube = h;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -1579,7 +1579,7 @@ namespace spot
|
||||||
v.reserve(num);
|
v.reserve(num);
|
||||||
while (num > 0)
|
while (num > 0)
|
||||||
{
|
{
|
||||||
v.push_back(parse_range(input));
|
v.emplace_back(parse_range(input));
|
||||||
--num;
|
--num;
|
||||||
}
|
}
|
||||||
c = acc_cond::acc_code::generalized_rabin(v.begin(), v.end());
|
c = acc_cond::acc_code::generalized_rabin(v.begin(), v.end());
|
||||||
|
|
|
||||||
|
|
@ -647,7 +647,7 @@ namespace spot
|
||||||
acc_word w;
|
acc_word w;
|
||||||
w.op = acc_op::And;
|
w.op = acc_op::And;
|
||||||
w.size = size();
|
w.size = size();
|
||||||
push_back(w);
|
emplace_back(w);
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -738,7 +738,7 @@ namespace spot
|
||||||
acc_word w;
|
acc_word w;
|
||||||
w.op = acc_op::And;
|
w.op = acc_op::And;
|
||||||
w.size = size();
|
w.size = size();
|
||||||
push_back(w);
|
emplace_back(w);
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -782,7 +782,7 @@ namespace spot
|
||||||
acc_word w;
|
acc_word w;
|
||||||
w.op = acc_op::Or;
|
w.op = acc_op::Or;
|
||||||
w.size = size();
|
w.size = size();
|
||||||
push_back(w);
|
emplace_back(w);
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -55,7 +55,7 @@ namespace spot
|
||||||
b = high;
|
b = high;
|
||||||
}
|
}
|
||||||
assert(b != bddfalse);
|
assert(b != bddfalse);
|
||||||
v.push_back(res);
|
v.emplace_back(res);
|
||||||
}
|
}
|
||||||
return formula::And(v);
|
return formula::And(v);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -135,7 +135,7 @@ namespace spot
|
||||||
t->condition = bddtrue;
|
t->condition = bddtrue;
|
||||||
t->acceptance_conditions = 0U;
|
t->acceptance_conditions = 0U;
|
||||||
t->dst = new taa_tgba::state_set;
|
t->dst = new taa_tgba::state_set;
|
||||||
succ_.push_back(t);
|
succ_.emplace_back(t);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -150,7 +150,7 @@ namespace spot
|
||||||
std::vector<iterator> pos;
|
std::vector<iterator> pos;
|
||||||
pos.reserve(bounds.size());
|
pos.reserve(bounds.size());
|
||||||
for (auto i: bounds)
|
for (auto i: bounds)
|
||||||
pos.push_back(i.first);
|
pos.emplace_back(i.first);
|
||||||
|
|
||||||
while (pos[0] != bounds[0].second)
|
while (pos[0] != bounds[0].second)
|
||||||
{
|
{
|
||||||
|
|
@ -207,10 +207,10 @@ namespace spot
|
||||||
if (t->condition != bddfalse
|
if (t->condition != bddfalse
|
||||||
&& (i == seen_.end() || j == i->second.end()))
|
&& (i == seen_.end() || j == i->second.end()))
|
||||||
{
|
{
|
||||||
seen_[b].push_back(t);
|
seen_[b].emplace_back(t);
|
||||||
if (i != seen_.end())
|
if (i != seen_.end())
|
||||||
delete b;
|
delete b;
|
||||||
succ_.push_back(t);
|
succ_.emplace_back(t);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -178,7 +178,7 @@ namespace spot
|
||||||
t->dst = dst;
|
t->dst = dst;
|
||||||
t->condition = bddtrue;
|
t->condition = bddtrue;
|
||||||
t->acceptance_conditions = 0U;
|
t->acceptance_conditions = 0U;
|
||||||
src->push_back(t);
|
src->emplace_back(t);
|
||||||
return t;
|
return t;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -186,7 +186,7 @@ namespace spot
|
||||||
create_transition(const label& s, const label& d)
|
create_transition(const label& s, const label& d)
|
||||||
{
|
{
|
||||||
std::vector<std::string> vec;
|
std::vector<std::string> vec;
|
||||||
vec.push_back(d);
|
vec.emplace_back(d);
|
||||||
return create_transition(s, vec);
|
return create_transition(s, vec);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -266,7 +266,7 @@ namespace spot
|
||||||
state_set* ss = new state_set;
|
state_set* ss = new state_set;
|
||||||
for (unsigned i = 0; i < names.size(); ++i)
|
for (unsigned i = 0; i < names.size(); ++i)
|
||||||
ss->insert(add_state(names[i]));
|
ss->insert(add_state(names[i]));
|
||||||
state_set_vec_.push_back(ss);
|
state_set_vec_.emplace_back(ss);
|
||||||
return ss;
|
return ss;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -728,7 +728,7 @@ namespace spot
|
||||||
int res = dict_->has_registered_proposition(ap, this);
|
int res = dict_->has_registered_proposition(ap, this);
|
||||||
if (res < 0)
|
if (res < 0)
|
||||||
{
|
{
|
||||||
aps_.push_back(ap);
|
aps_.emplace_back(ap);
|
||||||
res = dict_->register_proposition(ap, this);
|
res = dict_->register_proposition(ap, this);
|
||||||
bddaps_ &= bdd_ithvar(res);
|
bddaps_ &= bdd_ithvar(res);
|
||||||
}
|
}
|
||||||
|
|
@ -768,7 +768,7 @@ namespace spot
|
||||||
for (unsigned n = 0; n < s; ++n)
|
for (unsigned n = 0; n < s; ++n)
|
||||||
if (m[n].refs.find(this) != m[n].refs.end())
|
if (m[n].refs.find(this) != m[n].refs.end())
|
||||||
{
|
{
|
||||||
aps_.push_back(m[n].f);
|
aps_.emplace_back(m[n].f);
|
||||||
bddaps_ &= bdd_ithvar(n);
|
bddaps_ &= bdd_ithvar(n);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -216,7 +216,7 @@ namespace spot
|
||||||
if (tid == 0U)
|
if (tid == 0U)
|
||||||
{
|
{
|
||||||
todo.pop_back();
|
todo.pop_back();
|
||||||
order.push_back(src);
|
order.emplace_back(src);
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
auto& t = g_.edge_storage(tid);
|
auto& t = g_.edge_storage(tid);
|
||||||
|
|
|
||||||
|
|
@ -69,7 +69,7 @@ namespace spot
|
||||||
// BFS queue.
|
// BFS queue.
|
||||||
std::deque<const state*> todo;
|
std::deque<const state*> todo;
|
||||||
// Initial state.
|
// Initial state.
|
||||||
todo.push_back(start);
|
todo.emplace_back(start);
|
||||||
|
|
||||||
while (!todo.empty())
|
while (!todo.empty())
|
||||||
{
|
{
|
||||||
|
|
@ -97,7 +97,7 @@ namespace spot
|
||||||
// for unvisited states.
|
// for unvisited states.
|
||||||
if (father.find(dest) == father.end())
|
if (father.find(dest) == father.end())
|
||||||
{
|
{
|
||||||
todo.push_back(dest);
|
todo.emplace_back(dest);
|
||||||
father[dest] = s;
|
father[dest] = s;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -61,7 +61,7 @@ namespace
|
||||||
std::sort(signature[s].ingoing.begin(), signature[s].ingoing.end());
|
std::sort(signature[s].ingoing.begin(), signature[s].ingoing.end());
|
||||||
std::sort(signature[s].outgoing.begin(), signature[s].outgoing.end());
|
std::sort(signature[s].outgoing.begin(), signature[s].outgoing.end());
|
||||||
signature[s].classnum = state2class[s];
|
signature[s].classnum = state2class[s];
|
||||||
sig2states[signature[s]].push_back(s);
|
sig2states[signature[s]].emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
return sig2states;
|
return sig2states;
|
||||||
|
|
|
||||||
|
|
@ -66,17 +66,17 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula c = f[i];
|
formula c = f[i];
|
||||||
if (c.is_boolean())
|
if (c.is_boolean())
|
||||||
res.push_back(c);
|
res.emplace_back(c);
|
||||||
else if (oblig_ && c.is_syntactic_obligation())
|
else if (oblig_ && c.is_syntactic_obligation())
|
||||||
oblig.push_back(c);
|
oblig.emplace_back(c);
|
||||||
else if (c.is_eventual() && c.is_universal())
|
else if (c.is_eventual() && c.is_universal())
|
||||||
susp.push_back(c);
|
susp.emplace_back(c);
|
||||||
else
|
else
|
||||||
res.push_back(recurse(c));
|
res.emplace_back(recurse(c));
|
||||||
}
|
}
|
||||||
if (!oblig.empty())
|
if (!oblig.empty())
|
||||||
{
|
{
|
||||||
res.push_back(recurse(formula::multop(o, oblig)));
|
res.emplace_back(recurse(formula::multop(o, oblig)));
|
||||||
}
|
}
|
||||||
if (!susp.empty())
|
if (!susp.empty())
|
||||||
{
|
{
|
||||||
|
|
@ -85,7 +85,7 @@ namespace spot
|
||||||
formula g = recurse(x);
|
formula g = recurse(x);
|
||||||
if (o == op::And)
|
if (o == op::And)
|
||||||
{
|
{
|
||||||
res.push_back(g);
|
res.emplace_back(g);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -191,7 +191,7 @@ namespace spot
|
||||||
p.second = ris;
|
p.second = ris;
|
||||||
unsigned i = res->new_state();
|
unsigned i = res->new_state();
|
||||||
seen[p] = i;
|
seen[p] = i;
|
||||||
todo.push_back(p);
|
todo.emplace_back(p);
|
||||||
res->set_init_state(i);
|
res->set_init_state(i);
|
||||||
|
|
||||||
while (!todo.empty())
|
while (!todo.empty())
|
||||||
|
|
@ -252,7 +252,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
dest = res->new_state();
|
dest = res->new_state();
|
||||||
seen[d] = dest;
|
seen[d] = dest;
|
||||||
todo.push_back(d);
|
todo.emplace_back(d);
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_cond::mark_t a = li->acc() | (racc << lsets);
|
acc_cond::mark_t a = li->acc() | (racc << lsets);
|
||||||
|
|
|
||||||
|
|
@ -77,9 +77,9 @@ namespace spot
|
||||||
if (p.second)
|
if (p.second)
|
||||||
{
|
{
|
||||||
p.first->second = out->new_state();
|
p.first->second = out->new_state();
|
||||||
todo.push_back(p.first);
|
todo.emplace_back(p.first);
|
||||||
if (names)
|
if (names)
|
||||||
names->push_back(aut->format_state(s));
|
names->emplace_back(aut->format_state(s));
|
||||||
if (ohstates)
|
if (ohstates)
|
||||||
{
|
{
|
||||||
auto q = ohstates->find(aut_g->state_number(s));
|
auto q = ohstates->find(aut_g->state_number(s));
|
||||||
|
|
|
||||||
|
|
@ -33,7 +33,7 @@ namespace spot
|
||||||
enumerate_cycles::nocycle(unsigned x, unsigned y)
|
enumerate_cycles::nocycle(unsigned x, unsigned y)
|
||||||
{
|
{
|
||||||
// insert x in B(y)
|
// insert x in B(y)
|
||||||
info_[y].b.push_back(x);
|
info_[y].b.emplace_back(x);
|
||||||
// remove y from A(x)
|
// remove y from A(x)
|
||||||
info_[x].del[y] = true;
|
info_[x].del[y] = true;
|
||||||
}
|
}
|
||||||
|
|
@ -42,7 +42,7 @@ namespace spot
|
||||||
enumerate_cycles::unmark(unsigned y)
|
enumerate_cycles::unmark(unsigned y)
|
||||||
{
|
{
|
||||||
std::vector<unsigned> q;
|
std::vector<unsigned> q;
|
||||||
q.push_back(y);
|
q.emplace_back(y);
|
||||||
|
|
||||||
while (!q.empty())
|
while (!q.empty())
|
||||||
{
|
{
|
||||||
|
|
@ -57,7 +57,7 @@ namespace spot
|
||||||
info_[x].del[y] = false;
|
info_[x].del[y] = false;
|
||||||
// unmark x recursively if marked
|
// unmark x recursively if marked
|
||||||
if (info_[x].mark)
|
if (info_[x].mark)
|
||||||
q.push_back(x);
|
q.emplace_back(x);
|
||||||
}
|
}
|
||||||
// empty B(y)
|
// empty B(y)
|
||||||
info_[y].b.clear();
|
info_[y].b.clear();
|
||||||
|
|
|
||||||
|
|
@ -220,7 +220,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
// FIXME: revisit this comment once everything compiles again.
|
// FIXME: revisit this comment once everything compiles again.
|
||||||
//
|
//
|
||||||
// The order is arbitrary, but it turns out that using push_back
|
// The order is arbitrary, but it turns out that using emplace_back
|
||||||
// instead of push_front often gives better results because
|
// instead of push_front often gives better results because
|
||||||
// acceptance sets at the beginning if the cycle are more often
|
// acceptance sets at the beginning if the cycle are more often
|
||||||
// used in the automaton. (This surprising fact is probably
|
// used in the automaton. (This surprising fact is probably
|
||||||
|
|
@ -228,7 +228,7 @@ namespace spot
|
||||||
// during the translation.)
|
// during the translation.)
|
||||||
unsigned n = a->num_sets();
|
unsigned n = a->num_sets();
|
||||||
for (unsigned i = n; i > 0; --i)
|
for (unsigned i = n; i > 0; --i)
|
||||||
order.push_back(i - 1);
|
order.emplace_back(i - 1);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Initialize scc_orders
|
// Initialize scc_orders
|
||||||
|
|
@ -289,7 +289,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
ds2num[s] = res->new_state();
|
ds2num[s] = res->new_state();
|
||||||
todo.push_back(s);
|
todo.emplace_back(s);
|
||||||
|
|
||||||
// If use_lvl_cache is on insert initial state to level cache
|
// If use_lvl_cache is on insert initial state to level cache
|
||||||
// Level cache stores first encountered level for each state.
|
// Level cache stores first encountered level for each state.
|
||||||
|
|
@ -507,7 +507,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
dest = res->new_state();
|
dest = res->new_state();
|
||||||
ds2num[d] = dest;
|
ds2num[d] = dest;
|
||||||
todo.push_back(d);
|
todo.emplace_back(d);
|
||||||
// Insert new state to cache
|
// Insert new state to cache
|
||||||
|
|
||||||
if (use_lvl_cache)
|
if (use_lvl_cache)
|
||||||
|
|
|
||||||
|
|
@ -315,11 +315,11 @@ namespace spot
|
||||||
assert(pair.second);
|
assert(pair.second);
|
||||||
ss = ss.compute_succ(aut, ap, scc, implications, is_connected,
|
ss = ss.compute_succ(aut, ap, scc, implications, is_connected,
|
||||||
use_scc, use_simulation);
|
use_scc, use_simulation);
|
||||||
colors.push_back(ss.color_);
|
colors.emplace_back(ss.color_);
|
||||||
stop = safra2id.find(ss) != safra2id.end();
|
stop = safra2id.find(ss) != safra2id.end();
|
||||||
}
|
}
|
||||||
// Add color of final transition that loops back
|
// Add color of final transition that loops back
|
||||||
colors.push_back(ss.color_);
|
colors.emplace_back(ss.color_);
|
||||||
unsigned int loop_start = safra2id[ss];
|
unsigned int loop_start = safra2id[ss];
|
||||||
for (auto& min: safra2id)
|
for (auto& min: safra2id)
|
||||||
{
|
{
|
||||||
|
|
@ -352,7 +352,7 @@ namespace spot
|
||||||
scc.scc_of(n1.first);
|
scc.scc_of(n1.first);
|
||||||
if (!is_connected[idx] && bdd_implies(implications.at(n1.first),
|
if (!is_connected[idx] && bdd_implies(implications.at(n1.first),
|
||||||
implications.at(n2.first)))
|
implications.at(n2.first)))
|
||||||
to_remove.push_back(n1.first);
|
to_remove.emplace_back(n1.first);
|
||||||
}
|
}
|
||||||
for (auto& n: to_remove)
|
for (auto& n: to_remove)
|
||||||
{
|
{
|
||||||
|
|
@ -515,7 +515,7 @@ namespace spot
|
||||||
nodes_.emplace(state_num, std::move(braces));
|
nodes_.emplace(state_num, std::move(braces));
|
||||||
// First brace has init_state hence one state inside the first
|
// First brace has init_state hence one state inside the first
|
||||||
// braces.
|
// braces.
|
||||||
nb_braces_.push_back(1);
|
nb_braces_.emplace_back(1);
|
||||||
// One brace set
|
// One brace set
|
||||||
is_green_.push_back(true);
|
is_green_.push_back(true);
|
||||||
}
|
}
|
||||||
|
|
@ -625,7 +625,7 @@ namespace spot
|
||||||
all -= one;
|
all -= one;
|
||||||
auto p = bdd2num.emplace(one, num2bdd.size());
|
auto p = bdd2num.emplace(one, num2bdd.size());
|
||||||
if (p.second)
|
if (p.second)
|
||||||
num2bdd.push_back(one);
|
num2bdd.emplace_back(one);
|
||||||
bddnums.emplace_back(p.first->second);
|
bddnums.emplace_back(p.first->second);
|
||||||
}
|
}
|
||||||
deltas[t.cond] = std::make_pair(prev, bddnums.size());
|
deltas[t.cond] = std::make_pair(prev, bddnums.size());
|
||||||
|
|
@ -652,7 +652,7 @@ namespace spot
|
||||||
res->set_init_state(num);
|
res->set_init_state(num);
|
||||||
seen.insert(std::make_pair(init, num));
|
seen.insert(std::make_pair(init, num));
|
||||||
std::deque<safra_state> todo;
|
std::deque<safra_state> todo;
|
||||||
todo.push_back(init);
|
todo.emplace_back(init);
|
||||||
unsigned sets = 0;
|
unsigned sets = 0;
|
||||||
using succs_t = safra_state::succs_t;
|
using succs_t = safra_state::succs_t;
|
||||||
succs_t succs;
|
succs_t succs;
|
||||||
|
|
@ -678,7 +678,7 @@ namespace spot
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
dst_num = res->new_state();
|
dst_num = res->new_state();
|
||||||
todo.push_back(s.first);
|
todo.emplace_back(s.first);
|
||||||
seen.insert(std::make_pair(s.first, dst_num));
|
seen.insert(std::make_pair(s.first, dst_num));
|
||||||
}
|
}
|
||||||
if (s.first.color_ != -1U)
|
if (s.first.color_ != -1U)
|
||||||
|
|
|
||||||
|
|
@ -444,27 +444,27 @@ namespace spot
|
||||||
d.cand_inf_trim_map = split_dnf_acc_by_inf(d.cand_acc);
|
d.cand_inf_trim_map = split_dnf_acc_by_inf(d.cand_acc);
|
||||||
|
|
||||||
bdd_dict_ptr bd = aut->get_dict();
|
bdd_dict_ptr bd = aut->get_dict();
|
||||||
d.all_cand_acc.push_back(0U);
|
d.all_cand_acc.emplace_back(0U);
|
||||||
for (unsigned n = 0; n < d.cand_nacc; ++n)
|
for (unsigned n = 0; n < d.cand_nacc; ++n)
|
||||||
{
|
{
|
||||||
auto c = d.cacc.mark(n);
|
auto c = d.cacc.mark(n);
|
||||||
|
|
||||||
size_t ss = d.all_silly_cand_acc.size();
|
size_t ss = d.all_silly_cand_acc.size();
|
||||||
for (size_t i = 0; i < ss; ++i)
|
for (size_t i = 0; i < ss; ++i)
|
||||||
d.all_silly_cand_acc.push_back(d.all_silly_cand_acc[i] | c);
|
d.all_silly_cand_acc.emplace_back(d.all_silly_cand_acc[i] | c);
|
||||||
|
|
||||||
size_t s = d.all_cand_acc.size();
|
size_t s = d.all_cand_acc.size();
|
||||||
for (size_t i = 0; i < s; ++i)
|
for (size_t i = 0; i < s; ++i)
|
||||||
{
|
{
|
||||||
acc_cond::mark_t m = d.all_cand_acc[i] | c;
|
acc_cond::mark_t m = d.all_cand_acc[i] | c;
|
||||||
if (d.cand_inf_trim(m) == m)
|
if (d.cand_inf_trim(m) == m)
|
||||||
d.all_cand_acc.push_back(m);
|
d.all_cand_acc.emplace_back(m);
|
||||||
else
|
else
|
||||||
d.all_silly_cand_acc.push_back(m);
|
d.all_silly_cand_acc.emplace_back(m);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
d.all_ref_acc.push_back(0U);
|
d.all_ref_acc.emplace_back(0U);
|
||||||
unsigned ref_nacc = aut->num_sets();
|
unsigned ref_nacc = aut->num_sets();
|
||||||
for (unsigned n = 0; n < ref_nacc; ++n)
|
for (unsigned n = 0; n < ref_nacc; ++n)
|
||||||
{
|
{
|
||||||
|
|
@ -475,7 +475,7 @@ namespace spot
|
||||||
acc_cond::mark_t m = d.all_ref_acc[i] | c;
|
acc_cond::mark_t m = d.all_ref_acc[i] | c;
|
||||||
if (d.ref_inf_trim(m) != m)
|
if (d.ref_inf_trim(m) != m)
|
||||||
continue;
|
continue;
|
||||||
d.all_ref_acc.push_back(m);
|
d.all_ref_acc.emplace_back(m);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -235,12 +235,12 @@ namespace spot
|
||||||
for (step s : run.prefix)
|
for (step s : run.prefix)
|
||||||
{
|
{
|
||||||
s.s = s.s->clone();
|
s.s = s.s->clone();
|
||||||
prefix.push_back(s);
|
prefix.emplace_back(s);
|
||||||
}
|
}
|
||||||
for (step s : run.cycle)
|
for (step s : run.cycle)
|
||||||
{
|
{
|
||||||
s.s = s.s->clone();
|
s.s = s.s->clone();
|
||||||
cycle.push_back(s);
|
cycle.emplace_back(s);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -374,7 +374,7 @@ namespace spot
|
||||||
seen_acc |= seg->acc;
|
seen_acc |= seg->acc;
|
||||||
|
|
||||||
twa_run::step st = { seg->s->clone(), seg->label, seg->acc };
|
twa_run::step st = { seg->s->clone(), seg->label, seg->acc };
|
||||||
res->cycle.push_back(st);
|
res->cycle.emplace_back(st);
|
||||||
|
|
||||||
++seg;
|
++seg;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -180,7 +180,7 @@ namespace spot
|
||||||
trace << " s.lowlink = " << top << std::endl
|
trace << " s.lowlink = " << top << std::endl
|
||||||
<< " s.acc = " << ss.acc << std::endl;
|
<< " s.acc = " << ss.acc << std::endl;
|
||||||
|
|
||||||
stack.push_back(ss);
|
stack.emplace_back(ss);
|
||||||
dftop = top;
|
dftop = top;
|
||||||
inc_depth();
|
inc_depth();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -186,7 +186,7 @@ namespace spot
|
||||||
int v = bdd_var(all);
|
int v = bdd_var(all);
|
||||||
all = bdd_high(all);
|
all = bdd_high(all);
|
||||||
ap.insert(std::make_pair(v, vap.size()));
|
ap.insert(std::make_pair(v, vap.size()));
|
||||||
vap.push_back(v);
|
vap.emplace_back(v);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (use_implicit_labels)
|
if (use_implicit_labels)
|
||||||
|
|
|
||||||
|
|
@ -64,7 +64,7 @@ namespace spot
|
||||||
std::vector<formula> empty;
|
std::vector<formula> empty;
|
||||||
res_->create_transition(init_, empty);
|
res_->create_transition(init_, empty);
|
||||||
succ_state ss = { empty, f, empty };
|
succ_state ss = { empty, f, empty };
|
||||||
succ_.push_back(ss);
|
succ_.emplace_back(ss);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
case op::eword:
|
case op::eword:
|
||||||
|
|
@ -79,7 +79,7 @@ namespace spot
|
||||||
taa_tgba::transition* t = res_->create_transition(init_, empty);
|
taa_tgba::transition* t = res_->create_transition(init_, empty);
|
||||||
res_->add_condition(t, f);
|
res_->add_condition(t, f);
|
||||||
succ_state ss = { empty, f, empty };
|
succ_state ss = { empty, f, empty };
|
||||||
succ_.push_back(ss);
|
succ_.emplace_back(ss);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
case op::X:
|
case op::X:
|
||||||
|
|
@ -89,10 +89,10 @@ namespace spot
|
||||||
std::vector<formula> a;
|
std::vector<formula> a;
|
||||||
if (v.succ_.empty()) // Handle X(0)
|
if (v.succ_.empty()) // Handle X(0)
|
||||||
return;
|
return;
|
||||||
dst.push_back(v.init_);
|
dst.emplace_back(v.init_);
|
||||||
res_->create_transition(init_, dst);
|
res_->create_transition(init_, dst);
|
||||||
succ_state ss = { dst, formula::tt(), a };
|
succ_state ss = { dst, formula::tt(), a };
|
||||||
succ_.push_back(ss);
|
succ_.emplace_back(ss);
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
case op::F:
|
case op::F:
|
||||||
|
|
@ -165,9 +165,9 @@ namespace spot
|
||||||
i1->Q.erase
|
i1->Q.erase
|
||||||
(remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end());
|
(remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end());
|
||||||
|
|
||||||
i1->Q.push_back(init_); // Add the initial state
|
i1->Q.emplace_back(init_); // Add the initial state
|
||||||
if (strong)
|
if (strong)
|
||||||
i1->acc.push_back(f[1]);
|
i1->acc.emplace_back(f[1]);
|
||||||
t = res_->create_transition(init_, i1->Q);
|
t = res_->create_transition(init_, i1->Q);
|
||||||
res_->add_condition(t, i1->condition);
|
res_->add_condition(t, i1->condition);
|
||||||
if (strong)
|
if (strong)
|
||||||
|
|
@ -175,13 +175,13 @@ namespace spot
|
||||||
else
|
else
|
||||||
for (unsigned i = 0; i < i1->acc.size(); ++i)
|
for (unsigned i = 0; i < i1->acc.size(); ++i)
|
||||||
res_->add_acceptance_condition(t, i1->acc[i]);
|
res_->add_acceptance_condition(t, i1->acc[i]);
|
||||||
succ_.push_back(*i1);
|
succ_.emplace_back(*i1);
|
||||||
}
|
}
|
||||||
for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
|
for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
|
||||||
{
|
{
|
||||||
t = res_->create_transition(init_, i2->Q);
|
t = res_->create_transition(init_, i2->Q);
|
||||||
res_->add_condition(t, i2->condition);
|
res_->add_condition(t, i2->condition);
|
||||||
succ_.push_back(*i2);
|
succ_.emplace_back(*i2);
|
||||||
}
|
}
|
||||||
return;
|
return;
|
||||||
case op::M: // Strong Release
|
case op::M: // Strong Release
|
||||||
|
|
@ -207,7 +207,7 @@ namespace spot
|
||||||
t = res_->create_transition(init_, u);
|
t = res_->create_transition(init_, u);
|
||||||
res_->add_condition(t, f);
|
res_->add_condition(t, f);
|
||||||
succ_state ss = { u, f, a };
|
succ_state ss = { u, f, a };
|
||||||
succ_.push_back(ss);
|
succ_.emplace_back(ss);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (refined_) // Refined rule
|
if (refined_) // Refined rule
|
||||||
|
|
@ -215,19 +215,19 @@ namespace spot
|
||||||
(remove(i2->Q.begin(), i2->Q.end(), v2.init_), i2->Q.end());
|
(remove(i2->Q.begin(), i2->Q.end(), v2.init_), i2->Q.end());
|
||||||
|
|
||||||
|
|
||||||
i2->Q.push_back(init_); // Add the initial state
|
i2->Q.emplace_back(init_); // Add the initial state
|
||||||
t = res_->create_transition(init_, i2->Q);
|
t = res_->create_transition(init_, i2->Q);
|
||||||
res_->add_condition(t, i2->condition);
|
res_->add_condition(t, i2->condition);
|
||||||
|
|
||||||
if (strong)
|
if (strong)
|
||||||
{
|
{
|
||||||
i2->acc.push_back(f[0]);
|
i2->acc.emplace_back(f[0]);
|
||||||
res_->add_acceptance_condition(t, f[0]);
|
res_->add_acceptance_condition(t, f[0]);
|
||||||
}
|
}
|
||||||
else if (refined_)
|
else if (refined_)
|
||||||
for (unsigned i = 0; i < i2->acc.size(); ++i)
|
for (unsigned i = 0; i < i2->acc.size(); ++i)
|
||||||
res_->add_acceptance_condition(t, i2->acc[i]);
|
res_->add_acceptance_condition(t, i2->acc[i]);
|
||||||
succ_.push_back(*i2);
|
succ_.emplace_back(*i2);
|
||||||
}
|
}
|
||||||
return;
|
return;
|
||||||
default:
|
default:
|
||||||
|
|
@ -243,7 +243,7 @@ namespace spot
|
||||||
std::vector<ltl2taa_visitor> vs;
|
std::vector<ltl2taa_visitor> vs;
|
||||||
for (unsigned n = 0, s = f.size(); n < s; ++n)
|
for (unsigned n = 0, s = f.size(); n < s; ++n)
|
||||||
{
|
{
|
||||||
vs.push_back(recurse(f[n]));
|
vs.emplace_back(recurse(f[n]));
|
||||||
if (vs[n].succ_.empty()) // Handle 0
|
if (vs[n].succ_.empty()) // Handle 0
|
||||||
ok = false;
|
ok = false;
|
||||||
}
|
}
|
||||||
|
|
@ -268,7 +268,7 @@ namespace spot
|
||||||
if (!binary_search(p[n].Q.begin(), p[n].Q.end(),
|
if (!binary_search(p[n].Q.begin(), p[n].Q.end(),
|
||||||
vs[m].init_))
|
vs[m].init_))
|
||||||
break;
|
break;
|
||||||
v.push_back(vs[m].init_);
|
v.emplace_back(vs[m].init_);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (v.size() == f.size())
|
if (v.size() == f.size())
|
||||||
|
|
@ -277,19 +277,19 @@ namespace spot
|
||||||
sort(v.begin(), v.end());
|
sort(v.begin(), v.end());
|
||||||
for (unsigned m = 0; m < p[n].Q.size(); ++m)
|
for (unsigned m = 0; m < p[n].Q.size(); ++m)
|
||||||
if (!binary_search(v.begin(), v.end(), p[n].Q[m]))
|
if (!binary_search(v.begin(), v.end(), p[n].Q[m]))
|
||||||
Q.push_back(p[n].Q[m]);
|
Q.emplace_back(p[n].Q[m]);
|
||||||
Q.push_back(init_);
|
Q.emplace_back(init_);
|
||||||
t = res_->create_transition(init_, Q);
|
t = res_->create_transition(init_, Q);
|
||||||
res_->add_condition(t, p[n].condition);
|
res_->add_condition(t, p[n].condition);
|
||||||
for (unsigned i = 0; i < p[n].acc.size(); ++i)
|
for (unsigned i = 0; i < p[n].acc.size(); ++i)
|
||||||
res_->add_acceptance_condition(t, p[n].acc[i]);
|
res_->add_acceptance_condition(t, p[n].acc[i]);
|
||||||
succ_.push_back(p[n]);
|
succ_.emplace_back(p[n]);
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
t = res_->create_transition(init_, p[n].Q);
|
t = res_->create_transition(init_, p[n].Q);
|
||||||
res_->add_condition(t, p[n].condition);
|
res_->add_condition(t, p[n].condition);
|
||||||
succ_.push_back(p[n]);
|
succ_.emplace_back(p[n]);
|
||||||
}
|
}
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
@ -299,7 +299,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
t = res_->create_transition(init_, i.Q);
|
t = res_->create_transition(init_, i.Q);
|
||||||
res_->add_condition(t, i.condition);
|
res_->add_condition(t, i.condition);
|
||||||
succ_.push_back(i);
|
succ_.emplace_back(i);
|
||||||
}
|
}
|
||||||
return;
|
return;
|
||||||
default:
|
default:
|
||||||
|
|
@ -359,11 +359,11 @@ namespace spot
|
||||||
for (unsigned i = 0; i < ss.acc.size(); ++i)
|
for (unsigned i = 0; i < ss.acc.size(); ++i)
|
||||||
{
|
{
|
||||||
formula g = ss.acc[i];
|
formula g = ss.acc[i];
|
||||||
a.push_back(g);
|
a.emplace_back(g);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
succ_state ss = { u, f, a };
|
succ_state ss = { u, f, a };
|
||||||
product.push_back(ss);
|
product.emplace_back(ss);
|
||||||
|
|
||||||
for (int i = vs.size() - 1; i >= 0; --i)
|
for (int i = vs.size() - 1; i >= 0; --i)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -247,7 +247,7 @@ namespace spot
|
||||||
a = bdd_low(a);
|
a = bdd_low(a);
|
||||||
if (h != bddfalse)
|
if (h != bddfalse)
|
||||||
{
|
{
|
||||||
t.push_back(bm[v]);
|
t.emplace_back(bm[v]);
|
||||||
if (a == bddfalse)
|
if (a == bddfalse)
|
||||||
a = h;
|
a = h;
|
||||||
}
|
}
|
||||||
|
|
@ -434,7 +434,7 @@ namespace spot
|
||||||
b = high;
|
b = high;
|
||||||
}
|
}
|
||||||
assert(b != bddfalse);
|
assert(b != bddfalse);
|
||||||
v.push_back(res);
|
v.emplace_back(res);
|
||||||
}
|
}
|
||||||
return formula::multop(o, std::move(v));
|
return formula::multop(o, std::move(v));
|
||||||
}
|
}
|
||||||
|
|
@ -455,7 +455,7 @@ namespace spot
|
||||||
minato_isop isop(f);
|
minato_isop isop(f);
|
||||||
bdd cube;
|
bdd cube;
|
||||||
while ((cube = isop.next()) != bddfalse)
|
while ((cube = isop.next()) != bddfalse)
|
||||||
v.push_back(conj_bdd_to_formula(cube));
|
v.emplace_back(conj_bdd_to_formula(cube));
|
||||||
return formula::Or(std::move(v));
|
return formula::Or(std::move(v));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -469,7 +469,7 @@ namespace spot
|
||||||
minato_isop isop(f);
|
minato_isop isop(f);
|
||||||
bdd cube;
|
bdd cube;
|
||||||
while ((cube = isop.next()) != bddfalse)
|
while ((cube = isop.next()) != bddfalse)
|
||||||
v.push_back(conj_bdd_to_sere(cube));
|
v.emplace_back(conj_bdd_to_sere(cube));
|
||||||
return formula::OrRat(std::move(v));
|
return formula::OrRat(std::move(v));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -742,9 +742,9 @@ namespace spot
|
||||||
|
|
||||||
for (auto g: f)
|
for (auto g: f)
|
||||||
if (g.accepts_eword())
|
if (g.accepts_eword())
|
||||||
final.push_back(g);
|
final.emplace_back(g);
|
||||||
else
|
else
|
||||||
non_final.push_back(g);
|
non_final.emplace_back(g);
|
||||||
|
|
||||||
if (non_final.empty())
|
if (non_final.empty())
|
||||||
// (a* & b*);c = (a*|b*);c
|
// (a* & b*);c = (a*|b*);c
|
||||||
|
|
@ -780,9 +780,9 @@ namespace spot
|
||||||
formula g = f[m];
|
formula g = f[m];
|
||||||
if (n != m)
|
if (n != m)
|
||||||
g = formula::Concat({g, star});
|
g = formula::Concat({g, star});
|
||||||
conj.push_back(g);
|
conj.emplace_back(g);
|
||||||
}
|
}
|
||||||
disj.push_back(formula::AndRat(std::move(conj)));
|
disj.emplace_back(formula::AndRat(std::move(conj)));
|
||||||
}
|
}
|
||||||
return recurse_and_concat(formula::OrRat(std::move(disj)));
|
return recurse_and_concat(formula::OrRat(std::move(disj)));
|
||||||
}
|
}
|
||||||
|
|
@ -813,9 +813,9 @@ namespace spot
|
||||||
unsigned s = f.size();
|
unsigned s = f.size();
|
||||||
v.reserve(s);
|
v.reserve(s);
|
||||||
for (unsigned n = 1; n < s; ++n)
|
for (unsigned n = 1; n < s; ++n)
|
||||||
v.push_back(f[n]);
|
v.emplace_back(f[n]);
|
||||||
if (to_concat_)
|
if (to_concat_)
|
||||||
v.push_back(to_concat_);
|
v.emplace_back(to_concat_);
|
||||||
return recurse(f[0], formula::Concat(std::move(v)));
|
return recurse(f[0], formula::Concat(std::move(v)));
|
||||||
}
|
}
|
||||||
case op::Fusion:
|
case op::Fusion:
|
||||||
|
|
@ -2092,7 +2092,7 @@ namespace spot
|
||||||
|
|
||||||
bdd conds = bdd_existcomp(label, d.var_set);
|
bdd conds = bdd_existcomp(label, d.var_set);
|
||||||
bdd promises = bdd_existcomp(label, d.a_set);
|
bdd promises = bdd_existcomp(label, d.a_set);
|
||||||
dests.push_back(transition(dest, conds, promises));
|
dests.emplace_back(transition(dest, conds, promises));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -346,21 +346,21 @@ namespace spot
|
||||||
for (; i != end; ++i, ++j)
|
for (; i != end; ++i, ++j)
|
||||||
{
|
{
|
||||||
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
||||||
l->push_back(s);
|
l->emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
l = &run->cycle;
|
l = &run->cycle;
|
||||||
|
|
||||||
j = ms_->st_red.rbegin();
|
j = ms_->st_red.rbegin();
|
||||||
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
||||||
l->push_back(s);
|
l->emplace_back(s);
|
||||||
|
|
||||||
i = j; ++j;
|
i = j; ++j;
|
||||||
end = ms_->st_red.rend(); --end;
|
end = ms_->st_red.rend(); --end;
|
||||||
for (; i != end; ++i, ++j)
|
for (; i != end; ++i, ++j)
|
||||||
{
|
{
|
||||||
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
||||||
l->push_back(s);
|
l->emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
return run;
|
return run;
|
||||||
|
|
|
||||||
|
|
@ -54,7 +54,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
tmp = cpy->new_state();
|
tmp = cpy->new_state();
|
||||||
seen[old_state] = tmp;
|
seen[old_state] = tmp;
|
||||||
todo.push_back(old_state);
|
todo.emplace_back(old_state);
|
||||||
}
|
}
|
||||||
return tmp;
|
return tmp;
|
||||||
};
|
};
|
||||||
|
|
|
||||||
|
|
@ -293,9 +293,9 @@ namespace spot
|
||||||
used_var[set_num] = s;
|
used_var[set_num] = s;
|
||||||
free_var.erase(set_num);
|
free_var.erase(set_num);
|
||||||
if (s > 1)
|
if (s > 1)
|
||||||
cur_run.push_back(final);
|
cur_run.emplace_back(final);
|
||||||
else
|
else
|
||||||
done.push_back(final);
|
done.emplace_back(final);
|
||||||
for (hash_set::const_iterator i = final->begin();
|
for (hash_set::const_iterator i = final->begin();
|
||||||
i != final->end(); ++i)
|
i != final->end(); ++i)
|
||||||
state_set_map[*i] = set_num;
|
state_set_map[*i] = set_num;
|
||||||
|
|
@ -314,9 +314,9 @@ namespace spot
|
||||||
used_var[num] = s;
|
used_var[num] = s;
|
||||||
free_var.erase(num);
|
free_var.erase(num);
|
||||||
if (s > 1)
|
if (s > 1)
|
||||||
cur_run.push_back(non_final);
|
cur_run.emplace_back(non_final);
|
||||||
else
|
else
|
||||||
done.push_back(non_final);
|
done.emplace_back(non_final);
|
||||||
for (hash_set::const_iterator i = non_final->begin();
|
for (hash_set::const_iterator i = non_final->begin();
|
||||||
i != non_final->end(); ++i)
|
i != non_final->end(); ++i)
|
||||||
state_set_map[*i] = num;
|
state_set_map[*i] = num;
|
||||||
|
|
@ -388,7 +388,7 @@ namespace spot
|
||||||
// The set was not split.
|
// The set was not split.
|
||||||
trace << "set " << format_hash_set(bsi->second, det_a)
|
trace << "set " << format_hash_set(bsi->second, det_a)
|
||||||
<< " was not split" << std::endl;
|
<< " was not split" << std::endl;
|
||||||
next_run.push_back(bsi->second);
|
next_run.emplace_back(bsi->second);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -421,13 +421,13 @@ namespace spot
|
||||||
{
|
{
|
||||||
trace << "set " << format_hash_set(set, det_a)
|
trace << "set " << format_hash_set(set, det_a)
|
||||||
<< " is minimal" << std::endl;
|
<< " is minimal" << std::endl;
|
||||||
done.push_back(set);
|
done.emplace_back(set);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
trace << "set " << format_hash_set(set, det_a)
|
trace << "set " << format_hash_set(set, det_a)
|
||||||
<< " should be processed further" << std::endl;
|
<< " should be processed further" << std::endl;
|
||||||
next_run.push_back(set);
|
next_run.emplace_back(set);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -121,7 +121,7 @@ namespace spot
|
||||||
bdd one = bdd_satoneset(all, allap, bddfalse);
|
bdd one = bdd_satoneset(all, allap, bddfalse);
|
||||||
all -= one;
|
all -= one;
|
||||||
bdd2num.emplace(one, num2bdd.size());
|
bdd2num.emplace(one, num2bdd.size());
|
||||||
num2bdd.push_back(one);
|
num2bdd.emplace_back(one);
|
||||||
}
|
}
|
||||||
|
|
||||||
size_t nc = num2bdd.size(); // number of conditions
|
size_t nc = num2bdd.size(); // number of conditions
|
||||||
|
|
@ -167,7 +167,7 @@ namespace spot
|
||||||
seen[bvi] = num;
|
seen[bvi] = num;
|
||||||
assert(pm.map_.size() == num);
|
assert(pm.map_.size() == num);
|
||||||
pm.map_.emplace_back(std::move(ps));
|
pm.map_.emplace_back(std::move(ps));
|
||||||
toclean.push_back(bvi);
|
toclean.emplace_back(bvi);
|
||||||
}
|
}
|
||||||
|
|
||||||
// outgoing map
|
// outgoing map
|
||||||
|
|
@ -201,7 +201,7 @@ namespace spot
|
||||||
dst_num = res->new_state();
|
dst_num = res->new_state();
|
||||||
auto dst2 = dst->clone();
|
auto dst2 = dst->clone();
|
||||||
seen[dst2] = dst_num;
|
seen[dst2] = dst_num;
|
||||||
toclean.push_back(dst2);
|
toclean.emplace_back(dst2);
|
||||||
auto ps = bv_to_ps(dst);
|
auto ps = bv_to_ps(dst);
|
||||||
assert(pm.map_.size() == dst_num);
|
assert(pm.map_.size() == dst_num);
|
||||||
pm.map_.emplace_back(std::move(ps));
|
pm.map_.emplace_back(std::move(ps));
|
||||||
|
|
@ -340,7 +340,7 @@ namespace spot
|
||||||
while (i != dfs_.end());
|
while (i != dfs_.end());
|
||||||
if (is_acc)
|
if (is_acc)
|
||||||
{
|
{
|
||||||
accept_.push_back(ts);
|
accept_.emplace_back(ts);
|
||||||
all_.insert(ts.begin(), ts.end());
|
all_.insert(ts.begin(), ts.end());
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
|
||||||
|
|
@ -76,7 +76,7 @@ namespace spot
|
||||||
p.first->second = res->new_state();
|
p.first->second = res->new_state();
|
||||||
todo.emplace_back(x, p.first->second);
|
todo.emplace_back(x, p.first->second);
|
||||||
assert(p.first->second == v->size());
|
assert(p.first->second == v->size());
|
||||||
v->push_back(x);
|
v->emplace_back(x);
|
||||||
}
|
}
|
||||||
return p.first->second;
|
return p.first->second;
|
||||||
};
|
};
|
||||||
|
|
|
||||||
|
|
@ -63,7 +63,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
labels.push_back(current);
|
labels.emplace_back(current);
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -189,7 +189,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
for (unsigned i = 0; i < nsucc; ++i)
|
for (unsigned i = 0; i < nsucc; ++i)
|
||||||
labels.push_back(random_labels(props, props_n, t));
|
labels.emplace_back(random_labels(props, props_n, t));
|
||||||
|
|
||||||
int possibilities = n;
|
int possibilities = n;
|
||||||
unsigned dst;
|
unsigned dst;
|
||||||
|
|
|
||||||
|
|
@ -130,7 +130,7 @@ namespace spot
|
||||||
void
|
void
|
||||||
twa_reachable_iterator_breadth_first::add_state(const state* s)
|
twa_reachable_iterator_breadth_first::add_state(const state* s)
|
||||||
{
|
{
|
||||||
todo.push_back(s);
|
todo.emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
const state*
|
const state*
|
||||||
|
|
@ -170,7 +170,7 @@ namespace spot
|
||||||
twa_succ_iterator* si = aut_->succ_iter(s);
|
twa_succ_iterator* si = aut_->succ_iter(s);
|
||||||
process_state(s, sn, si);
|
process_state(s, sn, si);
|
||||||
stack_item item = { s, sn, si };
|
stack_item item = { s, sn, si };
|
||||||
todo.push_back(item);
|
todo.emplace_back(item);
|
||||||
si->first();
|
si->first();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -34,7 +34,7 @@ namespace spot
|
||||||
int oldv = aut->register_ap(p.first);
|
int oldv = aut->register_ap(p.first);
|
||||||
int newv = aut->register_ap(p.second);
|
int newv = aut->register_ap(p.second);
|
||||||
bdd_setpair(pairs, oldv, newv);
|
bdd_setpair(pairs, oldv, newv);
|
||||||
vars.push_back(oldv);
|
vars.emplace_back(oldv);
|
||||||
newvars.insert(newv);
|
newvars.insert(newv);
|
||||||
}
|
}
|
||||||
for (auto& t: aut->edges())
|
for (auto& t: aut->edges())
|
||||||
|
|
|
||||||
|
|
@ -537,7 +537,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
// The empty Fin should always come first
|
// The empty Fin should always come first
|
||||||
assert(p.first != 0U || rem.empty());
|
assert(p.first != 0U || rem.empty());
|
||||||
rem.push_back(p.first);
|
rem.emplace_back(p.first);
|
||||||
allfin |= p.first;
|
allfin |= p.first;
|
||||||
acc_cond::mark_t inf = 0U;
|
acc_cond::mark_t inf = 0U;
|
||||||
if (!p.second.empty())
|
if (!p.second.empty())
|
||||||
|
|
@ -568,10 +568,10 @@ namespace spot
|
||||||
{
|
{
|
||||||
has_true_term = true;
|
has_true_term = true;
|
||||||
}
|
}
|
||||||
code.push_back(std::move(p.second));
|
code.emplace_back(std::move(p.second));
|
||||||
keep.push_back(inf);
|
keep.emplace_back(inf);
|
||||||
allinf |= inf;
|
allinf |= inf;
|
||||||
add.push_back(0U);
|
add.emplace_back(0U);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
assert(add.size() > 0);
|
assert(add.size() > 0);
|
||||||
|
|
|
||||||
|
|
@ -297,9 +297,9 @@ namespace spot
|
||||||
inout.reserve(in_n);
|
inout.reserve(in_n);
|
||||||
for (unsigned i = 0; i < in_n; ++i)
|
for (unsigned i = 0; i < in_n; ++i)
|
||||||
if (filter.state(i))
|
if (filter.state(i))
|
||||||
inout.push_back(out_n++);
|
inout.emplace_back(out_n++);
|
||||||
else
|
else
|
||||||
inout.push_back(-1U);
|
inout.emplace_back(-1U);
|
||||||
|
|
||||||
filter.fix_acceptance(filtered);
|
filter.fix_acceptance(filtered);
|
||||||
filtered->new_states(out_n);
|
filtered->new_states(out_n);
|
||||||
|
|
|
||||||
|
|
@ -356,7 +356,7 @@ namespace spot
|
||||||
if (l == &run->prefix && i->s->compare(target) == 0)
|
if (l == &run->prefix && i->s->compare(target) == 0)
|
||||||
l = &run->cycle;
|
l = &run->cycle;
|
||||||
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
||||||
l->push_back(s);
|
l->emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (l == &run->prefix && i->s->compare(target) == 0)
|
if (l == &run->prefix && i->s->compare(target) == 0)
|
||||||
|
|
@ -365,14 +365,14 @@ namespace spot
|
||||||
|
|
||||||
j = ms_->st_red.rbegin();
|
j = ms_->st_red.rbegin();
|
||||||
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
||||||
l->push_back(s);
|
l->emplace_back(s);
|
||||||
|
|
||||||
i = j; ++j;
|
i = j; ++j;
|
||||||
end = ms_->st_red.rend(); --end;
|
end = ms_->st_red.rend(); --end;
|
||||||
for (; i != end; ++i, ++j)
|
for (; i != end; ++i, ++j)
|
||||||
{
|
{
|
||||||
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
twa_run::step s = { i->s->clone(), j->label, j->acc };
|
||||||
l->push_back(s);
|
l->emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
return run;
|
return run;
|
||||||
|
|
|
||||||
|
|
@ -146,7 +146,7 @@ namespace spot
|
||||||
std::vector<unsigned> res;
|
std::vector<unsigned> res;
|
||||||
while (b != bddtrue)
|
while (b != bddtrue)
|
||||||
{
|
{
|
||||||
res.push_back(bdd_var(b) - acc_vars);
|
res.emplace_back(bdd_var(b) - acc_vars);
|
||||||
b = bdd_high(b);
|
b = bdd_high(b);
|
||||||
}
|
}
|
||||||
return acc_cond::mark_t(res.begin(), res.end());
|
return acc_cond::mark_t(res.begin(), res.end());
|
||||||
|
|
@ -238,7 +238,7 @@ namespace spot
|
||||||
bdd_initial = bdd_ithvar(set_num++);
|
bdd_initial = bdd_ithvar(set_num++);
|
||||||
bdd init = bdd_ithvar(set_num++);
|
bdd init = bdd_ithvar(set_num++);
|
||||||
|
|
||||||
used_var_.push_back(init);
|
used_var_.emplace_back(init);
|
||||||
|
|
||||||
// Initialize all classes to init.
|
// Initialize all classes to init.
|
||||||
previous_class_.resize(size_a_);
|
previous_class_.resize(size_a_);
|
||||||
|
|
@ -348,7 +348,7 @@ namespace spot
|
||||||
void update_sig()
|
void update_sig()
|
||||||
{
|
{
|
||||||
for (unsigned s = 0; s < size_a_; ++s)
|
for (unsigned s = 0; s < size_a_; ++s)
|
||||||
bdd_lstate_[compute_sig(s)].push_back(s);
|
bdd_lstate_[compute_sig(s)].emplace_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -363,7 +363,7 @@ namespace spot
|
||||||
for (int i = 0; i < nb_new_color; ++i)
|
for (int i = 0; i < nb_new_color; ++i)
|
||||||
{
|
{
|
||||||
assert(!free_var_.empty());
|
assert(!free_var_.empty());
|
||||||
used_var_.push_back(bdd_ithvar(free_var_.front()));
|
used_var_.emplace_back(bdd_ithvar(free_var_.front()));
|
||||||
free_var_.pop();
|
free_var_.pop();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -300,7 +300,7 @@ namespace spot
|
||||||
stutter_state s(s0, bddfalse);
|
stutter_state s(s0, bddfalse);
|
||||||
ss2num[s] = 0;
|
ss2num[s] = 0;
|
||||||
res->new_state();
|
res->new_state();
|
||||||
todo.push_back(s);
|
todo.emplace_back(s);
|
||||||
|
|
||||||
while (!todo.empty())
|
while (!todo.empty())
|
||||||
{
|
{
|
||||||
|
|
@ -325,7 +325,7 @@ namespace spot
|
||||||
|
|
||||||
if (r.second)
|
if (r.second)
|
||||||
{
|
{
|
||||||
todo.push_back(d);
|
todo.emplace_back(d);
|
||||||
unsigned u = res->new_state();
|
unsigned u = res->new_state();
|
||||||
assert(u == dest);
|
assert(u == dest);
|
||||||
(void)u;
|
(void)u;
|
||||||
|
|
@ -439,8 +439,8 @@ namespace spot
|
||||||
|
|
||||||
for (auto it = trans.begin(); it != trans.end(); ++it)
|
for (auto it = trans.begin(); it != trans.end(); ++it)
|
||||||
{
|
{
|
||||||
todo.push_back(it.trans());
|
todo.emplace_back(it.trans());
|
||||||
dst2trans[it->dst].push_back(it.trans());
|
dst2trans[it->dst].emplace_back(it.trans());
|
||||||
}
|
}
|
||||||
|
|
||||||
while (!todo.empty())
|
while (!todo.empty())
|
||||||
|
|
@ -465,7 +465,7 @@ namespace spot
|
||||||
ts.cond |= cond;
|
ts.cond |= cond;
|
||||||
if (std::find(todo.begin(), todo.end(), t)
|
if (std::find(todo.begin(), todo.end(), t)
|
||||||
== todo.end())
|
== todo.end())
|
||||||
todo.push_back(t);
|
todo.emplace_back(t);
|
||||||
}
|
}
|
||||||
need_new_trans = false;
|
need_new_trans = false;
|
||||||
break;
|
break;
|
||||||
|
|
@ -478,7 +478,7 @@ namespace spot
|
||||||
ts.acc = acc;
|
ts.acc = acc;
|
||||||
if (std::find(todo.begin(), todo.end(), t)
|
if (std::find(todo.begin(), todo.end(), t)
|
||||||
== todo.end())
|
== todo.end())
|
||||||
todo.push_back(t);
|
todo.emplace_back(t);
|
||||||
}
|
}
|
||||||
need_new_trans = false;
|
need_new_trans = false;
|
||||||
break;
|
break;
|
||||||
|
|
@ -490,8 +490,8 @@ namespace spot
|
||||||
// invalidated by new_edge().
|
// invalidated by new_edge().
|
||||||
auto dst = t2.dst;
|
auto dst = t2.dst;
|
||||||
auto i = a->new_edge(state, dst, cond, acc);
|
auto i = a->new_edge(state, dst, cond, acc);
|
||||||
dst2trans[dst].push_back(i);
|
dst2trans[dst].emplace_back(i);
|
||||||
todo.push_back(i);
|
todo.emplace_back(i);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -161,7 +161,7 @@ namespace spot
|
||||||
std::vector<unsigned> res;
|
std::vector<unsigned> res;
|
||||||
unsigned max = a_->num_sets();
|
unsigned max = a_->num_sets();
|
||||||
for (unsigned n = 0; n < max && acc.has(n); ++n)
|
for (unsigned n = 0; n < max && acc.has(n); ++n)
|
||||||
res.push_back(n);
|
res.emplace_back(n);
|
||||||
return acc_cond::mark_t(res.begin(), res.end());
|
return acc_cond::mark_t(res.begin(), res.end());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -84,7 +84,7 @@ namespace spot
|
||||||
m |= pos[-1].mark;
|
m |= pos[-1].mark;
|
||||||
pos -= 2;
|
pos -= 2;
|
||||||
}
|
}
|
||||||
res.push_back(m);
|
res.emplace_back(m);
|
||||||
}
|
}
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
@ -162,7 +162,7 @@ namespace spot
|
||||||
|
|
||||||
st2gba_state s(in->get_init_state_number());
|
st2gba_state s(in->get_init_state_number());
|
||||||
bs2num[s] = out->new_state();
|
bs2num[s] = out->new_state();
|
||||||
todo.push_back(s);
|
todo.emplace_back(s);
|
||||||
|
|
||||||
bool sbacc = in->prop_state_acc().is_true();
|
bool sbacc = in->prop_state_acc().is_true();
|
||||||
|
|
||||||
|
|
@ -234,7 +234,7 @@ namespace spot
|
||||||
else // No, this is a new state
|
else // No, this is a new state
|
||||||
{
|
{
|
||||||
dest = dres.first->second = out->new_state();
|
dest = dres.first->second = out->new_state();
|
||||||
todo.push_back(d);
|
todo.emplace_back(d);
|
||||||
}
|
}
|
||||||
out->new_edge(src, dest, t.cond, acc);
|
out->new_edge(src, dest, t.cond, acc);
|
||||||
|
|
||||||
|
|
@ -264,7 +264,7 @@ namespace spot
|
||||||
else // No, this is a new state
|
else // No, this is a new state
|
||||||
{
|
{
|
||||||
dest = dres.first->second = out->new_state();
|
dest = dres.first->second = out->new_state();
|
||||||
todo.push_back(d);
|
todo.emplace_back(d);
|
||||||
}
|
}
|
||||||
out->new_edge(src, dest, t.cond);
|
out->new_edge(src, dest, t.cond);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -30,9 +30,9 @@ namespace spot
|
||||||
: dict_(run->aut->get_dict())
|
: dict_(run->aut->get_dict())
|
||||||
{
|
{
|
||||||
for (auto& i: run->prefix)
|
for (auto& i: run->prefix)
|
||||||
prefix.push_back(i.label);
|
prefix.emplace_back(i.label);
|
||||||
for (auto& i: run->cycle)
|
for (auto& i: run->cycle)
|
||||||
cycle.push_back(i.label);
|
cycle.emplace_back(i.label);
|
||||||
dict_->register_all_variables_of(run->aut, this);
|
dict_->register_all_variables_of(run->aut, this);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -58,7 +58,7 @@ namespace spot
|
||||||
if (all != bddfalse)
|
if (all != bddfalse)
|
||||||
{
|
{
|
||||||
cycle.clear();
|
cycle.clear();
|
||||||
cycle.push_back(all);
|
cycle.emplace_back(all);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// If the last formula of the prefix is compatible with the
|
// If the last formula of the prefix is compatible with the
|
||||||
|
|
@ -175,7 +175,7 @@ namespace spot
|
||||||
if (!pf.errors.empty())
|
if (!pf.errors.empty())
|
||||||
word_parse_error(word, i, pf);
|
word_parse_error(word, i, pf);
|
||||||
atomic_prop_collect(pf.f, &aps);
|
atomic_prop_collect(pf.f, &aps);
|
||||||
seq.push_back(tls.as_bdd(pf.f));
|
seq.emplace_back(tls.as_bdd(pf.f));
|
||||||
if (word[ind] == '}')
|
if (word[ind] == '}')
|
||||||
return true;
|
return true;
|
||||||
// Skip blanks after semi-colon
|
// Skip blanks after semi-colon
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -68,7 +68,7 @@ int main()
|
||||||
<< ' ' << v->is_subset_of(*w) << '\n';
|
<< ' ' << v->is_subset_of(*w) << '\n';
|
||||||
|
|
||||||
for (size_t i = 0; i < 30; ++i)
|
for (size_t i = 0; i < 30; ++i)
|
||||||
w->push_back((i & 3) == 0);
|
w->emplace_back((i & 3) == 0);
|
||||||
ECHO(w);
|
ECHO(w);
|
||||||
*x &= *w;
|
*x &= *w;
|
||||||
ECHO(x);
|
ECHO(x);
|
||||||
|
|
@ -77,7 +77,7 @@ int main()
|
||||||
|
|
||||||
ruler();
|
ruler();
|
||||||
|
|
||||||
w->push_back(0x09, 4);
|
w->emplace_back(0x09, 4);
|
||||||
ECHO(w);
|
ECHO(w);
|
||||||
spot::bitvect* y = w->extract_range(0, 71);
|
spot::bitvect* y = w->extract_range(0, 71);
|
||||||
ECHO(y);
|
ECHO(y);
|
||||||
|
|
@ -116,7 +116,7 @@ int main()
|
||||||
ruler();
|
ruler();
|
||||||
|
|
||||||
for (size_t i = 0; i < 12; ++i)
|
for (size_t i = 0; i < 12; ++i)
|
||||||
a->at(4).push_back((i & 2) == 0);
|
a->at(4).emplace_back((i & 2) == 0);
|
||||||
a->at(6) = a->at(4);
|
a->at(6) = a->at(4);
|
||||||
a->at(8) = a->at(7);
|
a->at(8) = a->at(7);
|
||||||
a->at(6) ^= a->at(8);
|
a->at(6) ^= a->at(8);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue