Cap finite cardinalities at 2^64, as discussed in the meeting last week.

Replace all cardinality comparison functions <=, ==, !=, >=, <, >, with a single compare() function that can return UNKNOWN in the case of unknown (or large-finite and thus not *precisely* known) cardinalities.

2 files changed, 173 insertions, 164 deletions

diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h
index 5927e1bfa..02c80441c 100644
--- a/test/unit/util/cardinality_public.h
+++ b/test/unit/util/cardinality_public.h
@@ -47,58 +47,58 @@ public:
     Cardinality r(Cardinality::REALS);
     Cardinality i(Cardinality::INTEGERS);
 
-    TS_ASSERT( zero < one );
-    TS_ASSERT( one < two );
-    TS_ASSERT( two < invalid );
-    TS_ASSERT( invalid < big );
-    TS_ASSERT( big < i );
-    TS_ASSERT( i < r );
-
-    TS_ASSERT( zero <= one );
-    TS_ASSERT( zero <= zero );
-    TS_ASSERT( one <= two );
-    TS_ASSERT( one <= one );
-    TS_ASSERT( two <= invalid );
-    TS_ASSERT( two <= two );
-    TS_ASSERT( invalid <= big );
-    TS_ASSERT( invalid <= invalid );
-    TS_ASSERT( big <= i );
-    TS_ASSERT( big <= big );
-    TS_ASSERT( i <= r );
-    TS_ASSERT( i <= i );
-    TS_ASSERT( r <= r );
-
-    TS_ASSERT( zero == zero );
-    TS_ASSERT( one == one );
-    TS_ASSERT( two == two );
-    TS_ASSERT( invalid == invalid );
-    TS_ASSERT( copy == copy );
-    TS_ASSERT( copy == one );
-    TS_ASSERT( one == copy );
-    TS_ASSERT( big == big );
-    TS_ASSERT( i == i );
-    TS_ASSERT( r == r );
-
-    TS_ASSERT( zero != one );
-    TS_ASSERT( one != two );
-    TS_ASSERT( two != invalid );
-    TS_ASSERT( copy != r );
-    TS_ASSERT( copy != i );
-    TS_ASSERT( big != i );
-    TS_ASSERT( i != big );
-    TS_ASSERT( big != zero );
-    TS_ASSERT( r != i );
-    TS_ASSERT( i != r );
-
-    TS_ASSERT( r > zero );
-    TS_ASSERT( r > one );
-    TS_ASSERT( r > two );
-    TS_ASSERT( r > copy );
-    TS_ASSERT( r > invalid );
-    TS_ASSERT( r > big );
-    TS_ASSERT( r > i );
-    TS_ASSERT( !( r > r ) );
-    TS_ASSERT( r >= r );
+    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() );
@@ -109,12 +109,21 @@ public:
     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( big.getFiniteCardinality() == Integer("3983982192391747295721957") );
+    TS_ASSERT_THROWS( big.getFiniteCardinality(), IllegalArgumentException );
     TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException );
     TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException );
 
@@ -127,127 +136,127 @@ public:
     TS_ASSERT( i.getBethNumber() == 0 );
     TS_ASSERT( r.getBethNumber() == 1 );
 
-    TS_ASSERT( zero != Cardinality::INTEGERS );
-    TS_ASSERT( one != Cardinality::INTEGERS );
-    TS_ASSERT( two != Cardinality::INTEGERS );
-    TS_ASSERT( copy != Cardinality::INTEGERS );
-    TS_ASSERT( invalid != Cardinality::INTEGERS );
-    TS_ASSERT( big != Cardinality::INTEGERS );
-    TS_ASSERT( r != Cardinality::INTEGERS );
-    TS_ASSERT( i == Cardinality::INTEGERS );
-
-    TS_ASSERT( zero != Cardinality::REALS );
-    TS_ASSERT( one != Cardinality::REALS );
-    TS_ASSERT( two != Cardinality::REALS );
-    TS_ASSERT( copy != Cardinality::REALS );
-    TS_ASSERT( invalid != Cardinality::REALS );
-    TS_ASSERT( big != Cardinality::REALS );
-    TS_ASSERT( i != Cardinality::REALS );
-    TS_ASSERT( r == Cardinality::REALS );
+    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 != zero );
-    TS_ASSERT( Cardinality::INTEGERS != one );
-    TS_ASSERT( Cardinality::INTEGERS != two );
-    TS_ASSERT( Cardinality::INTEGERS != copy );
-    TS_ASSERT( Cardinality::INTEGERS != invalid );
-    TS_ASSERT( Cardinality::INTEGERS != big );
-    TS_ASSERT( Cardinality::INTEGERS != r );
-    TS_ASSERT( Cardinality::INTEGERS == i );
-
-    TS_ASSERT( Cardinality::REALS != zero );
-    TS_ASSERT( Cardinality::REALS != one );
-    TS_ASSERT( Cardinality::REALS != two );
-    TS_ASSERT( Cardinality::REALS != copy );
-    TS_ASSERT( Cardinality::REALS != invalid );
-    TS_ASSERT( Cardinality::REALS != big );
-    TS_ASSERT( Cardinality::REALS != i );
-    TS_ASSERT( Cardinality::REALS == r );
+    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 == zero );
-    TS_ASSERT( zero * zero == zero );
-    TS_ASSERT( (zero ^ zero) == one );
-    TS_ASSERT( zero + one == one );
-    TS_ASSERT( zero * one == zero );
-    TS_ASSERT( (zero ^ one) == zero );
-    TS_ASSERT( one + zero == one );
-    TS_ASSERT( one * zero == zero );
-    TS_ASSERT( (one ^ zero) == one );
-    TS_ASSERT( two + two == 4 );
-    TS_ASSERT( (two ^ two) == 4 );
-    TS_ASSERT( two * two == 4 );
-    TS_ASSERT( (two += two) == 4 );
-    TS_ASSERT( two == 4 );
-    TS_ASSERT( (two = 2) == 2 );
-    TS_ASSERT( two == 2 );
-    TS_ASSERT( (two *= 2) == 4 );
-    TS_ASSERT( two == 4 );
-    TS_ASSERT( ((two = 2) ^= 2) == 4 );
-    TS_ASSERT( two == 4 );
-    TS_ASSERT( (two = 2) == 2 );
+    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 == i && y == r );
-    TS_ASSERT( x != r && y != i );
-    TS_ASSERT( x != z && y != z );
+    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 < x );
-    TS_ASSERT( x < y );
-    TS_ASSERT( y < z );
+    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) == zero );
-    TS_ASSERT( (one ^ x) == one );
-    TS_ASSERT( (two ^ x) == y && (two ^ x) != x );
-    TS_ASSERT( (big ^ x) == y && (big ^ x) != x );
-    TS_ASSERT( (two ^ x) == (big ^ x) );
-
-    TS_ASSERT( (x ^ zero) == one );
-    TS_ASSERT( (x ^ one) == x );
-    TS_ASSERT( (x ^ two) == x );
-    TS_ASSERT( (x ^ big) == x );
-    TS_ASSERT( (x ^ big) == (x ^ two) );
-
-    TS_ASSERT( (zero ^ y) == zero );
-    TS_ASSERT( (one ^ y) == one );
-    TS_ASSERT( (two ^ y) != x && (two ^ y) != y );
-    TS_ASSERT( (big ^ y) != y && (big ^ y) != y );
+    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) == (big ^ y) );
-
-    TS_ASSERT( (y ^ zero) == one );
-    TS_ASSERT( (y ^ one) == y );
-    TS_ASSERT( (y ^ two) == y );
-    TS_ASSERT( (y ^ big) == y );
-    TS_ASSERT( (y ^ big) == (y ^ two) );
-
-    TS_ASSERT( (x ^ x) == y );
-    TS_ASSERT( (y ^ x) == y );
-    TS_ASSERT( (x ^ y) == z );
-    TS_ASSERT( (y ^ y) == z );
-    TS_ASSERT( (z ^ x) == z );
-    TS_ASSERT( (z ^ y) == z );
-    TS_ASSERT( (zero ^ z) == 0 );
-    TS_ASSERT( (z ^ zero) == 1 );
-    TS_ASSERT( (z ^ 0) == 1 );
-    TS_ASSERT( (two ^ z) > z );
-    TS_ASSERT( (big ^ z) == (two ^ z) );
-    TS_ASSERT( (x ^ z) == (two ^ z) );
-    TS_ASSERT( (y ^ z) == (x ^ z) );
-    TS_ASSERT( (z ^ z) == (x ^ z) );
+    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() */
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 6c449233c..5042852fc 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -71,8 +71,8 @@ public:
     TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException);
 
     TS_ASSERT(colorsType.getDatatype().isFinite());
-    TS_ASSERT(colorsType.getDatatype().getCardinality() == 4);
-    TS_ASSERT(ctor.getType().getCardinality() == 1);
+    TS_ASSERT(colorsType.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL);
+    TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL);
     TS_ASSERT(colorsType.getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl
                          << "  is " << colorsType.mkGroundTerm() << endl;
@@ -108,7 +108,7 @@ public:
     Debug("datatypes") << apply << std::endl;
 
     TS_ASSERT(! natType.getDatatype().isFinite());
-    TS_ASSERT(natType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(natType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(natType.getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl
                          << "  is " << natType.mkGroundTerm() << endl;
@@ -149,7 +149,7 @@ public:
     TS_ASSERT_THROWS(treeType.getConstructor("leff"), IllegalArgumentException);
 
     TS_ASSERT(! treeType.getDatatype().isFinite());
-    TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(treeType.getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl
                          << "  is " << treeType.mkGroundTerm() << endl;
@@ -183,7 +183,7 @@ public:
     Debug("datatypes") << listType << std::endl;
 
     TS_ASSERT(! listType.getDatatype().isFinite());
-    TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(listType.getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
                          << "  is " << listType.mkGroundTerm() << endl;
@@ -217,7 +217,7 @@ public:
     Debug("datatypes") << listType << std::endl;
 
     TS_ASSERT(! listType.getDatatype().isFinite());
-    TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::REALS);
+    TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL);
     TS_ASSERT(listType.getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
                          << "  is " << listType.mkGroundTerm() << endl;
@@ -251,7 +251,7 @@ public:
     Debug("datatypes") << listType << std::endl;
 
     TS_ASSERT(! listType.getDatatype().isFinite());
-    TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(listType.getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
                          << "  is " << listType.mkGroundTerm() << endl;
@@ -316,7 +316,7 @@ public:
     TS_ASSERT(dtts[1].getDatatype().isResolved());
 
     TS_ASSERT(! dtts[0].getDatatype().isFinite());
-    TS_ASSERT(dtts[0].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(dtts[0].getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl
                          << "  is " << dtts[0].mkGroundTerm() << endl;
@@ -333,7 +333,7 @@ public:
     }
 
     TS_ASSERT(! dtts[1].getDatatype().isFinite());
-    TS_ASSERT(dtts[1].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(dtts[1].getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl
                          << "  is " << dtts[1].mkGroundTerm() << endl;
@@ -364,7 +364,7 @@ public:
     TS_ASSERT_DIFFERS(dtts[0], dtts2[0]);
 
     TS_ASSERT(! dtts2[0].getDatatype().isFinite());
-    TS_ASSERT(dtts2[0].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(dtts2[0].getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl
                          << "  is " << dtts2[0].mkGroundTerm() << endl;
@@ -381,7 +381,7 @@ public:
     }
 
     TS_ASSERT(! dtts2[1].getDatatype().isFinite());
-    TS_ASSERT(dtts2[1].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts2[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(dtts2[1].getDatatype().isWellFounded());
     Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl
                          << "  is " << dtts2[1].mkGroundTerm() << endl;
@@ -411,7 +411,7 @@ public:
     Debug("datatypes") << treeType << std::endl;
 
     TS_ASSERT(! treeType.getDatatype().isFinite());
-    TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(! treeType.getDatatype().isWellFounded());
     TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() );
     TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) );