introduce partitioned_relabel_here

Function taking an automaton and trying to relabel
it by partitioning the old conditions and encode the
different subsets of the partition with new variables

* spot/priv/Makefile.am: Add
* spot/priv/partitioned_relabel.hh
, spot/priv/partitioned_relabel.cc: try_partition_me,
computes the partition of a given vector of bdds
* spot/twaalgos/relabel.hh
, spot/twaalgos/relabel.cc: Here. Adapt also relabel()
to cope with the different type of relabeling_maps
* tests/python/_partitioned_relabel.ipynb
, tests/python/except.py: Test and Usage
* tests/Makefile.am: Add test

spot/priv/Makefile.am

@@ -29,6 +29,8 @@ libpriv_la_SOURCES = \
   bddalloc.hh \
   freelist.cc \
   freelist.hh \
+  partitioned_relabel.cc \
+  partitioned_relabel.hh \
   robin_hood.hh \
   satcommon.hh\
   satcommon.cc\

spot/priv/partitioned_relabel.cc

@@ -0,0 +1,147 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2022 Laboratoire de Recherche
+// de l'Epita (LRE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "config.h"
+
+#include <spot/priv/partitioned_relabel.hh>
+
+
+relabeling_map
+bdd_partition::to_relabeling_map(twa_graph& for_me) const
+{
+  relabeling_map res;
+  // Change to unordered_map?
+  bdd_dict_ptr bdddict = for_me.get_dict();
+
+  bool use_inner = ig->state_storage(0).new_label != bddfalse;
+  std::vector<bool> doskip
+      = use_inner ? std::vector<bool>(ig->num_states(), false)
+                  : std::vector<bool>();
+
+  auto bdd2form = [&bdddict](const bdd& cond)
+    {
+      return bdd_to_formula(cond, bdddict);
+    };
+
+  for (const auto& [old_letter, s] : treated)
+    {
+      formula new_letter_form = bdd2form(ig->state_storage(s).new_label);
+      assert(res.count(new_letter_form) == 0);
+      if (use_inner)
+          doskip[s] = true;
+      res[new_letter_form] = bdd2form(old_letter);
+    }
+
+  if (use_inner)
+    {
+      // This implies that the split option was false,
+      // so we can store further info
+      auto& all_cond = *all_cond_ptr;
+      const unsigned Norig = all_cond.size();
+
+      for (unsigned i = 0; i < Norig; ++i)
+        {
+          // Internal node -> new ?
+          if (doskip[i])
+              continue;
+          // Leave node -> already exists
+          if (ig->state_storage(i).succ == 0)
+              continue;
+          doskip[i] = true;
+          formula new_letter_form
+              = bdd2form(ig->state_storage(i).new_label);
+#ifdef NDEBUG
+          res[new_letter_form] = bdd2form(all_cond[i]);
+#else
+          // Check if they are the same
+          formula old_form = bdd2form(all_cond[i]);
+          if (res.count(new_letter_form) == 0)
+              res[new_letter_form] = old_form;
+          else
+              assert(res[new_letter_form] == old_form);
+#endif
+        }
+      }
+  return res;
+}
+
+/// \brief Tries to partition the given condition vector \a all_cond
+/// abandons at \a max_letter.
+/// \return The corresponding bdd_partition
+/// \note A pointer to all_cond is captured internally, it needs
+/// to outlive the returned bdd_partition
+bdd_partition
+try_partition_me(const std::vector<bdd>& all_cond, unsigned max_letter)
+{
+  // We create vector that will be succesively filled.
+  // Each entry corresponds to a "letter", of the partition
+  const size_t Norig = all_cond.size();
+
+  bdd_partition result(all_cond);
+
+  auto& treated = result.treated;
+  auto& ig = *result.ig;
+
+  for (unsigned io = 0; io < Norig; ++io)
+    {
+      bdd cond = all_cond[io];
+      const auto Nt = treated.size();
+      for (size_t in = 0; in < Nt; ++in)
+        {
+          if (cond == bddfalse)
+            break;
+          if (treated[in].first == cond)
+            {
+              // Found this very condition -> make transition
+              ig.new_edge(io, treated[in].second);
+              cond = bddfalse;
+              break;
+            }
+          if (bdd_have_common_assignment(treated[in].first, cond))
+            {
+              bdd inter = treated[in].first & cond;
+              // Create two new states
+              unsigned ssplit = ig.new_states(2);
+              // ssplit becomes the state without the intersection
+              // ssplit + 1 becomes the intersection
+              // Both of them are implied by the original node,
+              // Only inter is implied by the current letter
+              ig.new_edge(treated[in].second, ssplit);
+              ig.new_edge(treated[in].second, ssplit+1);
+              ig.new_edge(io, ssplit+1);
+              treated.emplace_back(inter, ssplit+1);
+              // Update
+              cond -= inter;
+              treated[in].first -= inter;
+              treated[in].second = ssplit;
+              if (treated.size() > max_letter)
+                return bdd_partition{};
+            }
+        }
+        if (cond != bddfalse)
+          {
+            unsigned sc = ig.new_state();
+            treated.emplace_back(cond, sc);
+            ig.new_edge(io, sc);
+          }
+    }
+
+  result.relabel_succ = true;
+  return result;
+}

spot/priv/partitioned_relabel.hh

@@ -0,0 +1,81 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2022 Laboratoire de Recherche
+// de l'Epita (LRE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <bddx.h>
+#include <spot/graph/graph.hh>
+#include <spot/tl/formula.hh>
+#include <spot/tl/relabel.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/formula2bdd.hh>
+#include <spot/twa/twagraph.hh>
+
+
+using namespace spot;
+
+struct bdd_partition
+{
+  struct S
+  {
+    bdd new_label = bddfalse;
+  };
+  struct T
+  {
+  };
+  using implication_graph = digraph<S, T>;
+
+  // A pointer to the conditions to be partitioned
+  const std::vector<bdd>* all_cond_ptr;
+  // Graph with the invariant that
+  // children imply parents
+  // Leaves from the partition
+  // original conditions are "root" nodes
+  std::unique_ptr<implication_graph> ig;
+  // todo: technically there are at most two successors, so a graph
+  // is "too" generic
+  // All conditions currently part of the partition
+  // unsigned corresponds to the associated node
+  std::vector<std::pair<bdd, unsigned>> treated;
+  std::vector<formula> new_aps;
+  bool relabel_succ = false;
+
+  bdd_partition() = default;
+  bdd_partition(const std::vector<bdd>& all_cond)
+    : all_cond_ptr(&all_cond)
+    , ig{std::make_unique<implication_graph>(2*all_cond.size(),
+                                             2*all_cond.size())}
+  {
+    // Create the roots of all old conditions
+    // Each condition is associated to the state with
+    // the same index
+    const unsigned Norig = all_cond.size();
+    ig->new_states(Norig);
+  }
+
+  // Facilitate conversion
+  // This can only be called when letters have already
+  // been computed
+  relabeling_map
+  to_relabeling_map(twa_graph& for_me) const;
+}; // bdd_partition
+
+
+bdd_partition
+try_partition_me(const std::vector<bdd>& all_cond, unsigned max_letter);

spot/twaalgos/relabel.cc

@@ -20,60 +20,275 @@
 #include "config.h"
 #include <spot/twaalgos/relabel.hh>
 #include <spot/twa/formula2bdd.hh>
+#include <spot/tl/formula.hh>
+
+#include <spot/priv/partitioned_relabel.hh>
+
+#include <cmath>
+#include <algorithm>
+#include <iostream>
+
 
 namespace spot
 {
-  void
+  namespace
-  relabel_here(twa_graph_ptr& aut, relabeling_map* relmap)
   {
-    std::unique_ptr<bddPair> pairs(bdd_newpair());
-    auto d = aut->get_dict();
-    std::vector<int> vars;
-    std::set<int> newvars;
-    vars.reserve(relmap->size());
-    bool bool_subst = false;
-    auto aplist = aut->ap();
 
-    for (auto& p: *relmap)
+    void
-      {
+    comp_new_letters(bdd_partition& part,
-        if (!p.first.is(op::ap))
+                    twa_graph& aut,
-          throw std::runtime_error
+                    const std::string& var_prefix,
-            ("relabel_here: old labels should be atomic propositions");
+                    bool split)
-        if (!p.second.is_boolean())
+    {
-          throw std::runtime_error
+      auto& ig = *part.ig;
-            ("relabel_here: new labels should be Boolean formulas");
+      const auto& treated = part.treated;
+      auto& new_aps = part.new_aps;
+      // Get the new variables and their negations
+      const unsigned Nnl = treated.size();
+      const unsigned Nnv = std::ceil(std::log2(Nnl));
+      std::vector<std::array<bdd, 2>> Nv_vec(Nnv);
 
-        // Don't attempt to rename APs that are not used.
+      new_aps.reserve(Nnv);
-        if (std::find(aplist.begin(), aplist.end(), p.first) == aplist.end())
+      for (unsigned i = 0; i < Nnv; ++i)
-          continue;
+        {
+          // todo check if it does not exist / use anonymous?
+          new_aps.push_back(formula::ap(var_prefix+std::to_string(i)));
+          int v = aut.register_ap(new_aps.back());
+          Nv_vec[i] = {bdd_nithvar(v), bdd_ithvar(v)};
+        }
 
-        int oldv = aut->register_ap(p.first);
+      auto leaveidx2label = [&](unsigned idx)
-        vars.emplace_back(oldv);
+        {
-        if (p.second.is(op::ap))
+          unsigned c = 0;
-          {
+          unsigned rem = idx;
-            int newv = aut->register_ap(p.second);
+          bdd thisbdd = bddtrue;
-            newvars.insert(newv);
+          while (rem)
-            bdd_setpair(pairs.get(), oldv, newv);
+            {
-          }
+              thisbdd &= Nv_vec[c][rem & 1];
-        else
+              ++c;
-          {
+              rem >>= 1;
-            p.second.traverse([&](const formula& f)
+            }
-                              {
+          for (; c < Nnv; ++c)
-                                if (f.is(op::ap))
+            thisbdd &= Nv_vec[c][0];
-                                  newvars.insert(aut->register_ap(f));
+          return thisbdd;
-                                return false;
+        };
-                              });
+
-            bdd newb = formula_to_bdd(p.second, d, aut);
+      // Compute only labels of leaves
-            bdd_setbddpair(pairs.get(), oldv, newb);
+      for (unsigned idx = 0; idx < Nnl; ++idx)
-            bool_subst = true;
+        ig.state_storage(treated[idx].second).new_label = leaveidx2label(idx);
-          }
+
+      // We will label the implication graph with the new letters
+      auto relabel_impl = [&](unsigned s, auto&& relabel_impl_rec)
+        {
+          auto& ss = ig.state_storage(s);
+          if (ss.new_label != bddfalse)
+            return ss.new_label;
+          else
+            {
+              assert((ss.succ != 0) && "Should not be a leave");
+              bdd thisbdd = bddfalse;
+              for (const auto& e : ig.out(s))
+                thisbdd |= relabel_impl_rec(e.dst, relabel_impl_rec);
+              ss.new_label = thisbdd;
+              return thisbdd;
+            }
+        };
+
+      if (!split)
+        {
+          // For split only leaves is ok,
+          // disjunction is done via transitions
+          // This will compute the new_label for all states in the ig
+          const unsigned Norig = part.all_cond_ptr->size();
+          for (unsigned i = 0; i < Norig; ++i)
+            relabel_impl(i, relabel_impl);
+        }
+    } // comp_new_letters
+
+    // Recursive traversal of implication graph
+    void replace_label_(unsigned si,
+                        unsigned esrc, unsigned edst,
+                        bdd& econd,
+                        const bdd_partition::implication_graph& ig,
+                        twa_graph& aut)
+    {
+      auto& sstore = ig.state_storage(si);
+      if (sstore.succ == 0)
+        {
+          if (econd == bddfalse)
+            econd = sstore.new_label;
+          else
+            aut.new_edge(esrc, edst, sstore.new_label);
+        }
+      else
+        {
+          for (const auto& e_ig : ig.out(si))
+            replace_label_(e_ig.dst, esrc, edst, econd, ig, aut);
+        }
+    }
+
+    relabeling_map
+    partitioned_relabel_here_(twa_graph& aut, bool split,
+                              unsigned max_letter,
+                              unsigned max_letter_mult,
+                              const bdd& concerned_ap,
+                              bool treat_all,
+                              const std::string& var_prefix)
+    {
+      auto abandon = []()
+        {
+          return relabeling_map{};
+        };
+
+
+      // When split we need to distiguish effectively new and old edges
+      if (split)
+        {
+          aut.get_graph().remove_dead_edges_();
+          aut.get_graph().sort_edges_();
+          aut.get_graph().chain_edges_();
+        }
+
+      // Get all conditions present in the automaton
+      std::vector<bdd> all_cond;
+      bdd ignoredcon = bddtrue;
+      std::unordered_map<int, unsigned> all_cond_id2idx;
+
+      all_cond.reserve(0.1*aut.num_edges());
+      all_cond_id2idx.reserve(0.1*aut.num_edges());
+
+      // Map for all supports
+      // and whether or not they are to be relabeled
+      std::unordered_map<bdd, std::pair<bool, bdd>, bdd_hash> all_supports;
+
+      for (const auto& e : aut.edges())
+        {
+          auto it = all_supports.find(e.cond);
+          if (it != all_supports.end())
+            continue; // Already treated
+          bdd se = bddtrue;
+          bool is_concerned = true;
+          if (!treat_all)
+            {
+              se = bdd_support(e.cond);
+              is_concerned = bdd_implies(concerned_ap, se);
+            }
+
+          all_supports.emplace(e.cond,
+                               std::make_pair(is_concerned, se));
+
+          if (!is_concerned)
+            {
+              assert(bdd_existcomp(se, concerned_ap) == bddtrue
+                     && "APs are not partitioned");
+              continue;
+            }
+
+          auto [_, ins] =
+              all_cond_id2idx.try_emplace(e.cond.id(), all_cond.size());
+          if (ins)
+            {
+              all_cond.push_back(e.cond);
+              if (all_cond.size() > max_letter)
+                return abandon();
+            }
+        }
+
+      unsigned stop = max_letter;
+      if (max_letter_mult != -1u)
+        {
+          // Make sure it does not overflow
+          if (max_letter_mult <= (-1u / ((unsigned) all_cond.size())))
+            stop = std::min(stop,
+                            (unsigned) (max_letter_mult*all_cond.size()));
+        }
+
+      auto this_partition = try_partition_me(all_cond, stop);
+
+      if (!this_partition.relabel_succ)
+        return abandon();
+
+      comp_new_letters(this_partition, aut, var_prefix, split);
+
+      // An original condition is represented by all leaves that imply it
+      auto& ig = *this_partition.ig;
+      const unsigned Ns = aut.num_states();
+      const unsigned Nt = aut.num_edges();
+      for (unsigned s = 0; s < Ns; ++s)
+        {
+          for (auto& e : aut.out(s))
+            {
+              if (aut.edge_number(e) > Nt)
+                continue;
+              if (!all_supports.at(e.cond).first)
+                continue; // Edge not concerned
+              unsigned idx = all_cond_id2idx[e.cond.id()];
+
+              if (split)
+                {
+                  // initial call
+                  // We can not hold a ref to the edge
+                  // as the edgevector might get reallocated
+                  bdd econd = bddfalse;
+                  unsigned eidx = aut.edge_number(e);
+                  replace_label_(idx, e.src, e.dst,
+                                econd, ig, aut);
+                  aut.edge_storage(eidx).cond = econd;
+                }
+              else
+                e.cond = ig.state_storage(idx).new_label;
+            } // for edge
+        } // for state
+      return this_partition.to_relabeling_map(aut);
+    }
+
+    void
+    relabel_here_ap_(twa_graph_ptr& aut_ptr, relabeling_map relmap)
+    {
+      assert(aut_ptr);
+      twa_graph& aut = *aut_ptr;
+
+      std::unique_ptr<bddPair> pairs(bdd_newpair());
+      auto d = aut.get_dict();
+      std::vector<int> vars;
+      std::set<int> newvars;
+      vars.reserve(relmap.size());
+      bool bool_subst = false;
+      auto aplist = aut.ap();
+
+      for (auto& p: relmap)
+        {
+          // Don't attempt to rename APs that are not used.
+          if (std::find(aplist.begin(), aplist.end(), p.first) == aplist.end())
+            continue;
+
+          int oldv = aut.register_ap(p.first);
+          vars.emplace_back(oldv);
+          if (p.second.is(op::ap))
+            {
+              int newv = aut.register_ap(p.second);
+              newvars.insert(newv);
+              bdd_setpair(pairs.get(), oldv, newv);
+            }
+          else
+            {
+              p.second.traverse([&](const formula& f)
+                                {
+                                  if (f.is(op::ap))
+                                    newvars.insert(aut.register_ap(f));
+                                  return false;
+                                });
+              bdd newb = formula_to_bdd(p.second, d, aut_ptr);
+              bdd_setbddpair(pairs.get(), oldv, newb);
+              bool_subst = true;
+            }
       }
 
     bool need_cleanup = false;
     typedef bdd (*op_t)(const bdd&, bddPair*);
     op_t op = bool_subst ?
       static_cast<op_t>(bdd_veccompose) : static_cast<op_t>(bdd_replace);
-    for (auto& t: aut->edges())
+    for (auto& t: aut.edges())
       {
         bdd c = (*op)(t.cond, pairs.get());
         t.cond = c;
@@ -86,14 +301,172 @@ namespace spot
     // p0)
     for (auto v: vars)
       if (newvars.find(v) == newvars.end())
-        aut->unregister_ap(v);
+        aut.unregister_ap(v);
 
     // If some of the edges were relabeled false, we need to clean the
     // automaton.
     if (need_cleanup)
       {
-        aut->merge_edges();     // remove any edge labeled by 0
+        aut.merge_edges();     // remove any edge labeled by 0
-        aut->purge_dead_states(); // remove useless states
+        aut.purge_dead_states(); // remove useless states
       }
+    }
+
+  void
+  relabel_here_gen_(twa_graph_ptr& aut_ptr, relabeling_map relmap)
+    {
+      assert(aut_ptr);
+      twa_graph& aut = *aut_ptr;
+
+      auto form2bdd = [this_dict = aut.get_dict()](const formula& f)
+        {
+          return formula_to_bdd(f, this_dict, this_dict);
+        };
+
+      auto bdd2form = [bdddict = aut.get_dict()](const bdd& cond)
+        {
+          return bdd_to_formula(cond, bdddict);
+        };
+
+
+      // translate formula -> bdd
+      std::unordered_map<bdd, bdd, bdd_hash> base_letters;
+      base_letters.reserve(relmap.size());
+
+      std::unordered_map<bdd, bdd, bdd_hash> comp_letters;
+      std::unordered_set<bdd, bdd_hash> ignored_letters;
+
+      // Necessary to detect unused
+      bdd new_var_supp = bddtrue;
+      auto translate = [&](bdd& cond)
+        {
+          // Check if known
+          for (const auto& map : {base_letters, comp_letters})
+            {
+              auto it = map.find(cond);
+              if (it != map.end())
+                {
+                  cond = it->second;
+                  return;
+                }
+            }
+
+          // Check if known to be ignored
+          if (auto it = ignored_letters.find(cond);
+                it != ignored_letters.end())
+            return;
+
+          // Check if ignored
+          bdd cond_supp = bdd_support(cond);
+          if (!bdd_implies(new_var_supp, cond_supp))
+            {
+              ignored_letters.insert(cond);
+              assert(bdd_existcomp(cond_supp, new_var_supp) == bddtrue
+                     && "APs are not partitioned");
+              return;
+            }
+
+          // Compute
+          // compose the given cond from a disjunction of base_letters
+          bdd old_cond = bddfalse;
+          for (const auto& [k, v] : base_letters)
+            {
+              if (bdd_implies(k, cond))
+                old_cond |= v;
+            }
+          comp_letters[cond] = old_cond;
+          cond = old_cond;
+          return;
+        };
+
+      for (const auto& [new_f, old_f] : relmap)
+        {
+          bdd new_cond = form2bdd(new_f);
+          new_var_supp &= bdd_support(new_cond);
+          base_letters[new_cond] = form2bdd(old_f);
+        }
+
+
+      // Save the composed letters? With a special seperator like T/F?
+      // Is swapping between formula <-> bdd expensive
+      for (auto& e : aut.edges())
+        translate(e.cond);
+
+      // Remove the new auxilliary variables from the aut
+      bdd c_supp = new_var_supp;
+      while (c_supp != bddtrue)
+        {
+          aut.unregister_ap(bdd_var(c_supp));
+          c_supp = bdd_high(c_supp);
+        }
+
+      return;
+    }
+
+  } // Namespace
+
+  void
+  relabel_here(twa_graph_ptr& aut, relabeling_map* relmap)
+  {
+    if (!relmap || relmap->empty())
+      return;
+
+    // There are two different types of relabeling maps:
+    // 1) The "traditional":
+    // New atomic propositions (keys) correspond to general formulas over
+    // the original propositions (values)
+    // 2) The one resulting from partitioned_relabel_here
+    // Here general (boolean) formulas over new propositions (keys)
+    // are associated to general formulas over
+    // the original propositions (values)
+
+    if (!std::all_of(relmap->begin(), relmap->end(),
+                    [](const auto& it){return it.first.is_boolean()
+                                              && it.second.is_boolean(); }))
+      throw std::runtime_error
+            ("relabel_here: old labels and new labels "
+             "should be Boolean formulas");
+
+    bool only_ap = std::all_of(relmap->cbegin(), relmap->cend(),
+                               [](const auto& p)
+                                 {
+                                   return p.first.is(op::ap);
+                                 });
+
+    if (only_ap)
+      relabel_here_ap_(aut, *relmap);
+    else
+      relabel_here_gen_(aut, *relmap);
+  }
+
+  relabeling_map
+  partitioned_relabel_here(twa_graph_ptr& aut,
+                           bool split,
+                           unsigned max_letter,
+                           unsigned max_letter_mult,
+                           const bdd& concerned_ap,
+                           std::string var_prefix)
+  {
+    if (!aut)
+      throw std::runtime_error("aut is null!");
+
+    if (std::find_if(aut->ap().cbegin(), aut->ap().cend(),
+                     [var_prefix](const auto& ap)
+                      {
+                        return ap.ap_name().find(var_prefix) == 0;
+                      }) != aut->ap().cend())
+      throw std::runtime_error("partitioned_relabel_here(): "
+          "The given prefix for new variables may not appear as "
+          "a prefix of existing variables.");
+
+    // If concerned_ap == bddtrue -> all aps are concerned
+    bool treat_all = concerned_ap == bddtrue;
+    bdd concerned_ap_
+      = treat_all ? aut->ap_vars() : concerned_ap;
+    return partitioned_relabel_here_(*aut, split,
+                                     max_letter, max_letter_mult,
+                                     concerned_ap_,
+                                     treat_all,
+                                     var_prefix);
   }
 }

spot/twaalgos/relabel.hh

@@ -21,6 +21,10 @@
 
 #include <spot/tl/relabel.hh>
 #include <spot/twa/twagraph.hh>
+#include <spot/misc/bddlt.hh>
+
+#include <optional>
+#include <functional>
 
 namespace spot
 {
@@ -33,4 +37,33 @@ namespace spot
   /// or relabel_bse().
   SPOT_API void
   relabel_here(twa_graph_ptr& aut, relabeling_map* relmap);
+
+
+  /// \brief Replace conditions in \a aut with non-overlapping conditions
+  /// over fresh variables.
+  ///
+  /// Partitions the conditions in the automaton, then (binary) encodes
+  /// them using fresh propositions.
+  /// This can lead to an exponential explosion in the number of
+  /// conditions. The operations is aborted if either
+  /// the number of new letters (subsets of the partition) exceeds
+  /// \a max_letter OR \a max_letter_mult times the number of conditions
+  ///  in the original automaton.
+  /// The argument \a concerned_ap can be used to filter out transitions.
+  /// If given, only the transitions whose support intersects the
+  /// concerned_ap (or whose condition is T) are taken into account.
+  /// The fresh aps will be enumerated and prefixed by \a var_prefix.
+  /// These variables need to be fresh, i.e. may not exist yet (not checked)
+  ///
+  /// \note If concerned_ap is given, then there may not be an edge
+  /// whose condition uses ap inside AND outside of concerned_ap.
+  /// Mostly used in a game setting to distinguish between
+  /// env and player transitions.
+  SPOT_API relabeling_map
+  partitioned_relabel_here(twa_graph_ptr& aut, bool split = false,
+                           unsigned max_letter = -1u,
+                           unsigned max_letter_mult = -1u,
+                           const bdd& concerned_ap = bddtrue,
+                           std::string var_prefix = "__nv");
+
 }

tests/Makefile.am

@@ -436,6 +436,7 @@ TESTS_python = \
   python/origstate.py \
   python/otfcrash.py \
   python/parsetgba.py \
+  python/_partitioned_relabel.ipynb \
   python/parity.py \
   python/pdegen.py \
   python/prodexpt.py \

tests/python/except.py

@@ -359,3 +359,18 @@ except RuntimeError as e:
     tc.assertIn(filename, str(e))
 else:
     report_missing_exception()
+
+
+# Relabeling must use new variables
+aut = spot.make_twa_graph()
+aut.new_states(2)
+ap = buddy.bdd_ithvar(aut.register_ap("__nv0"))
+aut.new_edge(0,1,ap)
+
+try:
+    spot.partitioned_relabel_here(aut)
+except RuntimeError as e:
+    tc.assertIn("The given prefix for new variables",
+                str(e))
+else:
+    report_missing_exception()