diff options
| -rw-r--r-- | src/util/cardinality.cpp | 133 | ||||
| -rw-r--r-- | src/util/cardinality.h | 85 | ||||
| -rw-r--r-- | src/util/integer_cln_imp.cpp | 10 | ||||
| -rw-r--r-- | src/util/integer_cln_imp.h | 11 | ||||
| -rw-r--r-- | src/util/integer_gmp_imp.h | 4 |
5 files changed, 107 insertions, 136 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 */ 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 */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index aa6cb03af..a7412b503 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -145,4 +145,14 @@ bool Integer::fitsUnsignedLong() const { return sgn() >= 0 && d_value <= s_unsignedLongMax; } +Integer Integer::pow(unsigned long int exp) const { + if (exp == 0) { + return Integer(1); + } else { + Assert(exp > 0); + cln::cl_I result = cln::expt_pos(d_value, exp); + return Integer(result); + } +} + } /* namespace CVC4 */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 6bfebbaf1..12619520f 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -321,16 +321,7 @@ public: * * @param exp the exponent */ - Integer pow(unsigned long int exp) const { - if(exp > 0){ - cln::cl_I result= cln::expt_pos(d_value,exp); - return Integer( result ); - }else if(exp == 0){ - return Integer( 1 ); - }else{ - throw Exception("Negative exponent in Integer::pow()"); - } - } + Integer pow(unsigned long int exp) const; /** * Return the greatest common divisor of this integer with another. diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 3a95c6b85..5af902ac6 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -361,8 +361,8 @@ public: */ Integer pow(unsigned long int exp) const { mpz_class result; - mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp); - return Integer( result ); + mpz_pow_ui(result.get_mpz_t(), d_value.get_mpz_t(), exp); + return Integer(result); } /** |