SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

(this commit was certified error- and warning-free by the test-and-commit script.)

3 files changed, 168 insertions, 85 deletions

diff --git a/src/options/base_options b/src/options/base_options
index f7d1a77d4..cd1bec00a 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -40,19 +40,33 @@
 #                     | :read-write
 #                     | :link linked-options..
 #
-#   alias smt-option-name = (smt-option-name[=argument])+
-#   alias (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
+#   common-alias ALIAS_SPECIFICATION
+#   alias ALIAS_SPECIFICATION
+#   expert-alias ALIAS_SPECIFICATION
+#   undocumented-alias ALIAS_SPECIFICATION
 #
-#     The alias command creates a new SmtEngine option name, or short option, or long option,
-#     and binds it to act the same way as if the options to the right of "=" were passed.
-#     For example, if there are options to --disable-warning-1 and --disable-warning-2, etc.,
-#     a useful alias might be:
+#       ALIAS_SPECIFICATION ::=   (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
+#                               | (-short-option=ARG | --long-option=ARG) = (-option[=ARG|argument] | --long-option[=ARG|argument])+
+#
+#     The alias command creates a new short or long option, and binds it
+#     to act the same way as if the options to the right of "=" were passed.
+#     For example, if there are options to --disable-warning-1 and
+#     --disable-warning-2, etc., a useful alias might be:
 #
 #       alias --disable-all-warnings = --disable-warning-1 --disable-warning-2
 #
-#     Aliases cannot take arguments, and command-line aliases cannot set SmtEngine properties,
-#     and SmtEngine aliases cannot set command-line properties.  For these things, you need a
-#     custom handler.
+#     It's also possible to pass an argument through to another option.
+#     This alias makes "--output-language" synonymous with "--output-lang".
+#     Without the "=L" parts, --output-language would not take an argument,
+#     and option processing would fail (because --output-lang expects one).
+#
+#       alias --output-language=L = --output-lang=L
+#
+#     You can also ignore such an argument:
+#
+#       alias --some-option=VALUE = --other-option --option2=foo --option3=bar
+#
+#     or use it for multiple options on the right-hand side, etc.
 #
 #   warning message
 #
@@ -74,9 +88,14 @@ option err std::ostream* :default &std::cerr :include <iostream>
 common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write
  force input language (default is "auto"; see --lang help)
 common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write
- force input language (default is "auto"; see --lang help)
+ force output language (default is "auto"; see --output-lang help)
 option languageHelp bool
 
+# Allow also --language and --output-language, it's a common mistake to
+# type these, but no need to document it.
+undocumented-alias --language=L = --lang=L
+undocumented-alias --output-language=L = --output-lang=L
+
 option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_options_handlers.h"
  the verbosity level of CVC4
 common-option - -v --verbose void :handler CVC4::options::increaseVerbosity
@@ -86,6 +105,8 @@ common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity
 
 common-option statistics statistics --stats bool
  give statistics on exit
+undocumented-alias --statistics = --stats
+undocumented-alias --no-statistics = --no-stats
 
 common-option parseOnly parse-only --parse-only bool :read-write
  exit after parsing input
@@ -104,7 +125,7 @@ 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
+alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
  SMT-LIBv2 compliance mode (implies other options)
 
 endmodule
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 93885d75f..9e5fb2b81 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -543,7 +543,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], true, NULL);$run_links
+      assignBool(options::$internal, option, true, NULL);$run_links
       break;
 "
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -552,12 +552,12 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-  $handler(option, optarg, smt);"
+  $handler(option, optionarg, smt);"
         done
       else
         run_handlers="
 #line $lineno \"$kf\"
-  handleOption<$type>(option, optarg);"
+  handleOption<$type>(option, optionarg);"
       fi
       if [ -n "$predicates" ]; then
         for predicate in $predicates; do
@@ -568,7 +568,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
       fi
       all_custom_handlers="${all_custom_handlers}
 #line $lineno \"$kf\"
-template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optarg, SmtEngine* smt) {
+template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optionarg, SmtEngine* smt) {
 #line $lineno \"$kf\"
   options::${internal}__option_t::type retval = $run_handlers
 #line $lineno \"$kf\"
@@ -576,7 +576,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 }"
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assign(options::$internal, argv[old_optind == 0 ? 1 : old_optind], optarg, NULL);$run_links
+      assign(options::$internal, option, optionarg, NULL);$run_links
       break;
 "
     elif [ -n "$expect_arg" ]; then
@@ -589,7 +589,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-      $handler(argv[old_optind == 0 ? 1 : old_optind], optarg, smt);"
+      $handler(option, optionarg, smt);"
         done
       fi
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
@@ -607,7 +607,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-      $handler(argv[old_optind == 0 ? 1 : old_optind], smt);"
+      $handler(option, smt);"
         done
       fi
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
@@ -621,7 +621,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], false, NULL);$run_links_alternate
+      assignBool(options::$internal, option, false, NULL);$run_links_alternate
       break;
 "
     else
@@ -646,7 +646,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assignBool(options::$internal, \"$smtname\", optarg == \"true\", smt);$run_links
+    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links
     return;
   }"
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -655,7 +655,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", optarg, smt);
+    $handler(\"$smtname\", optionarg, smt);
 "
         done
       fi
@@ -663,7 +663,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assign(options::$internal, \"$smtname\", optarg, smt);$run_links
+    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links
     return;
   }"
     elif [ -n "$expect_arg" ]; then
@@ -671,7 +671,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       for handler in $handlers; do
         run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", optarg, smt);
+    $handler(\"$smtname\", optionarg, smt);
 "
       done
       smt_setoption_handlers="${smt_setoption_handlers}
@@ -727,12 +727,34 @@ template <> void Options::assign(options::${internal}__option_t, std::string opt
   fi
 }
 
+function common-alias {
+  # common-alias -option[=arg] = (-option[=arg])+
+  handle_alias COMMON "$@"
+}
+
 function alias {
-  # alias (smtname | -option) = (smtname [arg] | -option [arg])+
+  # alias -option[=arg] = (-option[=arg])+
+  handle_alias STANDARD "$@"
+}
+
+function expert-alias {
+  # expert-alias -option[=arg] = (-option[=arg])+
+  handle_alias EXPERT "$@"
+}
+
+function undocumented-alias {
+  # undocumented-alias -option[=arg] = (-option[=arg])+
+  handle_alias UNDOCUMENTED "$@"
+}
+
+function handle_alias {
+  # handle_alias CATEGORY -option[=arg] = (-option[=arg])+
   check_module_seen
   check_doc
 
-  category=STANDARD
+  category="$1"
+  shift
+
   internal=-
   smtname=
   short_option=
@@ -752,16 +774,24 @@ function alias {
   options_already_documented=false
   alternate_options_already_documented=false
 
+  if [ "$category" = UNDOCUMENTED ]; then
+    expect_doc=false
+  else
+    expect_doc=true
+  fi
+  expect_doc_alternate=false
+
   if [ $# -lt 3 ]; then
     echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
     exit 1
   fi
-  options=
-  while [ $# -gt 0 -a "$1" != = ]; do
-    options="$options $1"
-    shift
-  done
-  if [ $# -eq 0 ]; then
+  if [ "$1" = '=' ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2
+    exit 1
+  fi
+  option="$1"
+  shift
+  if [ "$1" != '=' ]; then
     echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
     exit 1
   fi
@@ -771,42 +801,76 @@ function alias {
     exit 1
   fi
   cases=
-  for option in $options; do
-    if ! expr "$option" : - &>/dev/null; then
-      echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
-      exit 1
-    fi
-    if expr "$option" : -- &>/dev/null; then
+  if ! expr "$option" : - &>/dev/null; then
+    echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
+    exit 1
+  fi
+  if expr "$option" : -- &>/dev/null; then
+    if expr "$option" : '.*=' &>/dev/null; then
+      expect_arg_long=required_argument
+      arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
+      option="$(echo "$option" | sed 's,--,,;s,=.*,,')"
+      echo "warning: not yet handling long-option alias =$arg" >&2
+    else
+      expect_arg_long=no_argument
+      arg=
       option="$(echo "$option" | sed 's,--,,')"
-      all_modules_long_options="${all_modules_long_options}
-  { \"$(echo "$option" | sed 's,=.*,,')\", no_argument, NULL, $n_long },"
+    fi
+    all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
       cases="${cases}
     case $n_long:// --$option"
-      let ++n_long
-      long_option="${long_option:+$long_option | --}$option"
-    else
-      if ! expr "$option" : '-.$' &>/dev/null; then
+    let ++n_long
+    long_option="${long_option:+$long_option | --}$option"
+  else
+    if ! expr "$option" : '-.$' &>/dev/null; then
+      if ! expr "$option" : '-.=' &>/dev/null; then
         echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
         exit 1
       fi
+      expect_arg=:
+      arg="$(echo "$option" | sed 's,[^=]*=,,')"
+      option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')"
+      echo "warning: not yet handling short-option alias =$arg" >&2
+    else
+      expect_arg=
+      arg=
       option="$(echo "$option" | sed 's,-,,')"
-      all_modules_short_options="${all_modules_short_options}$option"
+    fi
+    all_modules_short_options="${all_modules_short_options}$option$expect_arg"
       cases="${cases}
     case '$option':"
-      short_option="${short_option:+$short_option | -}$option"
-    fi
-  done
+    short_option="${short_option:+$short_option | -}$option"
+  fi
+
   while [ $# -gt 0 ]; do
+    linkopt="$1"
+    # on the RHS, we're looking for =ARG, where "ARG" is *exactly* what
+    # was given on the LHS
+    if expr "$linkopt" : '.*=' &>/dev/null; then
+      linkarg="$(echo "$linkopt" | sed 's,[^=]*=,,')"
+      if [ "$linkarg" = "$arg" ]; then
+        # we found =ARG
+        linkopt="$(echo "$linkopt" | sed 's,=.*,,')"
+      else
+        # false positive: =SOMETHING, where SOMETHING != ARG
+        linkarg=
+      fi
+    fi
     links="$links
 #line $lineno \"$kf\"
-      preemptGetopt(extra_argc, extra_argv, \"$1\");"
+      preemptGetopt(extra_argc, extra_argv, \"$linkopt\");"
+    if [ "$linkarg" ]; then
+      # include also the arg
+      links="$links
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, optionarg.c_str());"
+    fi
     shift
   done
   all_modules_option_handlers="$all_modules_option_handlers$cases$links
       break;
 "
-  expect_doc=true
-  expect_doc_alternate=false
 }
 
 function warning {
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index bae0ef169..dd8a7af57 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -67,15 +67,15 @@ CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
  */
 template <class T, bool is_numeric, bool is_integer>
 struct OptionHandler {
-  static T handle(std::string option, std::string optarg);
+  static T handle(std::string option, std::string optionarg);
 };/* struct OptionHandler<> */
 
 /** Variant for integral C++ types */
 template <class T>
 struct OptionHandler<T, true, true> {
-  static T handle(std::string option, std::string optarg) {
+  static T handle(std::string option, std::string optionarg) {
     try {
-      Integer i(optarg, 10);
+      Integer i(optionarg, 10);
 
       if(! std::numeric_limits<T>::is_signed && i < 0) {
         // unsigned type but user gave negative argument
@@ -107,8 +107,8 @@ struct OptionHandler<T, true, true> {
 /** Variant for numeric but non-integral C++ types */
 template <class T>
 struct OptionHandler<T, true, false> {
-  static T handle(std::string option, std::string optarg) {
-    std::stringstream in(optarg);
+  static T handle(std::string option, std::string optionarg) {
+    std::stringstream in(optionarg);
     long double r;
     in >> r;
     if(! in.eof()) {
@@ -138,7 +138,7 @@ struct OptionHandler<T, true, false> {
 /** Variant for non-numeric C++ types */
 template <class T>
 struct OptionHandler<T, false, false> {
-  static T handle(std::string option, std::string optarg) {
+  static T handle(std::string option, std::string optionarg) {
     T::unsupported_handleOption_call___please_write_me;
     // The above line causes a compiler error if this version of the template
     // is ever instantiated (meaning that a specialization is missing).  So
@@ -151,14 +151,14 @@ struct OptionHandler<T, false, false> {
 
 /** Handle an option of type T in the default way. */
 template <class T>
-T handleOption(std::string option, std::string optarg) {
-  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optarg);
+T handleOption(std::string option, std::string optionarg) {
+  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
 }
 
 /** Handle an option of type std::string in the default way. */
 template <>
-std::string handleOption<std::string>(std::string option, std::string optarg) {
-  return optarg;
+std::string handleOption<std::string>(std::string option, std::string optionarg) {
+  return optionarg;
 }
 
 /**
@@ -166,12 +166,12 @@ std::string handleOption<std::string>(std::string option, std::string optarg) {
  * If a user specifies a :handler or :predicates, it overrides this.
  */
 template <class T>
-typename T::type runHandlerAndPredicates(T, std::string option, std::string optarg, SmtEngine* smt) {
+typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, SmtEngine* smt) {
   // By default, parse the option argument in a way appropriate for its type.
   // E.g., for "unsigned int" options, ensure that the provided argument is
   // a nonnegative integer that fits in the unsigned int type.
 
-  return handleOption<typename T::type>(option, optarg);
+  return handleOption<typename T::type>(option, optionarg);
 }
 
 template <class T>
@@ -384,6 +384,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
   for(;;) {
     int c = -1;
     optopt = 0;
+    std::string option, optionarg;
     Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl;
     if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
 #if HAVE_DECL_OPTRESET
@@ -400,6 +401,16 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
                       "+:${all_modules_short_options}",
                       cmdlineOptions, NULL);
       Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl;
+      if(optopt == 0 ||
+         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
+        // long option
+        option = argv[old_optind == 0 ? 1 : old_optind];
+        optionarg = (optarg == NULL) ? "" : optarg;
+      } else {
+        // short option
+        option = std::string("-") + char(optopt);
+        optionarg = (optarg == NULL) ? "" : optarg;
+      }
       if(optind >= extra_argc) {
         Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
         unsigned i = 1;
@@ -435,31 +446,25 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
                       cmdlineOptions, NULL);
       main_optind = optind;
       Debug("options") << "[ next option will be at pos: " << optind << " ]" << std::endl;
-      if(optind < argc) Debug("options") << "next is option: " << argv[optind] << std::endl;
       if(c == -1) {
         Debug("options") << "done with option parsing" << std::endl;
         break;
       }
+      option = argv[old_optind == 0 ? 1 : old_optind];
+      optionarg = (optarg == NULL) ? "" : optarg;
     }
 
-    Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "')" << std::endl;
+    Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl;
 
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 451 "${template}"
+#line 463 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
       // name of it is different.
-      if(optopt == 0 ||
-         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
-        // was a long option
-        throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
-      } else {
-        // was a short option
-        throw OptionException(std::string("option `-") + char(optopt) + "' missing its required argument");
-      }
+      throw OptionException(std::string("option `") + option + "' missing its required argument");
 
     case '?':
     default:
@@ -467,13 +472,13 @@ ${all_modules_option_handlers}
           !strncmp(argv[optind - 1], "--thread", 8) &&
           strlen(argv[optind - 1]) > 8 ) {
         if(! isdigit(argv[optind - 1][8])) {
-          throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
+          throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
         }
         std::vector<std::string>& threadArgv = d_holder->threadArgv;
         char *end;
         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
         if(tnum < 0 || (*end != '\0' && *end != '=')) {
-          throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
+          throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
         }
         if(threadArgv.size() <= size_t(tnum)) {
           threadArgv.resize(tnum + 1);
@@ -483,13 +488,13 @@ ${all_modules_option_handlers}
         }
         if(*end == '\0') { // e.g., we have --thread0 "foo"
           if(argc <= optind) {
-            throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
+            throw OptionException(std::string("option `") + option + "' missing its required argument");
           }
           Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl;
           threadArgv[tnum] += argv[(*optind_ref)++];
         } else { // e.g., we have --thread0="foo"
           if(end[1] == '\0') {
-            throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
+            throw OptionException(std::string("option `") + option + "' missing its required argument");
           }
           Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl;
           threadArgv[tnum] += end + 1;
@@ -498,14 +503,7 @@ ${all_modules_option_handlers}
         break;
       }
 
-      // This can be a long or short option, and the way to get at the name of it is different.
-      if(optopt == 0 ||
-         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
-        // was a long option
-        throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'");
-      } else { // was a short option
-        throw OptionException(std::string("can't understand option `-") + char(optopt) + "'");
-      }
+      throw OptionException(std::string("can't understand option `") + option + "'");
     }
   }