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

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 */