diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/Makefile.am | 4 | ||||
-rw-r--r-- | src/printer/printer.cpp | 6 | ||||
-rw-r--r-- | src/printer/smt1/smt1_printer.cpp (renamed from src/printer/smt/smt_printer.cpp) | 30 | ||||
-rw-r--r-- | src/printer/smt1/smt1_printer.h (renamed from src/printer/smt/smt_printer.h) | 16 |
4 files changed, 28 insertions, 28 deletions
diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am index 7a6ef1158..bb94d75de 100644 --- a/src/printer/Makefile.am +++ b/src/printer/Makefile.am @@ -12,8 +12,8 @@ libprinter_la_SOURCES = \ dagification_visitor.cpp \ ast/ast_printer.h \ ast/ast_printer.cpp \ - smt/smt_printer.h \ - smt/smt_printer.cpp \ + smt1/smt1_printer.h \ + smt1/smt1_printer.cpp \ smt2/smt2_printer.h \ smt2/smt2_printer.cpp \ cvc/cvc_printer.h \ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 222a22e34..f20ab2901 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -20,7 +20,7 @@ #include "util/language.h" -#include "printer/smt/smt_printer.h" +#include "printer/smt1/smt1_printer.h" #include "printer/smt2/smt2_printer.h" #include "printer/cvc/cvc_printer.h" #include "printer/ast/ast_printer.h" @@ -37,8 +37,8 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { using namespace CVC4::language::output; switch(lang) { - case LANG_SMTLIB: - return new printer::smt::SmtPrinter(); + case LANG_SMTLIB_V1: + return new printer::smt1::Smt1Printer(); case LANG_SMTLIB_V2: return new printer::smt2::Smt2Printer(); diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt1/smt1_printer.cpp index bc61368c1..553692dc5 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt1/smt1_printer.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_printer.cpp +/*! \file smt1_printer.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -16,7 +16,7 @@ ** The pretty-printer interface for the SMT output language. **/ -#include "printer/smt/smt_printer.h" +#include "printer/smt1/smt1_printer.h" #include "expr/expr.h" // for ExprSetDepth etc.. #include "util/language.h" // for LANG_AST #include "expr/node_manager.h" // for VarNameAttr @@ -31,31 +31,31 @@ using namespace std; namespace CVC4 { namespace printer { -namespace smt { +namespace smt1 { -void SmtPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types, size_t dag) const throw() { +void Smt1Printer::toStream(std::ostream& out, TNode n, + int toDepth, bool types, size_t dag) const throw() { n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types, size_t dag) const throw() { +void Smt1Printer::toStream(std::ostream& out, const Command* c, + int toDepth, bool types, size_t dag) const throw() { c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { +void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { s->toStream(out, language::output::LANG_SMTLIB_V2); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { +void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { +void Smt1Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c); } -}/* CVC4::printer::smt namespace */ +}/* CVC4::printer::smt1 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt1/smt1_printer.h index a3d62a287..d1b36208c 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt1/smt1_printer.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_printer.h +/*! \file smt1_printer.h ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PRINTER__SMT_PRINTER_H -#define __CVC4__PRINTER__SMT_PRINTER_H +#ifndef __CVC4__PRINTER__SMT1_PRINTER_H +#define __CVC4__PRINTER__SMT1_PRINTER_H #include <iostream> @@ -27,9 +27,9 @@ namespace CVC4 { namespace printer { -namespace smt { +namespace smt1 { -class SmtPrinter : public CVC4::Printer { +class Smt1Printer : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); @@ -37,11 +37,11 @@ public: void toStream(std::ostream& out, const SExpr& sexpr) const throw(); //for models void toStream(std::ostream& out, Model* m, const Command* c) const throw(); -};/* class SmtPrinter */ +};/* class Smt1Printer */ -}/* CVC4::printer::smt namespace */ +}/* CVC4::printer::smt1 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PRINTER__SMT_PRINTER_H */ +#endif /* __CVC4__PRINTER__SMT1_PRINTER_H */ |