From: Tim King Date: Sat, 1 Oct 2016 21:06:20 +0000 (-0700) Subject: Removing the throw specifiers from SExpr. X-Git-Tag: cvc5-1.0.0~6028^2~10 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ecadd3bf0575a9502ce0a6af63ac936cadf4291;p=cvc5.git Removing the throw specifiers from SExpr. --- 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& 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& 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& kids = sexpr.getChildren(); out << (indent > 0 && kids.size() > 1 ? "( " : "("); bool first = true; - for(std::vector::const_iterator i = kids.begin(); i != kids.end(); ++i) { - if(first) { + for (std::vector::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::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& atoms) { std::vector parsedAtoms; typedef std::vector::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 >& atoms_lists) { +SExpr SExpr::parseListOfListOfAtoms( + const std::vector >& atoms_lists) { std::vector parsedListsOfAtoms; - typedef std::vector< std::vector >::const_iterator const_iterator; - for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){ + typedef std::vector >::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..2948cba4b 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -40,18 +40,18 @@ 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 */ +}; /* 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 +138,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 +156,23 @@ public: /** * Parses a list of list of atoms. */ - static SExpr parseListOfListOfAtoms(const std::vector< std::vector >& atoms_lists); - + static SExpr parseListOfListOfAtoms( + const std::vector >& 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 +182,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 +224,12 @@ private: * Whenever the SExpr isAtom() holds, this points at NULL. * * This should be a pointer in case the implementation of vector 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 +248,7 @@ class CVC4_PUBLIC PrettySExprs { */ bool d_prettySExprs; -public: + public: /** * Construct a PrettySExprs with the given setting. */ @@ -273,21 +276,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 +298,6 @@ public: */ std::ostream& operator<<(std::ostream& out, PrettySExprs ps); - -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SEXPR_H */