* 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, 14 insertions, 12 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index aa63846cf..6b09fcc27 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -61,13 +61,13 @@ BUILT_SOURCES = \
 
 TOKENS_FILES = \
 	cvc_tokens.h \
-	smt_tokens.h \
+	smt1_tokens.h \
 	smt2_tokens.h \
 	tptp_tokens.h
 
 cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
-smt_tokens.h: @srcdir@/../parser/smt/Smt.g
+smt1_tokens.h: @srcdir@/../parser/smt1/Smt1.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
 smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 20b4c2bc2..a3086d96c 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -153,7 +153,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
+      } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
         opts.set(options::inputLanguage, language::input::LANG_TPTP);
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";
diff --git a/src/main/options b/src/main/options
index 58ea5e544..02c4643b3 100644
--- a/src/main/options
+++ b/src/main/options
@@ -20,7 +20,7 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl
  show all available tags for tracing
 
 expert-option earlyExit --early-exit bool :default true
- do not run destructors at exit; default on except in debug mode
+ do not run destructors at exit; default on except in debug builds
 
 # portfolio options
 option printWinner bool