From 2c435c6c114e7a34e50d590c356f966ee2977c6c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 30 Sep 2021 17:05:18 +0200
Subject: [PATCH] zlktree: simplify heuristic computation

* spot/twaalgos/zlktree.cc: Here.
* spot/twaalgos/zlktree.hh: Add a way to remove an option.
---
 spot/twaalgos/zlktree.cc | 14 ++++++++++----
 spot/twaalgos/zlktree.hh |  9 +++++++++
 2 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc
index a85ef0b55..eec9a88d4 100644
--- a/spot/twaalgos/zlktree.cc
+++ b/spot/twaalgos/zlktree.cc
@@ -386,6 +386,10 @@ namespace spot
     acc_cond posacc = aut->acc();
     acc_cond negacc(posacc.num_sets(), posacc.get_acceptance().complement());
 
+    if (nstates <= 1)
+      // The ordering heuristic does not help if we have a single state.
+      opt_ = opt_ - acd_options::ORDER_HEURISTIC;
+
     // The bitvectors store edge and state-vectors that are shared
     // among the different trees.
     auto allocate_vectors_maybe = [&](unsigned n)
@@ -508,19 +512,20 @@ namespace spot
               seen_dup->add_common(*seen_src, *seen_dst);
               *seen_src |= *seen_dst;
             }
+          if (seen_dup->is_fully_clear())
+            goto skip_sort;
           // Now the union in seen_src is not useful anymore.  Process
           // each node again, but consider only the states that are in
           // seen_dup.
           for (auto& [sz, bv]: out)
             {
               seen_src->clear_all(); // local source of the node
-              bv->foreach_set_index([&aut, &seen_src, &seen_dup](unsigned e)
+              bv->foreach_set_index([&aut, &seen_src](unsigned e)
               {
-                unsigned idx = aut->edge_storage(e).src;
-                if (seen_dup->get(idx))
-                  seen_src->set(idx); // store duplicates
+                seen_src->set(aut->edge_storage(e).src);
               });
               seen_dst->clear_all();
+              *seen_src &= *seen_dup;
               // Count the number of states reached by leaving this node.
               seen_src->foreach_set_index([&aut, bv=bv.get(),
                                            &seen_dst](unsigned s)
@@ -536,6 +541,7 @@ namespace spot
                            [&](auto& p1, auto& p2) {
                              return p1.size > p2.size;
                            });
+        skip_sort:;
         }
 
       unsigned before_size = nodes_.size();
diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh
index 1fa8dfee8..83a9cfacc 100644
--- a/spot/twaalgos/zlktree.hh
+++ b/spot/twaalgos/zlktree.hh
@@ -196,6 +196,15 @@ namespace spot
     return static_cast<acd_options>(static_cast<ut>(left)
                                     | static_cast<ut>(right));
   }
+
+  inline
+  acd_options operator-(acd_options left, acd_options right)
+  {
+    typedef std::underlying_type_t<acd_options> ut;
+    return static_cast<acd_options>(static_cast<ut>(left)
+                                    & ~static_cast<ut>(right));
+  }
+
 #endif
 
   /// \ingroup twa_acc_transform