* 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, 82 insertions, 26 deletions

diff --git a/src/options/base_options b/src/options/base_options
index cd1bec00a..91b6354d1 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -125,7 +125,8 @@ option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag
 option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
  print the "success" output required of SMT-LIBv2
 
-alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
+alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
  SMT-LIBv2 compliance mode (implies other options)
+undocumented-alias --smtlib2 = --smtlib
 
 endmodule
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index f29e98a9b..83bcfdf32 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -71,11 +71,16 @@ inline void decreaseVerbosity(std::string option, SmtEngine* smt) {
 }
 
 inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") {
+  if(optarg == "cvc4" || optarg == "pl" ||
+     optarg == "presentation" || optarg == "native" ||
+     optarg == "LANG_CVC4") {
     return language::output::LANG_CVC4;
-  } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") {
-    return language::output::LANG_SMTLIB;
-  } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") {
+  } else if(optarg == "smtlib1" || optarg == "smt1" ||
+            optarg == "LANG_SMTLIB_V1") {
+    return language::output::LANG_SMTLIB_V1;
+  } else if(optarg == "smtlib" || optarg == "smt" ||
+            optarg == "smtlib2" || optarg == "smt2" ||
+            optarg == "LANG_SMTLIB_V2") {
     return language::output::LANG_SMTLIB_V2;
   } else if(optarg == "tptp" || optarg == "LANG_TPTP") {
     return language::output::LANG_TPTP;
@@ -86,8 +91,8 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt
   }
 
   if(optarg != "help") {
-    throw OptionException(std::string("unknown language for ") + option + ": `" +
-                          optarg + "'.  Try --output-lang help.");
+    throw OptionException(std::string("unknown language for ") + option +
+                          ": `" + optarg + "'.  Try --output-lang help.");
   }
 
   options::languageHelp.set(true);
@@ -95,11 +100,16 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt
 }
 
 inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") {
+  if(optarg == "cvc4" || optarg == "pl" ||
+     optarg == "presentation" || optarg == "native" ||
+     optarg == "LANG_CVC4") {
     return language::input::LANG_CVC4;
-  } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") {
-    return language::input::LANG_SMTLIB;
-  } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") {
+  } else if(optarg == "smtlib1" || optarg == "smt1" ||
+            optarg == "LANG_SMTLIB_V1") {
+    return language::input::LANG_SMTLIB_V1;
+  } else if(optarg == "smtlib" || optarg == "smt" ||
+            optarg == "smtlib2" || optarg == "smt2" ||
+            optarg == "LANG_SMTLIB_V2") {
     return language::input::LANG_SMTLIB_V2;
   } else if(optarg == "tptp" || optarg == "LANG_TPTP") {
     return language::input::LANG_TPTP;
@@ -108,8 +118,8 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar
   }
 
   if(optarg != "help") {
-    throw OptionException(std::string("unknown language for ") + option + ": `" +
-                          optarg + "'.  Try --lang help.");
+    throw OptionException(std::string("unknown language for ") + option +
+                          ": `" + optarg + "'.  Try --lang help.");
   }
 
   options::languageHelp.set(true);
diff --git a/src/options/mkoptions b/src/options/mkoptions
index cc581e69c..f023686ad 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -112,6 +112,7 @@ function module {
 
   seen_module=true
   if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then
+    echo >&2
     echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2
     exit 1
   fi
@@ -144,6 +145,7 @@ function endmodule {
   check_doc
   seen_endmodule=true
   if [ $# -ne 0 ]; then
+    echo >&2
     echo "$kf:$lineno: error: endmodule takes no arguments" >&2
     exit 1
   fi
@@ -223,12 +225,14 @@ function handle_option {
     while [ $i -lt $type_pos ]; do
       if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
         if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo >&2
           echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
           exit 1
         fi
         long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
         if [ -n "$long_option" ]; then
           if ! expr "$long_option" : '--.' &>/dev/null; then
+            echo >&2
             echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2
             exit 1
           fi
@@ -239,6 +243,7 @@ function handle_option {
           long_option_alternate_set=set
           if [ -n "$long_option_alternate" ]; then
             if ! expr "$long_option_alternate" : '--.' &>/dev/null; then
+              echo >&2
               echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2
               exit 1
             fi
@@ -247,12 +252,14 @@ function handle_option {
         fi
       elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
         if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo >&2
           echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
           exit 1
         fi
         short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
         if [ -n "$short_option" ]; then
           if ! expr "$short_option" : '-.$' &>/dev/null; then
+            echo >&2
             echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2
             exit 1
           fi
@@ -262,6 +269,7 @@ function handle_option {
           short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
           if expr "$short_option_alternate" : - &>/dev/null; then
             if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then
+              echo >&2
               echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2
               exit 1
             fi
@@ -270,6 +278,7 @@ function handle_option {
         fi
       else
         if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo >&2
           echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
           exit 1
         fi
@@ -280,9 +289,11 @@ function handle_option {
   fi
 
   if [ "$type" = void -a "$internal" != - ]; then
+    echo >&2
     echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2
     exit 1
   elif [ "$type" != void -a "$internal" = - ]; then
+    echo >&2
     echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2
     exit 1
   fi
@@ -296,9 +307,11 @@ function handle_option {
     long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')"
   fi
   if [ "$type" != bool -a -n "$short_option_alternate" ]; then
+    echo >&2
     echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2
     exit 1
   elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
+    echo >&2
     echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2
     exit 1
   fi
@@ -306,6 +319,7 @@ function handle_option {
   # check for duplicates
   if [ "$internal" != - ]; then
     if echo " $all_declared_internal_options " | grep -q " $internal "; then
+      echo >&2
       echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2
       exit 1
     fi
@@ -313,6 +327,7 @@ function handle_option {
   fi
   if [ -n "$long_option" ]; then
     if echo " $all_declared_long_options " | grep -q " $long_option "; then
+      echo >&2
       echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2
       exit 1
     fi
@@ -320,6 +335,7 @@ function handle_option {
   fi
   if [ -n "$long_option_alternate" ]; then
     if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then
+      echo >&2
       echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2
       exit 1
     fi
@@ -327,6 +343,7 @@ function handle_option {
   fi
   if [ -n "$short_option" ]; then
     if echo " $all_declared_short_options " | grep -q " $short_option "; then
+      echo >&2
       echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2
       exit 1
     fi
@@ -334,6 +351,7 @@ function handle_option {
   fi
   if [ -n "$short_option_alternate" ]; then
     if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then
+      echo >&2
       echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2
       exit 1
     fi
@@ -341,6 +359,7 @@ function handle_option {
   fi
   if [ -n "$smtname" ]; then
     if echo " $all_declared_smt_options " | grep -q " $smtname "; then
+      echo >&2
       echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2
       exit 1
     fi
@@ -359,6 +378,7 @@ function handle_option {
     :handler)
        let ++i
        if [ -n "$handlers" ]; then
+         echo >&2
          echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2
          exit 1
        fi
@@ -406,6 +426,7 @@ function handle_option {
        readOnly=true
        ;;
     *)
+       echo >&2
        echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2
        exit 1
     esac
@@ -529,6 +550,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
   if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
     run_handlers=
     if [ -n "$handlers" ]; then
+      echo >&2
       echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2
       exit 1
     fi
@@ -590,6 +612,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     elif [ -n "$expect_arg" ]; then
       run_handlers=
       if [ -n "$predicates" ]; then
+        echo >&2
         echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
         exit 1
       fi
@@ -608,6 +631,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     else
       run_handlers=
       if [ -n "$predicates" ]; then
+        echo >&2
         echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
         exit 1
       fi
@@ -633,6 +657,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       break;
 "
     else
+      echo >&2
       echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2
       exit 1
     fi
@@ -790,26 +815,31 @@ function handle_alias {
   expect_doc_alternate=false
 
   if [ $# -lt 3 ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
     exit 1
   fi
   if [ "$1" = '=' ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2
     exit 1
   fi
   option="$1"
   shift
   if [ "$1" != '=' ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
     exit 1
   fi
   shift
   if [ $# -eq 0 ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
     exit 1
   fi
   cases=
   if ! expr "$option" : - &>/dev/null; then
+    echo >&2
     echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
     exit 1
   fi
@@ -832,6 +862,7 @@ function handle_alias {
   else
     if ! expr "$option" : '-.$' &>/dev/null; then
       if ! expr "$option" : '-.=' &>/dev/null; then
+        echo >&2
         echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
         exit 1
       fi
@@ -884,6 +915,7 @@ function warning {
   check_module_seen
   check_doc
 
+  echo >&2
   echo "$kf:$lineno: warning: $@" >&2
 }
 
@@ -1016,11 +1048,13 @@ function doc-alternate {
   expect_doc_alternate=false
 
   if $expect_doc; then
+    echo >&2
     echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2
     exit 1
   fi
 
   if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
+    echo >&2
     echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2
     exit 1
   fi
@@ -1100,18 +1134,23 @@ $@"
 function check_doc {
   if $expect_doc; then
     if [ "$internal" != - ]; then
+      echo >&2
       echo "$kf:$lineno: warning: $internal is lacking documentation" >&2
     elif [ -n "$long_option" ]; then
+      echo >&2
       echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2
     elif [ -n "$short_option" ]; then
+      echo >&2
       echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2
     elif [ -n "$smtname" ]; then
+      echo >&2
       echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2
     fi
     expect_doc=false
   fi
 
   if $expect_doc_alternate; then
+    echo >&2
     echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2
     expect_doc_alternate=false
   fi
@@ -1119,10 +1158,12 @@ function check_doc {
 
 function check_module_seen {
   if $seen_endmodule; then
+    echo >&2
     echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2
     exit 1
   fi
   if ! $seen_module; then
+    echo >&2
     echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2
     exit 1
   fi
@@ -1235,7 +1276,7 @@ EOF
     rm -f "$output.tmp"
   else
     mv -f "$output.tmp" "$output"
-    printf "\rregenerated %-60s\n" "$output"
+    printf "\rregenerated %-68s\n" "$output"
   fi
 }
 
@@ -1272,6 +1313,7 @@ while [ $# -gt 0 ]; do
     elif expr "$line" : '\.[ 	]*$' &>/dev/null; then
       doc ""
     elif expr "$line" : '\.' &>/dev/null; then
+      echo >&2
       echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2
       exit 1
     elif expr "$line" : '/.*' &>/dev/null; then
@@ -1279,16 +1321,19 @@ while [ $# -gt 0 ]; do
     else
       line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
       if ! eval "$line"; then
+        echo >&2
         echo "$kf:$lineno: error was due to evaluation of this line" >&2
         exit 1
       fi
     fi
   done < "$kf"
   if ! $seen_module; then
+    echo >&2
     echo "$kf: error: no module content found in file!" >&2
     exit 1
   fi
   if ! $seen_endmodule; then
+    echo >&2
     echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2
     exit 1
   fi
@@ -1412,7 +1457,7 @@ cat "$output.working"
 
 rm -f "$output.working"
 rm -f "$output.sed"
-diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-60s\n" "$output")
+diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-68s\n" "$output")
 rm -f "$output.tmp"
 progress "$output" $count $total
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index dd8a7af57..63ab085b1 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -233,19 +233,19 @@ static const std::string optionsFootnote = "\n\
 
 static const std::string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
-  auto           attempt to automatically determine the input language\n\
-  pl | cvc4      CVC4 presentation language\n\
-  smt | smtlib   SMT-LIB format 1.2\n\
-  smt2 | smtlib2 SMT-LIB format 2.0\n\
-  tptp           TPTP format (cnf and fof)\n\
+  auto                           attempt to automatically determine language\n\
+  cvc4 | presentation | pl       CVC4 presentation language\n\
+  smt1 | smtlib1                 SMT-LIB format 1.2\n\
+  smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
+  tptp                           TPTP format (cnf and fof)\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
-  auto           match the output language to the input language\n\
-  pl | cvc4      CVC4 presentation language\n\
-  smt | smtlib   SMT-LIB format 1.2\n\
-  smt2 | smtlib2 SMT-LIB format 2.0\n\
-  tptp           TPTP format\n\
-  ast            internal format (simple syntax-tree language)\n\
+  auto                           match output language to input language\n\
+  cvc4 | presentation | pl       CVC4 presentation language\n\
+  smt1 | smtlib1                 SMT-LIB format 1.2\n\
+  smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
+  tptp                           TPTP format\n\
+  ast                            internal format (simple syntax trees)\n\
 ";
 
 std::string Options::getDescription() const {