summaryrefslogtreecommitdiff
path: root/src/util/cardinality.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/cardinality.cpp')
-rw-r--r--src/util/cardinality.cpp133
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback