From ec4deb32193e4f2b3393b05b6afdc6e39659913e Mon Sep 17 00:00:00 2001
From: Jerome Dubois <jdubois@lrde.epita.fr>
Date: Fri, 22 Jan 2021 20:45:34 +0100
Subject: [PATCH] split: Improve performance of split_edges()

* spot/twaalgos/split.cc: Add cache to avoid
  computing multiple split on the same condition.
---
 spot/twaalgos/split.cc | 26 ++++++++++++++++++++++----
 1 file changed, 22 insertions(+), 4 deletions(-)

diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc
index f082e826f..18f1c32b6 100644
--- a/spot/twaalgos/split.cc
+++ b/spot/twaalgos/split.cc
@@ -24,6 +24,7 @@
 #include <spot/misc/bddlt.hh>
 
 #include <algorithm>
+#include <map>
 
 namespace spot
 {
@@ -39,6 +40,8 @@ namespace spot
     internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph());
 
     bdd all = aut->ap_vars();
+    std::map<unsigned, std::pair<unsigned, unsigned>> split_cond;
+
     for (auto& e: aut->edges())
       {
         bdd cond = e.cond;
@@ -50,11 +53,26 @@ namespace spot
             auto d = aut->univ_dests(dst);
             dst = uniq.new_univ_dests(d.begin(), d.end());
           }
-        while (cond != bddfalse)
+
+        auto& [begin, end] = split_cond[cond.id()];
+        if (begin == end)
           {
-            bdd cube = bdd_satoneset(cond, all, bddfalse);
-            cond -= cube;
-            out->new_edge(e.src, dst, cube, e.acc);
+            begin = aut->num_edges();
+
+            while (cond != bddfalse)
+              {
+                bdd cube = bdd_satoneset(cond, all, bddfalse);
+                cond -= cube;
+                out->new_edge(e.src, dst, cube, e.acc);
+              }
+
+            end = aut->num_edges();
+          }
+        else
+          {
+            auto& g = aut->get_graph();
+            for (unsigned i = begin; i < end; ++i)
+              out->new_edge(e.src, dst, g.edge_storage(i).cond, e.acc);
           }
       }
     return out;