diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
commit | ad0a71e2782bc291ba9f808d24df2e1d8ca1b41e (patch) | |
tree | 744a9ae0f10f6dd8837d7e0dcd8bd2b25d34e481 /src/printer | |
parent | 51daaee8eb1ee55ee3323c5395a95fd121fe87a8 (diff) |
* Rename SMT parts (printer, parser) to SMT1
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
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 */ |