#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;
}
/** 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;
}
/** 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 {
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;
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());
return out;
}
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
class CVC4_PUBLIC CardinalityBeth {
Integer d_index;
-public:
+ public:
CardinalityBeth(const Integer& beth);
- const Integer& getNumber() const throw() {
- return d_index;
- }
+ const Integer& getNumber() const { return d_index; }
-};/* class CardinalityBeth */
+}; /* class CardinalityBeth */
/**
* Representation for an unknown cardinality.
*/
class CVC4_PUBLIC CardinalityUnknown {
-public:
- CardinalityUnknown() throw() {}
- ~CardinalityUnknown() throw() {}
-};/* class CardinalityUnknown */
+ public:
+ CardinalityUnknown() {}
+ ~CardinalityUnknown() {}
+}; /* class CardinalityUnknown */
/**
* A simple representation of a cardinality. We store an
*/
Integer d_card;
-public:
-
+ public:
/** The cardinality of the set of integers. */
static const Cardinality INTEGERS;
EQUAL,
GREATER,
UNKNOWN
- };/* enum CardinalityComparison */
+ }; /* enum CardinalityComparison */
/**
* Construct a finite cardinality equal to the integer argument.
/**
* Construct an infinite cardinality equal to the given Beth number.
*/
- Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
- }
+ Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {}
/**
* Construct an unknown cardinality.
*/
- Cardinality(CardinalityUnknown) : d_card(0) {
- }
+ Cardinality(CardinalityUnknown) : d_card(0) {}
/**
* Returns true iff this cardinality is unknown. "Unknown" in this
* at the "ceiling" return "false" for isUnknown() and true for
* isFinite() and isLargeFinite().
*/
- bool isUnknown() const throw() {
- return d_card == 0;
- }
+ bool isUnknown() const { return d_card == 0; }
/** Returns true iff this cardinality is finite. */
- bool isFinite() const throw() {
- return d_card > 0;
- }
+ bool isFinite() const { return d_card > 0; }
/** Returns true iff this cardinality is one */
- bool isOne() const throw() {
- return d_card == 1;
- }
+ bool isOne() const { return d_card == 1; }
/**
* 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;
- }
+ bool isLargeFinite() const { return d_card >= s_largeFiniteCard; }
/** Returns true iff this cardinality is infinite. */
- bool isInfinite() const throw() {
- return d_card < 0;
- }
+ bool isInfinite() const { return d_card < 0; }
/**
* Returns true iff this cardinality is finite or countably
* infinite.
*/
- bool isCountable() const throw() {
- return isFinite() || d_card == s_intCard;
- }
+ bool isCountable() const { return isFinite() || d_card == s_intCard; }
/**
* In the case that this cardinality is finite, return its
* cardinality. (If this cardinality is infinite, this function
* throws an IllegalArgumentException.)
*/
- Integer getFiniteCardinality() const throw(IllegalArgumentException);
+ Integer getFiniteCardinality() const;
/**
* In the case that this cardinality is infinite, return its Beth
* number. (If this cardinality is finite, this function throws an
* IllegalArgumentException.)
*/
- Integer getBethNumber() const throw(IllegalArgumentException);
+ Integer getBethNumber() const;
/** Assigning addition of this cardinality with another. */
- Cardinality& operator+=(const Cardinality& c) throw();
+ Cardinality& operator+=(const Cardinality& c);
/** Assigning multiplication of this cardinality with another. */
- Cardinality& operator*=(const Cardinality& c) throw();
+ Cardinality& operator*=(const Cardinality& c);
/** Assigning exponentiation of this cardinality with another. */
- Cardinality& operator^=(const Cardinality& c) throw();
+ Cardinality& operator^=(const Cardinality& c);
/** Add two cardinalities. */
- Cardinality operator+(const Cardinality& c) const throw() {
+ Cardinality operator+(const Cardinality& c) const {
Cardinality card(*this);
card += c;
return card;
}
/** Multiply two cardinalities. */
- Cardinality operator*(const Cardinality& c) const throw() {
+ Cardinality operator*(const Cardinality& c) const {
Cardinality card(*this);
card *= c;
return card;
/**
* Exponentiation of two cardinalities.
*/
- Cardinality operator^(const Cardinality& c) const throw() {
+ Cardinality operator^(const Cardinality& c) const {
Cardinality card(*this);
card ^= c;
return card;
* represented), or if one or the other is the special "unknown"
* cardinality.
*/
- Cardinality::CardinalityComparison compare(const Cardinality& c) const throw();
+ Cardinality::CardinalityComparison compare(const Cardinality& c) const;
/**
* Return a string representation of this cardinality.
*/
- std::string toString() const throw();
+ std::string toString() const;
/**
* Compare two cardinalities and if it is known that the current
* cardinality is smaller or equal to c, it returns true.
*/
- bool knownLessThanOrEqual(const Cardinality& c) const throw();
-};/* class Cardinality */
-
+ bool knownLessThanOrEqual(const Cardinality& c) const;
+}; /* class Cardinality */
/** Print an element of the InfiniteCardinality enumeration. */
-std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
- throw() CVC4_PUBLIC;
-
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b) CVC4_PUBLIC;
/** Print a cardinality in a human-readable fashion. */
-std::ostream& operator<<(std::ostream& out, const Cardinality& c)
- throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const Cardinality& c) CVC4_PUBLIC;
-}/* CVC4 namespace */
+} /* CVC4 namespace */
#endif /* __CVC4__CARDINALITY_H */
projects / cvc5.git / commitdiff