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

derive: option for some optimisations

Browse source
This commit is contained in:
Antoine Martin 2022-11-10 07:18:29 +01:00
parent 13f953c27f
commit 9953cacbc6
2 changed files with 22 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

17
spot/tl/derive.cc
View file

@ -204,7 +204,7 @@ namespace spot
twa_graph_ptr
derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic)
bool deterministic, derive_opts options)
{
auto aut = make_twa_graph(bdd_dict);
@ -264,7 +264,7 @@ namespace spot
for (const bdd one : minterms_of(firsts, firsts_support))
{
formula derivative =
partial_derivation(curr_f, one, bdd_dict, aut.get());
partial_derivation(curr_f, one, bdd_dict, aut.get(), options);
// no transition possible from this letter
if (derivative.is(op::ff))
@ -422,7 +422,7 @@ namespace spot
formula
partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d,
void* owner)
void* owner, derive_opts options)
{
if (f.is_boolean())
{
@ -472,6 +472,17 @@ namespace spot
formula d_E = partial_derivation(f[0], var, d, owner);
if (options.concat_star_distribute && !f[0].is_finite() && d_E.is(op::OrRat))
{
std::vector<formula> distributed;
for (auto g : d_E)
{
distributed.push_back(formula::Concat({g, formula::Star(f[0], min, max)}));
}
return formula::OrRat(distributed);
}
return formula::Concat({ d_E, formula::Star(f[0], min, max) });
}

10
spot/tl/derive.hh
View file

@ -29,11 +29,17 @@
namespace spot
{
struct derive_opts
{
bool concat_star_distribute = true;
};
/// \ingroup tl_misc
/// \brief Produce a SERE formula's partial derivative
SPOT_API formula
partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d,
void* owner);
void* owner, derive_opts options = {});
SPOT_API twa_graph_ptr
derive_automaton(formula f, bool deterministic = true);
@ -47,7 +53,7 @@ namespace spot
SPOT_API twa_graph_ptr
derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic = true);
bool deterministic = true, derive_opts options = {});
SPOT_API formula
rewrite_and_nlm(formula f);