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

expansions: optimize sigma star encoding

Browse source
This commit is contained in:
Antoine Martin 2023-04-04 14:52:14 +02:00
parent a4091ffc37
commit bbbcdc331a
2 changed files with 28 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

31
spot/tl/expansions.cc
View file

@ -106,9 +106,10 @@ namespace spot
class bdd_finalizer
{
public:
bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& exp, bdd_dict_ptr d)
bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& exp, bdd_dict_ptr d, bool opt_sigma_star)
: anon_set_(bddtrue)
, d_(d)
, opt_sigma_star_(opt_sigma_star)
{
for (const auto& [prefix, suffix] : exp)
{
@ -120,12 +121,25 @@ namespace spot
}
else
{
anon_var_num = d_->register_anonymous_variables(1, this);
if (opt_sigma_star_ && (suffix.is(op::Star)
&& suffix[0].is(op::tt)
&& suffix.min() == 0
&& suffix.max() == formula::unbounded()))
{
anon_var_num = -1;
}
else
{
anon_var_num = d_->register_anonymous_variables(1, this);
}
formula2bdd_.insert({suffix, anon_var_num});
bdd2formula_.insert({anon_var_num, suffix});
}
bdd var = bdd_ithvar(anon_var_num);
bdd var = bddtrue;
if (anon_var_num != -1)
var = bdd_ithvar(anon_var_num);
anon_set_ &= var;
exp_ |= prefix & var;
}
@ -145,6 +159,7 @@ namespace spot
std::map<formula, int> formula2bdd_;
std::map<int, formula> bdd2formula_;
bdd_dict_ptr d_;
bool opt_sigma_star_;
formula var_to_formula(int var);
formula conj_bdd_to_sere(bdd b);
@ -177,7 +192,13 @@ namespace spot
bdd_finalizer::conj_bdd_to_sere(bdd b)
{
if (b == bddtrue)
return formula::tt();
{
if (opt_sigma_star_){
return formula::Star(formula::tt(), 0, formula::unbounded());
} else {
return formula::tt();
}
}
if (b == bddfalse)
return formula::ff();
@ -261,7 +282,7 @@ namespace spot
if (opts & (exp_opts::expand_opt::BddIsop
| exp_opts::expand_opt::BddMinterm))
{
bdd_finalizer bddf(exp, d);
bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar);
exp = bddf.simplify(opts);
}

3
spot/tl/expansions.hh
View file

@ -40,7 +40,8 @@ namespace spot
UniquePrefix = 2,
BddIsop = 4,
BddMinterm = 8,
MergeEdges = 16,
BddSigmaStar = 16,
MergeEdges = 32,
};
};