From: Aina Niemetz Date: Wed, 9 Dec 2020 20:17:26 +0000 (-0800) Subject: google test: expr: Migrate kind_map_black. (#5640) X-Git-Tag: cvc5-1.0.0~2464 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eed1028716c90df8f26aa1afa948f2deeb1cbdb7;p=cvc5.git google test: expr: Migrate kind_map_black. (#5640) --- diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index ef8500ec3..e9036838b 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -190,17 +190,18 @@ public: } /** Test equality between two maps. */ - bool operator==(KindMap m) { - for(unsigned i = 0; i < SIZE; ++i) { - if(d_bitmap[i] != m.d_bitmap[i]) { + bool operator==(const KindMap& m) const + { + for (size_t i = 0; i < SIZE; ++i) + { + if (d_bitmap[i] != m.d_bitmap[i]) + { return false; } } return true; } - bool operator!=(KindMap m) { - return !(*this == m); - } + bool operator!=(const KindMap& m) const { return !(*this == m); } };/* class KindMap */ inline KindMap operator~(Kind k) { diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 1b619b2f2..3d732df5e 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -14,7 +14,7 @@ cvc4_add_unit_test_black(attribute_black expr) cvc4_add_unit_test_white(attribute_white expr) cvc4_add_cxx_unit_test_black(kind_black expr) -cvc4_add_cxx_unit_test_black(kind_map_black expr) +cvc4_add_unit_test_black(kind_map_black expr) cvc4_add_cxx_unit_test_black(node_black expr) cvc4_add_cxx_unit_test_black(node_algorithm_black expr) cvc4_add_cxx_unit_test_black(node_builder_black expr) diff --git a/test/unit/expr/kind_map_black.cpp b/test/unit/expr/kind_map_black.cpp new file mode 100644 index 000000000..0ad26d004 --- /dev/null +++ b/test/unit/expr/kind_map_black.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file kind_map_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of CVC4::KindMap + ** + ** Black box testing of CVC4::KindMap. + **/ + +#include +#include +#include + +#include "expr/kind_map.h" +#include "test_expr.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestExprBlackKindMap : public TestExprBlack +{ +}; + +TEST_F(TestExprBlackKindMap, simple) +{ + KindMap map; + ASSERT_TRUE(map.isEmpty()); + 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()); + +#ifdef CVC4_ASSERTIONS + ASSERT_THROW(~LAST_KIND, AssertArgumentException); +#endif +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h deleted file mode 100644 index 59d54c91f..000000000 --- a/test/unit/expr/kind_map_black.h +++ /dev/null @@ -1,107 +0,0 @@ -/********************* */ -/*! \file kind_map_black.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of CVC4::KindMap - ** - ** Black box testing of CVC4::KindMap. - **/ - -#include - -#include -#include -#include - -#include "expr/kind_map.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace std; - -class KindMapBlack : public CxxTest::TestSuite { - -public: - - void testSimple() { - KindMap map; - TS_ASSERT(map.isEmpty()); - map.set(AND); - TS_ASSERT(!map.isEmpty()); - KindMap map2 = map; - TS_ASSERT(!map2.isEmpty()); - TS_ASSERT_EQUALS(map, map2); - TS_ASSERT(map.tst(AND)); - TS_ASSERT(map2.tst(AND)); - TS_ASSERT(!map.tst(OR)); - TS_ASSERT(!map2.tst(OR)); - map2 = ~map2; - TS_ASSERT(map2.tst(OR)); - TS_ASSERT(!map2.tst(AND)); - TS_ASSERT(map != map2); - TS_ASSERT(map.begin() != map.end()); - TS_ASSERT(map2.begin() != map2.end()); - map &= ~AND; - TS_ASSERT(map.isEmpty()); - map2.clear(); - TS_ASSERT(map2.isEmpty()); - TS_ASSERT_EQUALS(map2, map); - TS_ASSERT_EQUALS(map.begin(), map.end()); - TS_ASSERT_EQUALS(map2.begin(), map2.end()); - } - - void testIteration() { - KindMap m = AND & OR; - TS_ASSERT(m.isEmpty()); - for(KindMap::iterator i = m.begin(); i != m.end(); ++i) { - TS_FAIL("expected empty iterator range"); - } - m = AND | OR; - KindMap::iterator i = m.begin(); - TS_ASSERT(i != m.end()); - TS_ASSERT_EQUALS(*i, AND); - ++i; - TS_ASSERT(i != m.end()); - TS_ASSERT_EQUALS(*i, OR); - ++i; - TS_ASSERT(i == m.end()); - - m = ~m; - unsigned k = 0; - for(i = m.begin(); i != m.end(); ++i, ++k) { - while(k == AND || k == OR) { - ++k; - } - TS_ASSERT_DIFFERS(Kind(k), UNDEFINED_KIND); - TS_ASSERT_DIFFERS(Kind(k), LAST_KIND); - TS_ASSERT_EQUALS(*i, Kind(k)); - } - } - - void testConstruction() { - TS_ASSERT(!(AND & AND).isEmpty()); - TS_ASSERT((AND & ~AND).isEmpty()); - TS_ASSERT(!(AND & AND & AND).isEmpty()); - - TS_ASSERT(!(AND | AND).isEmpty()); - TS_ASSERT(!(AND | ~AND).isEmpty()); - TS_ASSERT(((AND | AND) & ~AND).isEmpty()); - TS_ASSERT(!((AND | OR) & ~AND).isEmpty()); - - TS_ASSERT((AND ^ AND).isEmpty()); - TS_ASSERT(!(AND ^ OR).isEmpty()); - TS_ASSERT(!(AND ^ AND ^ AND).isEmpty()); - -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException&); -#endif /* CVC4_ASSERTIONS */ - } - -};/* class KindMapBlack */