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 | |
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')
-rw-r--r-- | src/util/sexpr.cpp | 381 | ||||
-rw-r--r-- | src/util/sexpr.h | 356 |
2 files changed, 123 insertions, 614 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 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 <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 |