Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.

5 files changed, 154 insertions, 60 deletions

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index f89fca922..1eb3fdac4 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -176,6 +176,7 @@ options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options
 		@srcdir@/options_template.cpp @builddir@/options.cpp \
 		@srcdir@/../smt/smt_options_template.cpp @builddir@/../smt/smt_options.cpp \
 		@top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \
+		@top_builddir@/doc/libcvc4.3_template @top_builddir@/doc/libcvc4.3 \
 		-t \
 		@srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \
 		$(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(patsubst %/,%,$(dir $(o)))") \
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 6cb74c637..76ba9e295 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -127,6 +127,7 @@ class comparator {
   bool d_hasLbound;
 
 public:
+  comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
   comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
   comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
 
@@ -142,26 +143,31 @@ public:
 };/* class comparator */
 
 struct greater : public comparator<std::greater> {
+  greater(int i) throw() : comparator<std::greater>(i) {}
   greater(long l) throw() : comparator<std::greater>(l) {}
   greater(double d) throw() : comparator<std::greater>(d) {}
 };/* struct greater */
 
 struct greater_equal : public comparator<std::greater_equal> {
+  greater_equal(int i) throw() : comparator<std::greater_equal>(i) {}
   greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
   greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
 };/* struct greater_equal */
 
 struct less : public comparator<std::less> {
+  less(int i) throw() : comparator<std::less>(i) {}
   less(long l) throw() : comparator<std::less>(l) {}
   less(double d) throw() : comparator<std::less>(d) {}
 };/* struct less */
 
 struct less_equal : public comparator<std::less_equal> {
+  less_equal(int i) throw() : comparator<std::less_equal>(i) {}
   less_equal(long l) throw() : comparator<std::less_equal>(l) {}
   less_equal(double d) throw() : comparator<std::less_equal>(d) {}
 };/* struct less_equal */
 
 struct not_equal : public comparator<std::not_equal_to> {
+  not_equal(int i) throw() : comparator<std::not_equal_to>(i) {}
   not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
   not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
 };/* struct not_equal_to */
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2c514293b..73a2b94a3 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -62,6 +62,8 @@ common_documentation=
 remaining_documentation=
 common_manpage_documentation=
 remaining_manpage_documentation=
+common_manpage_smt_documentation=
+remaining_manpage_smt_documentation=
 
 seen_module=false
 seen_endmodule=false
@@ -122,6 +124,10 @@ function module {
   remaining_manpage_documentation="${remaining_manpage_documentation}
 .SH `echo "$module_name" | tr a-z A-Z` OPTIONS
 "
+  remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
+.TP
+.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
+"
 }
 
 function endmodule {
@@ -831,73 +837,104 @@ function doc {
     return
   fi
 
-  if ! $options_already_documented; then
-    options_already_documented=true
-    the_opt=
-    if [ "$long_option" ]; then
-      the_opt="--$long_option"
-      if [ "$short_option" ]; then
-        shortoptarg=
-        if expr "$the_opt" : '.*=' &>/dev/null; then
-          shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
-        fi
-        the_opt="$the_opt | -$short_option$shortoptarg"
+  the_opt=
+  if [ "$long_option" ]; then
+    the_opt="--$long_option"
+    if [ "$short_option" ]; then
+      shortoptarg=
+      if expr "$the_opt" : '.*=' &>/dev/null; then
+        shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
       fi
-    elif [ "$short_option" ]; then
-      the_opt="-$short_option"
-    fi
-    if [ -z "$the_opt" ]; then
-      # nothing to document
-      return
+      the_opt="$the_opt | -$short_option$shortoptarg"
     fi
+  elif [ "$short_option" ]; then
+    the_opt="-$short_option"
+  elif [ -z "$smtname" ]; then
+    # nothing to document
+    return
+  fi
+
+  if ! $options_already_documented; then
+    options_already_documented=true
 
     the_doc="$@"
+    mandoc="$@"
+    mansmtdoc="$@"
     if [ "$category" = EXPERT ]; then
       the_doc="$the_doc (EXPERTS only)"
+      mandoc="$mandoc (EXPERTS only)"
+      mansmtdoc="$mansmtdoc (EXPERTS only)"
     fi
 
     if [ "$type" = bool -a -n "$long_option" -a "$long_option_alternate" = "no-$long_option" ]; then
       the_doc="$the_doc [*]"
+      mandoc="$mandoc [*]"
     fi
 
-    doc_line=
-    while [ -n "$the_doc" ]; do
-      remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
-      the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
-      if [ -z "$doc_line" ]; then
-        if expr "$the_opt" : '.\{23\}' &>/dev/null; then
-          # break into two lines
-          doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
+    if [ "$the_opt" ]; then
+      doc_line=
+      while [ -n "$the_doc" ]; do
+        remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
+        the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
+        if [ -z "$doc_line" ]; then
+          if expr "$the_opt" : '.\{23\}' &>/dev/null; then
+            # break into two lines
+            doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
+          else
+            doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
+          fi
         else
-          doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
+          doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
         fi
-      else
-        doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
-      fi
-      the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
-    done
+        the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
+      done
 
-    if [ "$category" = COMMON ]; then
-      common_documentation="${common_documentation}\\n\"
+      if [ "$category" = COMMON ]; then
+        common_documentation="${common_documentation}\\n\"
 #line $lineno \"$kf\"
 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
-      common_manpage_documentation="${common_manpage_documentation}
+        common_manpage_documentation="${common_manpage_documentation}
 .IP \"$the_opt\"
-$@"
-    else
-      remaining_documentation="${remaining_documentation}\\n\"
+$mandoc"
+      else
+        remaining_documentation="${remaining_documentation}\\n\"
 #line $lineno \"$kf\"
 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
-      remaining_manpage_documentation="${remaining_manpage_documentation}
+        remaining_manpage_documentation="${remaining_manpage_documentation}
 .IP \"$the_opt\"
-$@"
+$mandoc"
+      fi
+    fi
+
+    if [ "$smtname" ]; then
+      if [ "$category" = COMMON ]; then
+        common_manpage_smt_documentation="${common_manpage_smt_documentation}
+.TP
+.B \"$smtname\"
+($type) $mansmtdoc"
+      else
+        remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
+.TP
+.B \"$smtname\"
+($type) $mansmtdoc"
+      fi
     fi
   else
-    if [ "$category" = COMMON ]; then
-      common_manpage_documentation="${common_manpage_documentation}
+    if [ "$the_opt" ]; then
+      if [ "$category" = COMMON ]; then
+        common_manpage_documentation="${common_manpage_documentation}
+$@"
+      else
+        remaining_manpage_documentation="${remaining_manpage_documentation}
+$@"
+      fi
+    fi
+
+    if [ "$smtname" ]; then
+        common_manpage_smt_documentation="${common_manpage_smt_documentation}
 $@"
     else
-      remaining_manpage_documentation="${remaining_manpage_documentation}
+        remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
 $@"
     fi
   fi
@@ -1202,6 +1239,8 @@ for var in \
     remaining_documentation \
     common_manpage_documentation \
     remaining_manpage_documentation \
+    common_manpage_smt_documentation \
+    remaining_manpage_smt_documentation \
     smt_getoption_handlers \
     smt_setoption_handlers \
     long_option_value_begin \
diff --git a/src/options/options.h b/src/options/options.h
index c966670f5..4f7e2a692 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -24,6 +24,7 @@
 #include <iostream>
 #include <fstream>
 #include <string>
+#include <vector>
 
 #include "options/option_exception.h"
 #include "util/language.h"
@@ -120,8 +121,10 @@ public:
 
   /**
    * Initialize the options based on the given command-line arguments.
+   * The return value is what's left of the command line (that is, the
+   * non-option arguments).
    */
-  int parseOptions(int argc, char* argv[]) throw(OptionException);
+  std::vector<std::string> parseOptions(int argc, char* argv[]) throw(OptionException);
 
   /**
    * Set the output language based on the given string.
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index ff863bf61..bae0ef169 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -343,8 +343,12 @@ public:
 
 }/* CVC4::options namespace */
 
-/** Parse argc/argv and put the result into a CVC4::Options. */
-int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
+/**
+ * Parse argc/argv and put the result into a CVC4::Options.
+ * The return value is what's left of the command line (that is, the
+ * non-option arguments).
+ */
+std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
   options::OptionsGuard guard(&s_current, this);
 
   const char *progName = main_argv[0];
@@ -371,21 +375,29 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
 
   int extra_optind = 0, main_optind = 0;
   int old_optind;
+  int *optind_ref = &main_optind;
 
   char** argv = main_argv;
 
+  std::vector<std::string> nonOptions;
+
   for(;;) {
     int c = -1;
+    optopt = 0;
     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
       optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
 #endif /* HAVE_DECL_OPTRESET */
       old_optind = optind = extra_optind;
+      optind_ref = &extra_optind;
       argv = extra_argv;
       Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl;
+      if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') {
+        InternalError("preempted args cannot give non-options command-line args (found `%s')", extra_argv[extra_optind == 0 ? 1 : extra_optind]);
+      }
       c = getopt_long(extra_argc, extra_argv,
-                      ":${all_modules_short_options}",
+                      "+:${all_modules_short_options}",
                       cmdlineOptions, NULL);
       Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl;
       if(optind >= extra_argc) {
@@ -407,12 +419,25 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
       optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
 #endif /* HAVE_DECL_OPTRESET */
       old_optind = optind = main_optind;
+      optind_ref = &main_optind;
       argv = main_argv;
+      if(main_optind < argc && main_argv[main_optind][0] != '-') {
+        do {
+          if(main_optind != 0) {
+            nonOptions.push_back(main_argv[main_optind]);
+          }
+          ++main_optind;
+        } while(main_optind < argc && main_argv[main_optind][0] != '-');
+        continue;
+      }
       c = getopt_long(argc, main_argv,
-                      ":${all_modules_short_options}",
+                      "+:${all_modules_short_options}",
                       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;
       }
     }
@@ -422,7 +447,7 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 426 "${template}"
+#line 451 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
@@ -438,27 +463,45 @@ ${all_modules_option_handlers}
 
     case '?':
     default:
-      if(optopt == 0 &&
-         !strncmp(argv[optind - 1], "--thread", 8) &&
-         strlen(argv[optind - 1]) > 8 &&
-         isdigit(argv[optind - 1][8])) {
+      if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) &&
+          !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");
+        }
         std::vector<std::string>& threadArgv = d_holder->threadArgv;
-        int tnum = atoi(argv[optind - 1] + 8);
-        threadArgv.resize(tnum + 1);
+        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");
+        }
+        if(threadArgv.size() <= size_t(tnum)) {
+          threadArgv.resize(tnum + 1);
+        }
         if(threadArgv[tnum] != "") {
           threadArgv[tnum] += " ";
         }
-        const char* p = strchr(argv[optind - 1] + 9, '=');
-        if(p == NULL) { // e.g., we have --thread0 "foo"
-          threadArgv[tnum] += argv[optind++];
+        if(*end == '\0') { // e.g., we have --thread0 "foo"
+          if(argc <= optind) {
+            throw OptionException(std::string("option `") + argv[optind - 1] + "' 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"
-          threadArgv[tnum] += p + 1;
+          if(end[1] == '\0') {
+            throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
+          }
+          Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl;
+          threadArgv[tnum] += end + 1;
         }
+        Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum] << std::endl;
         break;
       }
 
       // This can be a long or short option, and the way to get at the name of it is different.
-      if(optopt == 0) { // was a long option
+      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) + "'");
@@ -470,7 +513,9 @@ ${all_modules_option_handlers}
     throw OptionException(std::string("The use of --incremental with --proof is not yet supported"));
   }
 
-  return optind;
+  Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
+
+  return nonOptions;
 }
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT