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.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 0c8accf7a394bbb9c6028d289062402fac0437c0..cdaaa05582c1dabe1f0ece47a3b6471bfcd5500d 100644 (file)
--- 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 9330f20154bb00413d00ffc9b9883efc75ce09d0..a88b7e022e0e32b1920a1ef5601585f01b377978 100644 (file)
--- 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 e625c21990ca198a64632ceb70c80a67355fc754..893bf9825b6adb2da7874008256981bcd85814be 100644 (file)
--- 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