* 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.)

2 files changed, 0 insertions, 108 deletions

diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
deleted file mode 100644
index bc61368c1..000000000
--- a/src/printer/smt/smt_printer.cpp
+++ /dev/null
@@ -1,61 +0,0 @@
-/*********************                                                        */
-/*! \file smt_printer.cpp
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-
-#include "printer/smt/smt_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager.h" // for VarNameAttr
-#include "expr/command.h"
-
-#include <iostream>
-#include <vector>
-#include <string>
-#include <typeinfo>
-
-using namespace std;
-
-namespace CVC4 {
-namespace printer {
-namespace smt {
-
-void SmtPrinter::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() */
-
-void SmtPrinter::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() */
-
-void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
-  s->toStream(out, language::output::LANG_SMTLIB_V2);
-}/* SmtPrinter::toStream() */
-
-void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
-}/* SmtPrinter::toStream() */
-
-void SmtPrinter::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 namespace */
-}/* CVC4 namespace */
-
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
deleted file mode 100644
index a3d62a287..000000000
--- a/src/printer/smt/smt_printer.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*********************                                                        */
-/*! \file smt_printer.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PRINTER__SMT_PRINTER_H
-#define __CVC4__PRINTER__SMT_PRINTER_H
-
-#include <iostream>
-
-#include "printer/printer.h"
-
-namespace CVC4 {
-namespace printer {
-namespace smt {
-
-class SmtPrinter : 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();
-  void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  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 */
-
-}/* CVC4::printer::smt namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__SMT_PRINTER_H */
-