From cbf05ceca6f49ba718337892a013ce84fa328aba Mon Sep 17 00:00:00 2001
From: MichalHe <michal.sk.com@gmail.com>
Date: Fri, 7 Feb 2025 10:47:06 +0100
Subject: [PATCH 1/2] feat(utils): add implementation of BitSet

---
 include/mata/utils/bit-set.hh | 84 +++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 include/mata/utils/bit-set.hh

diff --git a/include/mata/utils/bit-set.hh b/include/mata/utils/bit-set.hh
new file mode 100644
index 000000000..afcc64c66
--- /dev/null
+++ b/include/mata/utils/bit-set.hh
@@ -0,0 +1,84 @@
+/* ord-vector.hh -- Implementation of a set (ordered vector) using std::vector.
+ */
+
+#ifndef MATA_BIT_SET_HH_
+#define MATA_BIT_SET_HH_
+
+#include <vector>
+#include <algorithm>
+#include <cassert>
+
+#include "utils.hh"
+
+namespace mata::utils {
+    struct BitSet {
+        using SlotType = uint64_t;
+
+        std::vector<SlotType> data;
+        size_t bit_count;
+
+        BitSet(size_t bit_count) : bit_count(bit_count),
+                                   data((bit_count / sizeof(SlotType)) + (bit_count % sizeof(SlotType) > 0)) {}  // Zero initialize
+        BitSet(size_t bit_count, std::vector<SlotType>&& bit_data) : data(bit_data), bit_count(bit_count) {}
+
+        bool operator[](size_t pos) const {
+            size_t slot = pos / sizeof(SlotType);
+            size_t slot_offset = slot % sizeof(SlotType);
+
+            SlotType slot_data = this->data[slot];
+            return static_cast<bool>((slot_data & (1u << slot_offset)) > 0);
+        }
+
+        void set(size_t pos, bool value = true) {
+            size_t slot = pos / sizeof(SlotType);
+            size_t slot_offset = slot % sizeof(SlotType);
+
+            SlotType zero_affected_bit = ~(1u << slot_offset);
+            SlotType set_affected_bit  = static_cast<SlotType>(value) << slot_offset;
+            this->data[slot] = (this->data[slot] & zero_affected_bit) | set_affected_bit;
+        }
+
+        BitSet make_union(const BitSet& other) const {
+            size_t new_slot_count = std::max(this->data.size(), other.data.size());
+
+            std::vector<SlotType> new_data(new_slot_count);
+
+            for (size_t slot_idx = 0; slot_idx < this->data.size(); slot_idx++) {
+                new_data[slot_idx] = this->data[slot_idx];
+            }
+
+            for (size_t slot_idx = 0; slot_idx < other.data.size(); slot_idx++) {
+                new_data[slot_idx] |= other.data[slot_idx];
+            }
+
+            size_t new_bit_count = std::max(this->bit_count, other.bit_count);
+            return BitSet(new_bit_count, std::move(new_data));
+        }
+
+        BitSet make_intersection(const BitSet& other) const {
+            size_t new_slot_count = std::max(this->data.size(), other.data.size());
+
+            std::vector<SlotType> new_data(new_slot_count);
+
+            for (size_t slot_idx = 0; slot_idx < this->data.size(); slot_idx++) {
+                new_data[slot_idx] = this->data[slot_idx];
+            }
+
+            for (size_t slot_idx = 0; slot_idx < other.data.size(); slot_idx++) {
+                new_data[slot_idx] &= other.data[slot_idx];
+            }
+
+            size_t new_bit_count = std::max(this->bit_count, other.bit_count);
+            return BitSet(new_bit_count, std::move(new_data));
+        }
+
+        bool is_empty() const {
+            for (size_t slot_idx = 0; slot_idx < this->data.size(); slot_idx++) {
+                if (this->data[slot_idx] != 0) return false;
+            }
+            return true;
+        }
+    }
+} // Namespace mata::utils.
+
+#endif

From 4a24a694a123cd942cafcaec9806112031e4e7c4 Mon Sep 17 00:00:00 2001
From: MichalHe <michal.sk.com@gmail.com>
Date: Fri, 7 Feb 2025 10:54:43 +0100
Subject: [PATCH 2/2] feat(bit_set): add inclusion test

---
 include/mata/utils/bit-set.hh | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/include/mata/utils/bit-set.hh b/include/mata/utils/bit-set.hh
index afcc64c66..cc5f5cd00 100644
--- a/include/mata/utils/bit-set.hh
+++ b/include/mata/utils/bit-set.hh
@@ -72,6 +72,16 @@ namespace mata::utils {
             return BitSet(new_bit_count, std::move(new_data));
         }
 
+        bool is_subset_of(const BitSet& other) const {
+            const size_t& smaller_slot_size = std::min(this->data.size(), other.data.size());
+
+            for (size_t slot_idx = 0; slot_idx < smaller_slot_size; slot_idx++) {
+                if (smaller.data[slot_idx] != smaller.data[slot_idx] & larger.data[slot_idx]) return false;
+            }
+
+            return true;
+        }
+
         bool is_empty() const {
             for (size_t slot_idx = 0; slot_idx < this->data.size(); slot_idx++) {
                 if (this->data[slot_idx] != 0) return false;