From: Gereon Kremer Date: Fri, 16 Apr 2021 10:45:10 +0000 (+0200) Subject: Replace SExpr class by simpler conversion routines (#6363) X-Git-Tag: cvc5-1.0.0~1891 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7cae3947227391313d93fa1e2ef7bfb4e9e3986d;p=cvc5.git 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 --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2b4cc4795..a32ff4caa 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -6418,7 +6418,7 @@ std::string Solver::getInfo(const std::string& flag) const CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) << "Unrecognized flag for getInfo."; //////// all checks before this line - return d_smtEngine->getInfo(flag).toString(); + return d_smtEngine->getInfo(flag); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 88cb078ae..122e69488 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -66,6 +66,7 @@ #include "theory/theory_engine.h" #include "util/random.h" #include "util/resource_manager.h" +#include "util/sexpr.h" #include "util/statistics_registry.h" // required for hacks related to old proofs for unsat cores @@ -510,40 +511,30 @@ bool SmtEngine::isValidGetInfoFlag(const std::string& key) const return false; } -cvc5::SExpr SmtEngine::getInfo(const std::string& key) const +std::string SmtEngine::getInfo(const std::string& key) const { SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; if (key == "all-statistics") { - vector stats; - for (const auto& s : d_env->getStatisticsRegistry()) - { - std::stringstream ss; - ss << *s.second; - vector v; - v.push_back(s.first); - v.push_back(ss.str()); - stats.push_back(v); - } - return SExpr(stats); + return toSExpr(d_env->getStatisticsRegistry().begin(), d_env->getStatisticsRegistry().end()); } if (key == "error-behavior") { - return SExpr(SExpr::Keyword("immediate-exit")); + return "immediate-exit"; } if (key == "name") { - return SExpr(Configuration::getName()); + return toSExpr(Configuration::getName()); } if (key == "version") { - return SExpr(Configuration::getVersionString()); + return toSExpr(Configuration::getVersionString()); } if (key == "authors") { - return SExpr(Configuration::about()); + return toSExpr(Configuration::about()); } if (key == "status") { @@ -551,14 +542,14 @@ cvc5::SExpr SmtEngine::getInfo(const std::string& key) const Result status = d_state->getStatus(); switch (status.asSatisfiabilityResult().isSat()) { - case Result::SAT: return SExpr(SExpr::Keyword("sat")); - case Result::UNSAT: return SExpr(SExpr::Keyword("unsat")); - default: return SExpr(SExpr::Keyword("unknown")); + case Result::SAT: return "sat"; + case Result::UNSAT: return "unsat"; + default: return "unknown"; } } if (key == "time") { - return SExpr(std::clock()); + return toSExpr(std::clock()); } if (key == "reason-unknown") { @@ -567,9 +558,9 @@ cvc5::SExpr SmtEngine::getInfo(const std::string& key) const { std::stringstream ss; ss << status.whyUnknown(); - string s = ss.str(); + std::string s = ss.str(); transform(s.begin(), s.end(), s.begin(), ::tolower); - return SExpr(SExpr::Keyword(s)); + return s; } else { @@ -582,13 +573,11 @@ cvc5::SExpr SmtEngine::getInfo(const std::string& key) const { size_t ulevel = d_state->getNumUserLevels(); AlwaysAssert(ulevel <= std::numeric_limits::max()); - return SExpr(static_cast(ulevel)); + return toSExpr(ulevel); } Assert(key == "all-options"); // get the options, like all-statistics - std::vector> current_options = - Options::current()->getOptions(); - return SExpr::parseListOfListOfAtoms(current_options); + return toSExpr(Options::current()->getOptions()); } void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) @@ -1877,14 +1866,6 @@ NodeManager* SmtEngine::getNodeManager() const return d_env->getNodeManager(); } -SExpr SmtEngine::getStatistic(std::string name) const -{ - const auto* val = d_env->getStatisticsRegistry().get(name); - std::stringstream ss; - ss << *val; - return SExpr({SExpr(name), SExpr(ss.str())}); -} - void SmtEngine::printStatistics(std::ostream& out) const { d_env->getStatisticsRegistry().print(out); @@ -1964,18 +1945,17 @@ std::string SmtEngine::getOption(const std::string& key) const Trace("smt") << "SMT getOption(" << key << ")" << endl; - if (key.length() >= 18 && key.compare(0, 18, "command-verbosity:") == 0) + if (key.find("command-verbosity:") == 0) { - map::const_iterator i = - d_commandVerbosity.find(key.c_str() + 18); - if (i != d_commandVerbosity.end()) + auto it = d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:"))); + if (it != d_commandVerbosity.end()) { - return i->second.toString(); + return std::to_string(it->second); } - i = d_commandVerbosity.find("*"); - if (i != d_commandVerbosity.end()) + it = d_commandVerbosity.find("*"); + if (it != d_commandVerbosity.end()) { - return i->second.toString(); + return std::to_string(it->second); } return "2"; } @@ -1989,15 +1969,13 @@ std::string SmtEngine::getOption(const std::string& key) const { vector result; Node defaultVerbosity; - for (map::const_iterator i = d_commandVerbosity.begin(); - i != d_commandVerbosity.end(); - ++i) + for (const auto& verb: d_commandVerbosity) { // treat the command name as a variable name as opposed to a string // constant to avoid printing double quotes around the name - Node name = nm->mkBoundVar(i->first, nm->integerType()); - Node value = nm->mkConst(Rational(i->second)); - if ((*i).first == "*") + Node name = nm->mkBoundVar(verb.first, nm->integerType()); + Node value = nm->mkConst(Rational(verb.second)); + if (verb.first == "*") { // put the default at the end of the SExpr defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ff1a955ee..59081f63e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -30,7 +30,6 @@ #include "smt/smt_mode.h" #include "theory/logic_info.h" #include "util/result.h" -#include "util/sexpr.h" namespace cvc5 { @@ -217,7 +216,7 @@ class CVC4_EXPORT SmtEngine bool isValidGetInfoFlag(const std::string& key) const; /** Query information about the SMT environment. */ - cvc5::SExpr getInfo(const std::string& key) const; + std::string getInfo(const std::string& key) const; /** * Set an aspect of the current SMT execution environment. @@ -826,9 +825,6 @@ class CVC4_EXPORT SmtEngine /** Permit access to the underlying NodeManager. */ NodeManager* getNodeManager() const; - /** Get the value of one named statistic from this SmtEngine. */ - SExpr getStatistic(std::string name) const; - /** * Print statistics from the statistics registry in the env object owned by * this SmtEngine. @@ -1144,7 +1140,7 @@ class CVC4_EXPORT SmtEngine /** * Verbosity of various commands. */ - std::map d_commandVerbosity; + std::map d_commandVerbosity; /** The statistics class */ std::unique_ptr d_stats; 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 -#include -#include -#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& 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& 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) { - 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::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& 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) { - parsedAtoms.push_back(parseAtom(*i)); + catch (std::invalid_argument&) + { } - return SExpr(parsedAtoms); + out << "\"" << s << "\""; } - -SExpr SExpr::parseListOfListOfAtoms( - const std::vector >& atoms_lists) { - std::vector parsedListsOfAtoms; - 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); +void toSExpr(std::ostream& out, const std::unique_ptr& sbv) +{ + out << *sbv; } } // namespace cvc5 diff --git a/src/util/sexpr.h b/src/util/sexpr.h index b5144fbd2..18a579dec 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -10,296 +10,132 @@ * directory for licensing information. * **************************************************************************** * - * Simple representation of S-expressions + * Simple stateless conversion to s-expressions. * - * These are used when a simple, and obvious interface for basic - * expressions is appropriate. + * This file contains a collection of conversion routines from various data to + * s-expressions as strings. The actual conversion is provided by methods of + * the following form, where T is some type: * - * These are quite ineffecient. - * These are totally disconnected from any ExprManager. - * These keep unique copies of all of their children. - * These are VERY overly verbose and keep much more data than is needed. + * toSExpr(std::ostream& out, const T& t) + * + * A fallback is provided where T is a template type that forwards to the + * generic streaming operator `operator<<()` for T. + * To make usage easier, `std::string toSExpr(const T&)` is provided as well. + * For containers, an overload that accepts two iterators is available. */ -#include "cvc5_public.h" +#include "cvc5_private.h" #ifndef CVC5__SEXPR_H #define CVC5__SEXPR_H -#include +#include +#include +#include #include +#include +#include #include -#include "cvc4_export.h" -#include "options/language.h" -#include "util/integer.h" -#include "util/rational.h" - namespace cvc5 { -class SExprKeyword -{ - public: - SExprKeyword(const std::string& s) : d_str(s) {} - const std::string& getString() const { return d_str; } +// Forward declarations +struct StatisticBaseValue; - private: - std::string d_str; -}; /* class SExpr::Keyword */ +// Non-templated overloads that live in the source file +void toSExpr(std::ostream& out, const std::string& s); +void toSExpr(std::ostream& out, const std::unique_ptr& sbv); /** - * A simple S-expression. An S-expression is either an atom with a - * string value, or a list of other S-expressions. + * Fallback overload for basic types. + * + * Prints Boolean values as `true` and `false`, integral numbers as numbers and + * all other types using their respective streaming operators, enclosed with + * double quotes. */ -class CVC4_EXPORT SExpr +template +void toSExpr(std::ostream& out, const T& t) { - public: - typedef SExprKeyword Keyword; - - SExpr(); - SExpr(const SExpr&); - SExpr& operator=(const SExpr& other); - ~SExpr(); - - SExpr(const cvc5::Integer& value); - - SExpr(int value); - SExpr(long int value); - SExpr(unsigned int value); - SExpr(unsigned long int value); - - SExpr(const cvc5::Rational& value); - - SExpr(const std::string& value); - - /** - * 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(const char* value); - - /** - * This adds a convenience wrapper to SExpr to cast from bools. - * This is internally handled as the strings "true" and "false" - */ - SExpr(bool value); - SExpr(const Keyword& value); - SExpr(const std::vector& children); - - /** Is this S-expression an atom? */ - bool isAtom() const; - - /** Is this S-expression an integer? */ - bool isInteger() const; - - /** Is this S-expression a rational? */ - bool isRational() const; - - /** Is this S-expression a string? */ - bool isString() const; - - /** Is this S-expression a keyword? */ - bool isKeyword() const; - - /** - * This wraps the toStream() printer. - * NOTE: toString() and getValue() may differ on Keywords based on - * the current language set in expr. - */ - std::string toString() const; - - /** - * Get the string value of this S-expression. This will cause an - * error if this S-expression is not an atom. - */ - std::string getValue() const; - - /** - * Get the integer value of this S-expression. This will cause an - * error if this S-expression is not an integer. - */ - const cvc5::Integer& getIntegerValue() const; - - /** - * Get the rational value of this S-expression. This will cause an - * error if this S-expression is not a rational. - */ - const cvc5::Rational& getRationalValue() const; - - /** - * Get the children of this S-expression. This will cause an error - * if this S-expression is not a list. - */ - const std::vector& getChildren() const; - - /** Is this S-expression equal to another? */ - bool operator==(const SExpr& s) const; - - /** 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 - * "true", "false" -> SExpr(value) - * | is and integer -> as integer - * | is a rational -> as rational - * | _ -> SExpr() - */ - static SExpr parseAtom(const std::string& atom); - - /** - * Parses a list of atoms. - */ - static SExpr parseListOfAtoms(const std::vector& atoms); - - /** - * Parses a list of list of atoms. - */ - 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 - * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. - */ - 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); - - /** - * Outputs the SExpr onto the ostream out. - * If the languageQuotesKeywords(language), then a top level keyword, " X", - * that needs quoting according to the SMT2 language standard is printed with - * quotes, "| X|". - * 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 - * sense. - */ - 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); - - /** Returns true if this language quotes Keywords when printing. */ - static bool languageQuotesKeywords(OutputLanguage language); - - enum SExprTypes { - SEXPR_STRING, - SEXPR_KEYWORD, - SEXPR_INTEGER, - SEXPR_RATIONAL, - SEXPR_NOT_ATOM - } d_sexprType; - - /** The value of an atomic integer-valued S-expression. */ - cvc5::Integer d_integerValue; - - /** The value of an atomic rational-valued S-expression. */ - cvc5::Rational d_rationalValue; - - /** The value of an atomic S-expression. */ - std::string d_stringValue; - - typedef std::vector SExprVector; - - /** - * The children of a list S-expression. - * 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, - * either the size being infinite or SExpr() being an infinite loop. - */ - SExprVector* d_children; -}; /* class SExpr */ + if constexpr (std::is_same_v) + { + out << (t ? "true" : "false"); + } + if constexpr (std::is_integral_v) + { + out << t; + } + else + { + out << "\"" << t << "\""; + } +} -/** Prints an SExpr. */ -std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_EXPORT; +// Forward declarations of templated overloads +template +void toSExpr(std::ostream& out, const std::vector& v); /** - * IOStream manipulator to pretty-print SExprs. + * Render an `std::pair` to an s-expression string. */ -class CVC4_EXPORT PrettySExprs +template +void toSExpr(std::ostream& out, const std::pair& p) { - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * When this manipulator is used, the setting is stored here. - */ - bool d_prettySExprs; - - public: - /** - * Construct a PrettySExprs with the given setting. - */ - PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {} - - inline void applyPrettySExprs(std::ostream& out) { - out.iword(s_iosIndex) = d_prettySExprs; - } - - static inline bool getPrettySExprs(std::ostream& out) { - return out.iword(s_iosIndex); - } - - static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) { - out.iword(s_iosIndex) = prettySExprs; - } + out << "("; + toSExpr(out, p.first); + out << " "; + toSExpr(out, p.second); + out << ")"; +} - /** - * Set the pretty-sexprs state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - bool d_oldPrettySExprs; - - public: - inline Scope(std::ostream& out, bool prettySExprs) - : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { - PrettySExprs::setPrettySExprs(out, prettySExprs); +/** + * Render an arbitrary iterator range to an s-expression string. + */ +template +void toSExpr(std::ostream& out, Iterator begin, Iterator end) +{ + out << "("; + for (auto it = begin; it != end; ++it) + { + if (it != begin) + { + out << " "; } + toSExpr(out, *it); + } + out << ")"; +} - inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); } - - }; /* class PrettySExprs::Scope */ +/** + * Render a vector to an s-expression string. + * Convenience wrapper for `std::vector` around the overload using iterators. + */ +template +void toSExpr(std::ostream& out, const std::vector& v) +{ + toSExpr(out, v.begin(), v.end()); +} -}; /* class PrettySExprs */ +/** + * Convert arbitrary data to an s-expression string. + */ +template +std::string toSExpr(const T& t) +{ + std::stringstream ss; + toSExpr(ss, t); + return ss.str(); +} /** - * Sets the default pretty-sexprs setting for an ostream. Use like this: - * - * // let out be an ostream, s an SExpr - * out << PrettySExprs(true) << s << endl; - * - * The setting stays permanently (until set again) with the stream. + * Convert an arbitrary iterator range to an s-expression string. */ -std::ostream& operator<<(std::ostream& out, PrettySExprs ps); +template +std::string toSExpr(Iterator begin, Iterator end) +{ + std::stringstream ss; + toSExpr(ss, begin, end); + return ss.str(); +} } // namespace cvc5