From: Aina Niemetz Date: Fri, 4 Dec 2020 16:16:37 +0000 (-0800) Subject: google test: context: Migrate cdmap_black. (#5584) X-Git-Tag: cvc5-1.0.0~2502 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9be473aab6e1b5c46a27f50776778ba06afad41e;p=cvc5.git google test: context: Migrate cdmap_black. (#5584) --- diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index d88ee2661..d19ad60c0 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -12,7 +12,7 @@ # Add unit tests cvc4_add_unit_test_black(cdlist_black context) -cvc4_add_cxx_unit_test_black(cdmap_black context) +cvc4_add_unit_test_black(cdmap_black context) cvc4_add_cxx_unit_test_white(cdmap_white context) cvc4_add_cxx_unit_test_black(cdo_black context) cvc4_add_cxx_unit_test_black(context_black context) diff --git a/test/unit/context/cdmap_black.cpp b/test/unit/context/cdmap_black.cpp new file mode 100644 index 000000000..e9112db7e --- /dev/null +++ b/test/unit/context/cdmap_black.cpp @@ -0,0 +1,206 @@ +/********************* */ +/*! \file cdmap_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Dejan Jovanovic + ** 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::context::CDMap<>. + ** + ** Black box testing of CVC4::context::CDMap<>. + **/ + +#include + +#include "base/check.h" +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "test_context.h" + +namespace CVC4 { +namespace test { + +using CVC4::context::CDHashMap; +using CVC4::context::Context; + +class TestContextCDMapBlack : public TestContext +{ + protected: + /** Returns the elements in a CDHashMap. */ + static std::map get_elements( + const CDHashMap& map) + { + return std::map{map.begin(), map.end()}; + } + + /** + * Returns true if the elements in map are the same as expected. + * NOTE: This is mostly to help the type checker for matching expected within + * a ASSERT_*. + */ + static bool elements_are(const CDHashMap& map, + const std::map& expected) + { + return get_elements(map) == expected; + } +}; + +TEST_F(TestContextCDMapBlack, simple_sequence) +{ + CDHashMap map(d_context.get()); + ASSERT_TRUE(elements_are(map, {})); + + map.insert(3, 4); + ASSERT_TRUE(elements_are(map, {{3, 4}})); + + { + d_context->push(); + ASSERT_TRUE(elements_are(map, {{3, 4}})); + + map.insert(5, 6); + map.insert(9, 8); + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}})); + + { + d_context->push(); + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}})); + + map.insert(1, 2); + ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); + + { + d_context->push(); + ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); + + map.insertAtContextLevelZero(23, 317); + map.insert(1, 45); + + ASSERT_TRUE( + elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); + map.insert(23, 324); + + ASSERT_TRUE( + elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}})); + d_context->pop(); + } + + ASSERT_TRUE( + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); + d_context->pop(); + } + + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); + d_context->pop(); + } + + ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}})); +} + +TEST_F(TestContextCDMapBlack, simple_sequence_fewer_finds) +{ + // no intervening find() in this one (under the theory that this could trigger + // a bug) + CDHashMap map(d_context.get()); + map.insert(3, 4); + + { + d_context->push(); + + map.insert(5, 6); + map.insert(9, 8); + + { + d_context->push(); + + map.insert(1, 2); + + ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); + { + d_context->push(); + d_context->pop(); + } + + d_context->pop(); + } + + d_context->pop(); + } +} + +TEST_F(TestContextCDMapBlack, insert_at_context_level_zero) +{ + CDHashMap map(d_context.get()); + + map.insert(3, 4); + + ASSERT_TRUE(elements_are(map, {{3, 4}})); + { + d_context->push(); + ASSERT_TRUE(elements_are(map, {{3, 4}})); + + map.insert(5, 6); + map.insert(9, 8); + + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}})); + + { + d_context->push(); + + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}})); + + map.insert(1, 2); + + ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); + + map.insertAtContextLevelZero(23, 317); + + ASSERT_TRUE( + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); + + ASSERT_DEATH(map.insertAtContextLevelZero(23, 317), + "insertAtContextLevelZero"); + ASSERT_DEATH(map.insertAtContextLevelZero(23, 472), + "insertAtContextLevelZero"); + map.insert(23, 472); + + ASSERT_TRUE( + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); + { + d_context->push(); + + ASSERT_TRUE( + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); + + ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), + "insertAtContextLevelZero"); + map.insert(23, 1024); + + ASSERT_TRUE( + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}})); + d_context->pop(); + } + ASSERT_TRUE( + elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); + d_context->pop(); + } + + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); + + ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), + "insertAtContextLevelZero"); + map.insert(23, 477); + + ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}})); + d_context->pop(); + } + + ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), "insertAtContextLevelZero"); + + ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}})); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h deleted file mode 100644 index 5bded0a5d..000000000 --- a/test/unit/context/cdmap_black.h +++ /dev/null @@ -1,207 +0,0 @@ -/********************* */ -/*! \file cdmap_black.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner - ** 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::context::CDMap<>. - ** - ** Black box testing of CVC4::context::CDMap<>. - **/ - -#include - -#include - -#include "base/check.h" -#include "context/cdhashmap.h" -#include "context/cdlist.h" -#include "context/context.h" -#include "test_utils.h" - -using CVC4::context::Context; -using CVC4::context::CDHashMap; - -class CDMapBlack : public CxxTest::TestSuite { - Context* d_context; - - public: - void setUp() override - { - d_context = new Context; - // Debug.on("context"); - // Debug.on("gc"); - // Debug.on("pushpop"); - } - - void tearDown() override { delete d_context; } - - // Returns the elements in a CDHashMap. - static std::map GetElements(const CDHashMap& map) { - return std::map{map.begin(), map.end()}; - } - - // Returns true if the elements in map are the same as expected. - // NOTE: This is mostly to help the type checker for matching expected within - // a TS_ASSERT. - static bool ElementsAre(const CDHashMap& map, - const std::map& expected) { - return GetElements(map) == expected; - } - - void testSimpleSequence() { - CDHashMap map(d_context); - TS_ASSERT(ElementsAre(map, {})); - - map.insert(3, 4); - TS_ASSERT(ElementsAre(map, {{3, 4}})); - - { - d_context->push(); - TS_ASSERT(ElementsAre(map, {{3, 4}})); - - map.insert(5, 6); - map.insert(9, 8); - TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); - - { - d_context->push(); - TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); - - map.insert(1, 2); - TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - - { - d_context->push(); - TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - - map.insertAtContextLevelZero(23, 317); - map.insert(1, 45); - - TS_ASSERT( - ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); - map.insert(23, 324); - - TS_ASSERT( - ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}})); - d_context->pop(); - } - - TS_ASSERT( - ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); - d_context->pop(); - } - - TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); - d_context->pop(); - } - - TS_ASSERT(ElementsAre(map, {{3, 4}, {23, 317}})); - } - - // no intervening find() in this one - // (under the theory that this could trigger a bug) - void testSimpleSequenceFewerFinds() { - CDHashMap map(d_context); - map.insert(3, 4); - - { - d_context->push(); - - map.insert(5, 6); - map.insert(9, 8); - - { - d_context->push(); - - map.insert(1, 2); - - TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - { - d_context->push(); - d_context->pop(); - } - - d_context->pop(); - } - - d_context->pop(); - } - } - - void testInsertAtContextLevelZero() { - CDHashMap map(d_context); - - map.insert(3, 4); - - TS_ASSERT(ElementsAre(map, {{3, 4}})); - { - d_context->push(); - TS_ASSERT(ElementsAre(map, {{3, 4}})); - - map.insert(5, 6); - map.insert(9, 8); - - TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); - - { - d_context->push(); - - TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); - - map.insert(1, 2); - - TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); - - map.insertAtContextLevelZero(23, 317); - - TS_ASSERT( - ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); - - TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 317)); - TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 472)); - map.insert(23, 472); - - TS_ASSERT( - ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); - { - d_context->push(); - - TS_ASSERT( - ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); - - TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0)); - map.insert(23, 1024); - - TS_ASSERT( - ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}})); - d_context->pop(); - } - TS_ASSERT( - ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); - d_context->pop(); - } - - - TS_ASSERT( - ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); - - TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0)); - map.insert(23, 477); - - TS_ASSERT( - ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}})); - d_context->pop(); - } - - TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0)); - - TS_ASSERT( - ElementsAre(map, {{3, 4}, {23, 317}})); - } -};