google test: util: Migrate cardinality_black. (#6016)

3 files changed, 273 insertions, 265 deletions

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 <sstream>
+#include <string>
+
+#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 <sstream>
-#include <string>
-
-#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 */