From 10505e1b0de600f623fcb26e9a17137264d4f527 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 26 Feb 2021 16:30:39 -0800 Subject: [PATCH] google test: util: Migrate cardinality_black. (#6016) --- test/unit/util/CMakeLists.txt | 2 +- test/unit/util/cardinality_black.cpp | 272 +++++++++++++++++++++++++++ test/unit/util/cardinality_public.h | 264 -------------------------- 3 files changed, 273 insertions(+), 265 deletions(-) create mode 100644 test/unit/util/cardinality_black.cpp delete mode 100644 test/unit/util/cardinality_public.h diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 28d0ff148..710cbf28c 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -16,7 +16,7 @@ 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_cxx_unit_test_black(boolean_simplification_black util) -cvc4_add_cxx_unit_test_black(cardinality_public util) +cvc4_add_unit_test_black(cardinality_black util) cvc4_add_cxx_unit_test_white(check_white util) cvc4_add_cxx_unit_test_black(configuration_black util) cvc4_add_cxx_unit_test_black(datatype_black util) diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp new file mode 100644 index 000000000..832965836 --- /dev/null +++ b/test/unit/util/cardinality_black.cpp @@ -0,0 +1,272 @@ +/********************* */ +/*! \file cardinality_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 Public-box testing of CVC4::Cardinality + ** + ** Public-box testing of CVC4::Cardinality. + **/ + +#include +#include + +#include "test.h" +#include "util/cardinality.h" +#include "util/integer.h" + +namespace CVC4 { +namespace test { + +class TestUtilBlackCardinality : public TestInternal +{ + protected: + std::stringstream ss; +}; + +TEST_F(TestUtilBlackCardinality, cardinalities) +{ + Cardinality zero(0); + Cardinality one(1); + Cardinality two(2); + + Cardinality invalid(0); + ASSERT_THROW(invalid = Cardinality(-1), IllegalArgumentException); + ASSERT_THROW(invalid = Cardinality(-2), IllegalArgumentException); + ASSERT_THROW(invalid = Cardinality(Integer("-3983982192391747295721957")), + IllegalArgumentException); + invalid = one; // test assignment + invalid = Cardinality(5); // test assignment to temporary + + Cardinality copy(one); // test copy + Cardinality big(Integer("3983982192391747295721957")); + Cardinality r(Cardinality::REALS); + Cardinality i(Cardinality::INTEGERS); + + ASSERT_EQ(zero.compare(one), Cardinality::LESS); + ASSERT_EQ(one.compare(two), Cardinality::LESS); + ASSERT_EQ(two.compare(invalid), Cardinality::LESS); + ASSERT_EQ(invalid.compare(big), Cardinality::LESS); + ASSERT_EQ(big.compare(i), Cardinality::LESS); + ASSERT_EQ(i.compare(r), Cardinality::LESS); + + ASSERT_NE(zero.compare(one), Cardinality::GREATER); + ASSERT_NE(zero.compare(zero), Cardinality::GREATER); + ASSERT_NE(one.compare(two), Cardinality::GREATER); + ASSERT_NE(one.compare(one), Cardinality::GREATER); + ASSERT_NE(two.compare(invalid), Cardinality::GREATER); + ASSERT_NE(two.compare(two), Cardinality::GREATER); + ASSERT_NE(invalid.compare(big), Cardinality::GREATER); + ASSERT_NE(invalid.compare(invalid), Cardinality::GREATER); + ASSERT_NE(big.compare(i), Cardinality::GREATER); + ASSERT_NE(big.compare(big), Cardinality::GREATER); + ASSERT_NE(i.compare(r), Cardinality::GREATER); + ASSERT_NE(i.compare(i), Cardinality::GREATER); + ASSERT_NE(r.compare(r), Cardinality::GREATER); + + ASSERT_EQ(zero.compare(zero), Cardinality::EQUAL); + ASSERT_EQ(one.compare(one), Cardinality::EQUAL); + ASSERT_EQ(two.compare(two), Cardinality::EQUAL); + ASSERT_EQ(invalid.compare(invalid), Cardinality::EQUAL); + ASSERT_EQ(copy.compare(copy), Cardinality::EQUAL); + ASSERT_EQ(copy.compare(one), Cardinality::EQUAL); + ASSERT_EQ(one.compare(copy), Cardinality::EQUAL); + ASSERT_EQ(big.compare(big), Cardinality::UNKNOWN); + ASSERT_EQ(i.compare(i), Cardinality::EQUAL); + ASSERT_EQ(r.compare(r), Cardinality::EQUAL); + + ASSERT_NE(zero.compare(one), Cardinality::EQUAL); + ASSERT_NE(one.compare(two), Cardinality::EQUAL); + ASSERT_NE(two.compare(invalid), Cardinality::EQUAL); + ASSERT_NE(copy.compare(r), Cardinality::EQUAL); + ASSERT_NE(copy.compare(i), Cardinality::EQUAL); + ASSERT_NE(big.compare(i), Cardinality::EQUAL); + ASSERT_NE(i.compare(big), Cardinality::EQUAL); + ASSERT_NE(big.compare(zero), Cardinality::EQUAL); + ASSERT_NE(r.compare(i), Cardinality::EQUAL); + ASSERT_NE(i.compare(r), Cardinality::EQUAL); + + ASSERT_EQ(r.compare(zero), Cardinality::GREATER); + ASSERT_EQ(r.compare(one), Cardinality::GREATER); + ASSERT_EQ(r.compare(two), Cardinality::GREATER); + ASSERT_EQ(r.compare(copy), Cardinality::GREATER); + ASSERT_EQ(r.compare(invalid), Cardinality::GREATER); + ASSERT_EQ(r.compare(big), Cardinality::GREATER); + ASSERT_EQ(r.compare(i), Cardinality::GREATER); + ASSERT_NE(r.compare(r), Cardinality::GREATER); + ASSERT_NE(r.compare(r), Cardinality::LESS); + + ASSERT_TRUE(zero.isFinite()); + ASSERT_TRUE(one.isFinite()); + ASSERT_TRUE(two.isFinite()); + ASSERT_TRUE(copy.isFinite()); + ASSERT_TRUE(invalid.isFinite()); + ASSERT_TRUE(big.isFinite()); + ASSERT_FALSE(i.isFinite()); + ASSERT_FALSE(r.isFinite()); + + ASSERT_FALSE(zero.isLargeFinite()); + ASSERT_FALSE(one.isLargeFinite()); + ASSERT_FALSE(two.isLargeFinite()); + ASSERT_FALSE(copy.isLargeFinite()); + ASSERT_FALSE(invalid.isLargeFinite()); + ASSERT_TRUE(big.isLargeFinite()); + ASSERT_FALSE(i.isLargeFinite()); + ASSERT_FALSE(r.isLargeFinite()); + + ASSERT_EQ(zero.getFiniteCardinality(), 0); + ASSERT_EQ(one.getFiniteCardinality(), 1); + ASSERT_EQ(two.getFiniteCardinality(), 2); + ASSERT_EQ(copy.getFiniteCardinality(), 1); + ASSERT_EQ(invalid.getFiniteCardinality(), 5); + ASSERT_THROW(big.getFiniteCardinality(), IllegalArgumentException); + ASSERT_THROW(i.getFiniteCardinality(), IllegalArgumentException); + ASSERT_THROW(r.getFiniteCardinality(), IllegalArgumentException); + + ASSERT_THROW(zero.getBethNumber(), IllegalArgumentException); + ASSERT_THROW(one.getBethNumber(), IllegalArgumentException); + ASSERT_THROW(two.getBethNumber(), IllegalArgumentException); + ASSERT_THROW(copy.getBethNumber(), IllegalArgumentException); + ASSERT_THROW(invalid.getBethNumber(), IllegalArgumentException); + ASSERT_THROW(big.getBethNumber(), IllegalArgumentException); + ASSERT_TRUE(i.getBethNumber() == 0); + ASSERT_TRUE(r.getBethNumber() == 1); + + ASSERT_NE(zero.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_NE(one.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_NE(two.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_NE(copy.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_NE(invalid.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_NE(big.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_NE(r.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + ASSERT_EQ(i.compare(Cardinality::INTEGERS), Cardinality::EQUAL); + + ASSERT_NE(zero.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_NE(one.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_NE(two.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_NE(copy.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_NE(invalid.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_NE(big.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_NE(i.compare(Cardinality::REALS), Cardinality::EQUAL); + ASSERT_EQ(r.compare(Cardinality::REALS), Cardinality::EQUAL); + + // should work the other way too + + ASSERT_NE(Cardinality::INTEGERS.compare(zero), Cardinality::EQUAL); + ASSERT_NE(Cardinality::INTEGERS.compare(one), Cardinality::EQUAL); + ASSERT_NE(Cardinality::INTEGERS.compare(two), Cardinality::EQUAL); + ASSERT_NE(Cardinality::INTEGERS.compare(copy), Cardinality::EQUAL); + ASSERT_NE(Cardinality::INTEGERS.compare(invalid), Cardinality::EQUAL); + ASSERT_NE(Cardinality::INTEGERS.compare(big), Cardinality::EQUAL); + ASSERT_NE(Cardinality::INTEGERS.compare(r), Cardinality::EQUAL); + ASSERT_EQ(Cardinality::INTEGERS.compare(i), Cardinality::EQUAL); + + ASSERT_NE(Cardinality::REALS.compare(zero), Cardinality::EQUAL); + ASSERT_NE(Cardinality::REALS.compare(one), Cardinality::EQUAL); + ASSERT_NE(Cardinality::REALS.compare(two), Cardinality::EQUAL); + ASSERT_NE(Cardinality::REALS.compare(copy), Cardinality::EQUAL); + ASSERT_NE(Cardinality::REALS.compare(invalid), Cardinality::EQUAL); + ASSERT_NE(Cardinality::REALS.compare(big), Cardinality::EQUAL); + ASSERT_NE(Cardinality::REALS.compare(i), Cardinality::EQUAL); + ASSERT_EQ(Cardinality::REALS.compare(r), Cardinality::EQUAL); + + // finite cardinal arithmetic + + ASSERT_EQ((zero + zero).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((zero * zero).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((zero ^ zero).compare(one), Cardinality::EQUAL); + ASSERT_EQ((zero + one).compare(one), Cardinality::EQUAL); + ASSERT_EQ((zero * one).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((zero ^ one).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((one + zero).compare(one), Cardinality::EQUAL); + ASSERT_EQ((one * zero).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((one ^ zero).compare(one), Cardinality::EQUAL); + ASSERT_EQ((two + two).compare(4), Cardinality::EQUAL); + ASSERT_EQ((two ^ two).compare(4), Cardinality::EQUAL); + ASSERT_EQ((two * two).compare(4), Cardinality::EQUAL); + ASSERT_EQ((two += two).compare(4), Cardinality::EQUAL); + ASSERT_EQ(two.compare(4), Cardinality::EQUAL); + ASSERT_EQ((two = 2).compare(2), Cardinality::EQUAL); + ASSERT_EQ(two.compare(2), Cardinality::EQUAL); + ASSERT_EQ((two *= 2).compare(4), Cardinality::EQUAL); + ASSERT_EQ(two.compare(4), Cardinality::EQUAL); + ASSERT_EQ(((two = 2) ^= 2).compare(4), Cardinality::EQUAL); + ASSERT_EQ(two.compare(4), Cardinality::EQUAL); + ASSERT_EQ((two = 2).compare(2), Cardinality::EQUAL); + + // infinite cardinal arithmetic + + Cardinality x = i, y = Cardinality(2) ^ x, z = Cardinality(2) ^ y; + + ASSERT_TRUE(x.compare(i) == Cardinality::EQUAL + && y.compare(r) == Cardinality::EQUAL); + ASSERT_TRUE(x.compare(r) != Cardinality::EQUAL + && y.compare(i) != Cardinality::EQUAL); + ASSERT_TRUE(x.compare(z) != Cardinality::EQUAL + && y.compare(z) != Cardinality::EQUAL); + ASSERT_TRUE(x.isCountable() && !x.isFinite()); + ASSERT_FALSE(y.isCountable() && !y.isFinite()); + ASSERT_FALSE(z.isCountable() && !z.isFinite()); + + ASSERT_EQ(big.compare(x), Cardinality::LESS); + ASSERT_EQ(x.compare(y), Cardinality::LESS); + ASSERT_EQ(y.compare(z), Cardinality::LESS); + + ASSERT_THROW(big.getBethNumber(), IllegalArgumentException); + ASSERT_EQ(x.getBethNumber(), 0); + ASSERT_EQ(y.getBethNumber(), 1); + ASSERT_EQ(z.getBethNumber(), 2); + + ASSERT_EQ((zero ^ x).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((one ^ x).compare(one), Cardinality::EQUAL); + ASSERT_TRUE((two ^ x).compare(y) == Cardinality::EQUAL + && (two ^ x).compare(x) != Cardinality::EQUAL); + ASSERT_TRUE((big ^ x).compare(y) == Cardinality::EQUAL + && (big ^ x).compare(x) != Cardinality::EQUAL); + ASSERT_EQ((two ^ x).compare(big ^ x), Cardinality::EQUAL); + + ASSERT_EQ((x ^ zero).compare(one), Cardinality::EQUAL); + ASSERT_EQ((x ^ one).compare(x), Cardinality::EQUAL); + ASSERT_EQ((x ^ two).compare(x), Cardinality::EQUAL); + ASSERT_EQ((x ^ big).compare(x), Cardinality::EQUAL); + ASSERT_EQ((x ^ big).compare(x ^ two), Cardinality::EQUAL); + + ASSERT_EQ((zero ^ y).compare(zero), Cardinality::EQUAL); + ASSERT_EQ((one ^ y).compare(one), Cardinality::EQUAL); + ASSERT_TRUE((two ^ y).compare(x) != Cardinality::EQUAL + && (two ^ y).compare(y) != Cardinality::EQUAL); + ASSERT_TRUE((big ^ y).compare(y) != Cardinality::EQUAL + && (big ^ y).compare(y) != Cardinality::EQUAL); + ASSERT_EQ((big ^ y).getBethNumber(), 2); + ASSERT_EQ((two ^ y).compare(big ^ y), Cardinality::EQUAL); + + ASSERT_EQ((y ^ zero).compare(one), Cardinality::EQUAL); + ASSERT_EQ((y ^ one).compare(y), Cardinality::EQUAL); + ASSERT_EQ((y ^ two).compare(y), Cardinality::EQUAL); + ASSERT_EQ((y ^ big).compare(y), Cardinality::EQUAL); + ASSERT_EQ((y ^ big).compare(y ^ two), Cardinality::EQUAL); + + ASSERT_EQ((x ^ x).compare(y), Cardinality::EQUAL); + ASSERT_EQ((y ^ x).compare(y), Cardinality::EQUAL); + ASSERT_EQ((x ^ y).compare(z), Cardinality::EQUAL); + ASSERT_EQ((y ^ y).compare(z), Cardinality::EQUAL); + ASSERT_EQ((z ^ x).compare(z), Cardinality::EQUAL); + ASSERT_EQ((z ^ y).compare(z), Cardinality::EQUAL); + ASSERT_EQ((zero ^ z).compare(0), Cardinality::EQUAL); + ASSERT_EQ((z ^ zero).compare(1), Cardinality::EQUAL); + ASSERT_EQ((z ^ 0).compare(1), Cardinality::EQUAL); + ASSERT_EQ((two ^ z).compare(z), Cardinality::GREATER); + ASSERT_EQ((big ^ z).compare(two ^ z), Cardinality::EQUAL); + ASSERT_EQ((x ^ z).compare(two ^ z), Cardinality::EQUAL); + ASSERT_EQ((y ^ z).compare(x ^ z), Cardinality::EQUAL); + ASSERT_EQ((z ^ z).compare(x ^ z), Cardinality::EQUAL); + ASSERT_EQ((z ^ z).getBethNumber(), 3); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h deleted file mode 100644 index fad2019e0..000000000 --- a/test/unit/util/cardinality_public.h +++ /dev/null @@ -1,264 +0,0 @@ -/********************* */ -/*! \file cardinality_public.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 Public-box testing of CVC4::Cardinality - ** - ** Public-box testing of CVC4::Cardinality. - **/ - -#include -#include - -#include "util/integer.h" -#include "util/cardinality.h" - -using namespace CVC4; -using namespace std; - -class CardinalityPublic : public CxxTest::TestSuite { - stringstream ss; - -public: - - void testCardinalities() { - Cardinality zero(0); - Cardinality one(1); - Cardinality two(2); - - Cardinality invalid(0); - TS_ASSERT_THROWS(invalid = Cardinality(-1), IllegalArgumentException&); - TS_ASSERT_THROWS(invalid = Cardinality(-2), IllegalArgumentException&); - TS_ASSERT_THROWS( - invalid = Cardinality(Integer("-3983982192391747295721957")), - IllegalArgumentException&); - invalid = one; // test assignment - invalid = Cardinality(5); // test assignment to temporary - - Cardinality copy(one); // test copy - Cardinality big(Integer("3983982192391747295721957")); - Cardinality r(Cardinality::REALS); - Cardinality i(Cardinality::INTEGERS); - - TS_ASSERT( zero.compare(one) == Cardinality::LESS ); - TS_ASSERT( one.compare(two) == Cardinality::LESS ); - TS_ASSERT( two.compare(invalid) == Cardinality::LESS ); - TS_ASSERT( invalid.compare(big) == Cardinality::LESS ); - TS_ASSERT( big.compare(i) == Cardinality::LESS ); - TS_ASSERT( i.compare(r) == Cardinality::LESS ); - - TS_ASSERT( zero.compare(one) != Cardinality::GREATER ); - TS_ASSERT( zero.compare(zero) != Cardinality::GREATER ); - TS_ASSERT( one.compare(two) != Cardinality::GREATER ); - TS_ASSERT( one.compare(one) != Cardinality::GREATER ); - TS_ASSERT( two.compare(invalid) != Cardinality::GREATER ); - TS_ASSERT( two.compare(two) != Cardinality::GREATER ); - TS_ASSERT( invalid.compare(big) != Cardinality::GREATER ); - TS_ASSERT( invalid.compare(invalid) != Cardinality::GREATER ); - TS_ASSERT( big.compare(i) != Cardinality::GREATER ); - TS_ASSERT( big.compare(big) != Cardinality::GREATER ); - TS_ASSERT( i.compare(r) != Cardinality::GREATER ); - TS_ASSERT( i.compare(i) != Cardinality::GREATER ); - TS_ASSERT( r.compare(r) != Cardinality::GREATER ); - - TS_ASSERT( zero.compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( one.compare(one) == Cardinality::EQUAL ); - TS_ASSERT( two.compare(two) == Cardinality::EQUAL ); - TS_ASSERT( invalid.compare(invalid) == Cardinality::EQUAL ); - TS_ASSERT( copy.compare(copy) == Cardinality::EQUAL ); - TS_ASSERT( copy.compare(one) == Cardinality::EQUAL ); - TS_ASSERT( one.compare(copy) == Cardinality::EQUAL ); - TS_ASSERT( big.compare(big) == Cardinality::UNKNOWN ); - TS_ASSERT( i.compare(i) == Cardinality::EQUAL ); - TS_ASSERT( r.compare(r) == Cardinality::EQUAL ); - - TS_ASSERT( zero.compare(one) != Cardinality::EQUAL ); - TS_ASSERT( one.compare(two) != Cardinality::EQUAL ); - TS_ASSERT( two.compare(invalid) != Cardinality::EQUAL ); - TS_ASSERT( copy.compare(r) != Cardinality::EQUAL ); - TS_ASSERT( copy.compare(i) != Cardinality::EQUAL ); - TS_ASSERT( big.compare(i) != Cardinality::EQUAL ); - TS_ASSERT( i.compare(big) != Cardinality::EQUAL ); - TS_ASSERT( big.compare(zero) != Cardinality::EQUAL ); - TS_ASSERT( r.compare(i) != Cardinality::EQUAL ); - TS_ASSERT( i.compare(r) != Cardinality::EQUAL ); - - TS_ASSERT( r.compare(zero) == Cardinality::GREATER ); - TS_ASSERT( r.compare(one) == Cardinality::GREATER ); - TS_ASSERT( r.compare(two) == Cardinality::GREATER ); - TS_ASSERT( r.compare(copy) == Cardinality::GREATER ); - TS_ASSERT( r.compare(invalid) == Cardinality::GREATER ); - TS_ASSERT( r.compare(big) == Cardinality::GREATER ); - TS_ASSERT( r.compare(i) == Cardinality::GREATER ); - TS_ASSERT( r.compare(r) != Cardinality::GREATER ); - TS_ASSERT( r.compare(r) != Cardinality::LESS ); - - TS_ASSERT( zero.isFinite() ); - TS_ASSERT( one.isFinite() ); - TS_ASSERT( two.isFinite() ); - TS_ASSERT( copy.isFinite() ); - TS_ASSERT( invalid.isFinite() ); - TS_ASSERT( big.isFinite() ); - TS_ASSERT( !i.isFinite() ); - TS_ASSERT( !r.isFinite() ); - - TS_ASSERT( !zero.isLargeFinite() ); - TS_ASSERT( !one.isLargeFinite() ); - TS_ASSERT( !two.isLargeFinite() ); - TS_ASSERT( !copy.isLargeFinite() ); - TS_ASSERT( !invalid.isLargeFinite() ); - TS_ASSERT( big.isLargeFinite() ); - TS_ASSERT( !i.isLargeFinite() ); - TS_ASSERT( !r.isLargeFinite() ); - - TS_ASSERT( zero.getFiniteCardinality() == 0 ); - TS_ASSERT( one.getFiniteCardinality() == 1 ); - TS_ASSERT( two.getFiniteCardinality() == 2 ); - TS_ASSERT( copy.getFiniteCardinality() == 1 ); - TS_ASSERT( invalid.getFiniteCardinality() == 5 ); - TS_ASSERT_THROWS(big.getFiniteCardinality(), IllegalArgumentException&); - TS_ASSERT_THROWS(i.getFiniteCardinality(), IllegalArgumentException&); - TS_ASSERT_THROWS(r.getFiniteCardinality(), IllegalArgumentException&); - - TS_ASSERT_THROWS(zero.getBethNumber(), IllegalArgumentException&); - TS_ASSERT_THROWS(one.getBethNumber(), IllegalArgumentException&); - TS_ASSERT_THROWS(two.getBethNumber(), IllegalArgumentException&); - TS_ASSERT_THROWS(copy.getBethNumber(), IllegalArgumentException&); - TS_ASSERT_THROWS(invalid.getBethNumber(), IllegalArgumentException&); - TS_ASSERT_THROWS(big.getBethNumber(), IllegalArgumentException&); - TS_ASSERT( i.getBethNumber() == 0 ); - TS_ASSERT( r.getBethNumber() == 1 ); - - TS_ASSERT( zero.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( one.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( two.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( copy.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( invalid.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( big.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( r.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); - TS_ASSERT( i.compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); - - TS_ASSERT( zero.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( one.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( two.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( copy.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( invalid.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( big.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( i.compare(Cardinality::REALS) != Cardinality::EQUAL ); - TS_ASSERT( r.compare(Cardinality::REALS) == Cardinality::EQUAL ); - - // should work the other way too - - TS_ASSERT( Cardinality::INTEGERS.compare(zero) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(one) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(two) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(copy) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(invalid) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(big) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(r) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::INTEGERS.compare(i) == Cardinality::EQUAL ); - - TS_ASSERT( Cardinality::REALS.compare(zero) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(one) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(two) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(copy) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(invalid) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(big) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(i) != Cardinality::EQUAL ); - TS_ASSERT( Cardinality::REALS.compare(r) == Cardinality::EQUAL ); - - // finite cardinal arithmetic - - TS_ASSERT( (zero + zero).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (zero * zero).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (zero ^ zero).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (zero + one).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (zero * one).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (zero ^ one).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (one + zero).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (one * zero).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (one ^ zero).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (two + two).compare(4) == Cardinality::EQUAL ); - TS_ASSERT( (two ^ two).compare(4) == Cardinality::EQUAL ); - TS_ASSERT( (two * two).compare(4) == Cardinality::EQUAL ); - TS_ASSERT( (two += two).compare(4) == Cardinality::EQUAL ); - TS_ASSERT( two.compare(4) == Cardinality::EQUAL ); - TS_ASSERT( (two = 2).compare(2) == Cardinality::EQUAL ); - TS_ASSERT( two.compare(2) == Cardinality::EQUAL ); - TS_ASSERT( (two *= 2).compare(4) == Cardinality::EQUAL ); - TS_ASSERT( two.compare(4) == Cardinality::EQUAL ); - TS_ASSERT( ((two = 2) ^= 2).compare(4) == Cardinality::EQUAL ); - TS_ASSERT( two.compare(4) == Cardinality::EQUAL ); - TS_ASSERT( (two = 2).compare(2) == Cardinality::EQUAL ); - - // infinite cardinal arithmetic - - Cardinality x = i, y = Cardinality(2)^x, z = Cardinality(2)^y; - - TS_ASSERT( x.compare(i) == Cardinality::EQUAL && y.compare(r) == Cardinality::EQUAL ); - TS_ASSERT( x.compare(r) != Cardinality::EQUAL && y.compare(i) != Cardinality::EQUAL ); - TS_ASSERT( x.compare(z) != Cardinality::EQUAL && y.compare(z) != Cardinality::EQUAL ); - TS_ASSERT( x.isCountable() && !x.isFinite() ); - TS_ASSERT( !y.isCountable() && !y.isFinite() ); - TS_ASSERT( !z.isCountable() && !z.isFinite() ); - - TS_ASSERT( big.compare(x) == Cardinality::LESS ); - TS_ASSERT( x.compare(y) == Cardinality::LESS ); - TS_ASSERT( y.compare(z) == Cardinality::LESS ); - - TS_ASSERT_THROWS(big.getBethNumber(), IllegalArgumentException&); - TS_ASSERT( x.getBethNumber() == 0 ); - TS_ASSERT( y.getBethNumber() == 1 ); - TS_ASSERT( z.getBethNumber() == 2 ); - - TS_ASSERT( (zero ^ x).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (one ^ x).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (two ^ x).compare(y) == Cardinality::EQUAL && (two ^ x).compare(x) != Cardinality::EQUAL ); - TS_ASSERT( (big ^ x).compare(y) == Cardinality::EQUAL && (big ^ x).compare(x) != Cardinality::EQUAL ); - TS_ASSERT( (two ^ x).compare(big ^ x) == Cardinality::EQUAL ); - - TS_ASSERT( (x ^ zero).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (x ^ one).compare(x) == Cardinality::EQUAL ); - TS_ASSERT( (x ^ two).compare(x) == Cardinality::EQUAL ); - TS_ASSERT( (x ^ big).compare(x) == Cardinality::EQUAL ); - TS_ASSERT( (x ^ big).compare(x ^ two) == Cardinality::EQUAL ); - - TS_ASSERT( (zero ^ y).compare(zero) == Cardinality::EQUAL ); - TS_ASSERT( (one ^ y).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (two ^ y).compare(x) != Cardinality::EQUAL && (two ^ y).compare(y) != Cardinality::EQUAL ); - TS_ASSERT( (big ^ y).compare(y) != Cardinality::EQUAL && (big ^ y).compare(y) != Cardinality::EQUAL ); - TS_ASSERT( (big ^ y).getBethNumber() == 2 ); - TS_ASSERT( (two ^ y).compare(big ^ y) == Cardinality::EQUAL ); - - TS_ASSERT( (y ^ zero).compare(one) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ one).compare(y) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ two).compare(y) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ big).compare(y) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ big).compare(y ^ two) == Cardinality::EQUAL ); - - TS_ASSERT( (x ^ x).compare(y) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ x).compare(y) == Cardinality::EQUAL ); - TS_ASSERT( (x ^ y).compare(z) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ y).compare(z) == Cardinality::EQUAL ); - TS_ASSERT( (z ^ x).compare(z) == Cardinality::EQUAL ); - TS_ASSERT( (z ^ y).compare(z) == Cardinality::EQUAL ); - TS_ASSERT( (zero ^ z).compare(0) == Cardinality::EQUAL ); - TS_ASSERT( (z ^ zero).compare(1) == Cardinality::EQUAL ); - TS_ASSERT( (z ^ 0).compare(1) == Cardinality::EQUAL ); - TS_ASSERT( (two ^ z).compare(z) == Cardinality::GREATER ); - TS_ASSERT( (big ^ z).compare(two ^ z) == Cardinality::EQUAL ); - TS_ASSERT( (x ^ z).compare(two ^ z) == Cardinality::EQUAL ); - TS_ASSERT( (y ^ z).compare(x ^ z) == Cardinality::EQUAL ); - TS_ASSERT( (z ^ z).compare(x ^ z) == Cardinality::EQUAL ); - TS_ASSERT( (z ^ z).getBethNumber() == 3 ); - - }/* testCardinalities() */ - -};/* class CardinalityPublic */ -- 2.30.2