diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-22 22:31:59 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-22 22:31:59 +0000 |
commit | 3dff1d2eef828dc3ff17750a738d6a6bff0ed484 (patch) | |
tree | 52d26b9ba5ed3590bf728eb8ae384195e56c26fa /src | |
parent | 8ba847f7c4c6385cc4a788c3b965498acb3f0f08 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/util/cardinality.cpp | 118 | ||||
-rw-r--r-- | src/util/cardinality.h | 84 |
2 files changed, 137 insertions, 65 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 */ |