summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/cardinality.cpp133
-rw-r--r--src/util/cardinality.h85
-rw-r--r--src/util/integer_cln_imp.cpp10
-rw-r--r--src/util/integer_cln_imp.h11
-rw-r--r--src/util/integer_gmp_imp.h4
-rw-r--r--src/util/result.cpp383
-rw-r--r--src/util/result.h75
-rw-r--r--src/util/sexpr.cpp374
-rw-r--r--src/util/sexpr.h63
-rw-r--r--src/util/subrange_bound.cpp28
-rw-r--r--src/util/subrange_bound.h103
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback