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/util/cardinality.cpp | |
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/util/cardinality.cpp')
-rw-r--r-- | src/util/cardinality.cpp | 118 |
1 files changed, 97 insertions, 21 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(); } |