Refactor KindMap (#5646)

The KindMap class is only used in the EqualityEngine and implements way more than necessary.
This PR removes all the functionality that is never used.

1 files changed, 23 insertions, 202 deletions

diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index e9036838b..ef46c2093 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -20,216 +20,37 @@
 #ifndef CVC4__KIND_MAP_H
 #define CVC4__KIND_MAP_H
 
-#include <iterator>
+#include <bitset>
 
 #include "base/check.h"
 #include "expr/kind.h"
 
 namespace CVC4 {
 
-/** A bitmap of Kinds. */
-class KindMap {
-  static const size_t SIZE = (kind::LAST_KIND + 63) / 64;
-
-  uint64_t d_bitmap[SIZE];
-
-public:
-
-  /** An iterator over a KindMap. */
-  class iterator {
-    const KindMap* d_map;
-    Kind d_kind;
-
-  public:
-    typedef std::input_iterator_tag iterator_category;
-    typedef Kind value_type;
-
-    iterator() :
-      d_map(NULL),
-      d_kind(Kind(0)) {
-    }
-    iterator(const KindMap& m, Kind k) :
-      d_map(&m),
-      d_kind(k) {
-      AssertArgument(k >= Kind(0) && k <= kind::LAST_KIND, k, "invalid kind");
-      while(d_kind < kind::LAST_KIND &&
-            ! d_map->tst(d_kind)) {
-        d_kind = Kind(uint64_t(d_kind) + 1);
-      }
-    }
-    iterator& operator++() {
-      if(d_kind < kind::LAST_KIND) {
-        d_kind = Kind(uint64_t(d_kind) + 1);
-        while(d_kind < kind::LAST_KIND &&
-              ! d_map->tst(d_kind)) {
-          d_kind = Kind(uint64_t(d_kind) + 1);
-        }
-      }
-      return *this;
-    }
-    iterator operator++(int) const {
-      const_iterator i = *this;
-      ++i;
-      return i;
-    }
-    Kind operator*() const {
-      return d_kind;
-    }
-    bool operator==(iterator i) const {
-      return d_map == i.d_map && d_kind == i.d_kind;
-    }
-    bool operator!=(iterator i) const {
-      return !(*this == i);
-    }
-  };/* class KindMap::iterator */
-  typedef iterator const_iterator;
-
-  KindMap() {
-    clear();
-  }
-  KindMap(const KindMap& m) {
-    for(unsigned i = 0; i < SIZE; ++i) {
-      d_bitmap[i] = m.d_bitmap[i];
-    }
-  }
-  KindMap(Kind k) {
-    clear();
-    set(k);
-  }
-
-  /** Empty the map. */
-  void clear() {
-    for(unsigned i = 0; i < SIZE; ++i) {
-      d_bitmap[i] = uint64_t(0);
-    }
-  }
-  /** Tests whether the map is empty. */
-  bool isEmpty() const {
-    for(unsigned i = 0; i < SIZE; ++i) {
-      if(d_bitmap[i] != uint64_t(0)) {
-        return false;
-      }
-    }
-    return true;
-  }
-  /** Test whether k is in the map. */
-  bool tst(Kind k) const {
-    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
-    return (d_bitmap[k / 64] >> (k % 64)) & uint64_t(1);
-  }
-  /** Set k in the map. */
-  void set(Kind k) {
-    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
-    d_bitmap[k / 64] |= (uint64_t(1) << (k % 64));
-  }
-  /** Clear k from the map. */
-  void clr(Kind k) {
-    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
-    d_bitmap[k / 64] &= ~(uint64_t(1) << (k % 64));
-  }
-
-  /** Iterate over the map. */
-  const_iterator begin() const {
-    return const_iterator(*this, Kind(0));
-  }
-  const_iterator end() const {
-    return const_iterator(*this, kind::LAST_KIND);
-  }
-
-  /** Invert the map. */
-  KindMap operator~() const {
-    KindMap r;
-    for(unsigned i = 0; i < SIZE; ++i) {
-      r.d_bitmap[i] = ~d_bitmap[i];
-    }
-    return r;
-  }
-  /** Bitwise-AND the map (with assignment). */
-  KindMap& operator&=(const KindMap& m) {
-    for(unsigned i = 0; i < SIZE; ++i) {
-      d_bitmap[i] &= m.d_bitmap[i];
-    }
-    return *this;
-  }
-  /** Bitwise-AND the map. */
-  KindMap operator&(const KindMap& m) const {
-    KindMap r(*this);
-    r &= m;
-    return r;
-  }
-  /** Bitwise-OR the map (with assignment). */
-  KindMap& operator|=(const KindMap& m) {
-    for(unsigned i = 0; i < SIZE; ++i) {
-      d_bitmap[i] |= m.d_bitmap[i];
-    }
-    return *this;
-  }
-  /** Bitwise-OR the map. */
-  KindMap operator|(const KindMap& m) const {
-    KindMap r(*this);
-    r |= m;
-    return r;
-  }
-  /** Bitwise-XOR the map (with assignment). */
-  KindMap& operator^=(const KindMap& m) {
-    for(unsigned i = 0; i < SIZE; ++i) {
-      d_bitmap[i] ^= m.d_bitmap[i];
-    }
-    return *this;
-  }
-  /** Bitwise-XOR the map. */
-  KindMap operator^(const KindMap& m) const {
-    KindMap r(*this);
-    r ^= m;
-    return r;
-  }
-
-  /** Test whether k is in the map. */
-  bool operator[](Kind k) const {
-    return tst(k);
-  }
-
-  /** Test equality between two maps. */
-  bool operator==(const KindMap& m) const
+/** A very simple bitmap for Kinds */
+class KindMap
+{
+ public:
+  /** Set the bit for k */
+  void set(Kind k) { d_bits.set(fromKind(k)); }
+  /** Reset the bit for k */
+  void reset(Kind k) { d_bits.reset(fromKind(k)); }
+  /** Check whether the bit for k is set */
+  bool test(Kind k) const { return d_bits.test(fromKind(k)); }
+  /** Check whether the bit for k is set */
+  bool operator[](Kind k) const { return test(k); }
+
+ private:
+  /** Convert kind to std::size_t and check bounds */
+  static std::size_t fromKind(Kind k)
   {
-    for (size_t i = 0; i < SIZE; ++i)
-    {
-      if (d_bitmap[i] != m.d_bitmap[i])
-      {
-        return false;
-      }
-    }
-    return true;
+    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+    return static_cast<std::size_t>(k);
   }
-  bool operator!=(const KindMap& m) const { return !(*this == m); }
-};/* class KindMap */
-
-inline KindMap operator~(Kind k) {
-  KindMap m(k);
-  return ~m;
-}
-inline KindMap operator&(Kind k1, Kind k2) {
-  KindMap m(k1);
-  return m &= k2;
-}
-inline KindMap operator&(Kind k1, KindMap m2) {
-  return m2 & k1;
-}
-inline KindMap operator|(Kind k1, Kind k2) {
-  KindMap m(k1);
-  return m |= k2;
-}
-inline KindMap operator|(Kind k1, KindMap m2) {
-  return m2 | k1;
-}
-inline KindMap operator^(Kind k1, Kind k2) {
-  KindMap m(k1);
-  return m ^= k2;
-}
-inline KindMap operator^(Kind k1, KindMap m2) {
-  return m2 ^ k1;
-}
+  /** The bitmap */
+  std::bitset<kind::LAST_KIND> d_bits;
+};
 
-}/* CVC4 namespace */
+}  // namespace CVC4
 
 #endif /* CVC4__KIND_MAP_H */