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.

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 48b6940dd9d751792c50c828c8d69c2aa835ae01..7dd9df69abd1cb2fcd9f1cc60050ae4c09a4255c 100644 (file)
--- 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 a6f22fe2010175c0f3a104a301f2e2a3b64f1fe6..19d1f16e7351bdf95e571beab6951d292267bbae 100644 (file)
--- 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;

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2da9f0f638fdfbd3331fcaa5a691eba0157145b1..1f0e6b890e65c5966daa5b5083ced80eb54ae18d 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -706,8 +706,11 @@ mainCommand[CVC4::Command*& cmd]
 
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
-      { Message() << sexpr << std::endl; }
-    | { Message() << std::endl; }
+      { std::stringstream ss;
+        ss << sexpr;
+        cmd = new EchoCommand(ss.str());
+      }
+    | { cmd = new EchoCommand(); }
     )
 
   | EXIT_TOK

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2b5d54afa4b861e8b76ea541c846da2819bbacd7..19f77ac87842dcc92050e616d103713558824c92 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -372,6 +372,14 @@ extendedCommand[CVC4::Command*& cmd]
     LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
     { PARSER_STATE->popScope();
       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+  | ECHO_TOK
+    ( simpleSymbolicExpr[sexpr]
+      { std::stringstream ss;
+        ss << sexpr;
+        cmd = new EchoCommand(ss.str());
+      }
+    | { cmd = new EchoCommand(); }
+    )
   ;
 
 simpleSymbolicExpr[CVC4::SExpr& sexpr]
@@ -918,6 +926,7 @@ POP_TOK : 'pop';
 
 // extended commands
 DECLARE_DATATYPES_TOK : 'declare-datatypes';
+ECHO_TOK : 'echo';
 
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 1df59adc491c41952347f791aca65013c40c5657..f779a1bdccb1319383eea8f77b682657c0f91dfa 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -597,7 +597,8 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<GetOptionCommand>(out, c) ||
      tryToStream<DatatypeDeclarationCommand>(out, c) ||
      tryToStream<CommentCommand>(out, c) ||
-     tryToStream<EmptyCommand>(out, c)) {
+     tryToStream<EmptyCommand>(out, c) ||
+     tryToStream<EchoCommand>(out, c)) {
     return;
   }
 
@@ -807,6 +808,10 @@ static void toStream(std::ostream& out, const CommentCommand* c) throw() {
 static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 }
 
+static void toStream(std::ostream& out, const EchoCommand* c) throw() {
+  out << "ECHO \"" << c->getOutput() << "\";";
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) throw() {
   if(typeid(*c) == typeid(T)) {

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 25d3bf35a4390c60c42172d011de58e53e09eea5..a1ee99d8f441deed1ec2267e233d88ea31877443 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -423,7 +423,8 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<GetOptionCommand>(out, c) ||
      tryToStream<DatatypeDeclarationCommand>(out, c) ||
      tryToStream<CommentCommand>(out, c) ||
-     tryToStream<EmptyCommand>(out, c)) {
+     tryToStream<EmptyCommand>(out, c) ||
+     tryToStream<EchoCommand>(out, c)) {
     return;
   }
 
@@ -661,6 +662,10 @@ static void toStream(std::ostream& out, const CommentCommand* c) throw() {
 static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 }
 
+static void toStream(std::ostream& out, const EchoCommand* c) throw() {
+  out << "(echo \"" << c->getOutput() << "\")";
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) throw() {
   if(typeid(*c) == typeid(T)) {