diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-21 20:34:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-21 20:34:19 +0000 |
commit | b5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3 (patch) | |
tree | 38f605f758581026af28e5c4d4ad72e12b9cb944 /src/options | |
parent | 9c543757e459bfae5ce1254322212f72af0d37a4 (diff) |
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.)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/base_options | 43 | ||||
-rwxr-xr-x | src/options/mkoptions | 142 | ||||
-rw-r--r-- | src/options/options_template.cpp | 68 |
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 + "'"); } } |