From 975ea0c52af57ea134eb72ea949d88a455e45e8d Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Wed, 20 Sep 2023 17:52:18 +0200 Subject: [PATCH] expansions: UniquePrefixSeenOpt --- spot/tl/expansions.cc | 71 +++++++++++++++++++++++++++++++------------ spot/tl/expansions.hh | 3 +- 2 files changed, 54 insertions(+), 20 deletions(-) diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index 1086b0f67..8b0309246 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -301,7 +301,7 @@ namespace spot } void - finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d) + finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set* seen) { if (opts & (exp_opts::expand_opt::BddIsop | exp_opts::expand_opt::BddMinterm)) @@ -344,9 +344,37 @@ namespace spot } exp.clear(); + for (const auto [prefix, suffix] : unique_map) { - exp.insert({prefix, suffix}); + if ((opts & exp_opts::expand_opt::UniquePrefixSeenOpt) + && suffix.is(op::OrRat)) + { + std::vector merge; + std::vector single; + + for (const auto& sub_f : suffix) + { + if (seen->find(sub_f) != seen->end()) + { + single.push_back(sub_f); + } + else + { + merge.push_back(sub_f); + } + } + + for (const auto& sub_f : single) + exp.insert({prefix, sub_f}); + + if (!merge.empty()) + exp.insert({prefix, formula::OrRat(merge)}); + } + else + { + exp.insert({prefix, suffix}); + } } } @@ -399,7 +427,7 @@ namespace spot expansion_t - expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts) + expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen) { using exp_t = std::multimap; @@ -413,8 +441,8 @@ namespace spot return {{f_bdd, formula::eword()}}; } - auto rec = [&d, owner, opts](formula f){ - return expansion(f, d, owner, exp_opts::None); + auto rec = [&d, owner, seen](formula f){ + return expansion(f, d, owner, exp_opts::None, seen); }; @@ -426,7 +454,8 @@ namespace spot SPOT_UNREACHABLE(); case op::eword: - return {{bddfalse, formula::ff()}}; + // return {{bddfalse, formula::ff()}}; + return {}; case op::Concat: { @@ -447,7 +476,7 @@ namespace spot } } - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -484,7 +513,7 @@ namespace spot if (f.min() == 0) res.insert({bddtrue, formula::eword()}); - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -503,7 +532,7 @@ namespace spot res.insert({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})}); } - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -511,7 +540,7 @@ namespace spot { formula rewrite = rewrite_and_nlm(f); auto res = rec(rewrite); - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -541,7 +570,7 @@ namespace spot { for (auto& [_, dest] : res) dest = formula::first_match(dest); - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -561,7 +590,7 @@ namespace spot for (auto& [_, dest] : res_det) dest = formula::first_match(dest); - finalize(res_det, opts, d); + finalize(res_det, opts, d, seen); return res_det; } @@ -586,7 +615,7 @@ namespace spot res.insert({li, formula::Fusion({ei, F})}); } - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -636,7 +665,7 @@ namespace spot res = std::move(new_res); } - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -659,7 +688,7 @@ namespace spot res.insert({label, dest}); } - finalize(res, opts, d); + finalize(res, opts, d, seen); return res; } @@ -709,6 +738,8 @@ namespace spot auto formula2state = robin_hood::unordered_map(); auto signature2state = std::unordered_map, unsigned, signature_hash>(); + auto seen = std::unordered_set(); + seen.insert(f); unsigned init_state = aut->new_state(); aut->set_init_state(init_state); @@ -720,7 +751,7 @@ namespace spot aut->register_ap(ap); if (signature_merge) - signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts)}, init_state}); + signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts, &seen)}, init_state}); auto todo = std::vector>(); @@ -743,7 +774,7 @@ namespace spot { if (signature_merge) { - auto exp = expansion(suffix, d, aut.get(), opts); + auto exp = expansion(suffix, d, aut.get(), opts, &seen); bool accepting = suffix.accepts_eword(); auto it2 = signature2state.find({accepting, exp}); if (it2 != signature2state.end()) @@ -755,10 +786,11 @@ namespace spot dst = aut->new_state(); todo.push_back({suffix, dst}); + seen.insert(suffix); formula2state.insert({suffix, dst}); if (signature_merge) - signature2state.insert({{suffix.accepts_eword(), expansion(suffix, d, aut.get(), opts)}, dst}); + signature2state.insert({{suffix.accepts_eword(), expansion(suffix, d, aut.get(), opts, &seen)}, dst}); std::ostringstream ss; ss << suffix; @@ -777,11 +809,12 @@ namespace spot ? acc_mark : acc_cond::mark_t(); - auto exp = expansion(curr_f, d, aut.get(), opts); + auto exp = expansion(curr_f, d, aut.get(), opts, &seen); for (const auto& [letter, suffix] : exp) { if (suffix.is(op::ff)) + // TODO ASSERT NOT continue; auto dst = find_dst(suffix); diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh index eba71db9e..36476bd31 100644 --- a/spot/tl/expansions.hh +++ b/spot/tl/expansions.hh @@ -45,11 +45,12 @@ namespace spot MergeEdges = 64, SignatureMerge = 128, Determinize = 256, + UniquePrefixSeenOpt = 512, }; }; SPOT_API expansion_t - expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts); + expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen = nullptr); SPOT_API twa_graph_ptr expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);