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.

diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index e9036838bc30a947b1387c0dada293821eae8047..ef46c2093f9414c74d2f5dab7d98254fcd50cfd2 100644 (file)
--- 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 */

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 2173c6922d56ef7756c66d5e4da8ea4ebe75c497..7ad2430735354828bc35916a05474f1a6880deb8 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -276,16 +276,26 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   return newId;
 }
 
-void EqualityEngine::addFunctionKind(Kind fun, bool interpreted, bool extOperator) {
-  d_congruenceKinds |= fun;
-  if (fun != kind::EQUAL) {
-    if (interpreted) {
-      Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
-      d_congruenceKindsInterpreted |= fun;
+void EqualityEngine::addFunctionKind(Kind fun,
+                                     bool interpreted,
+                                     bool extOperator)
+{
+  d_congruenceKinds.set(fun);
+  if (fun != kind::EQUAL)
+  {
+    if (interpreted)
+    {
+      Debug("equality::evaluation")
+          << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted "
+          << std::endl;
+      d_congruenceKindsInterpreted.set(fun);
     }
-    if (extOperator) {
-      Debug("equality::extoperator") << d_name << "::eq::addFunctionKind(): " << fun << " is an external operator kind " << std::endl;
-      d_congruenceKindsExtOperators |= fun;
+    if (extOperator)
+    {
+      Debug("equality::extoperator")
+          << d_name << "::eq::addFunctionKind(): " << fun
+          << " is an external operator kind " << std::endl;
+      d_congruenceKindsExtOperators.set(fun);
     }
   }
 }
@@ -1744,8 +1754,9 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) {
     // equality is handled separately
     return addTriggerEquality(predicate);
   }
-  Assert(d_congruenceKinds.tst(predicate.getKind()))
-      << "No point in adding non-congruence predicates, kind is " << predicate.getKind();
+  Assert(d_congruenceKinds.test(predicate.getKind()))
+      << "No point in adding non-congruence predicates, kind is "
+      << predicate.getKind();
 
   if (d_done) {
     return;

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 70d5389c10afba4aaa48b380112683bdf6ad07ff..92665b358fb42a897d1f4442d43d50b8931c4a7f 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -683,22 +683,22 @@ private:
   /**
    * Returns true if this kind is used for congruence closure.
    */
-  bool isFunctionKind(Kind fun) const {
-    return d_congruenceKinds.tst(fun);
-  }
+  bool isFunctionKind(Kind fun) const { return d_congruenceKinds.test(fun); }
 
   /**
    * Returns true if this kind is used for congruence closure + evaluation of constants.
    */
-  bool isInterpretedFunctionKind(Kind fun) const {
-    return d_congruenceKindsInterpreted.tst(fun);
+  bool isInterpretedFunctionKind(Kind fun) const
+  {
+    return d_congruenceKindsInterpreted.test(fun);
   }
 
   /**
    * Returns true if this kind has an operator that is considered external (e.g. not internal).
    */
-  bool isExternalOperatorKind(Kind fun) const {
-    return d_congruenceKindsExtOperators.tst(fun);
+  bool isExternalOperatorKind(Kind fun) const
+  {
+    return d_congruenceKindsExtOperators.test(fun);
   }
 
   /**

diff --git a/test/unit/expr/kind_map_black.cpp b/test/unit/expr/kind_map_black.cpp
index 0ad26d0042bde9a1fb6485e9e4f61035cee5ee0b..83d0bb4521dd2b045a4b242731bde8ec280852b7 100644 (file)
--- a/test/unit/expr/kind_map_black.cpp
+++ b/test/unit/expr/kind_map_black.cpp
@@ -34,80 +34,13 @@ class TestExprBlackKindMap : public TestExprBlack
 TEST_F(TestExprBlackKindMap, simple)
 {
   KindMap map;
-  ASSERT_TRUE(map.isEmpty());
+  ASSERT_FALSE(map.test(AND));
   map.set(AND);
-  ASSERT_FALSE(map.isEmpty());
-  KindMap map2 = map;
-  ASSERT_FALSE(map2.isEmpty());
-  EXPECT_EQ(map, map2);
-  ASSERT_TRUE(map.tst(AND));
-  ASSERT_TRUE(map2.tst(AND));
-  ASSERT_FALSE(map.tst(OR));
-  ASSERT_FALSE(map2.tst(OR));
-  map2 = ~map2;
-  ASSERT_TRUE(map2.tst(OR));
-  ASSERT_FALSE(map2.tst(AND));
-  EXPECT_NE(map, map2);
-  EXPECT_NE(map.begin(), map.end());
-  EXPECT_NE(map2.begin(), map2.end());
-  map &= ~AND;
-  ASSERT_TRUE(map.isEmpty());
-  map2.clear();
-  ASSERT_TRUE(map2.isEmpty());
-  EXPECT_EQ(map2, map);
-  EXPECT_EQ(map.begin(), map.end());
-  EXPECT_EQ(map2.begin(), map2.end());
-}
-
-TEST_F(TestExprBlackKindMap, iteration)
-{
-  KindMap m = AND & OR;
-  ASSERT_TRUE(m.isEmpty());
-  for (KindMap::iterator i = m.begin(); i != m.end(); ++i)
-  {
-    ASSERT_TRUE(false) << "expected empty iterator range";
-  }
-  m = AND | OR;
-  KindMap::iterator i = m.begin();
-  EXPECT_NE(i, m.end());
-  EXPECT_EQ(*i, AND);
-  ++i;
-  EXPECT_NE(i, m.end());
-  EXPECT_EQ(*i, OR);
-  ++i;
-  EXPECT_EQ(i, m.end());
-
-  m = ~m;
-  uint32_t k = 0;
-  for (i = m.begin(); i != m.end(); ++i, ++k)
-  {
-    while (k == AND || k == OR)
-    {
-      ++k;
-    }
-    EXPECT_NE(Kind(k), UNDEFINED_KIND);
-    EXPECT_NE(Kind(k), LAST_KIND);
-    EXPECT_EQ(*i, Kind(k));
-  }
-}
-
-TEST_F(TestExprBlackKindMap, construction)
-{
-  ASSERT_FALSE((AND & AND).isEmpty());
-  ASSERT_TRUE((AND & ~AND).isEmpty());
-  ASSERT_FALSE((AND & AND & AND).isEmpty());
-
-  ASSERT_FALSE((AND | AND).isEmpty());
-  ASSERT_FALSE((AND | ~AND).isEmpty());
-  ASSERT_TRUE(((AND | AND) & ~AND).isEmpty());
-  ASSERT_FALSE(((AND | OR) & ~AND).isEmpty());
-
-  ASSERT_TRUE((AND ^ AND).isEmpty());
-  ASSERT_FALSE((AND ^ OR).isEmpty());
-  ASSERT_FALSE((AND ^ AND ^ AND).isEmpty());
-
+  ASSERT_TRUE(map.test(AND));
+  map.reset(AND);
+  ASSERT_FALSE(map.test(AND));
 #ifdef CVC4_ASSERTIONS
-  ASSERT_THROW(~LAST_KIND, AssertArgumentException);
+  ASSERT_THROW(map.set(LAST_KIND), AssertArgumentException);
 #endif
 }