From e4fd524b02054a3ac9724f184e55a983cb6cb6b9 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 10 Dec 2020 19:53:00 +0100 Subject: [PATCH] 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. --- src/expr/kind_map.h | 225 +++--------------------------- src/theory/uf/equality_engine.cpp | 33 +++-- src/theory/uf/equality_engine.h | 14 +- test/unit/expr/kind_map_black.cpp | 77 +--------- 4 files changed, 57 insertions(+), 292 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 +#include #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(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 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 2173c6922..7ad243073 100644 --- 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 70d5389c1..92665b358 100644 --- 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 0ad26d004..83d0bb452 100644 --- 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 } -- 2.30.2