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

gen: generalize fin_unit to mafins()

Browse source 
Based on work with Jan Strejček.

* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::mafins,
acc_cond::acc_code::mafins): New methods.
(fin_unit_one_split, fin_unit_one_split_improved): Use mafins()
instead on fin_unit().
* spot/twaalgos/genem.cc: Use mafins() instead on fin_unit().
This commit is contained in:
Alexandre Duret-Lutz 2023-07-25 16:44:21 +02:00
parent 40e30df7e3
commit 3b59240133
3 changed files with 114 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

111
spot/twa/acc.cc
View file

@ -2646,34 +2646,65 @@ namespace spot
namespace
{
int has_top_fin(const acc_cond::acc_word* pos, bool top = true)
static acc_cond::mark_t mafins_rec(const acc_cond::acc_word* pos)
{
acc_cond::mark_t res{};
auto sub = pos - pos->sub.size;
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
--pos;
do
{
res |= mafins_rec(pos);
pos -= pos->sub.size + 1;
}
while (sub < pos);
return res;
case acc_cond::acc_op::Or:
--pos;
res = mafins_rec(pos);
pos -= pos->sub.size + 1;
while (sub < pos)
{
if (!res)
return res;
res &= mafins_rec(pos);
pos -= pos->sub.size + 1;
}
return res;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
case acc_cond::acc_op::FinNeg:
return res;
case acc_cond::acc_op::Fin:
auto m = pos[-1].mark;
if (m.is_singleton())
return m;
return res;
}
SPOT_UNREACHABLE();
return res;
}
int has_top_fin(const acc_cond::acc_word* pos)
{
if (pos->sub.op == acc_cond::acc_op::Fin)
{
acc_cond::mark_t m = pos[-1].mark;
if (top || m.is_singleton())
return m.min_set() - 1;
return m.min_set() - 1;
}
else if (pos->sub.op == acc_cond::acc_op::And)
else if (pos->sub.op == acc_cond::acc_op::And
|| pos->sub.op == acc_cond::acc_op::Or)
{
auto sub = pos - pos->sub.size;
do
{
--pos;
if (int f = has_top_fin(pos, false); f >= 0)
return f;
pos -= pos->sub.size;
}
while (sub < pos);
}
else if (top && pos->sub.op == acc_cond::acc_op::Or)
{
auto sub = pos - pos->sub.size;
do
{
--pos;
if (int f = has_top_fin(pos); f >= 0)
return f;
acc_cond::mark_t m = mafins_rec(pos);
if (m)
return m.min_set() - 1;
pos -= pos->sub.size;
}
while (sub < pos);
@ -2740,12 +2771,6 @@ namespace spot
return false;
}
// Check whether pos looks like Fin(f) or Fin(f)&rest
bool is_conj_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
{
return has_fin<true>(pos, f);
}
acc_cond::acc_code extract_fin(const acc_cond::acc_word* pos,
acc_cond::mark_t f)
{
@ -2784,16 +2809,21 @@ namespace spot
template<bool deeper_check = false>
std::pair<acc_cond::acc_code, acc_cond::acc_code>
split_top_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
split_top_fin(const acc_cond::acc_word* pos, unsigned f)
{
auto start = pos - pos->sub.size;
switch (pos->sub.op)
{
case acc_cond::acc_op::And:
case acc_cond::acc_op::Fin:
if (is_conj_fin(pos, f))
{
auto m = pos[-1].mark;
return {acc_cond::acc_code::fin({f}),
acc_cond::acc_code::fin(m - acc_cond::mark_t{f})};
}
case acc_cond::acc_op::And:
if (mafins_rec(pos).has(f))
return {pos, acc_cond::acc_code::f()};
SPOT_FALLTHROUGH;
return {acc_cond::acc_code::f(), pos};
case acc_cond::acc_op::Inf:
return {acc_cond::acc_code::f(), pos};
case acc_cond::acc_op::Or:
@ -2803,20 +2833,19 @@ namespace spot
auto right = acc_cond::acc_code::f();
do
{
if (is_conj_fin(pos, f))
acc_cond::mark_t mf = mafins_rec(pos);
if (mf.has(f))
{
auto tmp = strip_rec(pos, f, true, false);
auto tmp = strip_rec(pos, {f}, true, false);
tmp |= std::move(left);
std::swap(tmp, left);
}
else if (deeper_check
&& has_top_fin(pos) == -1
&& has_fin(pos, f))
else if (deeper_check && !mf && has_fin(pos, {f}))
{
auto tmp = strip_rec(pos, f, true, false);
auto tmp = strip_rec(pos, {f}, true, false);
tmp |= std::move(left);
std::swap(tmp, left);
tmp = force_inf_rec(pos, f);
tmp = force_inf_rec(pos, {f});
tmp |= std::move(right);
std::swap(tmp, right);
}
@ -2863,7 +2892,7 @@ namespace spot
int selected_fin = has_top_fin(pos);
if (selected_fin >= 0)
{
auto [left, right] = split_top_fin(pos, {(unsigned) selected_fin});
auto [left, right] = split_top_fin(pos, (unsigned) selected_fin);
return {selected_fin, std::move(left), std::move(right)};
}
selected_fin = fin_one();
@ -2884,7 +2913,7 @@ namespace spot
if (selected_fin >= 0)
{
auto [left, right] =
split_top_fin<true>(pos, {(unsigned) selected_fin});
split_top_fin<true>(pos, (unsigned) selected_fin);
return {selected_fin, std::move(left), std::move(right)};
}
selected_fin = fin_one();
@ -3075,6 +3104,14 @@ namespace spot
return res;
}
acc_cond::mark_t
acc_cond::acc_code::mafins() const
{
if (empty() || is_f())
return {};
return mafins_rec(&back());
}
acc_cond::mark_t acc_cond::acc_code::inf_unit() const
{
mark_t res = {};

35
spot/twa/acc.hh
View file

@ -1254,8 +1254,24 @@ namespace spot
/// If multiple unit-Fin appear as unit-clauses, the set of
/// those will be returned. For instance applied to
/// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`.
///
/// \see acc_cond::acc_code::mafins
mark_t fin_unit() const;
/// \brief Find a `Fin(i)` that is mandatory.
///
/// This return a mark_t `{i}` such that `Fin(i)` appears in
/// all branches of the AST of the acceptance conditions. This
/// is therefore a bit stronger than fin_unit().
/// For instance on `Inf(1)&Fin(2) | Fin(2)&Fin(3)` this will
/// return `{2}`.
///
/// If multiple mandatory Fins exist, the set of those will be
/// returned.
///
/// \see acc_cond::acc_code::fin_unit
mark_t mafins() const;
/// \brief Find a `Inf(i)` that is a unit clause.
///
/// This return a mark_t `{i}` such that `Inf(i)` appears as a
@ -2204,11 +2220,30 @@ namespace spot
/// If multiple unit-Fin appear as unit-clauses, the set of
/// those will be returned. For instance applied to
/// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))``, this will return `{0,1}`.
///
/// \see acc_cond::mafins
mark_t fin_unit() const
{
return code_.fin_unit();
}
/// \brief Find a `Fin(i)` that is mandatory.
///
/// This return a mark_t `{i}` such that `Fin(i)` appears in
/// all branches of the AST of the acceptance conditions. This
/// is therefore a bit stronger than fin_unit().
/// For instance on `Inf(1)&Fin(2) | Fin(2)&Fin(3)` this will
/// return `{2}`.
///
/// If multiple mandatory Fins exist, the set of those will be
/// returned.
///
/// \see acc_cond::fin_unit
mark_t mafins() const
{
return code_.mafins();
}
/// \brief Find a `Inf(i)` that is a unit clause.
///
/// This return a mark_t `{i}` such that `Inf(i)` appears as a

10
spot/twaalgos/genem.cc
View file

@ -92,7 +92,7 @@ namespace spot
if (genem_version == spot211
|| genem_version == spot212
|| genem_version == spot210)
tocut |= acc.fin_unit();
tocut |= acc.mafins();
scc_and_mark_filter filt(si, scc, tocut);
filt.override_acceptance(acc);
scc_info upper_si(filt, EarlyStop
@ -167,7 +167,7 @@ namespace spot
{
acc_cond::acc_code rest = acc_cond::acc_code::f();
for (const acc_cond& disjunct: acc.top_disjuncts())
if (acc_cond::mark_t fu = disjunct.fin_unit())
if (acc_cond::mark_t fu = disjunct.mafins())
{
if (!scc_split_check<EarlyStop, Extra>
(si, scc, disjunct.remove(fu, true), extra, fu))
@ -244,10 +244,10 @@ namespace spot
}
return true;
}
// Filter with fin_unit() right away if possible.
// scc_and_mark_filter will have no effect if fin_unit() is
// Filter with mafins() right away if possible.
// scc_and_mark_filter will have no effect if mafins() is
// empty.
scc_and_mark_filter filt(aut, aut_acc.fin_unit());
scc_and_mark_filter filt(aut, aut_acc.mafins());
scc_info si(filt, scc_info_options::STOP_ON_ACC);
const int accepting_scc = si.one_accepting_scc();