Adding EchoCommand and associated printer and parser rules:

* SMT-LIBv2 parser now supports (echo...).
* Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats.
  This can make it much easier to interpret output.

2 files changed, 42 insertions, 0 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 48b6940dd..7dd9df69a 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -139,6 +139,35 @@ Command* EmptyCommand::clone() const {
   return new EmptyCommand(d_name);
 }
 
+/* class EchoCommand */
+
+EchoCommand::EchoCommand(std::string output) throw() :
+  d_output(output) {
+}
+
+std::string EchoCommand::getOutput() const throw() {
+  return d_output;
+}
+
+void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
+  /* we don't have an output stream here, nothing to do */
+  d_commandStatus = CommandSuccess::instance();
+}
+
+void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+  out << d_output << std::endl;
+  d_commandStatus = CommandSuccess::instance();
+  printResult(out);
+}
+
+Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new EchoCommand(d_output);
+}
+
+Command* EchoCommand::clone() const {
+  return new EchoCommand(d_output);
+}
+
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const BoolExpr& e) throw() :
diff --git a/src/expr/command.h b/src/expr/command.h
index a6f22fe20..19d1f16e7 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -264,6 +264,19 @@ public:
   Command* clone() const;
 };/* class EmptyCommand */
 
+class CVC4_PUBLIC EchoCommand : public Command {
+protected:
+  std::string d_output;
+public:
+  EchoCommand(std::string output = "") throw();
+  ~EchoCommand() throw() {}
+  std::string getOutput() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+};/* class EchoCommand */
+
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
   BoolExpr d_expr;