expansions: split

python/spot/impl.i

@@ -89,6 +89,7 @@
 #include <spot/tl/derive.hh>
 #include <spot/tl/dot.hh>
 #include <spot/tl/expansions.hh>
+#include <spot/tl/expansions2.hh>
 #include <spot/tl/nenoform.hh>
 #include <spot/tl/print.hh>
 #include <spot/tl/simplify.hh>
@@ -638,6 +639,7 @@ namespace std {
 %include <spot/tl/contain.hh>
 %include <spot/tl/derive.hh>
 %include <spot/tl/expansions.hh>
+%include <spot/tl/expansions2.hh>
 %include <spot/tl/dot.hh>
 %include <spot/tl/nenoform.hh>
 %include <spot/tl/sonf.hh>

spot/tl/Makefile.am

@@ -32,7 +32,7 @@ tl_HEADERS =					\
   dot.hh					\
   environment.hh				\
   exclusive.hh					\
-  expansions.hh					\
+  expansions2.hh					\
   formula.hh					\
   hierarchy.hh					\
   length.hh					\
@@ -60,6 +60,7 @@ libtl_la_SOURCES =				\
   dot.cc					\
   exclusive.cc					\
   expansions.cc					\
+  expansions2.cc					\
   formula.cc					\
   hierarchy.cc					\
   length.cc					\

spot/tl/expansions.cc

@@ -278,11 +278,11 @@ namespace spot
           bdd dest_bdd = bdd_restrict(exp_, letter);
           formula dest = bdd_to_sere(dest_bdd);
 
-          #ifndef NDEBUG
+          // #ifndef NDEBUG
-          // make sure it didn't exist before
+          // // make sure it didn't exist before
-          auto it = std::find(res.begin(), res.end(), {letter, dest});
+          // auto it = std::find(res.begin(), res.end(), {letter, dest});
-          SPOT_ASSERT(it == res.end());
+          // SPOT_ASSERT(it == res.end());
-          #endif
+          // #endif
 
           res.push_back({letter, dest});
         }
@@ -338,7 +338,7 @@ namespace spot
 
       expansion_t res;
 
-      for (const auto [prefix, suffix] : unique_map)
+      for (const auto& [prefix, suffix] : unique_map)
       {
         if (!suffix.is(op::OrRat))
         {
@@ -435,17 +435,22 @@ namespace spot
         }
 
         exp.clear();
-        for (const auto [suffix, prefix] : unique_map)
+        for (const auto& [suffix, prefix] : unique_map)
         {
           exp.push_back({prefix, suffix});
         }
       }
 
-      if (opts & exp_opts::expand_opt::UniquePrefix)
+      if (opts & exp_opts::expand_opt::UniquePrefix
+          || opts & exp_opts::expand_opt::UniquePrefixSeenOpt
+          || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
       {
-        exp = unique_prefix(exp);
+        if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
-        //exp = unique_prefix_seen(exp, seen);
+          exp = unique_prefix_seen(exp, seen);
-        //exp = unique_prefix_count(exp, seen);
+        else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+          exp = unique_prefix_count(exp, seen);
+        else
+          exp = unique_prefix(exp);
       }
 
       if (opts & exp_opts::expand_opt::UniqueSuffixPost)
@@ -462,7 +467,7 @@ namespace spot
         }
 
         exp.clear();
-        for (const auto [suffix, prefix] : unique_map)
+        for (const auto& [suffix, prefix] : unique_map)
         {
           exp.push_back({prefix, suffix});
         }
@@ -817,7 +822,7 @@ namespace spot
   struct signature_hash
   {
     std::size_t
-    operator() (const std::pair<bool, expansion_t>& sig) const
+    operator() (const std::pair<bool, expansion_t>& sig) const noexcept
     {
       size_t hash = std::hash<bool>()(sig.first);
 

spot/tl/expansions.hh

@@ -47,6 +47,8 @@ namespace spot
       Determinize = 256,
       UniquePrefixSeenOpt = 512,
       UniqueSuffixPost = 1024,
+      UniquePrefixSeenCountOpt = 2048,
+      TransitionBased = 4096,
     };
   };
 

spot/tl/expansions2.cc

@@ -0,0 +1,930 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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/misc/minato.hh>
+#include <spot/priv/robin_hood.hh>
+#include <spot/tl/expansions2.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/formula2bdd.hh>
+#include <spot/twaalgos/remprop.hh>
+
+namespace spot
+{
+  namespace
+  {
+    // FIXME: could probably just return a map directly
+    static std::vector<std::string>
+    formula_aps(formula f)
+    {
+      auto res = std::unordered_set<std::string>();
+
+      f.traverse([&res](formula f)
+      {
+        if (f.is(op::ap))
+        {
+          res.insert(f.ap_name());
+          return true;
+        }
+
+        return false;
+      });
+
+      return std::vector(res.begin(), res.end());
+    }
+
+    formula
+    rewrite_and_nlm(formula f)
+    {
+      unsigned s = f.size();
+      std::vector<formula> final;
+      std::vector<formula> non_final;
+
+      for (auto g: f)
+        if (g.accepts_eword())
+          final.emplace_back(g);
+        else
+          non_final.emplace_back(g);
+
+      if (non_final.empty())
+        // (a* & b*);c = (a*|b*);c
+        return formula::OrRat(std::move(final));
+      if (!final.empty())
+      {
+        // let F_i be final formulae
+        //     N_i be non final formula
+        // (F_1 & ... & F_n & N_1 & ... & N_m)
+        // =   (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
+        //   | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
+        formula f = formula::OrRat(std::move(final));
+        formula n = formula::AndNLM(std::move(non_final));
+        formula t = formula::one_star();
+        formula ft = formula::Concat({f, t});
+        formula nt = formula::Concat({n, t});
+        formula ftn = formula::AndRat({ft, n});
+        formula fnt = formula::AndRat({f, nt});
+        return formula::OrRat({ftn, fnt});
+      }
+      // No final formula.
+      // Translate N_1 & N_2 & ... & N_n into
+      //   N_1 && (N_2;[*]) && ... && (N_n;[*])
+      // | (N_1;[*]) && N_2 && ... && (N_n;[*])
+      // | (N_1;[*]) && (N_2;[*]) && ... && N_n
+      formula star = formula::one_star();
+      std::vector<formula> disj;
+      for (unsigned n = 0; n < s; ++n)
+      {
+        std::vector<formula> conj;
+        for (unsigned m = 0; m < s; ++m)
+        {
+          formula g = f[m];
+          if (n != m)
+            g = formula::Concat({g, star});
+          conj.emplace_back(g);
+        }
+        disj.emplace_back(formula::AndRat(std::move(conj)));
+      }
+      return formula::OrRat(std::move(disj));
+    }
+
+    class bdd_finalizer
+    {
+      public:
+        int encode(formula f)
+          {
+            bool is_anon = false;
+            int var_num;
+            auto it = formula2bdd_.find(f);
+            if (it != formula2bdd_.end())
+            {
+              var_num = it->second;
+            }
+            else
+            {
+              if (opt_sigma_star_ && (f.is(op::Star)
+                                      && f[0].is(op::tt)
+                                      && f.min() == 0
+                                      && f.max() == formula::unbounded()))
+                {
+                  var_num = bddtrue.id();
+                }
+              else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat)))
+                {
+                  bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse);
+                  for (const auto& sub_f : f)
+                    {
+                      int bddid = encode(sub_f);
+                      bdd subvar = bdd_ithvar(bddid);
+                      var = f.is(op::AndRat) ? var & subvar : var | subvar;
+                    }
+                  var_num = var.id();
+                }
+              else
+                {
+                  var_num = d_->register_anonymous_variables(1, this);
+                  is_anon = true;
+                }
+
+              formula2bdd_.insert({f, var_num});
+              bdd2formula_.insert({var_num, f});
+            }
+
+            bdd var = bdd_ithvar(var_num);
+
+            if (is_anon)
+              anon_set_ &= var;
+
+            return var_num;
+          }
+
+        bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode)
+          : anon_set_(bddtrue)
+          , d_(d)
+          , opt_sigma_star_(opt_sigma_star)
+          , opt_bdd_encode_(opt_bdd_encode)
+        {
+          for (const auto& [prefix, suffix] : exp)
+          {
+            int var_num = encode(suffix);
+            bdd var = bdd_ithvar(var_num);
+            exp_ |= prefix & var;
+          }
+        }
+
+        ~bdd_finalizer()
+        {
+          d_->unregister_all_my_variables(this);
+        }
+
+        expansion_t
+        simplify(exp_opts::expand_opt opts);
+
+      private:
+        bdd exp_;
+        bdd anon_set_;
+        std::map<formula, int> formula2bdd_;
+        std::map<int, formula> bdd2formula_;
+        bdd_dict_ptr d_;
+        bool opt_sigma_star_;
+        bool opt_bdd_encode_;
+
+        formula var_to_formula(int var);
+        formula conj_bdd_to_sere(bdd b);
+        formula bdd_to_sere(bdd b);
+    };
+
+    formula
+    bdd_finalizer::var_to_formula(int var)
+    {
+      formula f = bdd2formula_[var];
+      assert(f);
+      return f;
+    }
+
+    formula
+    bdd_finalizer::bdd_to_sere(bdd f)
+    {
+      if (f == bddfalse)
+        return formula::ff();
+
+      std::vector<formula> v;
+      minato_isop isop(f);
+      bdd cube;
+      while ((cube = isop.next()) != bddfalse)
+        v.emplace_back(conj_bdd_to_sere(cube));
+      return formula::OrRat(std::move(v));
+    }
+
+    formula
+    bdd_finalizer::conj_bdd_to_sere(bdd b)
+    {
+      if (b == bddtrue)
+        {
+          if (opt_sigma_star_){
+            return formula::Star(formula::tt(), 0, formula::unbounded());
+          } else {
+            return formula::tt();
+          }
+        }
+      if (b == bddfalse)
+        return formula::ff();
+
+      // Unroll the first loop of the next do/while loop so that we
+      // do not have to create v when b is not a conjunction.
+      formula res = var_to_formula(bdd_var(b));
+      bdd high = bdd_high(b);
+      if (high == bddfalse)
+      {
+        res = formula::Not(res);
+        b = bdd_low(b);
+      }
+      else
+      {
+        assert(bdd_low(b) == bddfalse);
+        b = high;
+      }
+      if (b == bddtrue)
+        return res;
+      std::vector<formula> v{std::move(res)};
+      do
+      {
+        res = var_to_formula(bdd_var(b));
+        high = bdd_high(b);
+        if (high == bddfalse)
+        {
+          res = formula::Not(res);
+          b = bdd_low(b);
+        }
+        else
+        {
+          assert(bdd_low(b) == bddfalse);
+          b = high;
+        }
+        assert(b != bddfalse);
+        v.emplace_back(std::move(res));
+      }
+      while (b != bddtrue);
+      return formula::multop(op::AndRat, std::move(v));
+    }
+
+    expansion_t
+    bdd_finalizer::simplify(exp_opts::expand_opt opts)
+    {
+      expansion_t res;
+
+      if (opts & exp_opts::expand_opt::BddMinterm)
+      {
+        bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
+        bdd or_labels = bdd_exist(exp_, anon_set_);
+        // TODO: check are_equivalent avec or_labels/exp_ en premier argument
+        for (bdd letter: minterms_of(or_labels, prop_set))
+        {
+          bdd dest_bdd = bdd_restrict(exp_, letter);
+          formula dest = bdd_to_sere(dest_bdd);
+
+          // #ifndef NDEBUG
+          // // make sure it didn't exist before
+          // auto it = std::find(res.begin(), res.end(), {letter, dest});
+          // SPOT_ASSERT(it == res.end());
+          // #endif
+
+          res.push_back({letter, dest});
+        }
+      }
+      else // BddIsop
+      {
+        minato_isop isop(exp_);
+        bdd cube;
+        while ((cube = isop.next()) != bddfalse)
+        {
+          bdd letter = bdd_exist(cube, anon_set_);
+          bdd suffix = bdd_existcomp(cube, anon_set_);
+          formula dest = conj_bdd_to_sere(suffix);
+
+          res.push_back({letter, dest});
+        }
+      }
+
+      return res;
+    }
+
+    expansion_t
+    unique_prefix(const expansion_t& exp)
+    {
+      std::map<bdd, formula, bdd_less_than> unique_map;
+      for (const auto& [prefix, suffix] : exp)
+      {
+        auto res = unique_map.insert({prefix, suffix});
+        if (!res.second)
+        {
+          auto it = res.first;
+          it->second = formula::OrRat({it->second, suffix});
+        }
+      }
+
+      expansion_t res(unique_map.begin(), unique_map.end());
+      return res;
+    }
+
+    expansion_t
+    unique_prefix_seen(const expansion_t& exp, std::unordered_set<formula>* seen)
+    {
+      std::map<bdd, formula, bdd_less_than> unique_map;
+      for (const auto& [prefix, suffix] : exp)
+      {
+        auto res = unique_map.insert({prefix, suffix});
+        if (!res.second)
+        {
+          auto it = res.first;
+          it->second = formula::OrRat({it->second, suffix});
+        }
+      }
+
+      expansion_t res;
+
+      for (const auto& [prefix, suffix] : unique_map)
+      {
+        if (!suffix.is(op::OrRat))
+        {
+          res.push_back({prefix, suffix});
+          continue;
+        }
+
+        std::vector<formula> merge;
+        std::vector<formula> single;
+
+        for (const auto& sub_f : suffix)
+          {
+            if (seen->find(sub_f) != seen->end())
+              {
+                single.push_back(sub_f);
+              }
+            else
+              {
+                merge.push_back(sub_f);
+              }
+          }
+
+        for (const auto& sub_f : single)
+          res.push_back({prefix, sub_f});
+
+        if (!merge.empty())
+          res.push_back({prefix, formula::OrRat(merge)});
+      }
+
+      return res;
+    }
+
+    size_t count_new(const expansion_t& exp, std::unordered_set<formula>* seen)
+    {
+      size_t count = 0;
+      for (const auto& [_, suffix] : exp)
+      {
+        if (seen->find(suffix) == seen->end())
+          count++;
+      }
+      return count;
+    }
+
+    const expansion_t&
+    find_smallest(const expansion_t& left,
+                  const expansion_t& right,
+                  std::unordered_set<formula>* seen)
+    {
+      size_t left_new = count_new(left, seen);
+      size_t right_new = count_new(right, seen);
+
+      if (left_new < right_new)
+        return left;
+
+      if (left_new == right_new && left.size() > right.size())
+        return right;
+
+      return right;
+    }
+
+    expansion_t
+    unique_prefix_count(const expansion_t& exp, std::unordered_set<formula>* seen)
+    {
+      expansion_t up = unique_prefix(exp);
+      expansion_t up_seen = unique_prefix_seen(exp, seen);
+
+      const expansion_t& maybe_smallest = find_smallest(exp, up, seen);
+      const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen);
+
+      return smallest;
+    }
+
+    void
+    finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set<formula>* seen)
+    {
+      if (opts & (exp_opts::expand_opt::BddIsop
+                  | exp_opts::expand_opt::BddMinterm))
+      {
+        bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode);
+        exp = bddf.simplify(opts);
+      }
+
+      if (opts & exp_opts::expand_opt::UniqueSuffixPre)
+      {
+        std::map<formula, bdd> unique_map;
+        for (const auto& [prefix, suffix] : exp)
+        {
+          auto res = unique_map.insert({suffix, prefix});
+          if (!res.second)
+          {
+            auto it = res.first;
+            it->second |= prefix;
+          }
+        }
+
+        exp.clear();
+        for (const auto& [suffix, prefix] : unique_map)
+        {
+          exp.push_back({prefix, suffix});
+        }
+      }
+
+      if (opts & exp_opts::expand_opt::UniquePrefix
+          || opts & exp_opts::expand_opt::UniquePrefixSeenOpt
+          || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+      {
+        if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
+          exp = unique_prefix_seen(exp, seen);
+        else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+          exp = unique_prefix_count(exp, seen);
+        else
+          exp = unique_prefix(exp);
+      }
+
+      if (opts & exp_opts::expand_opt::UniqueSuffixPost)
+      {
+        std::map<formula, bdd> unique_map;
+        for (const auto& [prefix, suffix] : exp)
+        {
+          auto res = unique_map.insert({suffix, prefix});
+          if (!res.second)
+          {
+            auto it = res.first;
+            it->second |= prefix;
+          }
+        }
+
+        exp.clear();
+        for (const auto& [suffix, prefix] : unique_map)
+        {
+          exp.push_back({prefix, suffix});
+        }
+      }
+
+      if (opts & exp_opts::expand_opt::Determinize)
+        {
+          expansion_t exp_new;
+
+          bdd props = bddtrue;
+          for (const auto& [prefix, _] : exp)
+            props &= bdd_support(prefix);
+
+          std::vector<formula> dests;
+          for (bdd letter : minterms_of(bddtrue, props))
+            {
+              for (const auto& [prefix, suffix] : exp)
+                {
+                  if (bdd_implies(letter, prefix))
+                    dests.push_back(suffix);
+                }
+              formula or_dests = formula::OrRat(dests);
+              exp_new.push_back({letter, or_dests});
+              dests.clear();
+            }
+          exp = exp_new;
+        }
+    }
+  }
+
+  formula
+  expansion_to_formula2(expansion_t e, bdd_dict_ptr& d)
+  {
+    std::vector<formula> res;
+
+    for (const auto& [key, val] : e)
+      {
+        formula prefix = bdd_to_formula(key, d);
+        res.push_back(formula::Concat({prefix, val}));
+      }
+
+    return formula::OrRat(res);
+  }
+
+  expansion_t
+  expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen)
+  {
+    using exp_t = expansion_t;
+
+    if (f.is_boolean())
+      {
+        auto f_bdd = formula_to_bdd(f, d, owner);
+
+        if (f_bdd == bddfalse)
+          return {};
+
+        return {{f_bdd, formula::eword()}};
+      }
+
+    auto rec = [&d, owner, opts, seen](formula f){
+      return expansion2(f, d, owner, exp_opts::None, seen);
+    };
+
+
+    switch (f.kind())
+      {
+        case op::ff:
+        case op::tt:
+        case op::ap:
+          SPOT_UNREACHABLE();
+
+        case op::eword:
+          // return {{bddfalse, formula::ff()}};
+          return {};
+
+        case op::Concat:
+          {
+            auto exps = rec(f[0]);
+
+            exp_t res;
+            for (const auto& [bdd_l, form] : exps)
+              {
+                res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})});
+              }
+
+            if (f[0].accepts_eword())
+              {
+                auto exps_rest = rec(f.all_but(0));
+                for (const auto& [bdd_l, form] : exps_rest)
+                  {
+                    res.push_back({bdd_l, form});
+                  }
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::FStar:
+          {
+            formula E = f[0];
+
+            if (f.min() == 0 && f.max() == 0)
+              return {{bddtrue, formula::eword()}};
+
+            auto min = f.min() == 0 ? 0 : (f.min() - 1);
+            auto max = f.max() == formula::unbounded()
+                         ? formula::unbounded()
+                         : (f.max() - 1);
+
+            auto E_i_j_minus = formula::FStar(E, min, max);
+
+            auto exp = rec(E);
+            exp_t res;
+            for (const auto& [li, ei] : exp)
+              {
+                res.push_back({li, formula::Fusion({ei, E_i_j_minus})});
+
+                if (ei.accepts_eword() && f.min() != 0)
+                  {
+                    for (const auto& [ki, fi] : rec(E_i_j_minus))
+                      {
+                        // FIXME: build bdd once
+                        if ((li & ki) != bddfalse)
+                          res.push_back({li & ki, fi});
+                      }
+                  }
+              }
+            if (f.min() == 0)
+              res.push_back({bddtrue, formula::eword()});
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::Star:
+          {
+            auto min = f.min() == 0 ? 0 : (f.min() - 1);
+            auto max = f.max() == formula::unbounded()
+                         ? formula::unbounded()
+                         : (f.max() - 1);
+
+            auto exps = rec(f[0]);
+
+            exp_t res;
+            for (const auto& [bdd_l, form] : exps)
+              {
+                res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::AndNLM:
+          {
+            formula rewrite = rewrite_and_nlm(f);
+            auto res = rec(rewrite);
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::first_match:
+          {
+            auto exps = rec(f[0]);
+
+            exp_t res;
+            for (const auto& [bdd_l, form] : exps)
+              {
+                res.push_back({bdd_l, form});
+              }
+
+            // determinize
+            bdd or_labels = bddfalse;
+            bdd support = bddtrue;
+            bool is_det = true;
+            for (const auto& [l, _] : res)
+              {
+                support &= bdd_support(l);
+                if (is_det)
+                  is_det = !bdd_have_common_assignment(l, or_labels);
+                or_labels |= l;
+              }
+
+            if (is_det)
+              {
+                for (auto& [_, dest] : res)
+                  dest = formula::first_match(dest);
+                finalize(res, opts, d, seen);
+                return res;
+              }
+
+            exp_t res_det;
+            std::vector<formula> dests;
+            for (bdd l: minterms_of(or_labels, support))
+              {
+                for (const auto& [ndet_label, ndet_dest] : res)
+                  {
+                    if (bdd_implies(l, ndet_label))
+                      dests.push_back(ndet_dest);
+                  }
+                formula or_dests = formula::OrRat(dests);
+                res_det.push_back({l, or_dests});
+                dests.clear();
+              }
+
+            for (auto& [_, dest] : res_det)
+              dest = formula::first_match(dest);
+            finalize(res_det, opts, d, seen);
+            return res_det;
+          }
+
+        case op::Fusion:
+          {
+            exp_t res;
+            formula E = f[0];
+            formula F = f.all_but(0);
+
+            exp_t Ei = rec(E);
+            // TODO: std::option
+            exp_t Fj = rec(F);
+
+            for (const auto& [li, ei] : Ei)
+              {
+                if (ei.accepts_eword())
+                  {
+                    for (const auto& [kj, fj] : Fj)
+                        if ((li & kj) != bddfalse)
+                          res.push_back({li & kj, fj});
+                  }
+                res.push_back({li, formula::Fusion({ei, F})});
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::AndRat:
+          {
+            exp_t res;
+            for (const auto& sub_f : f)
+              {
+                auto exps = rec(sub_f);
+
+                if (exps.empty())
+                  {
+                    // op::AndRat: one of the expansions was empty (the only
+                    //             edge was `false`), so the AndRat is empty as
+                    //             well
+                    res.clear();
+                    break;
+                  }
+
+                if (res.empty())
+                  {
+                    res = std::move(exps);
+                    continue;
+                  }
+
+                exp_t new_res;
+                bool inserted = false;
+                for (const auto& [l_key, l_val] : exps)
+                  {
+                    for (const auto& [r_key, r_val] : res)
+                      {
+                        if ((l_key & r_key) != bddfalse)
+                          {
+                            new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
+                            inserted = true;
+                          }
+                      }
+                  }
+
+                if (!inserted)
+                  {
+                    // all prefix conjuctions led to bddfalse, And is empty
+                    res.clear();
+                    break;
+                  }
+
+                res = std::move(new_res);
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::OrRat:
+          {
+            exp_t res;
+            for (const auto& sub_f : f)
+              {
+                auto exps = rec(sub_f);
+                if (exps.empty())
+                  continue;
+
+                if (res.empty())
+                  {
+                    res = std::move(exps);
+                    continue;
+                  }
+
+                for (const auto& [label, dest] : exps)
+                  res.push_back({label, dest});
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        default:
+          std::cerr << "unimplemented kind "
+                    << static_cast<int>(f.kind())
+                    << std::endl;
+          SPOT_UNIMPLEMENTED();
+      }
+
+    return {};
+  }
+
+  twa_graph_ptr
+  expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
+  {
+    auto finite = expand_finite_automaton2(f, d, opts);
+    return from_finite(finite);
+  }
+
+  struct signature_hash
+  {
+    std::size_t
+    operator() (const expansion_t& sig) const noexcept
+    {
+      size_t hash = 0;
+
+      for (const auto& keyvalue : sig)
+        {
+          hash ^= (bdd_hash()(keyvalue.first) ^ std::hash<formula>()(keyvalue.second))
+            + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+        }
+
+      return hash;
+    }
+  };
+
+  twa_graph_ptr
+  expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
+  {
+    bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge;
+
+    auto aut = make_twa_graph(d);
+
+    aut->prop_state_acc(false);
+    const auto acc_mark = aut->set_buchi();
+
+    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
+    auto signature2state = std::unordered_map<expansion_t, unsigned, signature_hash>();
+    auto seen = std::unordered_set<formula>();
+    seen.insert(f);
+
+    unsigned init_state = aut->new_state();
+    aut->set_init_state(init_state);
+    formula2state.insert({ f, init_state });
+
+
+    auto f_aps = formula_aps(f);
+    for (auto& ap : f_aps)
+        aut->register_ap(ap);
+
+    auto formula2signature = robin_hood::unordered_map<formula, expansion_t>();
+    auto get_signature = [&](const formula& form) -> expansion_t
+      {
+        auto it = formula2signature.find(form);
+        if (it != formula2signature.end())
+          {
+            return it->second;
+          }
+        auto exp = expansion2(form, d, aut.get(), opts, &seen);
+        formula2signature.insert({form, exp});
+        return exp;
+      };
+
+    if (signature_merge)
+      signature2state.insert({ get_signature(f), init_state});
+
+    auto todo = std::vector<std::pair<formula, unsigned>>();
+    todo.push_back({f, init_state});
+
+    auto state_names = new std::vector<std::string>();
+    std::ostringstream ss;
+    ss << f;
+    state_names->push_back(ss.str());
+
+    auto find_dst = [&](formula suffix) -> unsigned
+      {
+        unsigned dst;
+        auto it = formula2state.find(suffix);
+        if (it != formula2state.end())
+        {
+          dst = it->second;
+        }
+        else
+        {
+          if (signature_merge)
+            {
+              auto exp = get_signature(suffix);
+
+              auto it2 = signature2state.find(exp);
+              if (it2 != signature2state.end())
+                {
+                  formula2state.insert({suffix, it2->second});
+                  return it2->second;
+                }
+            }
+
+          dst = aut->new_state();
+          todo.push_back({suffix, dst});
+          seen.insert(suffix);
+
+          formula2state.insert({suffix, dst});
+          if (signature_merge)
+            signature2state.insert({get_signature(suffix), dst});
+
+          std::ostringstream ss;
+          ss << suffix;
+          state_names->push_back(ss.str());
+        }
+
+        return dst;
+      };
+
+    while (!todo.empty())
+      {
+        auto [curr_f, curr_state] = todo[todo.size() - 1];
+        todo.pop_back();
+
+
+        auto exp = get_signature(curr_f);
+
+        for (const auto& [letter, suffix] : exp)
+          {
+            if (suffix.is(op::ff))
+              // TODO ASSERT NOT
+              continue;
+
+            auto dst = find_dst(suffix);
+
+            auto curr_acc_mark = suffix.accepts_eword() ? acc_mark : acc_cond::mark_t();
+            aut->new_edge(curr_state, dst, letter, curr_acc_mark);
+          }
+      }
+
+    aut->set_named_prop("state-names", state_names);
+
+    if ((opts & exp_opts::MergeEdges)
+        && !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost))
+      aut->merge_edges();
+
+    return aut;
+  }
+}

spot/tl/expansions2.hh

@@ -0,0 +1,45 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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 <map>
+
+#include <bddx.h>
+
+#include <spot/misc/bddlt.hh>
+#include <spot/tl/expansions.hh>
+#include <spot/tl/formula.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  SPOT_API expansion_t
+  expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen = nullptr);
+
+  SPOT_API twa_graph_ptr
+  expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API twa_graph_ptr
+  expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API formula
+  expansion_to_formula2(expansion_t e, bdd_dict_ptr& d);
+}

tests/Makefile.am

@@ -69,7 +69,6 @@ check_PROGRAMS = \
   core/cube \
   core/emptchk \
   core/equals \
-  core/expand \
   core/graph \
   core/kind \
   core/length \
@@ -112,7 +111,6 @@ core_bricks_SOURCES = core/bricks.cc
 core_checkpsl_SOURCES = core/checkpsl.cc
 core_checkta_SOURCES = core/checkta.cc
 core_emptchk_SOURCES  = core/emptchk.cc
-core_expand_SOURCES  = core/expand.cc
 core_graph_SOURCES = core/graph.cc
 core_ikwiad_SOURCES = core/ikwiad.cc
 core_intvcomp_SOURCES = core/intvcomp.cc