Avoid calling the printers while converting sexpr to string. (#5842)

This PR modifies sexprToString to use Term::getString to get string constants instead of Term::toString, which depends on the output language. The previous behavior caused CVC4 to crash when AST is picked as the output language.

3 files changed, 11 insertions, 19 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 0c8accf7a..cdaaa0558 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -47,20 +47,15 @@ namespace CVC4 {
 
 std::string sexprToString(api::Term sexpr)
 {
-  // if sexpr is a spec constant and not a string, return the result of calling
-  // Term::toString
-  if (sexpr.getKind() == api::CONST_BOOLEAN
-      || sexpr.getKind() == api::CONST_FLOATINGPOINT
-      || sexpr.getKind() == api::CONST_RATIONAL)
+  // if sexpr is a constant string, return the stored constant string. We don't
+  // call Term::toString as its result depends on the output language.
+  // Notice that we only check for string constants. The sexprs generated by the
+  // parser don't contains other constants, so we can ignore them.
+  if (sexpr.isString())
   {
-    return sexpr.toString();
-  }
-
-  // if sexpr is a constant string, return the result of calling Term::toString.
-  // However, strip the surrounding quotes
-  if (sexpr.getKind() == api::CONST_STRING)
-  {
-    return sexpr.toString().substr(1, sexpr.toString().length() - 2);
+    // convert std::wstring to std::string
+    std::wstring wstring = sexpr.getString();
+    return std::string(wstring.cbegin(), wstring.cend());
   }
 
   // if sexpr is not a spec constant, make sure it is an array of sub-sexprs
@@ -1101,9 +1096,7 @@ std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
 DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
                                                api::Term func,
                                                api::Sort sort)
-    : DeclarationDefinitionCommand(id),
-      d_func(func),
-      d_sort(sort)
+    : DeclarationDefinitionCommand(id), d_func(func), d_sort(sort)
 {
 }
 
diff --git a/src/smt/command.h b/src/smt/command.h
index 9330f2015..a88b7e022 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -51,8 +51,7 @@ class Model;
 
 /**
  * Convert a symbolic expression to string. This method differs from
- * Term::toString in that it does not surround constant strings with double
- * quote symbols.
+ * Term::toString in that it does not depend on the output language.
  *
  * @param sexpr the symbolic expression to convert
  * @return the symbolic expression as string
diff --git a/src/util/string.cpp b/src/util/string.cpp
index e625c2199..893bf9825 100644
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -510,7 +510,7 @@ Rational String::toNumber() const
 }
 
 std::ostream &operator<<(std::ostream &os, const String &s) {
-  return os << "\"" << s.toString(true) << "\"";
+  return os << "\"" << s.toString() << "\"";
 }
 
 }  // namespace CVC4