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

expansions: expose easy expansion in python

Browse source
This commit is contained in:
Antoine Martin 2023-10-12 15:04:40 +02:00
parent 49f3c18ae3
commit b04c4d7fd9
3 changed files with 20 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
python/spot/impl.i
View file

@ -527,6 +527,8 @@ namespace std {
%template(pair_formula_vectorstring) pair<spot::formula, vector<string>>;
%template(atomic_prop_set) set<spot::formula>;
%template(relabeling_map) map<spot::formula, spot::formula>;
%template(pair_formula) pair<spot::formula, spot::formula>;
%template(vector_pair_formula) vector<pair<spot::formula, spot::formula>>;
}
%include <spot/tl/environment.hh>

15
spot/tl/expansions.cc
View file

@ -449,6 +449,21 @@ namespace spot
}
}
std::vector<std::pair<formula, formula>>
expansion_simple(formula f)
{
int owner = 42;
auto d = make_bdd_dict();
auto exp = expansion(f, d, &owner, exp_opts::None);
std::vector<std::pair<formula, formula>> res;
for (const auto& [bdd, f] : exp)
res.push_back({bdd_to_formula(bdd, d), f});
d->unregister_all_my_variables(&owner);
return res;
}
expansion_t
expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen)

3
spot/tl/expansions.hh
View file

@ -50,6 +50,9 @@ namespace spot
};
};
SPOT_API std::vector<std::pair<formula, formula>>
expansion_simple(formula f);
SPOT_API expansion_t
expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen = nullptr);