summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp106
-rw-r--r--src/printer/ast/ast_printer.h5
-rw-r--r--src/printer/cvc/cvc_printer.cpp123
-rw-r--r--src/printer/cvc/cvc_printer.h5
-rw-r--r--src/printer/printer.cpp11
-rw-r--r--src/printer/printer.h20
-rw-r--r--src/printer/smt/smt_printer.cpp8
-rw-r--r--src/printer/smt/smt_printer.h5
-rw-r--r--src/printer/smt2/smt2_printer.cpp129
-rw-r--r--src/printer/smt2/smt2_printer.h5
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback