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

1 files changed, 96 insertions, 260 deletions

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