From d326c17456d1a889a60ebb4d94e1f45916af364e Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Thu, 12 Oct 2023 15:04:40 +0200
Subject: [PATCH] expansions: expose easy expansion in python

---
 python/spot/impl.i    |  2 ++
 spot/tl/expansions.cc | 15 +++++++++++++++
 spot/tl/expansions.hh |  3 +++
 3 files changed, 20 insertions(+)

diff --git a/python/spot/impl.i b/python/spot/impl.i
index 725655c08..ee2c6a81e 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -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>
diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc
index ea1ec4b95..263f9a182 100644
--- a/spot/tl/expansions.cc
+++ b/spot/tl/expansions.cc
@@ -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)
diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh
index 9a350dbb8..036ac945a 100644
--- a/spot/tl/expansions.hh
+++ b/spot/tl/expansions.hh
@@ -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);