diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-04-16 12:45:10 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-16 10:45:10 +0000 |
commit | 7cae3947227391313d93fa1e2ef7bfb4e9e3986d (patch) | |
tree | 81860022a8288282678ebcfcf4976e8f20388ffc /src/util/sexpr.cpp | |
parent | 03c2724cef26fa20862634e25e3adc476d049db4 (diff) |
Replace SExpr class by simpler conversion routines (#6363)
This PR finally removes the SExpr class. SMT-LIB compatible output is retained by using new on-the-fly conversion to s-expression strings. This finally allows us to remove includes to integer and rational from smt_engine.h.
In detail:
- a new set of toSExpr() methods is implemented that converts certain types to s-expression strings (without an intermediate class representing s-expressions)
- SmtEngine::getInfo() returns a string instead of SExpr and uses the new toSExpr methods
- SmtEngine::getStatistic() is removed
- SExpr class is removed
- d_commandVerbosity uses int instead of Integer
Diffstat (limited to 'src/util/sexpr.cpp')
-rw-r--r-- | src/util/sexpr.cpp | 381 |
1 files changed, 27 insertions, 354 deletions
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 794eb7cfc..638208767 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -10,376 +10,49 @@ * directory for licensing information. * **************************************************************************** * - * Simple representation of S-expressions. - * - * SExprs have their own language specific printing procedures. The reason for - * 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. + * Simple stateless conversion to s-expressions. */ #include "util/sexpr.h" #include <iostream> -#include <sstream> -#include <vector> -#include "base/check.h" -#include "options/set_language.h" -#include "util/ostream_util.h" -#include "util/smt2_quote_string.h" +#include "util/integer.h" +#include "util/rational.h" +#include "util/statistics_value.h" namespace cvc5 { -const int PrettySExprs::s_iosIndex = std::ios_base::xalloc(); - -std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { - ps.applyPrettySExprs(out); - return out; -} - -SExpr::~SExpr() { - if (d_children != NULL) { - delete d_children; - d_children = NULL; - } - Assert(d_children == NULL); -} - -SExpr& SExpr::operator=(const SExpr& other) { - d_sexprType = other.d_sexprType; - d_integerValue = other.d_integerValue; - d_rationalValue = other.d_rationalValue; - d_stringValue = other.d_stringValue; - - if (d_children == NULL && other.d_children == NULL) { - // Do nothing. - } else if (d_children == NULL) { - d_children = new SExprVector(*other.d_children); - } 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()); - 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); - // d_children being NULL is equivalent to the node being an atom. - Assert((d_children == NULL) == isAtom()); -} - -SExpr::SExpr(const cvc5::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 cvc5::Rational& value) - : d_sexprType(SEXPR_RATIONAL), - d_integerValue(0), - d_rationalValue(value), - d_stringValue(""), - d_children(NULL) +void toSExpr(std::ostream& out, const std::string& s) { -} - -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. - * This cannot be removed in order to support SExpr("foo"). - * 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)) {} - -std::string SExpr::toString() const { - std::stringstream ss; - ss << (*this); - return ss.str(); -} - -/** Is this S-expression an 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; } - -/** Is this S-expression a 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; } - -/** Is this S-expression a 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) { - toStream(out, sexpr, language::SetLanguage::getLanguage(out)); -} - -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) { - if (sexpr.isKeyword() && languageQuotesKeywords(language)) { - out << quoteSymbol(sexpr.getValue()); - } else { - toStreamRec(out, sexpr, language, indent); + if (s == "true" || s == "false") + { + out << s; + return; } -} - -void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, - OutputLanguage language, int indent) { - StreamFormatScope scope(out); - - if (sexpr.isInteger()) { - out << sexpr.getIntegerValue(); - } 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()) { - std::string s = sexpr.getValue(); - // escape backslash and quote - for (size_t i = 0; i < s.length(); ++i) { - if (s[i] == '"') { - s.replace(i, 1, "\\\""); - ++i; - } else if (s[i] == '\\') { - s.replace(i, 1, "\\\\"); - ++i; - } - } - out << "\"" << s << "\""; - } else { - 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) { - first = false; - } else { - if (indent > 0) { - out << "\n" << std::string(indent, ' '); - } else { - out << ' '; - } - } - toStreamRec(out, *i, language, - indent <= 0 || indent > 2 ? 0 : indent + 2); - } - if (indent > 0 && kids.size() > 1) { - out << '\n'; - if (indent > 2) { - out << std::string(indent - 2, ' '); - } - } - out << ')'; + try + { + Integer tmp(s); + out << s; + return; } -} /* toStreamRec() */ - -bool SExpr::languageQuotesKeywords(OutputLanguage language) { - switch (language) { - case language::output::LANG_TPTP: - return true; - case language::output::LANG_AST: - case language::output::LANG_CVC3: - case language::output::LANG_CVC: - default: return language::isOutputLang_smt2(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(); + catch (std::invalid_argument&) + { } - return std::string(); -} - -const cvc5::Integer& SExpr::getIntegerValue() const -{ - PrettyCheckArgument(isInteger(), this); - return d_integerValue; -} - -const cvc5::Rational& SExpr::getRationalValue() const -{ - PrettyCheckArgument(isRational(), this); - return d_rationalValue; -} - -const std::vector<SExpr>& SExpr::getChildren() const { - 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 && - d_rationalValue == s.d_rationalValue && - d_stringValue == s.d_stringValue) { - if (d_children == NULL && s.d_children == NULL) { - return true; - } 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); } - -SExpr SExpr::parseAtom(const std::string& atom) { - if (atom == "true") { - return SExpr(true); - } else if (atom == "false") { - return SExpr(false); - } else { - try { - Integer z(atom); - return SExpr(z); - } catch (std::invalid_argument&) { - // Fall through to the next case - } - try { - Rational q(atom); - return SExpr(q); - } catch (std::invalid_argument&) { - // Fall through to the next case - } - return SExpr(atom); + try + { + Rational tmp(s); + out << s; + return; } -} - -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) { - parsedAtoms.push_back(parseAtom(*i)); + catch (std::invalid_argument&) + { } - return SExpr(parsedAtoms); + out << "\"" << s << "\""; } - -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) { - parsedListsOfAtoms.push_back(parseListOfAtoms(*i)); - } - return SExpr(parsedListsOfAtoms); +void toSExpr(std::ostream& out, const std::unique_ptr<StatisticBaseValue>& sbv) +{ + out << *sbv; } } // namespace cvc5 |