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.

5 files changed, 376 insertions, 287 deletions

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 8aba4ad41..fd2ac3d08 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -23,10 +23,11 @@ namespace CVC4 {
 const Integer Cardinality::s_unknownCard(0);
 const Integer Cardinality::s_intCard(-1);
 const Integer Cardinality::s_realCard(-2);
+const Integer Cardinality::s_largeFiniteCard(Integer("18446744073709551617")); // 2^64 + 1
 
 const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
 const Cardinality Cardinality::REALS(CardinalityBeth(1));
-const Cardinality Cardinality::UNKNOWN((CardinalityUnknown()));
+const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
 
 Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
   if(isUnknown()) {
@@ -36,15 +37,24 @@ Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
     return *this;
   }
 
+  if(c.isFinite() && isLargeFinite()) {
+    return *this;
+  } else if(isFinite() && c.isLargeFinite()) {
+    d_card = s_largeFiniteCard;
+    return *this;
+  }
+
   if(isFinite() && c.isFinite()) {
     d_card += c.d_card - 1;
     return *this;
   }
-  if(*this >= c) {
-    return *this;
-  } else {
+  if(compare(c) == LESS) {
     return *this = c;
+  } else {
+    return *this;
   }
+
+  Unreachable();
 }
 
 /** Assigning multiplication of this cardinality with another. */
@@ -56,13 +66,20 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
     return *this;
   }
 
-  if(*this == 0 || c == 0) {
+  if(c.isFinite() && isLargeFinite()) {
+    return *this;
+  } else if(isFinite() && c.isLargeFinite()) {
+    d_card = s_largeFiniteCard;
+    return *this;
+  }
+
+  if(compare(0) == EQUAL || c.compare(0) == EQUAL) {
     return *this = 0;
   } else if(!isFinite() || !c.isFinite()) {
-    if(*this >= c) {
-      return *this;
-    } else {
+    if(compare(c) == LESS) {
       return *this = c;
+    } else {
+      return *this;
     }
   } else {
     d_card -= 1;
@@ -70,11 +87,12 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
     d_card += 1;
     return *this;
   }
+
+  Unreachable();
 }
 
 /** Assigning exponentiation of this cardinality with another. */
-Cardinality& Cardinality::operator^=(const Cardinality& c)
-  throw(IllegalArgumentException) {
+Cardinality& Cardinality::operator^=(const Cardinality& c) throw() {
   if(isUnknown()) {
     return *this;
   } else if(c.isUnknown()) {
@@ -82,41 +100,99 @@ Cardinality& Cardinality::operator^=(const Cardinality& c)
     return *this;
   }
 
-  if(c == 0) {
+  if(c.isFinite() && isLargeFinite()) {
+    return *this;
+  } else if(isFinite() && c.isLargeFinite()) {
+    d_card = s_largeFiniteCard;
+    return *this;
+  }
+
+  if(c.compare(0) == EQUAL) {
     // (anything) ^ 0 == 1
-    d_card = 2;// remember +1 for finite cardinalities
+    d_card = 2; // remember, +1 for finite cardinalities
     return *this;
-  } else if(*this == 0) {
+  } else if(compare(0) == EQUAL) {
     // 0 ^ (>= 1) == 0
     return *this;
-  } else if(*this == 1) {
+  } else if(compare(1) == EQUAL) {
     // 1 ^ (>= 1) == 1
     return *this;
-  } else if(c == 1) {
+  } else if(c.compare(1) == EQUAL) {
     // (anything) ^ 1 == (that thing)
     return *this;
   } else if(isFinite() && c.isFinite()) {
     // finite ^ finite == finite
-    //
-    // Note: can throw an assertion if c is too big for
-    // exponentiation
-    d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
+    try {
+      // Note: can throw an assertion if c is too big for
+      // exponentiation
+      if(d_card - 1 >= 2 && c.d_card - 1 >= 64) {
+        // don't bother, it's too large anyways
+        d_card = s_largeFiniteCard;
+      } else {
+        d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
+      }
+    } catch(IllegalArgumentException&) {
+      d_card = s_largeFiniteCard;
+    }
     return *this;
   } else if(!isFinite() && c.isFinite()) {
     // inf ^ finite == inf
     return *this;
   } else {
-    Assert(*this >= 2 && !c.isFinite(),
+    Assert(compare(2) != LESS && !c.isFinite(),
            "fall-through case not as expected:\n%s\n%s",
            this->toString().c_str(), c.toString().c_str());
     // (>= 2) ^ beth_k == beth_(k+1)
     // unless the base is already > the exponent
-    if(*this > c) {
+    if(compare(c) == GREATER) {
       return *this;
     }
     d_card = c.d_card - 1;
     return *this;
   }
+
+  Unreachable();
+}
+
+Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) const throw() {
+  if(isUnknown() || c.isUnknown()) {
+    return UNKNOWN;
+  } else if(isLargeFinite()) {
+    if(c.isLargeFinite()) {
+      return UNKNOWN;
+    } else if(c.isFinite()) {
+        return GREATER;
+    } else {
+      Assert(c.isInfinite());
+      return LESS;
+    }
+  } else if(c.isLargeFinite()) {
+    if(isLargeFinite()) {
+      return UNKNOWN;
+    } else if(isFinite()) {
+      return LESS;
+    } else {
+      Assert(isInfinite());
+      return GREATER;
+    }
+  } else if(isInfinite()) {
+    if(c.isFinite()) {
+      return GREATER;
+    } else {
+      return d_card < c.d_card ? GREATER :
+               (d_card == c.d_card ? EQUAL : LESS);
+    }
+  } else if(c.isInfinite()) {
+    Assert(isFinite());
+    return LESS;
+  } else {
+    Assert(isFinite() && !isLargeFinite());
+    Assert(c.isFinite() && !c.isLargeFinite());
+    return d_card < c.d_card ? LESS :
+             (d_card == c.d_card ? EQUAL : GREATER);
+  }
+
+  Unreachable();
 }
 
 
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 057bb0b0c..30bdea78d 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -74,11 +74,18 @@ class CVC4_PUBLIC Cardinality {
   /** A representation for unknown cardinality */
   static const Integer s_unknownCard;
 
+  /** A representation for large, finite cardinality */
+  static const Integer s_largeFiniteCard;
+
   /**
    * In the case of finite cardinality, this is > 0, and is equal to
    * the cardinality+1.  If infinite, it is < 0, and is Beth[|card|-1].
    * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
    * If this field is 0, the cardinality is unknown.
+   *
+   * We impose a ceiling on finite cardinalities of 2^64.  If this field
+   * is >= 2^64 + 1, we consider it at "ceiling" cardinality, and
+   * comparisons between all such cardinalities result in "unknown."
    */
   Integer d_card;
 
@@ -91,7 +98,15 @@ public:
   static const Cardinality REALS;
 
   /** The unknown cardinality */
-  static const Cardinality UNKNOWN;
+  static const Cardinality UNKNOWN_CARD;
+
+  /** Used as a result code for Cardinality::compare(). */
+  enum CVC4_PUBLIC CardinalityComparison {
+    LESS,
+    EQUAL,
+    GREATER,
+    UNKNOWN
+  };/* enum CardinalityComparison */
 
   /**
    * Construct a finite cardinality equal to the integer argument.
@@ -131,7 +146,13 @@ public:
   Cardinality(CardinalityUnknown) : d_card(0) {
   }
 
-  /** Returns true iff this cardinality is unknown. */
+  /**
+   * Returns true iff this cardinality is unknown.  "Unknown" in this
+   * sense means that the cardinality is completely unknown; it might
+   * be finite, or infinite---anything.  Large, finite cardinalities
+   * at the "ceiling" return "false" for isUnknown() and true for
+   * isFinite() and isLargeFinite().
+   */
   bool isUnknown() const throw() {
     return d_card == 0;
   }
@@ -141,6 +162,14 @@ public:
     return d_card > 0;
   }
 
+  /**
+   * Returns true iff this cardinality is finite and large (i.e.,
+   * at the ceiling of representable finite cardinalities).
+ . */
+  bool isLargeFinite() const throw() {
+    return d_card >= s_largeFiniteCard;
+  }
+
   /** Returns true iff this cardinality is infinite. */
   bool isInfinite() const throw() {
     return d_card < 0;
@@ -161,6 +190,7 @@ public:
    */
   Integer getFiniteCardinality() const throw(IllegalArgumentException) {
     CheckArgument(isFinite(), *this, "This cardinality is not finite.");
+    CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
     return d_card - 1;
   }
 
@@ -182,7 +212,7 @@ public:
   Cardinality& operator*=(const Cardinality& c) throw();
 
   /** Assigning exponentiation of this cardinality with another. */
-  Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException);
+  Cardinality& operator^=(const Cardinality& c) throw();
 
   /** Add two cardinalities. */
   Cardinality operator+(const Cardinality& c) const throw() {
@@ -199,54 +229,21 @@ public:
   }
 
   /**
-   * Exponentiation of two cardinalities.  Throws an exception if both
-   * are finite and the exponent is too large.
+   * Exponentiation of two cardinalities.
    */
-  Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) {
+  Cardinality operator^(const Cardinality& c) const throw() {
     Cardinality card(*this);
     card ^= c;
     return card;
   }
 
-  /** Test for equality between cardinalities. */
-  bool operator==(const Cardinality& c) const throw() {
-    return !isUnknown() && d_card == c.d_card;
-  }
-
-  /** Test for disequality between cardinalities. */
-  bool operator!=(const Cardinality& c) const throw() {
-    return !isUnknown() && !c.isUnknown() && d_card != c.d_card;
-  }
-
-  /** Test whether this cardinality is less than another. */
-  bool operator<(const Cardinality& c) const throw() {
-    return
-      !isUnknown() && !c.isUnknown() &&
-      ( ( isFinite() && !c.isFinite() ) ||
-        ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
-        ( !isFinite() && !c.isFinite() && d_card > c.d_card ) );
-  }
-
-  /**
-   * Test whether this cardinality is less than or equal to
-   * another.
-   */
-  bool operator<=(const Cardinality& c) const throw() {
-    return !isUnknown() && !c.isUnknown() && (*this < c || *this == c);
-  }
-
-  /** Test whether this cardinality is greater than another. */
-  bool operator>(const Cardinality& c) const throw() {
-    return !isUnknown() && !c.isUnknown() && !(*this <= c);
-  }
-
   /**
-   * Test whether this cardinality is greater than or equal to
-   * another.
+   * Compare two cardinalities.  This can return UNKNOWN if two
+   * finite cardinalities are at the ceiling (and thus not precisely
+   * represented), or if one or the other is the special "unknown"
+   * cardinality.
    */
-  bool operator>=(const Cardinality& c) const throw() {
-    return !isUnknown() && !c.isUnknown() && !(*this < c);
-  }
+  Cardinality::CardinalityComparison compare(const Cardinality& c) const throw();
 
   /**
    * Return a string representation of this cardinality.
@@ -265,7 +262,6 @@ std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
 std::ostream& operator<<(std::ostream& out, const Cardinality& c)
   throw() CVC4_PUBLIC;
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__CARDINALITY_H */
diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 6d6b0740b..7ba212dd5 100644
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -46,9 +46,9 @@ public:
   }
 
   void testTheBasics() {
-    TS_ASSERT( d_em->booleanType().getCardinality() == 2 );
-    TS_ASSERT( d_em->integerType().getCardinality() == Cardinality::INTEGERS );
-    TS_ASSERT( d_em->realType().getCardinality() == Cardinality::REALS );
+    TS_ASSERT( d_em->booleanType().getCardinality().compare(2) == Cardinality::EQUAL );
+    TS_ASSERT( d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL );
+    TS_ASSERT( d_em->realType().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
   }
 
   void testArrays() {
@@ -62,16 +62,15 @@ public:
     Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType());
     Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType());
 
-    TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS );
-cout << "boolToBool " << boolToBool.getCardinality() << endl;
-    TS_ASSERT( boolToBool.getCardinality() == 4 );
+    TS_ASSERT( intToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( realToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( intToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( intToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( realToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( boolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( boolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL );
+    TS_ASSERT( boolToBool.getCardinality().compare(4) == Cardinality::EQUAL );
   }
 
   void testUnaryFunctions() {
@@ -85,15 +84,15 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl;
     Type boolToInt = d_em->mkFunctionType(d_em->booleanType(), d_em->integerType());
     Type boolToBool = d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType());
 
-    TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS );
-    TS_ASSERT( boolToBool.getCardinality() == 4 );
+    TS_ASSERT( intToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( realToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( intToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( intToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( realToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( boolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( boolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL );
+    TS_ASSERT( boolToBool.getCardinality().compare(4) == Cardinality::EQUAL );
   }
 
   void testBinaryFunctions() {
@@ -143,41 +142,41 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl;
     Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType());
     Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType());
 
-    TS_ASSERT( boolboolToBool.getCardinality() == 16 );
-    TS_ASSERT( boolboolToInt.getCardinality() == Cardinality::INTEGERS );
-    TS_ASSERT( boolboolToReal.getCardinality() == Cardinality::REALS );
+    TS_ASSERT( boolboolToBool.getCardinality().compare(16) == Cardinality::EQUAL );
+    TS_ASSERT( boolboolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL );
+    TS_ASSERT( boolboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
 
-    TS_ASSERT( boolintToBool.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( boolintToInt.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( boolintToReal.getCardinality() == Cardinality::REALS );
+    TS_ASSERT( boolintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( boolintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( boolintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
 
-    TS_ASSERT( intboolToBool.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( intboolToInt.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( intboolToReal.getCardinality() == Cardinality::REALS );
+    TS_ASSERT( intboolToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( intboolToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( intboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
 
-    TS_ASSERT( intintToBool.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( intintToInt.getCardinality() == Cardinality::REALS );
-    TS_ASSERT( intintToReal.getCardinality() == Cardinality::REALS );
+    TS_ASSERT( intintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( intintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+    TS_ASSERT( intintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
 
-    TS_ASSERT( intrealToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( intrealToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( intrealToReal.getCardinality() > Cardinality::REALS );
+    TS_ASSERT( intrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( intrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( intrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
 
-    TS_ASSERT( realintToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realintToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realintToReal.getCardinality() > Cardinality::REALS );
+    TS_ASSERT( realintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
 
-    TS_ASSERT( realrealToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realrealToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realrealToReal.getCardinality() > Cardinality::REALS );
+    TS_ASSERT( realrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
 
-    TS_ASSERT( realboolToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realboolToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( realboolToReal.getCardinality() > Cardinality::REALS );
+    TS_ASSERT( realboolToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realboolToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( realboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
 
-    TS_ASSERT( boolrealToBool.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( boolrealToInt.getCardinality() > Cardinality::REALS );
-    TS_ASSERT( boolrealToReal.getCardinality() > Cardinality::REALS );
+    TS_ASSERT( boolrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( boolrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
+    TS_ASSERT( boolrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER );
   }
 
   void testTernaryFunctions() {
@@ -191,9 +190,9 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl;
     Type boolboolToBoolbool = d_em->mkFunctionType(boolbool, boolboolTuple);
     Type boolToBoolboolbool = d_em->mkFunctionType(d_em->booleanType(), boolboolboolTuple);
 
-    TS_ASSERT( boolboolboolToBool.getCardinality() == /* 2 ^ 8 */ 1 << 8 );
-    TS_ASSERT( boolboolToBoolbool.getCardinality() == /* 4 ^ 4 */ 4 * 4 * 4 * 4 );
-    TS_ASSERT( boolToBoolboolbool.getCardinality() == /* 8 ^ 2 */ 8 * 8 );
+    TS_ASSERT( boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8) == Cardinality::EQUAL );
+    TS_ASSERT( boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4) == Cardinality::EQUAL );
+    TS_ASSERT( boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8) == Cardinality::EQUAL );
   }
 
   void testUndefinedSorts() {
@@ -205,15 +204,24 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl;
 
   void testBitvectors() {
     Debug.on("bvcard");
-    TS_ASSERT( d_em->mkBitVectorType(0).getCardinality() == 0 );
-    for(unsigned i = 1; i < 128; ++i) {
+    TS_ASSERT( d_em->mkBitVectorType(0).getCardinality().compare(0) == Cardinality::EQUAL );
+    Cardinality lastCard = 0;
+    for(unsigned i = 1; i <= 65; ++i) {
       try {
         Cardinality card = Cardinality(2) ^ i;
-        if( d_em->mkBitVectorType(i).getCardinality() != card ) {
-          stringstream ss;
-          ss << "test failed for bitvector(" << i << ")";
-          TS_FAIL(ss.str().c_str());
+        Cardinality typeCard = d_em->mkBitVectorType(i).getCardinality();
+        TS_ASSERT( typeCard.compare(lastCard) == Cardinality::GREATER ||
+                   (typeCard.isLargeFinite() && lastCard.isLargeFinite()) );
+        if( typeCard.compare(card) != Cardinality::EQUAL ) {
+          if( typeCard.isLargeFinite() ) {
+            cout << "test hit large finite card at bitvector(" << i << ")" << endl;
+          } else {
+            stringstream ss;
+            ss << "test failed for bitvector(" << i << ")";
+            TS_FAIL(ss.str().c_str());
+          }
         }
+        lastCard = typeCard;
       } catch(Exception& e) {
         cout << endl << e << endl;
         throw;
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 ) );