From cc12d514bee6fb8a13cb196a4d6a80e24e6fc32c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 18 Apr 2020 23:23:44 +0200
Subject: [PATCH] avoid mark_t::count() when possible

count() may be implemented using a loop, so using it touch
check count() == 1 or count() > 1 is not advisable.

* spot/twa/acc.hh (mark_t::is_singleton, mark_t::has_many): Introduce
these two methods to replace count()==1 and count()>1
* spot/twa/acc.cc, spot/twaalgos/cleanacc.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/iscolored.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/toparity.cc: Adjust usage.
---
 spot/twa/acc.cc              | 362 +++++++++++++++++------------------
 spot/twa/acc.hh              |  22 +++
 spot/twaalgos/cleanacc.cc    |  14 +-
 spot/twaalgos/determinize.cc |   4 +-
 spot/twaalgos/dtwasat.cc     |   4 +-
 spot/twaalgos/iscolored.cc   |   6 +-
 spot/twaalgos/remfin.cc      |   2 +-
 spot/twaalgos/toparity.cc    |   2 +-
 8 files changed, 219 insertions(+), 197 deletions(-)

diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index 05393caef..0a7fde252 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -152,7 +152,7 @@ namespace spot
               {
                 if (!top)
                   // Avoid extra parentheses if there is only one set
-                  top = code[pos - 1].mark.count() == 1;
+                  top = code[pos - 1].mark.is_singleton();
                 unsigned level = 0;
                 const char* and_ = "";
                 const char* and_next_ = []() {
@@ -207,7 +207,7 @@ namespace spot
               {
                 if (!top)
                   // Avoid extra parentheses if there is only one set
-                  top = code[pos - 1].mark.count() == 1;
+                  top = code[pos - 1].mark.is_singleton();
                 unsigned level = 0;
                 const char* or_ = "";
                 if (!top)
@@ -491,7 +491,7 @@ namespace spot
             }
           if (o1 != acc_cond::acc_op::Fin
               || o2 != acc_cond::acc_op::Inf
-              || m1.count() != 1
+              || !m1.is_singleton()
               || m2 != (m1 << 1))
             return false;
           seen_fin |= m1;
@@ -519,7 +519,7 @@ namespace spot
           assert(code.size() == 2);
 
           auto m = code[0].mark;
-          if (mainop == singleop && m.count() != 1)
+          if (mainop == singleop && !m.is_singleton())
             return false;
 
           acc_cond::mark_t fin = {};
@@ -557,7 +557,7 @@ namespace spot
               acc_cond::mark_t fin = {};
               acc_cond::mark_t inf = {};
 
-              if (op == singleop && m.count() != 1)
+              if (op == singleop && !m.is_singleton())
                 {
                   pairs.clear();
                   return false;
@@ -595,8 +595,8 @@ namespace spot
                 }
               if (o1 != acc_cond::acc_op::Fin
                   || o2 != acc_cond::acc_op::Inf
-                  || m1.count() != 1
-                  || m2.count() != 1)
+                  || !m1.is_singleton()
+                  || !m2.is_singleton())
                 {
                   pairs.clear();
                   return false;
@@ -723,7 +723,7 @@ namespace spot
 
             if (o1 != acc_cond::acc_op::Fin
                 || o2 != acc_cond::acc_op::Inf
-                || m1.count() != 1)
+                || !m1.is_singleton())
               return false;
 
             unsigned i = m2.count();
@@ -826,7 +826,7 @@ namespace spot
 
             if (o1 != acc_cond::acc_op::Inf
                 || o2 != acc_cond::acc_op::Fin
-                || m1.count() != 1)
+                || !m1.is_singleton())
               return false;
 
             unsigned i = m2.count();
@@ -1069,34 +1069,33 @@ namespace spot
                           std::vector<acc_cond::acc_code> elements,
                           acc_cond::acc_op op)
     {
-      acc_cond::mark_t empty_m = {};
       if (elements.size() > 2)
-      {
-        new_cond = original;
-        return false;
-      }
+        {
+          new_cond = original;
+          return false;
+        }
       if (elements.size() == 2)
-      {
-        unsigned pos = elements[1].back().sub.op == op &&
-                       elements[1][0].mark.count() == 1;
-        if (!(elements[0].back().sub.op == op || pos))
         {
-          new_cond = original;
-          return false;
+          unsigned pos = (elements[1].back().sub.op == op
+                          && elements[1][0].mark.is_singleton());
+          if (!(elements[0].back().sub.op == op || pos))
+            {
+              new_cond = original;
+              return false;
+            }
+          if ((elements[1 - pos].used_sets() & elements[pos][0].mark))
+            {
+              new_cond = original;
+              return false;
+            }
+          if (!elements[pos][0].mark.is_singleton())
+            {
+              return false;
+            }
+          colors.push_back(elements[pos][0].mark.min_set() - 1);
+          elements[1 - pos].has_parity_prefix(new_cond, colors);
+          return true;
         }
-        if ((elements[1 - pos].used_sets() & elements[pos][0].mark) != empty_m)
-        {
-          new_cond = original;
-          return false;
-        }
-        if (elements[pos][0].mark.count() != 1)
-        {
-          return false;
-        }
-        colors.push_back(elements[pos][0].mark.min_set() - 1);
-        elements[1 - pos].has_parity_prefix(new_cond, colors);
-        return true;
-      }
       return false;
     }
   }
@@ -1329,105 +1328,106 @@ namespace spot
 
   bool
   acc_cond::acc_code::is_parity_max_equiv(std::vector<int>& permut,
-                    unsigned new_color,
-                    bool even) const
+                                          unsigned new_color,
+                                          bool even) const
   {
     auto conj = top_conjuncts();
     auto disj = top_disjuncts();
     if (conj.size() == 1)
-    {
-      if (disj.size() == 1)
       {
-        acc_cond::acc_code elem = conj[0];
-        if ((even && elem.back().sub.op == acc_cond::acc_op::Inf)
-          || (!even && elem.back().sub.op == acc_cond::acc_op::Fin))
-        {
-          for (auto color : disj[0][0].mark.sets())
+        if (disj.size() == 1)
           {
-            if (permut[color] != -1
-                && ((unsigned) permut[color]) != new_color)
-              return false;
-            permut[color] = new_color;
-          }
-          return true;
-        }
-        return false;
-      }
-      else
-      {
-        std::sort(disj.begin(), disj.end(),
-          [](acc_code c1, acc_code c2)
+            acc_cond::acc_code elem = conj[0];
+            if ((even && elem.back().sub.op == acc_cond::acc_op::Inf)
+                || (!even && elem.back().sub.op == acc_cond::acc_op::Fin))
               {
-                return (c1 != c2) &&
-                c1.back().sub.op == acc_cond::acc_op::Inf;
-              });
-        unsigned i = 0;
-        for (; i < disj.size() - 1; ++i)
-        {
-          if (disj[i].back().sub.op != acc_cond::acc_op::Inf
-            || disj[i][0].mark.count() != 1)
+                for (auto color : disj[0][0].mark.sets())
+                  {
+                    if (permut[color] != -1
+                        && ((unsigned) permut[color]) != new_color)
+                      return false;
+                    permut[color] = new_color;
+                  }
+                return true;
+              }
             return false;
-          for (auto color : disj[i][0].mark.sets())
-          {
-            if (permut[color] != -1
-              && ((unsigned) permut[color]) != new_color)
-                        return false;
-            permut[color] = new_color;
           }
-        }
-        if (disj[i].back().sub.op == acc_cond::acc_op::Inf)
-        {
-          if (!even || disj[i][0].mark.count() != 1)
-            return false;
-          for (auto color : disj[i][0].mark.sets())
+        else
           {
-            if (permut[color] != -1
-              && ((unsigned) permut[color]) != new_color)
-                        return false;
-            permut[color] = new_color;
+            std::sort(disj.begin(), disj.end(),
+                      [](acc_code c1, acc_code c2)
+                      {
+                        return (c1 != c2) &&
+                          c1.back().sub.op == acc_cond::acc_op::Inf;
+                      });
+            unsigned i = 0;
+            for (; i < disj.size() - 1; ++i)
+              {
+                if (disj[i].back().sub.op != acc_cond::acc_op::Inf
+                    || !disj[i][0].mark.is_singleton())
+                  return false;
+                for (auto color : disj[i][0].mark.sets())
+                  {
+                    if (permut[color] != -1
+                        && ((unsigned) permut[color]) != new_color)
+                      return false;
+                    permut[color] = new_color;
+                  }
+              }
+            if (disj[i].back().sub.op == acc_cond::acc_op::Inf)
+              {
+                if (!even || !disj[i][0].mark.is_singleton())
+                  return false;
+                for (auto color : disj[i][0].mark.sets())
+                  {
+                    if (permut[color] != -1
+                        && ((unsigned) permut[color]) != new_color)
+                      return false;
+                    permut[color] = new_color;
+                  }
+                return true;
+              }
+            return disj[i].is_parity_max_equiv(permut, new_color + 1, even);
           }
-          return true;
-        }
-        return disj[i].is_parity_max_equiv(permut, new_color + 1, even);
       }
-    }
     else
-      {       std::sort(conj.begin(), conj.end(),
-        [](acc_code c1, acc_code c2)
+      {
+        std::sort(conj.begin(), conj.end(),
+                  [](acc_code c1, acc_code c2)
+                  {
+                    return (c1 != c2)
+                      && c1.back().sub.op == acc_cond::acc_op::Fin;
+                  });
+        unsigned i = 0;
+        for (; i < conj.size() - 1; i++)
           {
-            return (c1 != c2)
-                  && c1.back().sub.op == acc_cond::acc_op::Fin;
-          });
-      unsigned i = 0;
-      for (; i < conj.size() - 1; i++)
-      {
-        if (conj[i].back().sub.op != acc_cond::acc_op::Fin
-          || conj[i][0].mark.count() != 1)
-            return false;
-        for (auto color : conj[i][0].mark.sets())
-        {
-          if (permut[color] != -1 && permut[color != new_color])
-            return false;
-          permut[color] = new_color;
-        }
-      }
-      if (conj[i].back().sub.op == acc_cond::acc_op::Fin)
-      {
-        if (even)
-          return 0;
-        if (conj[i][0].mark.count() != 1)
-          return false;
-        for (auto color : conj[i][0].mark.sets())
-        {
-          if (permut[color] != -1 && permut[color != new_color])
-            return false;
-          permut[color] = new_color;
-        }
-        return true;
-      }
+            if (conj[i].back().sub.op != acc_cond::acc_op::Fin
+                || !conj[i][0].mark.is_singleton())
+              return false;
+            for (auto color : conj[i][0].mark.sets())
+              {
+                if (permut[color] != -1 && permut[color != new_color])
+                  return false;
+                permut[color] = new_color;
+              }
+          }
+        if (conj[i].back().sub.op == acc_cond::acc_op::Fin)
+          {
+            if (even)
+              return 0;
+            if (!conj[i][0].mark.is_singleton())
+              return false;
+            for (auto color : conj[i][0].mark.sets())
+              {
+                if (permut[color] != -1 && permut[color != new_color])
+                  return false;
+                permut[color] = new_color;
+              }
+            return true;
+          }
 
-      return conj[i].is_parity_max_equiv(permut, new_color + 1, even);
-    }
+        return conj[i].is_parity_max_equiv(permut, new_color + 1, even);
+      }
   }
 
 
@@ -1688,7 +1688,7 @@ namespace spot
             break;
           case acc_cond::acc_op::Fin:
           case acc_cond::acc_op::FinNeg:
-            if (pos[-1].mark.count() > 1 && pos > and_scope)
+            if (pos[-1].mark.has_many() && pos > and_scope)
               return false;
             SPOT_FALLTHROUGH;
           case acc_cond::acc_op::Inf:
@@ -1721,7 +1721,7 @@ namespace spot
             break;
           case acc_cond::acc_op::Inf:
           case acc_cond::acc_op::InfNeg:
-            if (pos[-1].mark.count() > 1 && pos > or_scope)
+            if (pos[-1].mark.has_many() && pos > or_scope)
               return false;
             SPOT_FALLTHROUGH;
           case acc_cond::acc_op::Fin:
@@ -2564,69 +2564,69 @@ namespace spot
 
   namespace
   {
-  bool
-  find_unit_clause(acc_cond::acc_code code, bool& conj, bool& fin,
-                                         acc_cond::mark_t& res)
-  {
-    res = {};
-    acc_cond::mark_t possibles = ~code.used_once_sets();
-    bool found_one = false;
-    conj = false;
-    fin = false;
-    if (code.empty() || code.is_f())
-      return false;
-    const acc_cond::acc_word* pos = &code.back();
-    conj = (pos->sub.op == acc_cond::acc_op::And);
-    do
-      {
-        switch (pos->sub.op)
-          {
-          case acc_cond::acc_op::And:
-            if (!conj)
-              pos -= pos->sub.size + 1;
-            else
-              --pos;
-            break;
-          case acc_cond::acc_op::Or:
-            if (conj)
-              pos -= pos->sub.size + 1;
-            else
-              --pos;
-            break;
-          case acc_cond::acc_op::Inf:
-          case acc_cond::acc_op::InfNeg:
-          case acc_cond::acc_op::FinNeg:
-            if (!fin)
+    bool
+    find_unit_clause(acc_cond::acc_code code, bool& conj, bool& fin,
+                     acc_cond::mark_t& res)
+    {
+      res = {};
+      bool found_one = false;
+      conj = false;
+      fin = false;
+      if (code.empty() || code.is_f())
+        return false;
+      acc_cond::mark_t candidates = ~code.used_once_sets();
+      if (!candidates)
+        return false;
+      const acc_cond::acc_word* pos = &code.back();
+      conj = (pos->sub.op == acc_cond::acc_op::And);
+      do
+        {
+          switch (pos->sub.op)
             {
-              auto m = pos[-1].mark & possibles;
-              if ((!conj && pos[-1].mark.count() == 1)
-                || (conj && m.count() > 0))
-              {
-                found_one = true;
-                res |= m;
-              }
+            case acc_cond::acc_op::And:
+              if (!conj)
+                pos -= pos->sub.size + 1;
+              else
+                --pos;
+              break;
+            case acc_cond::acc_op::Or:
+              if (conj)
+                pos -= pos->sub.size + 1;
+              else
+                --pos;
+              break;
+            case acc_cond::acc_op::Inf:
+            case acc_cond::acc_op::InfNeg:
+            case acc_cond::acc_op::FinNeg:
+              if (!fin)
+                {
+                  auto m = pos[-1].mark & candidates;
+                  if (m && (conj || pos[-1].mark.is_singleton()))
+                    {
+                      found_one = true;
+                      res |= m;
+                    }
+                }
+              pos -= 2;
+              break;
+            case acc_cond::acc_op::Fin:
+              if (!found_one || fin)
+                {
+                  auto m = pos[-1].mark & candidates;
+                  if (m && (!conj || pos[-1].mark.is_singleton()))
+                    {
+                      found_one = true;
+                      fin = true;
+                      res |= m;
+                    }
+                }
+              pos -= 2;
+              break;
             }
-            pos -= 2;
-            break;
-          case acc_cond::acc_op::Fin:
-            if (!found_one || fin)
-            {
-              auto m = pos[-1].mark & possibles;
-              if ((conj && pos[-1].mark.count() == 1)
-                || (!conj && m.count() > 0))
-              {
-                found_one = true;
-                fin = true;
-                res |= m;
-              }
-            }
-            pos -= 2;
-            break;
-          }
-      }
-    while (pos >= &code.front());
-    return res != acc_cond::mark_t {};
-  }
+        }
+      while (pos >= &code.front());
+      return !!res;
+    }
   }
 
   acc_cond::acc_code
@@ -2733,7 +2733,7 @@ namespace spot
             break;
           case acc_cond::acc_op::Fin:
             auto m = pos[-1].mark;
-            if (m.count() == 1)
+            if (m.is_singleton())
               res |= m;
             pos -= 2;
             break;
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index 2ebfa1deb..7ca440fd0 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -389,6 +389,28 @@ namespace spot
         return id & -id;
       }
 
+      /// \brief Whether the mark contains only one bit set.
+      bool is_singleton() const
+      {
+#if __GNUC__
+        /* With GCC and Clang, count() is implemented using popcount. */
+        return count() == 1;
+#else
+        return id && !(id & (id - 1));
+#endif
+      }
+
+      /// \brief Whether the mark contains at least two bits set.
+      bool has_many() const
+      {
+#if __GNUC__
+        /* With GCC and Clang, count() is implemented using popcount. */
+        return count() > 1;
+#else
+        return !!(id & (id - 1));
+#endif
+      }
+
       /// \brief Remove n bits that where set.
       ///
       /// If there are less than n bits set, the output is empty.
diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc
index ff663596a..ee47edc84 100644
--- a/spot/twaalgos/cleanacc.cc
+++ b/spot/twaalgos/cleanacc.cc
@@ -177,7 +177,7 @@ namespace spot
               auto tmp = remove_compl_rec(pos, complement);
 
               if (!tmp.empty() && (tmp.back().sub.op == opfin
-                                   && tmp.front().mark.count() == 1))
+                                   && tmp.front().mark.is_singleton()))
                 seen_fin |= tmp.front().mark;
 
               if (opand == acc_cond::acc_op::And)
@@ -390,7 +390,7 @@ namespace spot
           case acc_cond::acc_op::FinNeg:
             {
               auto m = pos[-1].mark;
-              if (op == wanted && m == m.lowest())
+              if (op == wanted && m.is_singleton())
                 {
                   res |= m;
                 }
@@ -427,7 +427,7 @@ namespace spot
                         if (op == wanted)
                           {
                             auto m = pos[-1].mark;
-                            if (!seen && m == m.lowest())
+                            if (!seen && m.is_singleton())
                               {
                                 seen = true;
                                 res |= m;
@@ -513,7 +513,7 @@ namespace spot
                                   case acc_cond::acc_op::Fin:
                                     {
                                       auto m = pos[-1].mark;
-                                      if (op == wanted && m == m.lowest())
+                                      if (op == wanted && m.is_singleton())
                                         singletons.emplace_back(m, pos);
                                       pos -= 2;
                                     }
@@ -550,8 +550,8 @@ namespace spot
                             if (!can_receive)
                               return;
                             for (auto p: singletons)
-                              if (p.first != can_receive &&
-                                  p.first.lowest() == p.first)
+                              if (p.first != can_receive
+                                  && p.first.is_singleton())
                                 {
                                   // Mark fused singletons as false,
                                   // so that a future call to
@@ -596,7 +596,7 @@ namespace spot
       for (auto pair: to_fuse)
         if (pair.first & once) // can we remove pair.first?
           {
-            assert(pair.first.count() == 1);
+            assert(pair.first.is_singleton());
             for (auto& e: aut->edges())
               if (e.acc & pair.first)
                 e.acc = (e.acc - pair.first) | pair.second;
diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc
index a14fc8e43..4aeddc497 100644
--- a/spot/twaalgos/determinize.cc
+++ b/spot/twaalgos/determinize.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2019 Laboratoire de Recherche et
+// Copyright (C) 2015-2020 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -195,7 +195,7 @@ namespace spot
         int newb = brace;
         if (acc)
           {
-            assert(acc.has(0) && acc.count() == 1 && "Only TBA are accepted");
+            assert(acc.has(0) && acc.is_singleton() && "Only TBA are accepted");
             // Accepting edges generate new braces: step A1
             newb = braces_.size();
             braces_.emplace_back(brace);
diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc
index 7d5037eca..23b666517 100644
--- a/spot/twaalgos/dtwasat.cc
+++ b/spot/twaalgos/dtwasat.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2019 Laboratoire de Recherche
+// Copyright (C) 2013-2020 Laboratoire de Recherche
 // et Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -153,7 +153,7 @@ namespace spot
                       break;
                     case acc_cond::acc_op::Fin:
                       fin |= pos[-1].mark;
-                      assert(pos[-1].mark.count() == 1);
+                      assert(pos[-1].mark.is_singleton());
                       pos -= 2;
                       break;
                     case acc_cond::acc_op::Inf:
diff --git a/spot/twaalgos/iscolored.cc b/spot/twaalgos/iscolored.cc
index d38a36ee8..73a0dad56 100644
--- a/spot/twaalgos/iscolored.cc
+++ b/spot/twaalgos/iscolored.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2017-2018, 2020 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -26,7 +26,7 @@ namespace spot
   is_colored(const const_twa_graph_ptr& aut)
   {
     for (auto t: aut->edges())
-      if (t.acc.count() != 1)
+      if (!t.acc.is_singleton())
         return false;
     return true;
   }
diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index 5bfe0d0a0..d34110e62 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -356,7 +356,7 @@ namespace spot
                       break;
                     case acc_cond::acc_op::Fin:
                       fin |= pos[-1].mark;
-                      assert(pos[-1].mark.count() == 1);
+                      assert(pos[-1].mark.is_singleton());
                       pos -= 2;
                       break;
                     case acc_cond::acc_op::Inf:
diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc
index d59318eec..31d7b190b 100644
--- a/spot/twaalgos/toparity.cc
+++ b/spot/twaalgos/toparity.cc
@@ -660,7 +660,7 @@ get_inputs_states(const twa_graph_ptr& aut)
     for (auto e : aut->edges())
     {
         auto elements = e.acc & used;
-        if (elements.count() > 1)
+        if (elements.has_many())
             inputs[e.dst].insert(elements);
     }
     return inputs;