diff options
Diffstat (limited to 'src/util/cardinality.h')
-rw-r--r-- | src/util/cardinality.h | 84 |
1 files changed, 40 insertions, 44 deletions
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 */ |