From 7ea491461182a4740c91cac37b8752e042d1a4bb Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 1 Mar 2021 14:46:53 -0800 Subject: [PATCH] google test: util: Migrate bitvector_black. (#6015) --- test/unit/util/CMakeLists.txt | 2 +- test/unit/util/bitvector_black.cpp | 199 ++++++++++++++++++++++++++++ test/unit/util/bitvector_black.h | 200 ----------------------------- 3 files changed, 200 insertions(+), 201 deletions(-) create mode 100644 test/unit/util/bitvector_black.cpp delete mode 100644 test/unit/util/bitvector_black.h diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 82aa2e0a2..fb76f49e2 100644 --- 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 index 000000000..218d31465 --- /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 + +#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 index 417410c9e..000000000 --- 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 -#include - -#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; -}; -- 2.30.2