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, 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