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.

1 files changed, 9 insertions, 16 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)
 {
 }