diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index d73af33b0..8fec855af 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -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(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 std::pair - 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(pos, {(unsigned) selected_fin}); + split_top_fin(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 = {}; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 1b46e4024..6d673bb8c 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -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 diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 0b0d1fd5f..77597db9f 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -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 (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();