diff options
Diffstat (limited to 'src/util/cardinality.h')
-rw-r--r-- | src/util/cardinality.h | 85 |
1 files changed, 32 insertions, 53 deletions
diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 93b4ca618..b16f84324 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -35,23 +35,21 @@ namespace CVC4 { 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 @@ -83,8 +81,7 @@ class CVC4_PUBLIC Cardinality { */ Integer d_card; -public: - + public: /** The cardinality of the set of integers. */ static const Cardinality INTEGERS; @@ -100,7 +97,7 @@ public: EQUAL, GREATER, UNKNOWN - };/* enum CardinalityComparison */ + }; /* enum CardinalityComparison */ /** * Construct a finite cardinality equal to the integer argument. @@ -119,14 +116,12 @@ public: /** * 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 @@ -135,72 +130,60 @@ public: * 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; @@ -209,7 +192,7 @@ public: /** * Exponentiation of two cardinalities. */ - Cardinality operator^(const Cardinality& c) const throw() { + Cardinality operator^(const Cardinality& c) const { Cardinality card(*this); card ^= c; return card; @@ -221,30 +204,26 @@ public: * 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 */ |