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
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;
}
#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
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<SExpr> stats;
- for (const auto& s : d_env->getStatisticsRegistry())
- {
- std::stringstream ss;
- ss << *s.second;
- vector<SExpr> 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")
{
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")
{
{
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
{
{
size_t ulevel = d_state->getNumUserLevels();
AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max());
- return SExpr(static_cast<unsigned long int>(ulevel));
+ return toSExpr(ulevel);
}
Assert(key == "all-options");
// get the options, like all-statistics
- std::vector<std::vector<std::string>> current_options =
- Options::current()->getOptions();
- return SExpr::parseListOfListOfAtoms(current_options);
+ return toSExpr(Options::current()->getOptions());
}
void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
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);
Trace("smt") << "SMT getOption(" << key << ")" << endl;
- if (key.length() >= 18 && key.compare(0, 18, "command-verbosity:") == 0)
+ if (key.find("command-verbosity:") == 0)
{
- map<string, Integer>::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";
}
{
vector<Node> result;
Node defaultVerbosity;
- for (map<string, Integer>::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);
#include "smt/smt_mode.h"
#include "theory/logic_info.h"
#include "util/result.h"
-#include "util/sexpr.h"
namespace cvc5 {
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.
/** 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.
/**
* Verbosity of various commands.
*/
- std::map<std::string, Integer> d_commandVerbosity;
+ std::map<std::string, int> d_commandVerbosity;
/** The statistics class */
std::unique_ptr<smt::SmtEngineStatistics> d_stats;
* 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
* 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 <iosfwd>
+#include <iostream>
+#include <memory>
+#include <sstream>
#include <string>
+#include <type_traits>
+#include <utility>
#include <vector>
-#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<StatisticBaseValue>& 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 <typename T>
+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<SExpr>& 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<SExpr>& 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<std::string>& atoms);
-
- /**
- * Parses a list of list of atoms.
- */
- 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
- * 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<SExpr> 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<SExpr> 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<T, bool>)
+ {
+ out << (t ? "true" : "false");
+ }
+ if constexpr (std::is_integral_v<T>)
+ {
+ 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 <typename T>
+void toSExpr(std::ostream& out, const std::vector<T>& v);
/**
- * IOStream manipulator to pretty-print SExprs.
+ * Render an `std::pair` to an s-expression string.
*/
-class CVC4_EXPORT PrettySExprs
+template <typename T1, typename T2>
+void toSExpr(std::ostream& out, const std::pair<T1, T2>& 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 <typename Iterator>
+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 <typename T>
+void toSExpr(std::ostream& out, const std::vector<T>& v)
+{
+ toSExpr(out, v.begin(), v.end());
+}
-}; /* class PrettySExprs */
+/**
+ * Convert arbitrary data to an s-expression string.
+ */
+template <typename T>
+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 <typename Iterator>
+std::string toSExpr(Iterator begin, Iterator end)
+{
+ std::stringstream ss;
+ toSExpr(ss, begin, end);
+ return ss.str();
+}
} // namespace cvc5
projects / cvc5.git / commitdiff