From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 26 Feb 2021 19:59:38 +0000 (-0800)
Subject: google test: util: Migrate binary_heap_black. (#6012)
X-Git-Tag: cvc5-1.0.0~2202
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b9fe94d346b7448a0e092cc9f43013aadfe9548;p=cvc5.git

google test: util: Migrate binary_heap_black. (#6012)
---

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index bdc5a2b54..28d0ff148 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -13,7 +13,7 @@
 
 cvc4_add_cxx_unit_test_white(array_store_all_white util)
 cvc4_add_unit_test_white(assert_white util)
-cvc4_add_cxx_unit_test_black(binary_heap_black util)
+cvc4_add_unit_test_black(binary_heap_black util)
 cvc4_add_cxx_unit_test_black(bitvector_black util)
 cvc4_add_cxx_unit_test_black(boolean_simplification_black util)
 cvc4_add_cxx_unit_test_black(cardinality_public util)
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
new file mode 100644
index 000000000..a6a84f6e6
--- /dev/null
+++ b/test/unit/util/binary_heap_black.cpp
@@ -0,0 +1,233 @@
+/*********************                                                        */
+/*! \file binary_heap_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters
+ ** 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::BinaryHeap
+ **
+ ** Black box testing of CVC4::BinaryHeap.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "test.h"
+#include "util/bin_heap.h"
+
+namespace CVC4 {
+namespace test {
+
+class TestUtilBlackBinaryHeap : public TestInternal
+{
+ protected:
+  struct Elem
+  {
+    Elem(int32_t y) : d_x(y) {}
+    int32_t d_x;
+  };
+
+  struct Cmp
+  {
+    Cmp() : d_valid(false) {}
+    Cmp(int32_t x) : d_valid(true) {}
+
+    bool operator()(Elem x, Elem y) const
+    {
+      // ensure BinaryHeap<> calls our Cmp instance and not some fresh one
+      Assert(d_valid);
+      return x.d_x > y.d_x;
+    }
+
+    bool d_valid;
+  };
+};
+
+/**
+ * Test a a series of simple heaps (push a few then pop all then do others).
+ * Done as a series to test if the heap structure falls into a bad state
+ * after prolonged use.
+ */
+TEST_F(TestUtilBlackBinaryHeap, heap_series)
+{
+  BinaryHeap<int32_t> heap;
+
+  // First test a heap of 1 element
+  ASSERT_EQ(heap.size(), 0u);
+  ASSERT_TRUE(heap.empty());
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(heap.top(), "!empty\\(\\)");
+  ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
+#endif
+  ASSERT_EQ(heap.begin(), heap.end());
+
+  BinaryHeap<int32_t>::handle h5 = heap.push(5);
+  ASSERT_TRUE(h5 == h5);
+  ASSERT_EQ(heap.top(), 5);
+  ASSERT_EQ(heap.size(), 1u);
+  ASSERT_FALSE(heap.empty());
+  ASSERT_NE(heap.begin(), heap.end());
+  ASSERT_EQ(*h5, 5);
+  ASSERT_EQ(*heap.begin(), 5);
+  ASSERT_NO_THROW(heap.erase(h5));
+  ASSERT_TRUE(heap.empty());
+  ASSERT_EQ(heap.size(), 0u);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(heap.top(), "!empty\\(\\)");
+  ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
+#endif
+
+  // Next test a heap of 4 elements
+  h5 = heap.push(5);
+  BinaryHeap<int32_t>::handle h3 = heap.push(3);
+  BinaryHeap<int32_t>::handle h10 = heap.push(10);
+  BinaryHeap<int32_t>::handle h2 = heap.push(2);
+  ASSERT_NE(h5, h3);
+  ASSERT_NE(h5, h10);
+  ASSERT_NE(h5, h2);
+  ASSERT_NE(h3, h10);
+  ASSERT_NE(h3, h2);
+  ASSERT_NE(h10, h2);
+  ASSERT_NE(heap.begin(), heap.end());
+  ASSERT_EQ(*heap.begin(), 10);
+  ASSERT_EQ(*h2, 2);
+  ASSERT_EQ(*h3, 3);
+  ASSERT_EQ(*h5, 5);
+  ASSERT_EQ(*h10, 10);
+  ASSERT_EQ(heap.top(), 10);
+  // test the iterator (note the order of elements isn't guaranteed!)
+  BinaryHeap<int32_t>::const_iterator i = heap.begin();
+  ASSERT_NE(i, heap.end());
+  ASSERT_NO_THROW(*i++);
+  ASSERT_NE(i, heap.end());
+  ASSERT_NO_THROW(*i++);
+  ASSERT_NE(i, heap.end());
+  ASSERT_NO_THROW(*i++);
+  ASSERT_NE(i, heap.end());
+  ASSERT_NO_THROW(*i++);
+  ASSERT_EQ(i, heap.end());
+  ASSERT_FALSE(heap.empty());
+  ASSERT_EQ(heap.size(), 4u);
+  ASSERT_NO_THROW(heap.pop());
+  ASSERT_NE(heap.begin(), heap.end());
+  ASSERT_EQ(*heap.begin(), 5);
+  ASSERT_EQ(heap.top(), 5);
+  ASSERT_FALSE(heap.empty());
+  ASSERT_EQ(heap.size(), 3u);
+  ASSERT_NO_THROW(heap.pop());
+  ASSERT_NE(heap.begin(), heap.end());
+  ASSERT_EQ(*heap.begin(), 3);
+  ASSERT_EQ(heap.top(), 3);
+  ASSERT_FALSE(heap.empty());
+  ASSERT_EQ(heap.size(), 2u);
+  ASSERT_NO_THROW(heap.pop());
+  ASSERT_NE(heap.begin(), heap.end());
+  ASSERT_EQ(*heap.begin(), 2);
+  ASSERT_EQ(heap.top(), 2);
+  ASSERT_FALSE(heap.empty());
+  ASSERT_EQ(heap.size(), 1u);
+  ASSERT_NO_THROW(heap.pop());
+  ASSERT_EQ(heap.begin(), heap.end());
+  ASSERT_TRUE(heap.empty());
+  ASSERT_EQ(heap.size(), 0u);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(heap.top(), "!empty\\(\\)");
+  ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
+#endif
+
+  // Now with a few updates
+  h5 = heap.push(5);
+  h3 = heap.push(3);
+  h10 = heap.push(10);
+  h2 = heap.push(2);
+
+  ASSERT_EQ(*h5, 5);
+  ASSERT_EQ(*h3, 3);
+  ASSERT_EQ(*h10, 10);
+  ASSERT_EQ(*h2, 2);
+
+  ASSERT_EQ(heap.top(), 10);
+  heap.update(h10, -10);
+  ASSERT_EQ(*h10, -10);
+  ASSERT_EQ(heap.top(), 5);
+  heap.erase(h2);
+  ASSERT_EQ(heap.top(), 5);
+  heap.update(h3, -20);
+  ASSERT_EQ(*h3, -20);
+  ASSERT_EQ(heap.top(), 5);
+  heap.pop();
+  ASSERT_EQ(heap.top(), -10);
+  heap.pop();
+  ASSERT_EQ(heap.top(), -20);
+}
+
+TEST_F(TestUtilBlackBinaryHeap, large_heap)
+{
+  BinaryHeap<Elem, Cmp> heap(Cmp(0));
+  std::vector<BinaryHeap<Elem, Cmp>::handle> handles;
+  ASSERT_TRUE(heap.empty());
+  for (int32_t x = 0; x < 1000; ++x)
+  {
+    handles.push_back(heap.push(Elem(x)));
+  }
+  ASSERT_FALSE(heap.empty());
+  ASSERT_EQ(heap.size(), 1000u);
+  heap.update(handles[100], 50);
+  heap.update(handles[100], -50);
+  heap.update(handles[600], 2);
+  heap.update(handles[184], -9);
+  heap.update(handles[987], 9555);
+  heap.update(handles[672], -1003);
+  heap.update(handles[781], 481);
+  heap.update(handles[9], 9619);
+  heap.update(handles[919], 111);
+  ASSERT_EQ(heap.size(), 1000u);
+  heap.erase(handles[10]);
+  ASSERT_EQ(heap.size(), 999u);
+  ASSERT_FALSE(heap.empty());
+  handles.clear();
+  Elem last = heap.top();
+  for (int32_t x = 0; x < 800; ++x)
+  {
+    ASSERT_LE(last.d_x, heap.top().d_x);
+    last = heap.top();
+    heap.pop();
+    ASSERT_EQ(heap.size(), 998u - x);
+    ASSERT_FALSE(heap.empty());
+  }
+  ASSERT_EQ(heap.size(), 199u);
+  for (int32_t x = 0; x < 10000; ++x)
+  {
+    // two-thirds of the time insert large value, one-third insert small value
+    handles.push_back(heap.push(Elem(4 * ((x % 3 == 0) ? -x : x))));
+    if (x % 10 == 6)
+    {
+      // also every tenth insert somewhere in the middle
+      handles.push_back(heap.push(Elem(x / 10)));
+    }
+    // change a few
+    heap.update(handles[x / 10], 4 * (*handles[x / 10]).d_x);
+    heap.update(handles[x / 105], (*handles[x / 4]).d_x - 294);
+    heap.update(handles[x / 33], 6 * (*handles[x / 82]).d_x / 5 - 1);
+    ASSERT_EQ(heap.size(), size_t(x) + ((x + 4) / 10) + 200);
+  }
+  ASSERT_EQ(heap.size(), 11199u);
+  ASSERT_FALSE(heap.empty());
+  last = heap.top();
+  while (!heap.empty())
+  {
+    ASSERT_LE(last.d_x, heap.top().d_x);
+    last = heap.top();
+    heap.pop();
+  }
+  ASSERT_TRUE(heap.empty());
+  heap.clear();
+  ASSERT_TRUE(heap.empty());
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h
deleted file mode 100644
index 9514b62e9..000000000
--- a/test/unit/util/binary_heap_black.h
+++ /dev/null
@@ -1,226 +0,0 @@
-/*********************                                                        */
-/*! \file binary_heap_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner, 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::BinaryHeap
- **
- ** Black box testing of CVC4::BinaryHeap.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <sstream>
-
-#include "test_utils.h"
-#include "util/bin_heap.h"
-
-using namespace CVC4;
-using namespace std;
-
-class BinaryHeapBlack : public CxxTest::TestSuite {
- public:
-  void setUp() override {}
-
-  void tearDown() override {}
-
-  /**
-   * Test a a series of simple heaps (push a few then pop all then do others).
-   * Done as a series to test if the heap structure falls into a bad state
-   * after prolonged use.
-   */
-  void testHeapSeries()
-  {
-    BinaryHeap<int> heap;
-
-    // First test a heap of 1 element
-    TS_ASSERT_EQUALS(heap.size(), 0u);
-    TS_ASSERT(heap.empty());
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(heap.top());
-    TS_UTILS_EXPECT_ABORT(heap.pop());
-#endif /* CVC4_ASSERTIONS */
-    TS_ASSERT_EQUALS(heap.begin(), heap.end());
-
-    BinaryHeap<int>::handle h5 = heap.push(5);
-    TS_ASSERT(h5 == h5);
-    TS_ASSERT_EQUALS(heap.top(), 5);
-    TS_ASSERT_EQUALS(heap.size(), 1u);
-    TS_ASSERT(! heap.empty());
-    TS_ASSERT_DIFFERS(heap.begin(), heap.end());
-    TS_ASSERT_EQUALS(*h5, 5);
-    TS_ASSERT_EQUALS(*heap.begin(), 5);
-    TS_ASSERT_THROWS_NOTHING(heap.erase(h5));
-    TS_ASSERT(heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 0u);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(heap.top());
-    TS_UTILS_EXPECT_ABORT(heap.pop());
-#endif /* CVC4_ASSERTIONS */
-
-    // Next test a heap of 4 elements
-    h5 = heap.push(5);
-    BinaryHeap<int>::handle h3 = heap.push(3);
-    BinaryHeap<int>::handle h10 = heap.push(10);
-    BinaryHeap<int>::handle h2 = heap.push(2);
-    TS_ASSERT_DIFFERS(h5, h3);
-    TS_ASSERT_DIFFERS(h5, h10);
-    TS_ASSERT_DIFFERS(h5, h2);
-    TS_ASSERT_DIFFERS(h3, h10);
-    TS_ASSERT_DIFFERS(h3, h2);
-    TS_ASSERT_DIFFERS(h10, h2);
-    TS_ASSERT_DIFFERS(heap.begin(), heap.end());
-    TS_ASSERT_EQUALS(*heap.begin(), 10);
-    TS_ASSERT_EQUALS(*h2, 2);
-    TS_ASSERT_EQUALS(*h3, 3);
-    TS_ASSERT_EQUALS(*h5, 5);
-    TS_ASSERT_EQUALS(*h10, 10);
-    TS_ASSERT_EQUALS(heap.top(), 10);
-    // test the iterator (note the order of elements isn't guaranteed!)
-    BinaryHeap<int>::const_iterator i = heap.begin();
-    TS_ASSERT_DIFFERS(i, heap.end());
-    TS_ASSERT_THROWS_NOTHING(*i++);
-    TS_ASSERT_DIFFERS(i, heap.end());
-    TS_ASSERT_THROWS_NOTHING(*i++);
-    TS_ASSERT_DIFFERS(i, heap.end());
-    TS_ASSERT_THROWS_NOTHING(*i++);
-    TS_ASSERT_DIFFERS(i, heap.end());
-    TS_ASSERT_THROWS_NOTHING(*i++);
-    TS_ASSERT_EQUALS(i, heap.end());
-    TS_ASSERT(!heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 4u);
-    TS_ASSERT_THROWS_NOTHING(heap.pop());
-    TS_ASSERT_DIFFERS(heap.begin(), heap.end());
-    TS_ASSERT_EQUALS(*heap.begin(), 5);
-    TS_ASSERT_EQUALS(heap.top(), 5);
-    TS_ASSERT(!heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 3u);
-    TS_ASSERT_THROWS_NOTHING(heap.pop());
-    TS_ASSERT_DIFFERS(heap.begin(), heap.end());
-    TS_ASSERT_EQUALS(*heap.begin(), 3);
-    TS_ASSERT_EQUALS(heap.top(), 3);
-    TS_ASSERT(!heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 2u);
-    TS_ASSERT_THROWS_NOTHING(heap.pop());
-    TS_ASSERT_DIFFERS(heap.begin(), heap.end());
-    TS_ASSERT_EQUALS(*heap.begin(), 2);
-    TS_ASSERT_EQUALS(heap.top(), 2);
-    TS_ASSERT(!heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 1u);
-    TS_ASSERT_THROWS_NOTHING(heap.pop());
-    TS_ASSERT_EQUALS(heap.begin(), heap.end());
-    TS_ASSERT(heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 0u);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(heap.top());
-    TS_UTILS_EXPECT_ABORT(heap.pop());
-#endif /* CVC4_ASSERTIONS */
-
-    // Now with a few updates
-    h5 = heap.push(5);
-    h3 = heap.push(3);
-    h10 = heap.push(10);
-    h2 = heap.push(2);
-
-    TS_ASSERT_EQUALS(*h5, 5);
-    TS_ASSERT_EQUALS(*h3, 3);
-    TS_ASSERT_EQUALS(*h10, 10);
-    TS_ASSERT_EQUALS(*h2, 2);
-
-    TS_ASSERT_EQUALS(heap.top(), 10);
-    heap.update(h10, -10);
-    TS_ASSERT_EQUALS(*h10, -10);
-    TS_ASSERT_EQUALS(heap.top(), 5);
-    heap.erase(h2);
-    TS_ASSERT_EQUALS(heap.top(), 5);
-    heap.update(h3, -20);
-    TS_ASSERT_EQUALS(*h3, -20);
-    TS_ASSERT_EQUALS(heap.top(), 5);
-    heap.pop();
-    TS_ASSERT_EQUALS(heap.top(), -10);
-    heap.pop();
-    TS_ASSERT_EQUALS(heap.top(), -20);
-  }
-
-  struct Elem {
-    int x;
-    Elem(int y) : x(y) {}
-  };/* struct Elem */
-
-  struct Cmp {
-    bool valid;
-    Cmp() : valid(false) {}
-    Cmp(int x) : valid(true) {}
-    bool operator()(Elem x, Elem y) const {
-      // ensure BinaryHeap<> calls our Cmp instance and not some fresh one
-      TS_ASSERT(valid);
-      return x.x > y.x;
-    }
-  };/* struct Cmp */
-
-  void testLargeHeap() {
-    BinaryHeap<Elem, Cmp> heap(Cmp(0));
-    vector<BinaryHeap<Elem, Cmp>::handle> handles;
-    TS_ASSERT(heap.empty());
-    for(int x = 0; x < 1000; ++x) {
-      handles.push_back(heap.push(Elem(x)));
-    }
-    TS_ASSERT(!heap.empty());
-    TS_ASSERT_EQUALS(heap.size(), 1000u);
-    heap.update(handles[100], 50);
-    heap.update(handles[100], -50);
-    heap.update(handles[600], 2);
-    heap.update(handles[184], -9);
-    heap.update(handles[987], 9555);
-    heap.update(handles[672], -1003);
-    heap.update(handles[781], 481);
-    heap.update(handles[9], 9619);
-    heap.update(handles[919], 111);
-    TS_ASSERT_EQUALS(heap.size(), 1000u);
-    heap.erase(handles[10]);
-    TS_ASSERT_EQUALS(heap.size(), 999u);
-    TS_ASSERT(!heap.empty());
-    handles.clear();
-    Elem last = heap.top();
-    for(int x = 0; x < 800; ++x) {
-      TS_ASSERT_LESS_THAN_EQUALS(last.x, heap.top().x);
-      last = heap.top();
-      heap.pop();
-      TS_ASSERT_EQUALS(heap.size(), 998u - x);
-      TS_ASSERT(!heap.empty());
-    }
-    TS_ASSERT_EQUALS(heap.size(), 199u);
-    for(int x = 0; x < 10000; ++x) {
-      // two-thirds of the time insert large value, one-third insert small value
-      handles.push_back(heap.push(Elem(4 * ((x % 3 == 0) ? -x : x))));
-      if(x % 10 == 6) {
-        // also every tenth insert somewhere in the middle
-        handles.push_back(heap.push(Elem(x / 10)));
-      }
-      // change a few
-      heap.update(handles[x / 10], 4 * (*handles[x / 10]).x);
-      heap.update(handles[x / 105], (*handles[x / 4]).x - 294);
-      heap.update(handles[x / 33], 6 * (*handles[x / 82]).x / 5 - 1);
-      TS_ASSERT_EQUALS(heap.size(), size_t(x) + ((x + 4) / 10) + 200);
-    }
-    TS_ASSERT_EQUALS(heap.size(), 11199u);
-    TS_ASSERT(!heap.empty());
-    last = heap.top();
-    while(!heap.empty()) {
-      TS_ASSERT_LESS_THAN_EQUALS(last.x, heap.top().x);
-      last = heap.top();
-      heap.pop();
-    }
-    TS_ASSERT(heap.empty());
-    heap.clear();
-    TS_ASSERT(heap.empty());
-  }
-
-};/* class BinaryHeapBlack */