diff options
Diffstat (limited to 'src/util/cardinality.cpp')
-rw-r--r-- | src/util/cardinality.cpp | 133 |
1 files changed, 62 insertions, 71 deletions
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 2eea4c040..17c790731 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -18,77 +18,72 @@ #include "base/cvc4_assert.h" - 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 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_CARD((CardinalityUnknown())); -CardinalityBeth::CardinalityBeth(const Integer& beth) - : d_index(beth) -{ +CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) { PrettyCheckArgument(beth >= 0, beth, "Beth index must be a nonnegative integer, not %s.", beth.toString().c_str()); } -Cardinality::Cardinality(long card) - : d_card(card) -{ +Cardinality::Cardinality(long card) : d_card(card) { PrettyCheckArgument(card >= 0, card, "Cardinality must be a nonnegative integer, not %ld.", card); d_card += 1; } -Cardinality::Cardinality(const Integer& card) - : d_card(card) -{ +Cardinality::Cardinality(const Integer& card) : d_card(card) { PrettyCheckArgument(card >= 0, card, "Cardinality must be a nonnegative integer, not %s.", card.toString().c_str()); d_card += 1; } - -Integer Cardinality::getFiniteCardinality() const throw(IllegalArgumentException) { +Integer Cardinality::getFiniteCardinality() const { PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite."); - PrettyCheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent."); + PrettyCheckArgument( + !isLargeFinite(), *this, + "This cardinality is finite, but too large to represent."); return d_card - 1; } -Integer Cardinality::getBethNumber() const throw(IllegalArgumentException) { +Integer Cardinality::getBethNumber() const { PrettyCheckArgument(!isFinite() && !isUnknown(), *this, "This cardinality is not infinite (or is unknown)."); return -d_card - 1; } -Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { - if(isUnknown()) { +Cardinality& Cardinality::operator+=(const Cardinality& c) { + if (isUnknown()) { return *this; - } else if(c.isUnknown()) { + } else if (c.isUnknown()) { d_card = s_unknownCard; return *this; } - if(c.isFinite() && isLargeFinite()) { + if (c.isFinite() && isLargeFinite()) { return *this; - } else if(isFinite() && c.isLargeFinite()) { + } else if (isFinite() && c.isLargeFinite()) { d_card = s_largeFiniteCard; return *this; } - if(isFinite() && c.isFinite()) { + if (isFinite() && c.isFinite()) { d_card += c.d_card - 1; return *this; } - if(compare(c) == LESS) { + if (compare(c) == LESS) { return *this = c; } else { return *this; @@ -98,25 +93,25 @@ Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { } /** Assigning multiplication of this cardinality with another. */ -Cardinality& Cardinality::operator*=(const Cardinality& c) throw() { - if(isUnknown()) { +Cardinality& Cardinality::operator*=(const Cardinality& c) { + if (isUnknown()) { return *this; - } else if(c.isUnknown()) { + } else if (c.isUnknown()) { d_card = s_unknownCard; return *this; } - if(c.isFinite() && isLargeFinite()) { + if (c.isFinite() && isLargeFinite()) { return *this; - } else if(isFinite() && c.isLargeFinite()) { + } else if (isFinite() && c.isLargeFinite()) { d_card = s_largeFiniteCard; return *this; } - if(compare(0) == EQUAL || c.compare(0) == EQUAL) { + if (compare(0) == EQUAL || c.compare(0) == EQUAL) { return *this = 0; - } else if(!isFinite() || !c.isFinite()) { - if(compare(c) == LESS) { + } else if (!isFinite() || !c.isFinite()) { + if (compare(c) == LESS) { return *this = c; } else { return *this; @@ -132,50 +127,50 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() { } /** Assigning exponentiation of this cardinality with another. */ -Cardinality& Cardinality::operator^=(const Cardinality& c) throw() { - if(isUnknown()) { +Cardinality& Cardinality::operator^=(const Cardinality& c) { + if (isUnknown()) { return *this; - } else if(c.isUnknown()) { + } else if (c.isUnknown()) { d_card = s_unknownCard; return *this; } - if(c.isFinite() && isLargeFinite()) { + if (c.isFinite() && isLargeFinite()) { return *this; - } else if(isFinite() && c.isLargeFinite()) { + } else if (isFinite() && c.isLargeFinite()) { d_card = s_largeFiniteCard; return *this; } - if(c.compare(0) == EQUAL) { + 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(compare(0) == EQUAL) { + } else if (compare(0) == EQUAL) { // 0 ^ (>= 1) == 0 return *this; - } else if(compare(1) == EQUAL) { + } else if (compare(1) == EQUAL) { // 1 ^ (>= 1) == 1 return *this; - } else if(c.compare(1) == EQUAL) { + } else if (c.compare(1) == EQUAL) { // (anything) ^ 1 == (that thing) return *this; - } else if(isFinite() && c.isFinite()) { + } else if (isFinite() && c.isFinite()) { // finite ^ finite == finite try { // Note: can throw an assertion if c is too big for // exponentiation - if(d_card - 1 >= 2 && c.d_card - 1 >= 64) { + 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&) { + } catch (IllegalArgumentException&) { d_card = s_largeFiniteCard; } return *this; - } else if(!isFinite() && c.isFinite()) { + } else if (!isFinite() && c.isFinite()) { // inf ^ finite == inf return *this; } else { @@ -184,7 +179,7 @@ Cardinality& Cardinality::operator^=(const Cardinality& c) throw() { this->toString().c_str(), c.toString().c_str()); // (>= 2) ^ beth_k == beth_(k+1) // unless the base is already > the exponent - if(compare(c) == GREATER) { + if (compare(c) == GREATER) { return *this; } d_card = c.d_card - 1; @@ -194,70 +189,67 @@ Cardinality& Cardinality::operator^=(const Cardinality& c) throw() { Unreachable(); } -Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) const throw() { - if(isUnknown() || c.isUnknown()) { +Cardinality::CardinalityComparison Cardinality::compare( + const Cardinality& c) const { + if (isUnknown() || c.isUnknown()) { return UNKNOWN; - } else if(isLargeFinite()) { - if(c.isLargeFinite()) { + } else if (isLargeFinite()) { + if (c.isLargeFinite()) { return UNKNOWN; - } else if(c.isFinite()) { - return GREATER; + } else if (c.isFinite()) { + return GREATER; } else { Assert(c.isInfinite()); return LESS; } - } else if(c.isLargeFinite()) { - if(isLargeFinite()) { + } else if (c.isLargeFinite()) { + if (isLargeFinite()) { return UNKNOWN; - } else if(isFinite()) { + } else if (isFinite()) { return LESS; } else { Assert(isInfinite()); return GREATER; } - } else if(isInfinite()) { - if(c.isFinite()) { + } else if (isInfinite()) { + if (c.isFinite()) { return GREATER; } else { - return d_card < c.d_card ? GREATER : - (d_card == c.d_card ? EQUAL : LESS); + return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS); } - } else if(c.isInfinite()) { + } 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); + return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER); } Unreachable(); } -bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const throw() { +bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const { CardinalityComparison cmp = this->compare(c); return cmp == LESS || cmp == EQUAL; } -std::string Cardinality::toString() const throw() { +std::string Cardinality::toString() const { std::stringstream ss; ss << *this; return ss.str(); } - -std::ostream& operator<<(std::ostream& out, CardinalityBeth b) throw() { +std::ostream& operator<<(std::ostream& out, CardinalityBeth b) { out << "beth[" << b.getNumber() << ']'; return out; } - -std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() { - if(c.isUnknown()) { +std::ostream& operator<<(std::ostream& out, const Cardinality& c) { + if (c.isUnknown()) { out << "Cardinality::UNKNOWN"; - } else if(c.isFinite()) { + } else if (c.isFinite()) { out << c.getFiniteCardinality(); } else { out << CardinalityBeth(c.getBethNumber()); @@ -266,5 +258,4 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() { return out; } - -}/* CVC4 namespace */ +} /* CVC4 namespace */ |