From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Wed, 6 Oct 2021 00:41:05 +0000 (-0500)
Subject: Avoid calling `quoteSymbol` multiple times. (#7307)
X-Git-Tag: cvc5-1.0.0~1121
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa18d91091ef640fd38b29ed87f69260d8f80208;p=cvc5.git

Avoid calling `quoteSymbol` multiple times. (#7307)

Calling `quoteSymbol(...)` twice on an empty string `""` returns `"|__|"`.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 507937b2d..32b195be2 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1223,12 +1223,6 @@ static bool tryToStream(std::ostream& out, const Command* c);
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c, Variant v);
 
-static std::string quoteSymbol(TNode n) {
-  std::stringstream ss;
-  ss << n;
-  return cvc5::quoteSymbol(ss.str());
-}
-
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v);
 
@@ -1317,8 +1311,7 @@ void Smt2Printer::toStreamModelSort(std::ostream& out,
           || options::modelUninterpPrint()
                  == options::ModelUninterpPrintMode::DeclFun)
       {
-        out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
-            << endl;
+        out << "(declare-fun " << trn << " () " << tn << ")" << endl;
       }
     }
     else
@@ -1543,11 +1536,8 @@ void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
                                          TypeNode type) const
 {
   Assert(type.isSort() || type.isSortConstructor());
-  std::stringstream id;
-  id << type;
   size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
-  out << "(declare-sort " << cvc5::quoteSymbol(id.str()) << " " << arity << ")"
-      << std::endl;
+  out << "(declare-sort " << type << " " << arity << ")" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
@@ -1814,11 +1804,7 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
                                       bool isInv,
                                       TypeNode sygusType) const
 {
-  std::stringstream sym;
-  sym << f;
-  out << '(' << (isInv ? "synth-inv " : "synth-fun ")
-      << cvc5::quoteSymbol(sym.str()) << ' ';
-  out << '(';
+  out << '(' << (isInv ? "synth-inv " : "synth-fun ") << f << ' ' << '(';
   if (!vars.empty())
   {
     // print variable list