diff options
Diffstat (limited to 'src/util')
-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 | ||||
-rw-r--r-- | src/util/result.cpp | 383 | ||||
-rw-r--r-- | src/util/result.h | 75 | ||||
-rw-r--r-- | src/util/sexpr.cpp | 374 | ||||
-rw-r--r-- | src/util/sexpr.h | 63 | ||||
-rw-r--r-- | src/util/subrange_bound.cpp | 28 | ||||
-rw-r--r-- | src/util/subrange_bound.h | 103 |
11 files changed, 597 insertions, 672 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); } /** diff --git a/src/util/result.cpp b/src/util/result.cpp index 51b1a8de1..af28269f1 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -28,167 +28,152 @@ using namespace std; namespace CVC4 { Result::Result() - : d_sat(SAT_UNKNOWN) - , d_validity(VALIDITY_UNKNOWN) - , d_which(TYPE_NONE) - , d_unknownExplanation(UNKNOWN_REASON) - , d_inputName("") -{ } - + : d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName("") {} Result::Result(enum Sat s, std::string inputName) - : d_sat(s) - , d_validity(VALIDITY_UNKNOWN) - , d_which(TYPE_SAT) - , d_unknownExplanation(UNKNOWN_REASON) - , d_inputName(inputName) -{ + : d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { PrettyCheckArgument(s != SAT_UNKNOWN, "Must provide a reason for satisfiability being unknown"); } Result::Result(enum Validity v, std::string inputName) - : d_sat(SAT_UNKNOWN) - , d_validity(v) - , d_which(TYPE_VALIDITY) - , d_unknownExplanation(UNKNOWN_REASON) - , d_inputName(inputName) -{ + : d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { PrettyCheckArgument(v != VALIDITY_UNKNOWN, "Must provide a reason for validity being unknown"); } - Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName) - : d_sat(s) - , d_validity(VALIDITY_UNKNOWN) - , d_which(TYPE_SAT) - , d_unknownExplanation(unknownExplanation) - , d_inputName(inputName) -{ + : d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(unknownExplanation), + d_inputName(inputName) { PrettyCheckArgument(s == SAT_UNKNOWN, "improper use of unknown-result constructor"); } Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName) - : d_sat(SAT_UNKNOWN) - , d_validity(v) - , d_which(TYPE_VALIDITY) - , d_unknownExplanation(unknownExplanation) - , d_inputName(inputName) -{ + : d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(unknownExplanation), + d_inputName(inputName) { PrettyCheckArgument(v == VALIDITY_UNKNOWN, "improper use of unknown-result constructor"); } -Result::Result(const std::string& instr, std::string inputName) : - d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_NONE), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { +Result::Result(const std::string& instr, std::string inputName) + : d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { string s = instr; transform(s.begin(), s.end(), s.begin(), ::tolower); - if(s == "sat" || s == "satisfiable") { + if (s == "sat" || s == "satisfiable") { d_which = TYPE_SAT; d_sat = SAT; - } else if(s == "unsat" || s == "unsatisfiable") { + } else if (s == "unsat" || s == "unsatisfiable") { d_which = TYPE_SAT; d_sat = UNSAT; - } else if(s == "valid") { + } else if (s == "valid") { d_which = TYPE_VALIDITY; d_validity = VALID; - } else if(s == "invalid") { + } else if (s == "invalid") { d_which = TYPE_VALIDITY; d_validity = INVALID; - } else if(s == "incomplete") { + } else if (s == "incomplete") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = INCOMPLETE; - } else if(s == "timeout") { + } else if (s == "timeout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = TIMEOUT; - } else if(s == "resourceout") { + } else if (s == "resourceout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = RESOURCEOUT; - } else if(s == "memout") { + } else if (s == "memout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; - } else if(s == "interrupted") { + } else if (s == "interrupted") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = INTERRUPTED; - } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { + } else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; } else { - IllegalArgument(s, "expected satisfiability/validity result, " - "instead got `%s'", s.c_str()); + IllegalArgument(s, + "expected satisfiability/validity result, " + "instead got `%s'", + s.c_str()); } } Result::UnknownExplanation Result::whyUnknown() const { - PrettyCheckArgument( isUnknown(), this, - "This result is not unknown, so the reason for " - "being unknown cannot be inquired of it" ); + PrettyCheckArgument(isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it"); return d_unknownExplanation; } -bool Result::operator==(const Result& r) const throw() { - if(d_which != r.d_which) { +bool Result::operator==(const Result& r) const { + if (d_which != r.d_which) { return false; } - if(d_which == TYPE_SAT) { - return d_sat == r.d_sat && - ( d_sat != SAT_UNKNOWN || - d_unknownExplanation == r.d_unknownExplanation ); + if (d_which == TYPE_SAT) { + return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation); } - if(d_which == TYPE_VALIDITY) { + if (d_which == TYPE_VALIDITY) { return d_validity == r.d_validity && - ( d_validity != VALIDITY_UNKNOWN || - d_unknownExplanation == r.d_unknownExplanation ); + (d_validity != VALIDITY_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation); } return false; } -bool operator==(enum Result::Sat sr, const Result& r) throw() { - return r == sr; -} +bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; } -bool operator==(enum Result::Validity vr, const Result& r) throw() { - return r == vr; -} -bool operator!=(enum Result::Sat s, const Result& r) throw(){ - return !(s == r); -} -bool operator!=(enum Result::Validity v, const Result& r) throw(){ - return !(v == r); -} +bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; } +bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); } +bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); } -Result Result::asSatisfiabilityResult() const throw() { - if(d_which == TYPE_SAT) { +Result Result::asSatisfiabilityResult() const { + if (d_which == TYPE_SAT) { return *this; } - if(d_which == TYPE_VALIDITY) { - switch(d_validity) { - - case INVALID: - return Result(SAT, d_inputName); + if (d_which == TYPE_VALIDITY) { + switch (d_validity) { + case INVALID: + return Result(SAT, d_inputName); - case VALID: - return Result(UNSAT, d_inputName); + case VALID: + return Result(UNSAT, d_inputName); - case VALIDITY_UNKNOWN: - return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); - default: - Unhandled(d_validity); + default: + Unhandled(d_validity); } } @@ -196,25 +181,24 @@ Result Result::asSatisfiabilityResult() const throw() { return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); } -Result Result::asValidityResult() const throw() { - if(d_which == TYPE_VALIDITY) { +Result Result::asValidityResult() const { + if (d_which == TYPE_VALIDITY) { return *this; } - if(d_which == TYPE_SAT) { - switch(d_sat) { - - case SAT: - return Result(INVALID, d_inputName); + if (d_which == TYPE_SAT) { + switch (d_sat) { + case SAT: + return Result(INVALID, d_inputName); - case UNSAT: - return Result(VALID, d_inputName); + case UNSAT: + return Result(VALID, d_inputName); - case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); - default: - Unhandled(d_sat); + default: + Unhandled(d_sat); } } @@ -229,38 +213,73 @@ string Result::toString() const { } ostream& operator<<(ostream& out, enum Result::Sat s) { - switch(s) { - case Result::UNSAT: out << "UNSAT"; break; - case Result::SAT: out << "SAT"; break; - case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; - default: Unhandled(s); + switch (s) { + case Result::UNSAT: + out << "UNSAT"; + break; + case Result::SAT: + out << "SAT"; + break; + case Result::SAT_UNKNOWN: + out << "SAT_UNKNOWN"; + break; + default: + Unhandled(s); } return out; } ostream& operator<<(ostream& out, enum Result::Validity v) { - switch(v) { - case Result::INVALID: out << "INVALID"; break; - case Result::VALID: out << "VALID"; break; - case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; - default: Unhandled(v); + switch (v) { + case Result::INVALID: + out << "INVALID"; + break; + case Result::VALID: + out << "VALID"; + break; + case Result::VALIDITY_UNKNOWN: + out << "VALIDITY_UNKNOWN"; + break; + default: + Unhandled(v); } return out; } ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { - switch(e) { - case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; - case Result::INCOMPLETE: out << "INCOMPLETE"; break; - case Result::TIMEOUT: out << "TIMEOUT"; break; - case Result::RESOURCEOUT: out << "RESOURCEOUT"; break; - case Result::MEMOUT: out << "MEMOUT"; break; - case Result::INTERRUPTED: out << "INTERRUPTED"; break; - case Result::NO_STATUS: out << "NO_STATUS"; break; - case Result::UNSUPPORTED: out << "UNSUPPORTED"; break; - case Result::OTHER: out << "OTHER"; break; - case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; - default: Unhandled(e); + switch (e) { + case Result::REQUIRES_FULL_CHECK: + out << "REQUIRES_FULL_CHECK"; + break; + case Result::INCOMPLETE: + out << "INCOMPLETE"; + break; + case Result::TIMEOUT: + out << "TIMEOUT"; + break; + case Result::RESOURCEOUT: + out << "RESOURCEOUT"; + break; + case Result::MEMOUT: + out << "MEMOUT"; + break; + case Result::INTERRUPTED: + out << "INTERRUPTED"; + break; + case Result::NO_STATUS: + out << "NO_STATUS"; + break; + case Result::UNSUPPORTED: + out << "UNSUPPORTED"; + break; + case Result::OTHER: + out << "OTHER"; + break; + case Result::UNKNOWN_REASON: + out << "UNKNOWN_REASON"; + break; + default: + Unhandled(e); } return out; } @@ -268,61 +287,59 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { ostream& operator<<(ostream& out, const Result& r) { r.toStream(out, language::SetLanguage::getLanguage(out)); return out; -}/* operator<<(ostream&, const Result&) */ - - -void Result::toStreamDefault(std::ostream& out) const throw() { - if(getType() == Result::TYPE_SAT) { - switch(isSat()) { - case Result::UNSAT: - out << "unsat"; - break; - case Result::SAT: - out << "sat"; - break; - case Result::SAT_UNKNOWN: - out << "unknown"; - if(whyUnknown() != Result::UNKNOWN_REASON) { - out << " (" << whyUnknown() << ")"; - } - break; +} /* operator<<(ostream&, const Result&) */ + +void Result::toStreamDefault(std::ostream& out) const { + if (getType() == Result::TYPE_SAT) { + switch (isSat()) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if (whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; } } else { - switch(isValid()) { - case Result::INVALID: - out << "invalid"; - break; - case Result::VALID: - out << "valid"; - break; - case Result::VALIDITY_UNKNOWN: - out << "unknown"; - if(whyUnknown() != Result::UNKNOWN_REASON) { - out << " (" << whyUnknown() << ")"; - } - break; + switch (isValid()) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if (whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; } } -}/* Result::toStreamDefault() */ +} /* Result::toStreamDefault() */ - -void Result::toStreamSmt2(ostream& out) const throw(){ - if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { +void Result::toStreamSmt2(ostream& out) const { + if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { out << "unknown"; } else { toStreamDefault(out); } } -void Result::toStreamTptp(std::ostream& out) const throw() { +void Result::toStreamTptp(std::ostream& out) const { out << "% SZS status "; - if(isSat() == Result::SAT) { + if (isSat() == Result::SAT) { out << "Satisfiable"; - } else if(isSat() == Result::UNSAT) { + } else if (isSat() == Result::UNSAT) { out << "Unsatisfiable"; - } else if(isValid() == Result::VALID) { + } else if (isValid() == Result::VALID) { out << "Theorem"; - } else if(isValid() == Result::INVALID) { + } else if (isValid() == Result::INVALID) { out << "CounterSatisfiable"; } else { out << "GaveUp"; @@ -330,27 +347,27 @@ void Result::toStreamTptp(std::ostream& out) const throw() { out << " for " << getInputName(); } -void Result::toStream(std::ostream& out, OutputLanguage language) const throw() { - switch(language) { - case language::output::LANG_SMTLIB_V2_0: - case language::output::LANG_SMTLIB_V2_5: - case language::output::LANG_SYGUS: - case language::output::LANG_Z3STR: - toStreamSmt2(out); - break; - case language::output::LANG_TPTP: - toStreamTptp(out); - break; - case language::output::LANG_AST: - case language::output::LANG_AUTO: - case language::output::LANG_CVC3: - case language::output::LANG_CVC4: - case language::output::LANG_MAX: - case language::output::LANG_SMTLIB_V1: - default: - toStreamDefault(out); - break; +void Result::toStream(std::ostream& out, OutputLanguage language) const { + switch (language) { + case language::output::LANG_SMTLIB_V2_0: + case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SYGUS: + case language::output::LANG_Z3STR: + toStreamSmt2(out); + break; + case language::output::LANG_TPTP: + toStreamTptp(out); + break; + case language::output::LANG_AST: + case language::output::LANG_AUTO: + case language::output::LANG_CVC3: + case language::output::LANG_CVC4: + case language::output::LANG_MAX: + case language::output::LANG_SMTLIB_V1: + default: + toStreamDefault(out); + break; }; } -}/* CVC4 namespace */ +} /* CVC4 namespace */ diff --git a/src/util/result.h b/src/util/result.h index 8303ad0e8..80fbc0cf7 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -35,24 +35,12 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; * Three-valued SMT result, with optional explanation. */ class CVC4_PUBLIC Result { -public: - enum Sat { - UNSAT = 0, - SAT = 1, - SAT_UNKNOWN = 2 - }; + public: + enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; - enum Validity { - INVALID = 0, - VALID = 1, - VALIDITY_UNKNOWN = 2 - }; + enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; - enum Type { - TYPE_SAT, - TYPE_VALIDITY, - TYPE_NONE - }; + enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; enum UnknownExplanation { REQUIRES_FULL_CHECK, @@ -67,23 +55,21 @@ public: UNKNOWN_REASON }; -private: + private: enum Sat d_sat; enum Validity d_validity; enum Type d_which; enum UnknownExplanation d_unknownExplanation; std::string d_inputName; -public: - + public: Result(); Result(enum Sat s, std::string inputName = ""); Result(enum Validity v, std::string inputName = ""); - Result(enum Sat s, - enum UnknownExplanation unknownExplanation, + Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = ""); Result(enum Validity v, enum UnknownExplanation unknownExplanation, @@ -96,9 +82,7 @@ public: d_inputName = inputName; } - enum Sat isSat() const { - return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; - } + enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } enum Validity isValid() const { return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; @@ -108,20 +92,16 @@ public: return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } - Type getType() const { - return d_which; - } + Type getType() const { return d_which; } - bool isNull() const { - return d_which == TYPE_NONE; - } + bool isNull() const { return d_which == TYPE_NONE; } enum UnknownExplanation whyUnknown() const; - bool operator==(const Result& r) const throw(); - inline bool operator!=(const Result& r) const throw(); - Result asSatisfiabilityResult() const throw(); - Result asValidityResult() const throw(); + bool operator==(const Result& r) const; + inline bool operator!=(const Result& r) const; + Result asSatisfiabilityResult() const; + Result asValidityResult() const; std::string toString() const; @@ -130,19 +110,19 @@ public: /** * Write a Result out to a stream in this language. */ - void toStream(std::ostream& out, OutputLanguage language) const throw(); + void toStream(std::ostream& out, OutputLanguage language) const; /** * This is mostly the same the default * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN, * */ - void toStreamSmt2(std::ostream& out) const throw(); + void toStreamSmt2(std::ostream& out) const; /** * Write a Result out to a stream in the Tptp format */ - void toStreamTptp(std::ostream& out) const throw(); + void toStreamTptp(std::ostream& out) const; /** * Write a Result out to a stream. @@ -152,26 +132,23 @@ public: * is overridable by each Printer, since sometimes an output language * has a particular preference for how results should appear. */ - void toStreamDefault(std::ostream& out) const throw(); -};/* class Result */ + void toStreamDefault(std::ostream& out) const; +}; /* class Result */ -inline bool Result::operator!=(const Result& r) const throw() { - return !(*this == r); -} +inline bool Result::operator!=(const Result& r) const { return !(*this == r); } -std::ostream& operator<<(std::ostream& out, - enum Result::Sat s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::Validity v) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) CVC4_PUBLIC; -bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC; -bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC; +bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC; +bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC; -bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC; -bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC; +bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC; +bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__RESULT_H */ diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index efb90302f..a34689d1e 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -17,9 +17,9 @@ ** this being implemented on SExpr and not on the Printer class is that the ** Printer class lives in libcvc4. It has to currently as it prints fairly ** complicated objects, like Model, which in turn uses SmtEngine pointers. - ** However, SExprs need to be printed by Statistics. To get the output consistent - ** with the previous version, the printing of SExprs in different languages is - ** handled in the SExpr class and the libexpr library. + ** However, SExprs need to be printed by Statistics. To get the output + ** consistent with the previous version, the printing of SExprs in different + ** languages is handled in the SExpr class and the libexpr library. **/ #include "util/sexpr.h" @@ -41,9 +41,8 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { return out; } - SExpr::~SExpr() { - if(d_children != NULL){ + if (d_children != NULL) { delete d_children; d_children = NULL; } @@ -56,98 +55,88 @@ SExpr& SExpr::operator=(const SExpr& other) { d_rationalValue = other.d_rationalValue; d_stringValue = other.d_stringValue; - if(d_children == NULL && other.d_children == NULL){ + if (d_children == NULL && other.d_children == NULL) { // Do nothing. - } else if(d_children == NULL){ + } else if (d_children == NULL) { d_children = new SExprVector(*other.d_children); - } else if(other.d_children == NULL){ + } else if (other.d_children == NULL) { delete d_children; d_children = NULL; } else { (*d_children) = other.getChildren(); } - Assert( isAtom() == other.isAtom() ); - Assert( (d_children == NULL) == isAtom() ); + Assert(isAtom() == other.isAtom()); + Assert((d_children == NULL) == isAtom()); return *this; } -SExpr::SExpr() : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - - -SExpr::SExpr(const SExpr& other) : - d_sexprType(other.d_sexprType), - d_integerValue(other.d_integerValue), - d_rationalValue(other.d_rationalValue), - d_stringValue(other.d_stringValue), - d_children(NULL) -{ - d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children); +SExpr::SExpr() + : d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(const SExpr& other) + : d_sexprType(other.d_sexprType), + d_integerValue(other.d_integerValue), + d_rationalValue(other.d_rationalValue), + d_stringValue(other.d_stringValue), + d_children(NULL) { + d_children = + (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children); // d_children being NULL is equivalent to the node being an atom. - Assert( (d_children == NULL) == isAtom() ); -} - - -SExpr::SExpr(const CVC4::Integer& value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { - } - -SExpr::SExpr(int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(unsigned int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(unsigned long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(const CVC4::Rational& value) : - d_sexprType(SEXPR_RATIONAL), - d_integerValue(0), - d_rationalValue(value), - d_stringValue(""), - d_children(NULL) { -} - -SExpr::SExpr(const std::string& value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children(NULL) { -} + Assert((d_children == NULL) == isAtom()); +} + +SExpr::SExpr(const CVC4::Integer& value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(long int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(unsigned int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(unsigned long int value) + : d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(const CVC4::Rational& value) + : d_sexprType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children(NULL) {} + +SExpr::SExpr(const std::string& value) + : d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) {} /** * This constructs a string expression from a const char* value. @@ -155,37 +144,33 @@ SExpr::SExpr(const std::string& value) : * Given the other constructors this SExpr("foo") converts to bool. * instead of SExpr(string("foo")). */ -SExpr::SExpr(const char* value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children(NULL) { -} - -SExpr::SExpr(bool value) : - d_sexprType(SEXPR_KEYWORD), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value ? "true" : "false"), - d_children(NULL) { -} - -SExpr::SExpr(const Keyword& value) : - d_sexprType(SEXPR_KEYWORD), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value.getString()), - d_children(NULL) { -} - -SExpr::SExpr(const std::vector<SExpr>& children) : - d_sexprType(SEXPR_NOT_ATOM), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children(new SExprVector(children)) { -} +SExpr::SExpr(const char* value) + : d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) {} + +SExpr::SExpr(bool value) + : d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value ? "true" : "false"), + d_children(NULL) {} + +SExpr::SExpr(const Keyword& value) + : d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value.getString()), + d_children(NULL) {} + +SExpr::SExpr(const std::vector<SExpr>& children) + : d_sexprType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(new SExprVector(children)) {} std::string SExpr::toString() const { std::stringstream ss; @@ -194,68 +179,61 @@ std::string SExpr::toString() const { } /** Is this S-expression an atom? */ -bool SExpr::isAtom() const { - return d_sexprType != SEXPR_NOT_ATOM; -} +bool SExpr::isAtom() const { return d_sexprType != SEXPR_NOT_ATOM; } /** Is this S-expression an integer? */ -bool SExpr::isInteger() const { - return d_sexprType == SEXPR_INTEGER; -} +bool SExpr::isInteger() const { return d_sexprType == SEXPR_INTEGER; } /** Is this S-expression a rational? */ -bool SExpr::isRational() const { - return d_sexprType == SEXPR_RATIONAL; -} +bool SExpr::isRational() const { return d_sexprType == SEXPR_RATIONAL; } /** Is this S-expression a string? */ -bool SExpr::isString() const { - return d_sexprType == SEXPR_STRING; -} +bool SExpr::isString() const { return d_sexprType == SEXPR_STRING; } /** Is this S-expression a keyword? */ -bool SExpr::isKeyword() const { - return d_sexprType == SEXPR_KEYWORD; -} - +bool SExpr::isKeyword() const { return d_sexprType == SEXPR_KEYWORD; } std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { SExpr::toStream(out, sexpr); return out; } -void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() { +void SExpr::toStream(std::ostream& out, const SExpr& sexpr) { toStream(out, sexpr, language::SetLanguage::getLanguage(out)); } -void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() { - toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0); +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language) { + const int indent = PrettySExprs::getPrettySExprs(out) ? 2 : 0; + toStream(out, sexpr, language, indent); } -void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { - if( sexpr.isKeyword() && languageQuotesKeywords(language) ){ +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent) { + if (sexpr.isKeyword() && languageQuotesKeywords(language)) { out << quoteSymbol(sexpr.getValue()); } else { toStreamRec(out, sexpr, language, indent); } } - -void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { - if(sexpr.isInteger()) { +void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent) { + if (sexpr.isInteger()) { out << sexpr.getIntegerValue(); - } else if(sexpr.isRational()) { - out << std::fixed << sexpr.getRationalValue().getDouble(); - } else if(sexpr.isKeyword()) { + } else if (sexpr.isRational()) { + const double approximation = sexpr.getRationalValue().getDouble(); + out << std::fixed << approximation; + } else if (sexpr.isKeyword()) { out << sexpr.getValue(); - } else if(sexpr.isString()) { + } else if (sexpr.isString()) { std::string s = sexpr.getValue(); // escape backslash and quote - for(size_t i = 0; i < s.length(); ++i) { - if(s[i] == '"') { + for (size_t i = 0; i < s.length(); ++i) { + if (s[i] == '"') { s.replace(i, 1, "\\\""); ++i; - } else if(s[i] == '\\') { + } else if (s[i] == '\\') { s.replace(i, 1, "\\\\"); ++i; } @@ -265,31 +243,32 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage la const std::vector<SExpr>& kids = sexpr.getChildren(); out << (indent > 0 && kids.size() > 1 ? "( " : "("); bool first = true; - for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) { - if(first) { + for (std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); + ++i) { + if (first) { first = false; } else { - if(indent > 0) { + if (indent > 0) { out << "\n" << std::string(indent, ' '); } else { out << ' '; } } - toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2); + toStreamRec(out, *i, language, + indent <= 0 || indent > 2 ? 0 : indent + 2); } - if(indent > 0 && kids.size() > 1) { + if (indent > 0 && kids.size() > 1) { out << '\n'; - if(indent > 2) { + if (indent > 2) { out << std::string(indent - 2, ' '); } } out << ')'; } -}/* toStreamRec() */ - +} /* toStreamRec() */ bool SExpr::languageQuotesKeywords(OutputLanguage language) { - switch(language) { + switch (language) { case language::output::LANG_SMTLIB_V1: case language::output::LANG_SMTLIB_V2_0: case language::output::LANG_SMTLIB_V2_5: @@ -305,83 +284,76 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) { }; } - - std::string SExpr::getValue() const { - PrettyCheckArgument( isAtom(), this ); - switch(d_sexprType) { - case SEXPR_INTEGER: - return d_integerValue.toString(); - case SEXPR_RATIONAL: { - // We choose to represent rationals as decimal strings rather than - // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL - // could be added if we need both styles, even if it's backed by - // the same Rational object. - std::stringstream ss; - ss << std::fixed << d_rationalValue.getDouble(); - return ss.str(); - } - case SEXPR_STRING: - case SEXPR_KEYWORD: - return d_stringValue; - case SEXPR_NOT_ATOM: - return std::string(); + PrettyCheckArgument(isAtom(), this); + switch (d_sexprType) { + case SEXPR_INTEGER: + return d_integerValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } + case SEXPR_STRING: + case SEXPR_KEYWORD: + return d_stringValue; + case SEXPR_NOT_ATOM: + return std::string(); } return std::string(); - } const CVC4::Integer& SExpr::getIntegerValue() const { - PrettyCheckArgument( isInteger(), this ); + PrettyCheckArgument(isInteger(), this); return d_integerValue; } const CVC4::Rational& SExpr::getRationalValue() const { - PrettyCheckArgument( isRational(), this ); + PrettyCheckArgument(isRational(), this); return d_rationalValue; } const std::vector<SExpr>& SExpr::getChildren() const { - PrettyCheckArgument( !isAtom(), this ); - Assert( d_children != NULL ); + PrettyCheckArgument(!isAtom(), this); + Assert(d_children != NULL); return *d_children; } bool SExpr::operator==(const SExpr& s) const { - if (d_sexprType == s.d_sexprType && - d_integerValue == s.d_integerValue && + if (d_sexprType == s.d_sexprType && d_integerValue == s.d_integerValue && d_rationalValue == s.d_rationalValue && d_stringValue == s.d_stringValue) { - if(d_children == NULL && s.d_children == NULL){ + if (d_children == NULL && s.d_children == NULL) { return true; - } else if(d_children != NULL && s.d_children != NULL){ + } else if (d_children != NULL && s.d_children != NULL) { return getChildren() == s.getChildren(); } } return false; } -bool SExpr::operator!=(const SExpr& s) const { - return !(*this == s); -} - +bool SExpr::operator!=(const SExpr& s) const { return !(*this == s); } SExpr SExpr::parseAtom(const std::string& atom) { - if(atom == "true"){ + if (atom == "true") { return SExpr(true); - } else if(atom == "false"){ + } else if (atom == "false") { return SExpr(false); } else { try { Integer z(atom); return SExpr(z); - }catch(std::invalid_argument&){ + } catch (std::invalid_argument&) { // Fall through to the next case } try { Rational q(atom); return SExpr(q); - }catch(std::invalid_argument&){ + } catch (std::invalid_argument&) { // Fall through to the next case } return SExpr(atom); @@ -391,21 +363,21 @@ SExpr SExpr::parseAtom(const std::string& atom) { SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) { std::vector<SExpr> parsedAtoms; typedef std::vector<std::string>::const_iterator const_iterator; - for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){ + for (const_iterator i = atoms.begin(), i_end = atoms.end(); i != i_end; ++i) { parsedAtoms.push_back(parseAtom(*i)); } return SExpr(parsedAtoms); } -SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) { +SExpr SExpr::parseListOfListOfAtoms( + const std::vector<std::vector<std::string> >& atoms_lists) { std::vector<SExpr> parsedListsOfAtoms; - typedef std::vector< std::vector<std::string> >::const_iterator const_iterator; - for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){ + typedef std::vector<std::vector<std::string> >::const_iterator const_iterator; + for (const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); + i != i_end; ++i) { parsedListsOfAtoms.push_back(parseListOfAtoms(*i)); } return SExpr(parsedListsOfAtoms); } - - -}/* CVC4 namespace */ +} /* CVC4 namespace */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 9c80a1b1f..0b517570e 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -39,19 +39,20 @@ namespace CVC4 { class CVC4_PUBLIC SExprKeyword { - std::string d_str; -public: + public: SExprKeyword(const std::string& s) : d_str(s) {} const std::string& getString() const { return d_str; } -};/* class SExpr::Keyword */ + + private: + std::string d_str; +}; /* class SExpr::Keyword */ /** * A simple S-expression. An S-expression is either an atom with a * string value, or a list of other S-expressions. */ class CVC4_PUBLIC SExpr { -public: - + public: typedef SExprKeyword Keyword; SExpr(); @@ -138,7 +139,6 @@ public: /** Is this S-expression different from another? */ bool operator!=(const SExpr& s) const; - /** * This returns the best match in the following order: * match atom with @@ -157,21 +157,23 @@ public: /** * Parses a list of list of atoms. */ - static SExpr parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists); - + static SExpr parseListOfListOfAtoms( + const std::vector<std::vector<std::string> >& atoms_lists); /** * Outputs the SExpr onto the ostream out. This version reads defaults to the - * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is + * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level + * is * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. */ - static void toStream(std::ostream& out, const SExpr& sexpr) throw(); + static void toStream(std::ostream& out, const SExpr& sexpr); /** * Outputs the SExpr onto the ostream out. This version sets the indent level * to 2 if PrettySExprs::getPrettySExprs() is on. */ - static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw(); + static void toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language); /** * Outputs the SExpr onto the ostream out. @@ -181,19 +183,20 @@ public: * Otherwise this prints using toStreamRec(). * * TIM: Keywords that are children are not currently quoted. This seems - * incorrect but I am just reproduicing the old behavior even if it does not make + * incorrect but I am just reproduicing the old behavior even if it does not + * make * sense. */ - static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); - -private: + static void toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent); + private: /** * Simple printer for SExpr to an ostream. * The current implementation is language independent. */ - static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); - + static void toStreamRec(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent); /** Returns true if this language quotes Keywords when printing. */ static bool languageQuotesKeywords(OutputLanguage language); @@ -222,11 +225,12 @@ private: * Whenever the SExpr isAtom() holds, this points at NULL. * * This should be a pointer in case the implementation of vector<SExpr> ever - * directly contained or allocated an SExpr. If this happened this would trigger, + * directly contained or allocated an SExpr. If this happened this would + * trigger, * either the size being infinite or SExpr() being an infinite loop. */ SExprVector* d_children; -};/* class SExpr */ +}; /* class SExpr */ /** Prints an SExpr. */ std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; @@ -245,7 +249,7 @@ class CVC4_PUBLIC PrettySExprs { */ bool d_prettySExprs; -public: + public: /** * Construct a PrettySExprs with the given setting. */ @@ -273,21 +277,17 @@ public: std::ostream& d_out; bool d_oldPrettySExprs; - public: - - inline Scope(std::ostream& out, bool prettySExprs) : - d_out(out), - d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { + public: + inline Scope(std::ostream& out, bool prettySExprs) + : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { PrettySExprs::setPrettySExprs(out, prettySExprs); } - inline ~Scope() { - PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); - } + inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); } - };/* class PrettySExprs::Scope */ + }; /* class PrettySExprs::Scope */ -};/* class PrettySExprs */ +}; /* class PrettySExprs */ /** * Sets the default pretty-sexprs setting for an ostream. Use like this: @@ -299,7 +299,6 @@ public: */ std::ostream& operator<<(std::ostream& out, PrettySExprs ps); - -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SEXPR_H */ diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp index 085ecb930..a33c22f72 100644 --- a/src/util/subrange_bound.cpp +++ b/src/util/subrange_bound.cpp @@ -25,36 +25,34 @@ namespace CVC4 { -std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) -throw() { +std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) { out << bounds.lower << ".." << bounds.upper; return out; } /** Get the finite SubrangeBound, failing an assertion if infinite. */ -const Integer& SubrangeBound::getBound() const throw(IllegalArgumentException) { +const Integer& SubrangeBound::getBound() const { PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite"); return d_bound; } -SubrangeBounds::SubrangeBounds(const SubrangeBound& l, - const SubrangeBound& u) - : lower(l) - , upper(u) -{ - PrettyCheckArgument(!l.hasBound() || !u.hasBound() || - l.getBound() <= u.getBound(), - l, "Bad subrange bounds specified"); +SubrangeBounds::SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) + : lower(l), upper(u) { + PrettyCheckArgument( + !l.hasBound() || !u.hasBound() || l.getBound() <= u.getBound(), l, + "Bad subrange bounds specified"); } -bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ +bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, + const SubrangeBounds& b) { return (a.lower.hasBound() && b.lower.hasBound()) || - (a.upper.hasBound() && b.upper.hasBound()); + (a.upper.hasBound() && b.upper.hasBound()); } -SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, const SubrangeBounds& b){ - DebugCheckArgument(joinIsBounded(a,b), a); +SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, + const SubrangeBounds& b) { + DebugCheckArgument(joinIsBounded(a, b), a); SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); return SubrangeBounds(newLower, newUpper); diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 86c88e187..91c91af41 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -34,41 +34,33 @@ namespace CVC4 { * has a lower bound of -5 and an infinite upper bound. */ class CVC4_PUBLIC SubrangeBound { -public: - + public: /** Construct an infinite SubrangeBound. */ - SubrangeBound() throw() : - d_nobound(true), - d_bound() { - } + SubrangeBound() : d_nobound(true), d_bound() {} /** Construct a finite SubrangeBound. */ - SubrangeBound(const Integer& i) throw() : - d_nobound(false), - d_bound(i) { - } + SubrangeBound(const Integer& i) : d_nobound(false), d_bound(i) {} - ~SubrangeBound() throw() { - } + ~SubrangeBound() {} - /** Get the finite SubrangeBound, failing an assertion if infinite. */ - const Integer& getBound() const throw(IllegalArgumentException); + /** + * Get the finite SubrangeBound, failing an assertion if infinite. + * + * @throws IllegalArgumentException if the bound is infinite. + */ + const Integer& getBound() const; /** Returns true iff this is a finite SubrangeBound. */ - bool hasBound() const throw() { - return !d_nobound; - } + bool hasBound() const { return !d_nobound; } /** Test two SubrangeBounds for equality. */ - bool operator==(const SubrangeBound& b) const throw() { + bool operator==(const SubrangeBound& b) const { return hasBound() == b.hasBound() && - (!hasBound() || getBound() == b.getBound()); + (!hasBound() || getBound() == b.getBound()); } /** Test two SubrangeBounds for disequality. */ - bool operator!=(const SubrangeBound& b) const throw() { - return !(*this == b); - } + bool operator!=(const SubrangeBound& b) const { return !(*this == b); } /** * Is this SubrangeBound "less than" another? For two @@ -78,9 +70,9 @@ public: * behavior is due to the fact that a SubrangeBound without a bound * is the representation for both +infinity and -infinity. */ - bool operator<(const SubrangeBound& b) const throw() { + bool operator<(const SubrangeBound& b) const { return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || - ( hasBound() && b.hasBound() && getBound() < b.getBound() ); + (hasBound() && b.hasBound() && getBound() < b.getBound()); } /** @@ -91,9 +83,9 @@ public: * behavior is due to the fact that a SubrangeBound without a bound * is the representation for both +infinity and -infinity. */ - bool operator<=(const SubrangeBound& b) const throw() { + bool operator<=(const SubrangeBound& b) const { return !hasBound() || !b.hasBound() || - ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); + (hasBound() && b.hasBound() && getBound() <= b.getBound()); } /** @@ -104,9 +96,9 @@ public: * behavior is due to the fact that a SubrangeBound without a bound * is the representation for both +infinity and -infinity. */ - bool operator>(const SubrangeBound& b) const throw() { + bool operator>(const SubrangeBound& b) const { return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || - ( hasBound() && b.hasBound() && getBound() < b.getBound() ); + (hasBound() && b.hasBound() && getBound() < b.getBound()); } /** @@ -117,36 +109,34 @@ public: * strange behavior is due to the fact that a SubrangeBound without * a bound is the representation for both +infinity and -infinity. */ - bool operator>=(const SubrangeBound& b) const throw() { + bool operator>=(const SubrangeBound& b) const { return !hasBound() || !b.hasBound() || - ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); + (hasBound() && b.hasBound() && getBound() <= b.getBound()); } - - static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b){ - if(a.hasBound() && b.hasBound()){ + static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b) { + if (a.hasBound() && b.hasBound()) { return SubrangeBound(Integer::min(a.getBound(), b.getBound())); - }else{ + } else { return SubrangeBound(); } } - static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b){ - if(a.hasBound() && b.hasBound()){ + static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b) { + if (a.hasBound() && b.hasBound()) { return SubrangeBound(Integer::max(a.getBound(), b.getBound())); - }else{ + } else { return SubrangeBound(); } - } + } -private: + private: bool d_nobound; Integer d_bound; -};/* class SubrangeBound */ +}; /* class SubrangeBound */ class CVC4_PUBLIC SubrangeBounds { -public: - + public: SubrangeBound lower; SubrangeBound upper; @@ -167,7 +157,7 @@ public: */ bool operator<(const SubrangeBounds& bounds) const { return (lower > bounds.lower && upper <= bounds.upper) || - (lower >= bounds.lower && upper < bounds.upper); + (lower >= bounds.lower && upper < bounds.upper); } /** @@ -186,7 +176,7 @@ public: */ bool operator>(const SubrangeBounds& bounds) const { return (lower < bounds.lower && upper >= bounds.upper) || - (lower <= bounds.lower && upper > bounds.upper); + (lower <= bounds.lower && upper > bounds.upper); } /** @@ -209,24 +199,25 @@ public: */ static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b); -};/* class SubrangeBounds */ +}; /* class SubrangeBounds */ struct CVC4_PUBLIC SubrangeBoundsHashFunction { inline size_t operator()(const SubrangeBounds& bounds) const { // We use Integer::hash() rather than Integer::getUnsignedLong() // because the latter might overflow and throw an exception - size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max(); - size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max(); + size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() + : std::numeric_limits<size_t>::max(); + size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() + : std::numeric_limits<size_t>::max(); return l + 0x9e3779b9 + (u << 6) + (u >> 2); } -};/* struct SubrangeBoundsHashFunction */ +}; /* struct SubrangeBoundsHashFunction */ -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, + const SubrangeBound& bound) CVC4_PUBLIC; -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBound& bound) throw() { - if(bound.hasBound()) { +inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) { + if (bound.hasBound()) { out << bound.getBound(); } else { out << '_'; @@ -235,9 +226,9 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() { return out; } -std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) -throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + const SubrangeBounds& bounds) CVC4_PUBLIC; -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SUBRANGE_BOUND_H */ |