diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 106 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 5 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 123 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 5 | ||||
-rw-r--r-- | src/printer/printer.cpp | 11 | ||||
-rw-r--r-- | src/printer/printer.h | 20 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 8 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 5 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 129 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 5 |
10 files changed, 285 insertions, 132 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 082765765..b941957c4 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -34,7 +34,7 @@ namespace printer { namespace ast { void AstPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; @@ -95,13 +95,13 @@ void AstPrinter::toStream(std::ostream& out, TNode n, } } out << ')'; -}/* AstPrinter::toStream() */ +}/* AstPrinter::toStream(TNode) */ template <class T> -static bool tryToStream(std::ostream& out, const Command* c); +static bool tryToStream(std::ostream& out, const Command* c) throw(); void AstPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { expr::ExprSetDepth::Scope sdScope(out, toDepth); expr::ExprPrintTypes::Scope ptScope(out, types); @@ -134,27 +134,44 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, return; } - Unhandled("don't know how to print a Command of class: %s", typeid(*c).name()); + out << "ERROR: don't know how to print a Command of class: " + << typeid(*c).name() << endl; -}/* AstPrinter::toStream() */ +}/* AstPrinter::toStream(Command*) */ -static void toStream(std::ostream& out, const EmptyCommand* c) { +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); + +void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { + + if(tryToStream<CommandSuccess>(out, s) || + tryToStream<CommandFailure>(out, s) || + tryToStream<CommandUnsupported>(out, s)) { + return; + } + + out << "ERROR: don't know how to print a CommandStatus of class: " + << typeid(*s).name() << endl; + +}/* AstPrinter::toStream(CommandStatus*) */ + +static void toStream(std::ostream& out, const EmptyCommand* c) throw() { out << "EmptyCommand(" << c->getName() << ")"; } -static void toStream(std::ostream& out, const AssertCommand* c) { +static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "Assert(" << c->getExpr() << ")"; } -static void toStream(std::ostream& out, const PushCommand* c) { +static void toStream(std::ostream& out, const PushCommand* c) throw() { out << "Push()"; } -static void toStream(std::ostream& out, const PopCommand* c) { +static void toStream(std::ostream& out, const PopCommand* c) throw() { out << "Pop()"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) { +static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { BoolExpr e = c->getExpr(); if(e.isNull()) { out << "CheckSat()"; @@ -163,15 +180,15 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { } } -static void toStream(std::ostream& out, const QueryCommand* c) { +static void toStream(std::ostream& out, const QueryCommand* c) throw() { out << "Query(" << c->getExpr() << ')'; } -static void toStream(std::ostream& out, const QuitCommand* c) { +static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "Quit()"; } -static void toStream(std::ostream& out, const DeclarationSequence* c) { +static void toStream(std::ostream& out, const DeclarationSequence* c) throw() { out << "DeclarationSequence[" << endl; for(CommandSequence::const_iterator i = c->begin(); i != c->end(); @@ -181,7 +198,7 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) { out << "]"; } -static void toStream(std::ostream& out, const CommandSequence* c) { +static void toStream(std::ostream& out, const CommandSequence* c) throw() { out << "CommandSequence[" << endl; for(CommandSequence::const_iterator i = c->begin(); i != c->end(); @@ -191,11 +208,11 @@ static void toStream(std::ostream& out, const CommandSequence* c) { out << "]"; } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { out << "Declare(" << c->getSymbol() << "," << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { Expr func = c->getFunction(); const std::vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -208,12 +225,12 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "], << " << formula << " >> )"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) { +static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << "," << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineTypeCommand* c) { +static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { const vector<Type>& params = c->getParameters(); out << "DefineType(" << c->getSymbol() << ",["; if(params.size() > 0) { @@ -224,48 +241,48 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) { out << "]," << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); out << " )"; } -static void toStream(std::ostream& out, const SimplifyCommand* c) { +static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { out << "Simplify( << " << c->getTerm() << " >> )"; } -static void toStream(std::ostream& out, const GetValueCommand* c) { +static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "GetValue( << " << c->getTerm() << " >> )"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) { +static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "GetAssignment()"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) { +static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "GetAssertions()"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "SetBenchmarkStatus(" << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { out << "SetBenchmarkLogic(" << c->getLogic() << ")"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) { +static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) { +static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { out << "GetInfo(" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) { +static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) { +static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "GetOption(" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); out << "DatatypeDeclarationCommand(["; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), @@ -277,12 +294,12 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { out << "])"; } -static void toStream(std::ostream& out, const CommentCommand* c) { +static void toStream(std::ostream& out, const CommentCommand* c) throw() { out << "CommentCommand([" << c->getComment() << "])"; } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) { +static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { toStream(out, dynamic_cast<const T*>(c)); return true; @@ -290,6 +307,29 @@ static bool tryToStream(std::ostream& out, const Command* c) { return false; } +static void toStream(std::ostream& out, const CommandSuccess* s) throw() { + if(Command::printsuccess::getPrintSuccess(out)) { + out << "OK" << endl; + } +} + +static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { + out << "UNSUPPORTED" << endl; +} + +static void toStream(std::ostream& out, const CommandFailure* s) throw() { + out << s->getMessage() << endl; +} + +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { + if(typeid(*s) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(s)); + return true; + } + return false; +} + }/* CVC4::printer::ast namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 69c39915b..2cae4c672 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -31,8 +31,9 @@ namespace ast { class AstPrinter : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index fa1855ebe..0d47c9c6c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -37,7 +37,7 @@ namespace printer { namespace cvc { void CvcPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "NULL"; @@ -110,7 +110,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << "TYPE"; break; default: - Unhandled(tc); + out << tc; } break; case kind::BUILTIN: @@ -357,15 +357,16 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, return; } + // shouldn't ever happen (unless new metakinds are added) Unhandled(); -}/* CvcPrinter::toStream() */ +}/* CvcPrinter::toStream(TNode) */ template <class T> -static bool tryToStream(std::ostream& out, const Command* c); +static bool tryToStream(std::ostream& out, const Command* c) throw(); void CvcPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { expr::ExprSetDepth::Scope sdScope(out, toDepth); expr::ExprPrintTypes::Scope ptScope(out, types); @@ -398,23 +399,40 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, return; } - Unhandled("don't know how to print this command in CVC's presentation language: %s", c->toString().c_str()); + out << "ERROR: don't know how to print a Command of class: " + << typeid(*c).name() << endl; -}/* CvcPrinter::toStream() */ +}/* CvcPrinter::toStream(Command*) */ -static void toStream(std::ostream& out, const AssertCommand* c) { +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); + +void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { + + if(tryToStream<CommandSuccess>(out, s) || + tryToStream<CommandFailure>(out, s) || + tryToStream<CommandUnsupported>(out, s)) { + return; + } + + out << "ERROR: don't know how to print a CommandStatus of class: " + << typeid(*s).name() << endl; + +}/* CvcPrinter::toStream(CommandStatus*) */ + +static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "ASSERT " << c->getExpr() << ";"; } -static void toStream(std::ostream& out, const PushCommand* c) { +static void toStream(std::ostream& out, const PushCommand* c) throw() { out << "PUSH;"; } -static void toStream(std::ostream& out, const PopCommand* c) { +static void toStream(std::ostream& out, const PopCommand* c) throw() { out << "POP;"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) { +static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << "CHECKSAT " << e << ";"; @@ -423,7 +441,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { } } -static void toStream(std::ostream& out, const QueryCommand* c) { +static void toStream(std::ostream& out, const QueryCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << "QUERY " << e << ";"; @@ -432,11 +450,11 @@ static void toStream(std::ostream& out, const QueryCommand* c) { } } -static void toStream(std::ostream& out, const QuitCommand* c) { +static void toStream(std::ostream& out, const QuitCommand* c) throw() { //out << "EXIT;"; } -static void toStream(std::ostream& out, const CommandSequence* c) { +static void toStream(std::ostream& out, const CommandSequence* c) throw() { for(CommandSequence::const_iterator i = c->begin(); i != c->end(); ++i) { @@ -444,7 +462,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclarationSequence* c) { +static void toStream(std::ostream& out, const DeclarationSequence* c) throw() { DeclarationSequence::const_iterator i = c->begin(); for(;;) { DeclarationDefinitionCommand* dd = @@ -458,11 +476,11 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) { } } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { out << c->getSymbol() << " : " << c->getType() << ";"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -477,67 +495,69 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "): " << formula << ";"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) { +static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { if(c->getArity() > 0) { - Unhandled("Don't know how to print parameterized type declaration " - "in CVC language:\n%s", c->toString().c_str()); + out << "ERROR: Don't know how to print parameterized type declaration " + "in CVC language:" << endl << c->toString() << endl; + } else { + out << c->getSymbol() << " : TYPE;"; } - out << c->getSymbol() << " : TYPE;"; } -static void toStream(std::ostream& out, const DefineTypeCommand* c) { +static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { if(c->getParameters().size() > 0) { - Unhandled("Don't know how to print parameterized type definition " - "in CVC language:\n%s", c->toString().c_str()); + out << "ERROR: Don't know how to print parameterized type definition " + "in CVC language:" << endl << c->toString() << endl; + } else { + out << c->getSymbol() << " : TYPE = " << c->getType() << ";"; } - out << c->getSymbol() << " : TYPE = " << c->getType() << ";"; } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { toStream(out, static_cast<const DefineFunctionCommand*>(c)); } -static void toStream(std::ostream& out, const SimplifyCommand* c) { +static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { out << "TRANSFORM " << c->getTerm() << ";"; } -static void toStream(std::ostream& out, const GetValueCommand* c) { +static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "% (get-value " << c->getTerm() << ")"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) { +static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "% (get-assignment)"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) { +static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "% (get-assertions)"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "% (set-info :status " << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { out << "% (set-logic " << c->getLogic() << ")"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) { +static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) { +static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { out << "% (get-info " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) { +static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) { +static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "% (get-option " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); for(vector<DatatypeType>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); @@ -547,15 +567,15 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { } } -static void toStream(std::ostream& out, const CommentCommand* c) { +static void toStream(std::ostream& out, const CommentCommand* c) throw() { out << "% " << c->getComment(); } -static void toStream(std::ostream& out, const EmptyCommand* c) { +static void toStream(std::ostream& out, const EmptyCommand* c) throw() { } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) { +static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { toStream(out, dynamic_cast<const T*>(c)); return true; @@ -563,6 +583,29 @@ static bool tryToStream(std::ostream& out, const Command* c) { return false; } +static void toStream(std::ostream& out, const CommandSuccess* s) throw() { + if(Command::printsuccess::getPrintSuccess(out)) { + out << "OK" << endl; + } +} + +static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { + out << "UNSUPPORTED" << endl; +} + +static void toStream(std::ostream& out, const CommandFailure* s) throw() { + out << s->getMessage() << endl; +} + +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { + if(typeid(*s) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(s)); + return true; + } + return false; +} + }/* CVC4::printer::cvc namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index fd478dbe5..ba66145fc 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -31,8 +31,9 @@ namespace cvc { class CvcPrinter : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 6714d355e..e3b2ed796 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -29,25 +29,26 @@ namespace CVC4 { Printer* Printer::d_printers[language::output::LANG_MAX]; -Printer* Printer::makePrinter(OutputLanguage lang) { +Printer* Printer::makePrinter(OutputLanguage lang) throw() { using namespace CVC4::language::output; switch(lang) { case LANG_SMTLIB: - return new printer::smt::SmtPrinter; + return new printer::smt::SmtPrinter(); case LANG_SMTLIB_V2: - return new printer::smt2::Smt2Printer; + return new printer::smt2::Smt2Printer(); case LANG_CVC4: - return new printer::cvc::CvcPrinter; + return new printer::cvc::CvcPrinter(); case LANG_AST: - return new printer::ast::AstPrinter; + return new printer::ast::AstPrinter(); default: Unhandled(lang); } + }/* Printer::makePrinter() */ }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 7294ab231..9bcbba3b0 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -32,11 +32,19 @@ class Printer { static Printer* d_printers[language::output::LANG_MAX]; /** Make a Printer for a given OutputLanguage */ - static Printer* makePrinter(OutputLanguage lang); + static Printer* makePrinter(OutputLanguage lang) throw(); + + // disallow copy, assignment + Printer(const Printer&) CVC4_UNUSED; + Printer& operator=(const Printer&) CVC4_UNUSED; + +protected: + // derived classes can construct, but no one else. + Printer() throw() {} public: /** Get the Printer for a given OutputLanguage */ - static Printer* getPrinter(OutputLanguage lang) { + static Printer* getPrinter(OutputLanguage lang) throw() { if(d_printers[lang] == NULL) { d_printers[lang] = makePrinter(lang); } @@ -45,11 +53,15 @@ public: /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, TNode n, - int toDepth, bool types) const = 0; + int toDepth, bool types) const throw() = 0; /** Write a Command out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const = 0; + int toDepth, bool types) const throw() = 0; + + /** Write a CommandStatus out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0; + };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index ed7f8febf..2ac514988 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -34,15 +34,19 @@ namespace printer { namespace smt { void SmtPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ void SmtPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ +void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { + s->toStream(out, language::output::LANG_SMTLIB_V2); +} + }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 14d6c09e1..370e0908c 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -31,8 +31,9 @@ namespace smt { class SmtPrinter : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6741d5d2d..0f5fcd73b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -31,12 +31,12 @@ namespace CVC4 { namespace printer { namespace smt2 { -string smtKindString(Kind k); +static string smtKindString(Kind k) throw(); -void printBvParameterizedOp(std::ostream& out, TNode n); +static void printBvParameterizedOp(std::ostream& out, TNode n) throw(); void Smt2Printer::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; @@ -247,9 +247,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } } out << ')'; -}/* Smt2Printer::toStream() */ +}/* Smt2Printer::toStream(TNode) */ -string smtKindString(Kind k) { +static string smtKindString(Kind k) throw() { switch(k) { // builtin theory case kind::APPLY: break; @@ -330,7 +330,7 @@ string smtKindString(Kind k) { return kind::kindToString(k); } -void printBvParameterizedOp(std::ostream& out, TNode n) { +static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { out << "(_ "; switch(n.getKind()) { case kind::BITVECTOR_EXTRACT: { @@ -359,16 +359,16 @@ void printBvParameterizedOp(std::ostream& out, TNode n) { << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount; break; default: - Unhandled(n.getKind()); + out << n.getKind(); } out << ")"; } template <class T> -static bool tryToStream(std::ostream& out, const Command* c); +static bool tryToStream(std::ostream& out, const Command* c) throw(); void Smt2Printer::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { expr::ExprSetDepth::Scope sdScope(out, toDepth); expr::ExprPrintTypes::Scope ptScope(out, types); @@ -400,23 +400,40 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, return; } - Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str()); + out << "ERROR: don't know how to print a Command of class: " + << typeid(*c).name() << endl; -}/* Smt2Printer::toStream() */ +}/* Smt2Printer::toStream(Command*) */ -static void toStream(std::ostream& out, const AssertCommand* c) { +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); + +void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { + + if(tryToStream<CommandSuccess>(out, s) || + tryToStream<CommandFailure>(out, s) || + tryToStream<CommandUnsupported>(out, s)) { + return; + } + + out << "ERROR: don't know how to print a CommandStatus of class: " + << typeid(*s).name() << endl; + +}/* Smt2Printer::toStream(CommandStatus*) */ + +static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "(assert " << c->getExpr() << ")"; } -static void toStream(std::ostream& out, const PushCommand* c) { +static void toStream(std::ostream& out, const PushCommand* c) throw() { out << "(push 1)"; } -static void toStream(std::ostream& out, const PopCommand* c) { +static void toStream(std::ostream& out, const PopCommand* c) throw() { out << "(pop 1)"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) { +static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << PushCommand() << endl @@ -428,7 +445,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { } } -static void toStream(std::ostream& out, const QueryCommand* c) { +static void toStream(std::ostream& out, const QueryCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << PushCommand() << endl @@ -440,11 +457,11 @@ static void toStream(std::ostream& out, const QueryCommand* c) { } } -static void toStream(std::ostream& out, const QuitCommand* c) { +static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "(exit)"; } -static void toStream(std::ostream& out, const CommandSequence* c) { +static void toStream(std::ostream& out, const CommandSequence* c) throw() { for(CommandSequence::const_iterator i = c->begin(); i != c->end(); ++i) { @@ -452,7 +469,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { Type type = c->getType(); out << "(declare-fun " << c->getSymbol() << " ("; if(type.isFunction()) { @@ -469,7 +486,7 @@ static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { out << ") " << type << ")"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -487,11 +504,11 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) { +static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")"; } -static void toStream(std::ostream& out, const DefineTypeCommand* c) { +static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { const vector<Type>& params = c->getParameters(); out << "(define-sort " << c->getSymbol() << " ("; if(params.size() > 0) { @@ -502,55 +519,57 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) { out << ") " << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); out << " )"; - Unhandled("define named function command"); + + out << "ERROR: don't know how to output define-named-function command" << endl; } -static void toStream(std::ostream& out, const SimplifyCommand* c) { +static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { out << "Simplify( << " << c->getTerm() << " >> )"; - Unhandled("simplify command"); + + out << "ERROR: don't know how to output simplify command" << endl; } -static void toStream(std::ostream& out, const GetValueCommand* c) { +static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "(get-value " << c->getTerm() << ")"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) { +static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "(get-assignment)"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) { +static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "(get-assertions)"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "(set-info :status " << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { out << "(set-logic " << c->getLogic() << ")"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) { +static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) { +static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { out << "(get-info " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) { +static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) { +static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "(get-option " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); out << "DatatypeDeclarationCommand(["; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), @@ -560,18 +579,19 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { out << *i << ";" << endl; } out << "])"; - Unhandled("datatype declaration command"); + + out << "ERROR: don't know how to output datatype declaration command" << endl; } -static void toStream(std::ostream& out, const CommentCommand* c) { +static void toStream(std::ostream& out, const CommentCommand* c) throw() { out << "(set-info :notes \"" << c->getComment() << "\")"; } -static void toStream(std::ostream& out, const EmptyCommand* c) { +static void toStream(std::ostream& out, const EmptyCommand* c) throw() { } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) { +static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { toStream(out, dynamic_cast<const T*>(c)); return true; @@ -579,6 +599,35 @@ static bool tryToStream(std::ostream& out, const Command* c) { return false; } +static void toStream(std::ostream& out, const CommandSuccess* s) throw() { + if(Command::printsuccess::getPrintSuccess(out)) { + out << "success" << endl; + } +} + +static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { + out << "unsupported" << endl; +} + +static void toStream(std::ostream& out, const CommandFailure* s) throw() { + string message = s->getMessage(); + // escape all double-quotes + size_t pos; + while((pos = message.find('"')) != string::npos) { + message = message.replace(pos, 1, "\\\""); + } + out << "(error \"" << message << "\")" << endl; +} + +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { + if(typeid(*s) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(s)); + return true; + } + return false; +} + }/* CVC4::printer::smt2 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 2086370ae..a48104e45 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -31,8 +31,9 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ |