From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 30 Sep 2021 02:37:22 +0000 (-0700)
Subject: [Printer] Only quote `set-info` value if necessary (#7262)
X-Git-Tag: cvc5-1.0.0~1155
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=181cac8b630609dc982887c5c4cea1e46b319811;p=cvc5.git

[Printer] Only quote `set-info` value if necessary (#7262)

PR #7240 changed the printing of set-info to always include quote the
value. This commit changes the policy to only quote a symbol if
necessary using existing an existing helper method. Otherwise,
(set-info :status sat) is for example printed as (set-info :status |sat|), which is a bit unusual and may break certain scripts.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e6aff1ace..fd98bdeca 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1622,7 +1622,8 @@ void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
                                      const std::string& flag,
                                      const std::string& value) const
 {
-    out << "(set-info :" << flag << " |" << value << "|)" << std::endl;
+  out << "(set-info :" << flag << " " << cvc5::quoteSymbol(value) << ")"
+      << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,