google test: context: Migrate cdmap_black. (#5584)

diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index d88ee26614b1204db22a6fb4f5fcc1dd30f9dcc0..d19ad60c0aec3d92861efd52e1cacbf0e48ea571 100644 (file)
--- 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 (file)
index 0000000..e9112db
--- /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 <map>
+
+#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<int32_t, int32_t> get_elements(
+      const CDHashMap<int32_t, int32_t>& map)
+  {
+    return std::map<int32_t, int32_t>{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<int32_t, int32_t>& map,
+                           const std::map<int32_t, int32_t>& expected)
+  {
+    return get_elements(map) == expected;
+  }
+};
+
+TEST_F(TestContextCDMapBlack, simple_sequence)
+{
+  CDHashMap<int32_t, int32_t> 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<int, int> 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<int, int> 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 (file)
index 5bded0a..0000000
--- 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 <cxxtest/TestSuite.h>
-
-#include <map>
-
-#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<int, int> GetElements(const CDHashMap<int, int>& map) {
-    return std::map<int, int>{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<int, int>& map,
-                          const std::map<int, int>& expected) {
-    return GetElements(map) == expected;
-  }
-
-  void testSimpleSequence() {
-    CDHashMap<int, int> 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<int, int> 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<int, int> 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}}));
-  }
-};