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

1 files changed, 8 insertions, 8 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b0934c0ee..719c8f61d 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009-2012  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
@@ -64,9 +64,9 @@ static const std::string cvc_commands[] = {
 #include "main/cvc_tokens.h"
 };/* cvc_commands */
 
-static const std::string smt_commands[] = {
-#include "main/smt_tokens.h"
-};/* smt_commands */
+static const std::string smt1_commands[] = {
+#include "main/smt1_tokens.h"
+};/* smt1_commands */
 
 static const std::string smt2_commands[] = {
 #include "main/smt2_tokens.h"
@@ -105,10 +105,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = cvc_commands;
       commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
       break;
-    case output::LANG_SMTLIB:
-      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib";
-      commandsBegin = smt_commands;
-      commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands);
+    case output::LANG_SMTLIB_V1:
+      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1";
+      commandsBegin = smt1_commands;
+      commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
     case output::LANG_SMTLIB_V2:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";