google test: util: Migrate bitvector_black. (#6015)

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 82aa2e0a28367d657956afa2c5e071a464c53758..fb76f49e22eeeec81c19ac9c7a58d905ccdbc8f5 100644 (file)
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -14,7 +14,7 @@
 cvc4_add_unit_test_white(array_store_all_white util)
 cvc4_add_unit_test_white(assert_white util)
 cvc4_add_unit_test_black(binary_heap_black util)
-cvc4_add_cxx_unit_test_black(bitvector_black util)
+cvc4_add_unit_test_black(bitvector_black util)
 cvc4_add_unit_test_black(boolean_simplification_black util)
 cvc4_add_unit_test_black(cardinality_black util)
 cvc4_add_unit_test_white(check_white util)

diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
new file mode 100644 (file)
index 0000000..218d314
--- /dev/null
+++ b/test/unit/util/bitvector_black.cpp
@@ -0,0 +1,199 @@
+/*********************                                                        */
+/*! \file bitvector_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::BitVector
+ **
+ ** Black box testing of CVC4::BitVector.
+ **/
+
+#include <sstream>
+
+#include "test.h"
+#include "util/bitvector.h"
+
+namespace CVC4 {
+namespace test {
+
+class TestUtilBlackBitVector : public TestInternal
+{
+ protected:
+  void SetUp() override
+  {
+    d_zero = BitVector(4);
+    d_one = d_zero.setBit(0, true);
+    d_two = BitVector("0010", 2);
+    d_neg_one = BitVector(4, Integer(-1));
+    d_ones = BitVector::mkOnes(4);
+  }
+
+  BitVector d_zero;
+  BitVector d_one;
+  BitVector d_two;
+  BitVector d_neg_one;
+  BitVector d_ones;
+};
+
+TEST_F(TestUtilBlackBitVector, string_constructor)
+{
+  BitVector b1("0101", 2);
+  ASSERT_EQ(4u, b1.getSize());
+  ASSERT_EQ("0101", b1.toString());
+  ASSERT_EQ("5", b1.toString(10));
+  ASSERT_EQ("5", b1.toString(16));
+
+  BitVector b2("000001", 2);
+  ASSERT_EQ(6u, b2.getSize());
+  ASSERT_EQ("000001", b2.toString());
+  ASSERT_EQ("1", b2.toString(10));
+  ASSERT_EQ("1", b2.toString(16));
+
+  BitVector b3("7f", 16);
+  ASSERT_EQ(8u, b3.getSize());
+  ASSERT_EQ("01111111", b3.toString());
+  ASSERT_EQ("127", b3.toString(10));
+  ASSERT_EQ("7f", b3.toString(16));
+
+  BitVector b4("01a", 16);
+  ASSERT_EQ(12u, b4.getSize());
+  ASSERT_EQ("000000011010", b4.toString());
+  ASSERT_EQ("26", b4.toString(10));
+  ASSERT_EQ("1a", b4.toString(16));
+}
+
+TEST_F(TestUtilBlackBitVector, conversions)
+{
+  ASSERT_EQ(d_two.toSignedInteger(), Integer(2));
+  ASSERT_EQ(d_neg_one.toString(), "1111");
+  ASSERT_EQ(d_neg_one.getValue(), Integer(15));
+  ASSERT_EQ(d_neg_one.getSize(), 4);
+  ASSERT_EQ(d_neg_one.toInteger(), Integer(15));
+  ASSERT_EQ(d_neg_one.toSignedInteger(), Integer(-1));
+
+  ASSERT_EQ(d_zero.hash(), (d_one - d_one).hash());
+  ASSERT_NE(d_neg_one.hash(), d_zero.hash());
+}
+
+TEST_F(TestUtilBlackBitVector, setBit_getBit)
+{
+  ASSERT_EQ(d_one.setBit(1, true).setBit(2, true).setBit(3, true), d_ones);
+  ASSERT_EQ(d_ones.setBit(0, false).setBit(1, false).setBit(2, false).setBit(
+                3, false),
+            d_zero);
+  ASSERT_EQ(d_ones.setBit(0, false).setBit(0, true), d_ones);
+  ASSERT_EQ(d_ones.setBit(0, false), ~BitVector::mkOne(d_one.getSize()));
+
+  ASSERT_TRUE(d_ones.isBitSet(3));
+  ASSERT_FALSE(d_two.isBitSet(3));
+
+  ASSERT_EQ(d_one.getValue(), Integer(1));
+  ASSERT_EQ(d_zero.isPow2(), 0);
+  ASSERT_EQ(d_one.isPow2(), 1);
+  ASSERT_EQ(d_two.isPow2(), 2);
+  ASSERT_EQ(d_ones.isPow2(), 0);
+}
+
+TEST_F(TestUtilBlackBitVector, concat_extract)
+{
+  BitVector b = d_one.concat(d_zero);
+  ASSERT_EQ(b.toString(), "00010000");
+  ASSERT_EQ(b.extract(7, 4), d_one);
+  ASSERT_THROW(b.extract(4, 7), IllegalArgumentException);
+  ASSERT_THROW(b.extract(8, 3), IllegalArgumentException);
+  ASSERT_EQ(b.concat(BitVector()), b);
+}
+
+TEST_F(TestUtilBlackBitVector, comparisons)
+{
+  ASSERT_NE(d_zero, d_one);
+  ASSERT_TRUE(d_neg_one > d_zero);
+  ASSERT_TRUE(d_neg_one >= d_zero);
+  ASSERT_TRUE(d_neg_one >= d_neg_one);
+  ASSERT_TRUE(d_neg_one == d_neg_one);
+  ASSERT_TRUE(d_zero.unsignedLessThan(d_neg_one));
+  ASSERT_TRUE(d_zero.unsignedLessThanEq(d_neg_one));
+  ASSERT_TRUE(d_zero.unsignedLessThanEq(d_zero));
+  ASSERT_TRUE(d_zero < d_neg_one);
+  ASSERT_TRUE(d_zero <= d_neg_one);
+  ASSERT_TRUE(d_zero <= d_zero);
+  ASSERT_TRUE(d_neg_one.signedLessThan(d_zero));
+  ASSERT_TRUE(d_neg_one.signedLessThanEq(d_zero));
+  ASSERT_TRUE(d_neg_one.signedLessThanEq(d_neg_one));
+
+  BitVector b = d_neg_one.concat(d_neg_one);
+  ASSERT_THROW(b.unsignedLessThan(d_neg_one), IllegalArgumentException);
+  ASSERT_THROW(d_neg_one.unsignedLessThanEq(b), IllegalArgumentException);
+  ASSERT_THROW(b.signedLessThan(d_neg_one), IllegalArgumentException);
+  ASSERT_THROW(d_neg_one.signedLessThanEq(b), IllegalArgumentException);
+}
+
+TEST_F(TestUtilBlackBitVector, bitwise_operators)
+{
+  ASSERT_EQ((d_one ^ d_neg_one).toString(), "1110");
+  ASSERT_EQ((d_two | d_one).toString(), "0011");
+  ASSERT_EQ((d_neg_one & d_two).toString(), "0010");
+  ASSERT_EQ((~d_two).toString(), "1101");
+}
+
+TEST_F(TestUtilBlackBitVector, arithmetic)
+{
+  ASSERT_EQ(d_neg_one + d_one, d_zero);
+  ASSERT_EQ((d_neg_one - d_one).getValue(), Integer(14));
+  ASSERT_EQ((-d_neg_one).getValue(), Integer(1));
+
+  ASSERT_EQ((d_two * (d_two + d_one)).getValue(), Integer(6));
+
+  ASSERT_EQ(d_two.unsignedDivTotal(d_zero), d_neg_one);
+  ASSERT_EQ(d_neg_one.unsignedDivTotal(d_two).getValue(), Integer(7));
+
+  ASSERT_EQ(d_two.unsignedRemTotal(d_zero), d_two);
+  ASSERT_EQ(d_neg_one.unsignedRemTotal(d_two), d_one);
+
+  BitVector b = d_neg_one.concat(d_neg_one);
+  ASSERT_THROW(b + d_neg_one, IllegalArgumentException);
+  ASSERT_THROW(d_neg_one * b, IllegalArgumentException);
+  ASSERT_THROW(b.unsignedDivTotal(d_neg_one), IllegalArgumentException);
+  ASSERT_THROW(d_neg_one.unsignedRemTotal(b), IllegalArgumentException);
+}
+
+TEST_F(TestUtilBlackBitVector, extend_operators)
+{
+  ASSERT_EQ(d_one.zeroExtend(4), d_zero.concat(d_one));
+  ASSERT_EQ(d_one.zeroExtend(0), d_one);
+  ASSERT_EQ(d_neg_one.signExtend(4), d_neg_one.concat(d_neg_one));
+  ASSERT_EQ(d_one.signExtend(4), d_zero.concat(d_one));
+  ASSERT_EQ(d_one.signExtend(0), d_one);
+}
+
+TEST_F(TestUtilBlackBitVector, shift_operators)
+{
+  ASSERT_EQ(d_one.leftShift(d_one), d_two);
+  ASSERT_EQ(d_one.leftShift(d_neg_one), d_zero);
+  ASSERT_EQ(d_one.leftShift(d_zero), d_one);
+
+  ASSERT_EQ(d_two.logicalRightShift(d_one), d_one);
+  ASSERT_EQ(d_two.logicalRightShift(d_neg_one), d_zero);
+
+  ASSERT_EQ(d_two.arithRightShift(d_one), d_one);
+  ASSERT_EQ(d_neg_one.arithRightShift(d_one), d_neg_one);
+  ASSERT_EQ(d_neg_one.arithRightShift(d_neg_one), d_neg_one);
+  ASSERT_EQ(d_two.arithRightShift(d_neg_one), d_zero);
+}
+
+TEST_F(TestUtilBlackBitVector, static_helpers)
+{
+  ASSERT_EQ(BitVector::mkZero(4), d_zero);
+  ASSERT_EQ(BitVector::mkOne(4), d_one);
+  ASSERT_EQ(BitVector::mkOnes(4), d_neg_one);
+  ASSERT_EQ(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8));
+  ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
deleted file mode 100644 (file)
index 417410c..0000000
--- a/test/unit/util/bitvector_black.h
+++ /dev/null
@@ -1,200 +0,0 @@
-/*********************                                                        */
-/*! \file bitvector_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Christopher L. Conway, 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::BitVector
- **
- ** Black box testing of CVC4::BitVector.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <sstream>
-
-#include "util/bitvector.h"
-
-using namespace CVC4;
-using namespace std;
-
-class BitVectorBlack : public CxxTest::TestSuite {
-
-
-public:
- void setUp() override
- {
-   zero = BitVector(4);
-   one = zero.setBit(0, true);
-   two = BitVector("0010", 2);
-   negOne = BitVector(4, Integer(-1));
-   ones = BitVector::mkOnes(4);
- }
-
- void testStringConstructor()
- {
-   BitVector b1("0101", 2);
-   TS_ASSERT_EQUALS(4u, b1.getSize());
-   TS_ASSERT_EQUALS("0101", b1.toString());
-   TS_ASSERT_EQUALS("5", b1.toString(10));
-   TS_ASSERT_EQUALS("5", b1.toString(16));
-
-   BitVector b2("000001", 2);
-   TS_ASSERT_EQUALS(6u, b2.getSize());
-   TS_ASSERT_EQUALS("000001", b2.toString());
-   TS_ASSERT_EQUALS("1", b2.toString(10));
-   TS_ASSERT_EQUALS("1", b2.toString(16));
-
-   BitVector b3("7f", 16);
-   TS_ASSERT_EQUALS(8u, b3.getSize());
-   TS_ASSERT_EQUALS("01111111", b3.toString());
-   TS_ASSERT_EQUALS("127", b3.toString(10));
-   TS_ASSERT_EQUALS("7f", b3.toString(16));
-
-   BitVector b4("01a", 16);
-   TS_ASSERT_EQUALS(12u, b4.getSize());
-   TS_ASSERT_EQUALS("000000011010", b4.toString());
-   TS_ASSERT_EQUALS("26", b4.toString(10));
-   TS_ASSERT_EQUALS("1a", b4.toString(16));
-  }
-
-  void testConversions()
-  {
-    TS_ASSERT_EQUALS(two.toSignedInteger(), Integer(2));
-    TS_ASSERT_EQUALS(negOne.toString(), "1111");
-    TS_ASSERT_EQUALS(negOne.getValue(), Integer(15));
-    TS_ASSERT_EQUALS(negOne.getSize(), 4);
-    TS_ASSERT_EQUALS(negOne.toInteger(), Integer(15));
-    TS_ASSERT_EQUALS(negOne.toSignedInteger(), Integer(-1));
-
-    TS_ASSERT_EQUALS(zero.hash(), (one - one).hash());
-    TS_ASSERT_DIFFERS(negOne.hash(), zero.hash());
-  }
-
-  void testSetGetBit()
-  {
-    TS_ASSERT_EQUALS(one.setBit(1, true).setBit(2, true).setBit(3, true), ones);
-    TS_ASSERT_EQUALS(
-        ones.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3,
-                                                                       false),
-        zero);
-    TS_ASSERT_EQUALS(ones.setBit(0, false).setBit(0, true), ones);
-    TS_ASSERT_EQUALS(ones.setBit(0, false), ~BitVector::mkOne(one.getSize()));
-
-    TS_ASSERT(ones.isBitSet(3));
-    TS_ASSERT(!two.isBitSet(3));
-
-    TS_ASSERT_EQUALS(one.getValue(), Integer(1));
-    TS_ASSERT_EQUALS(zero.isPow2(), 0);
-    TS_ASSERT_EQUALS(one.isPow2(), 1);
-    TS_ASSERT_EQUALS(two.isPow2(), 2);
-    TS_ASSERT_EQUALS(ones.isPow2(), 0);
-  }
-
-  void testConcatExtract()
-  {
-    BitVector b = one.concat(zero);
-    TS_ASSERT_EQUALS(b.toString(), "00010000");
-    TS_ASSERT_EQUALS(b.extract(7, 4), one);
-    TS_ASSERT_THROWS(b.extract(4, 7), IllegalArgumentException&);
-    TS_ASSERT_THROWS(b.extract(8, 3), IllegalArgumentException&);
-    TS_ASSERT_EQUALS(b.concat(BitVector()), b);
-  }
-
-  void testComparisons()
-  {
-    TS_ASSERT_DIFFERS(zero, one);
-    TS_ASSERT(negOne > zero);
-    TS_ASSERT(negOne >= zero);
-    TS_ASSERT(negOne >= negOne);
-    TS_ASSERT(negOne == negOne);
-    TS_ASSERT(zero.unsignedLessThan(negOne));
-    TS_ASSERT(zero.unsignedLessThanEq(negOne));
-    TS_ASSERT(zero.unsignedLessThanEq(zero));
-    TS_ASSERT(zero < negOne);
-    TS_ASSERT(zero <= negOne);
-    TS_ASSERT(zero <= zero);
-    TS_ASSERT(negOne.signedLessThan(zero));
-    TS_ASSERT(negOne.signedLessThanEq(zero));
-    TS_ASSERT(negOne.signedLessThanEq(negOne));
-
-    BitVector b = negOne.concat(negOne);
-    TS_ASSERT_THROWS(b.unsignedLessThan(negOne), IllegalArgumentException&);
-    TS_ASSERT_THROWS(negOne.unsignedLessThanEq(b), IllegalArgumentException&);
-    TS_ASSERT_THROWS(b.signedLessThan(negOne), IllegalArgumentException&);
-    TS_ASSERT_THROWS(negOne.signedLessThanEq(b), IllegalArgumentException&);
-  }
-
-  void testBitwiseOps()
-  {
-    TS_ASSERT_EQUALS((one ^ negOne).toString(), "1110");
-    TS_ASSERT_EQUALS((two | one).toString(), "0011");
-    TS_ASSERT_EQUALS((negOne & two).toString(), "0010");
-    TS_ASSERT_EQUALS((~two).toString(), "1101");
-  }
-
-  void testArithmetic()
-  {
-    TS_ASSERT_EQUALS(negOne + one, zero);
-    TS_ASSERT_EQUALS((negOne - one).getValue(), Integer(14));
-    TS_ASSERT_EQUALS((-negOne).getValue(), Integer(1));
-
-    TS_ASSERT_EQUALS((two * (two + one)).getValue(), Integer(6));
-
-    TS_ASSERT_EQUALS(two.unsignedDivTotal(zero), negOne);
-    TS_ASSERT_EQUALS(negOne.unsignedDivTotal(two).getValue(), Integer(7));
-
-    TS_ASSERT_EQUALS(two.unsignedRemTotal(zero), two);
-    TS_ASSERT_EQUALS(negOne.unsignedRemTotal(two), one);
-
-    BitVector b = negOne.concat(negOne);
-    TS_ASSERT_THROWS(b + negOne, IllegalArgumentException&);
-    TS_ASSERT_THROWS(negOne * b, IllegalArgumentException&);
-    TS_ASSERT_THROWS(b.unsignedDivTotal(negOne), IllegalArgumentException&);
-    TS_ASSERT_THROWS(negOne.unsignedRemTotal(b), IllegalArgumentException&);
-  }
-
-  void testExtendOps()
-  {
-    TS_ASSERT_EQUALS(one.zeroExtend(4), zero.concat(one));
-    TS_ASSERT_EQUALS(one.zeroExtend(0), one);
-    TS_ASSERT_EQUALS(negOne.signExtend(4), negOne.concat(negOne));
-    TS_ASSERT_EQUALS(one.signExtend(4), zero.concat(one));
-    TS_ASSERT_EQUALS(one.signExtend(0), one);
-  }
-
-  void testShifts()
-  {
-    TS_ASSERT_EQUALS(one.leftShift(one), two);
-    TS_ASSERT_EQUALS(one.leftShift(negOne), zero);
-    TS_ASSERT_EQUALS(one.leftShift(zero), one);
-
-    TS_ASSERT_EQUALS(two.logicalRightShift(one), one);
-    TS_ASSERT_EQUALS(two.logicalRightShift(negOne), zero);
-
-    TS_ASSERT_EQUALS(two.arithRightShift(one), one);
-    TS_ASSERT_EQUALS(negOne.arithRightShift(one), negOne);
-    TS_ASSERT_EQUALS(negOne.arithRightShift(negOne), negOne);
-    TS_ASSERT_EQUALS(two.arithRightShift(negOne), zero);
-  }
-
-  void testStaticHelpers()
-  {
-    TS_ASSERT_EQUALS(BitVector::mkZero(4), zero);
-    TS_ASSERT_EQUALS(BitVector::mkOne(4), one);
-    TS_ASSERT_EQUALS(BitVector::mkOnes(4), negOne);
-    TS_ASSERT_EQUALS(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8));
-    TS_ASSERT_EQUALS(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
-  }
-
- private:
-  BitVector zero;
-  BitVector one;
-  BitVector two;
-  BitVector negOne;
-  BitVector ones;
-};