diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-14 15:13:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-14 15:13:37 +0000 |
commit | 080fc73c61ca11a539fd5239146a828e86b9e29a (patch) | |
tree | e85086eafa39013a06b04f7704a17e8a5d977b57 /src/options | |
parent | 01dfa806851502267e1032483fec48e8b4373634 (diff) |
Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/Makefile.am | 1 | ||||
-rw-r--r-- | src/options/base_options_handlers.h | 6 | ||||
-rwxr-xr-x | src/options/mkoptions | 123 | ||||
-rw-r--r-- | src/options/options.h | 5 | ||||
-rw-r--r-- | src/options/options_template.cpp | 79 |
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 |