From 1eb5be543d184d4fac012dd0d27b2ee1c3849596 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 2 Mar 2017 14:17:06 +0100
Subject: [PATCH] acc: implement min_set() and max_set() using gcc builtins

Fixes #238.

* spot/twa/acc.hh (max_set): Add a version using __builtin_clz().
(min_set): New method.
* tests/core/acc.cc, tests/core/acc.test: Add some tests.
---
 spot/twa/acc.hh     | 29 +++++++++++++++++++++++++++--
 tests/core/acc.cc   | 13 ++++++++++---
 tests/core/acc.test |  7 +++++--
 3 files changed, 42 insertions(+), 7 deletions(-)

diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index 2ecff352f..758ac476f 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -230,10 +230,13 @@ namespace spot
       }
 
       // Return the number of the highest set used plus one.
-      // So if no set is used, this returns 0,
-      // but if the sets {1,3,8} are used, this returns 9.
+      // If no set is used, this returns 0,
+      // If the sets {1,3,8} are used, this returns 9.
       unsigned max_set() const
       {
+#ifdef __GNUC__
+        return (id == 0) ? 0 : (sizeof(unsigned) * 8 - __builtin_clz(id));
+#else
         auto i = id;
         int res = 0;
         while (i)
@@ -242,6 +245,28 @@ namespace spot
             i >>= 1;
           }
         return res;
+#endif
+      }
+
+      // Return the number of the lowest set used plus one.
+      // If no set is used, this returns 0.
+      // If the sets {1,3,8} are used, this returns 2.
+      unsigned min_set() const
+      {
+        if (id == 0)
+          return 0;
+#ifdef __GNUC__
+        return __builtin_ctz(id) + 1;
+#else
+        auto i = id;
+        int res = 1;
+        while ((i & 1) == 0)
+          {
+            ++res;
+            i >>= 1;
+          }
+        return res;
+#endif
       }
 
       // Return the lowest acceptance mark
diff --git a/tests/core/acc.cc b/tests/core/acc.cc
index dbd5c481d..6c534c751 100644
--- a/tests/core/acc.cc
+++ b/tests/core/acc.cc
@@ -1,6 +1,6 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// -*- coding: utf-8 -*-x
+// Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -63,6 +63,10 @@ int main()
   auto m2 = spot::acc_cond::mark_t({0, 3});
   auto m3 = spot::acc_cond::mark_t({2, 1});
 
+  spot::acc_cond::mark_t m0 = 0U;
+  std::cout << m0.max_set() << ' ' << m0.min_set() << '\n';
+  std::cout << m3.max_set() << ' ' << m3.min_set() << '\n';
+
   check(ac, m1);
   check(ac, m2);
   check(ac, m3);
@@ -92,6 +96,9 @@ int main()
   std::cout << ac.num_sets() << " + "
             << ac2.num_sets() << " = " << ac3.num_sets() << '\n';
   auto m5 = m2 | (m3 << ac.num_sets());
+
+  std::cout << m5.max_set() << ' ' << m5.min_set() << '\n';
+
   check(ac3, m5);
   auto m6 = ac.comp(m2 & m3) | (m3 << ac.num_sets());
   check(ac3, m6);
diff --git a/tests/core/acc.test b/tests/core/acc.test
index 43b8e6470..634244dcf 100755
--- a/tests/core/acc.test
+++ b/tests/core/acc.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -25,6 +25,8 @@ set -e
 
 cat >expect <<EOF
 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+0 0
+3 2
 #2: {0,2}
 #2: {0,3}
 #2: {1,2}
@@ -41,6 +43,7 @@ Inf(0)&Inf(1)&Inf(2)&Inf(3)
 #5: {0,1,2,3,4} accepting
 #2: {1,2}
 5 + 5 = 10
+8 1
 #4: {0,3,6,7}
 #7: {0,1,2,3,4,6,7}
 #10: {0,1,2,3,4,5,6,7,8,9} accepting
-- 
GitLab