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 90ea02d42a
commit ed3d1ef4aa
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

@ -547,6 +547,8 @@ namespace std {
%template(vectorofvectorofformulas) vector<vector<spot::formula>>;
%template(setunsigned) set<unsigned>;
%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);