From 0a7dc7687a4989641d8c101ba3b2d4737eaea24f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 7 Jun 2012 16:16:48 +0000 Subject: [PATCH] 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. --- src/expr/command.cpp | 29 +++++++++++++++++++++++++++++ src/expr/command.h | 13 +++++++++++++ src/parser/cvc/Cvc.g | 7 +++++-- src/parser/smt2/Smt2.g | 9 +++++++++ src/printer/cvc/cvc_printer.cpp | 7 ++++++- src/printer/smt2/smt2_printer.cpp | 7 ++++++- 6 files changed, 68 insertions(+), 4 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; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2da9f0f63..1f0e6b890 100644 --- 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 2b5d54afa..19f77ac87 100644 --- 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 1df59adc4..f779a1bdc 100644 --- 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(out, c) || tryToStream(out, c) || tryToStream(out, c) || - tryToStream(out, c)) { + tryToStream(out, c) || + tryToStream(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 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 25d3bf35a..a1ee99d8f 100644 --- 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(out, c) || tryToStream(out, c) || tryToStream(out, c) || - tryToStream(out, c)) { + tryToStream(out, c) || + tryToStream(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 static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { -- 2.30.2