summaryrefslogtreecommitdiff
path: root/src/smt/command.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r--src/smt/command.cpp17
1 files changed, 5 insertions, 12 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 311d6713a..e8ee6d59c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,6 +38,7 @@
#include "proof/unsat_core.h"
#include "smt/dump.h"
#include "smt/model.h"
+#include "util/smt2_quote_string.h"
#include "util/unsafe_interrupt_exception.h"
#include "util/utility.h"
@@ -302,19 +303,10 @@ void EmptyCommand::toStream(std::ostream& out,
/* class EchoCommand */
/* -------------------------------------------------------------------------- */
-EchoCommand::EchoCommand(std::string output)
-{
- // escape all double-quotes
- size_t pos = 0;
- while ((pos = output.find('"', pos)) != string::npos)
- {
- output.replace(pos, 1, "\"\"");
- pos += 2;
- }
- d_output = '"' + output + '"';
-}
+EchoCommand::EchoCommand(std::string output) : d_output(output) {}
std::string EchoCommand::getOutput() const { return d_output; }
+
void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
/* we don't have an output stream here, nothing to do */
@@ -325,7 +317,7 @@ void EchoCommand::invoke(api::Solver* solver,
SymbolManager* sm,
std::ostream& out)
{
- out << d_output << std::endl;
+ out << cvc5::quoteString(d_output) << std::endl;
Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
<< std::endl;
d_commandStatus = CommandSuccess::instance();
@@ -335,6 +327,7 @@ void EchoCommand::invoke(api::Solver* solver,
}
Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
+
std::string EchoCommand::getCommandName() const { return "echo"; }
void EchoCommand::toStream(std::ostream& out,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback