** 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"
return out;
}
-
SExpr::~SExpr() {
- if(d_children != NULL){
+ if (d_children != NULL) {
delete d_children;
d_children = NULL;
}
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.
* 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;
}
/** 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;
}
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:
};
}
-
-
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);
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 */
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();
/** 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
/**
* 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.
* 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);
* 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;
*/
bool d_prettySExprs;
-public:
+ public:
/**
* Construct a PrettySExprs with the given setting.
*/
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:
*/
std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
#endif /* __CVC4__SEXPR_H */
projects / cvc5.git / commitdiff