From c94008073d2b9ddec19ca9713d0c30eb41777eb6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 23 Aug 2021 12:11:13 -0700 Subject: [PATCH] Move options parsing code to main (#7054) This PR moves the code responsible for parsing the command line to the main folder. Note that the options themselves, and converting strings to the options proper types, calling predicates etc, stays in libcvc5. The PR also slightly refactors the options code to get rid of the assign_* functions. --- src/main/CMakeLists.txt | 7 +- src/main/driver_unified.cpp | 9 +- src/main/main.h | 1 - src/main/options.h | 64 ++++++ src/main/options_template.cpp | 287 +++++++++++++++++++++++ src/options/didyoumean.h | 4 +- src/options/mkoptions.py | 126 ++++------ src/options/option_exception.h | 3 +- src/options/options_public.h | 41 ---- src/options/options_public_template.cpp | 290 +----------------------- test/unit/node/node_black.cpp | 11 +- 11 files changed, 426 insertions(+), 417 deletions(-) create mode 100644 src/main/options.h create mode 100644 src/main/options_template.cpp diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 029397832..27086d3fb 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -19,17 +19,22 @@ set(libmain_src_files interactive_shell.cpp interactive_shell.h main.h + options.h signal_handlers.cpp signal_handlers.h time_limit.cpp time_limit.h ) +set(libmain_gen_src_files + ${CMAKE_CURRENT_BINARY_DIR}/options.cpp +) +set_source_files_properties(${libmain_gen_src_files} PROPERTIES GENERATED TRUE) #-----------------------------------------------------------------------------# # Build object library since we will use the object files for cvc5-bin and # main-test library. -add_library(main OBJECT ${libmain_src_files}) +add_library(main OBJECT ${libmain_src_files} ${libmain_gen_src_files}) target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER) if(ENABLE_SHARED) set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 93d458c32..9ceed82f7 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -31,6 +31,7 @@ #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" +#include "main/options.h" #include "main/signal_handlers.h" #include "main/time_limit.h" #include "options/base_options.h" @@ -89,9 +90,9 @@ void printUsage(const Options& opts, bool full) { << endl << "cvc5 options:" << endl; if(full) { - options::printUsage(ss.str(), *opts.base.out); + main::printUsage(ss.str(), *opts.base.out); } else { - options::printShortUsage(ss.str(), *opts.base.out); + main::printShortUsage(ss.str(), *opts.base.out); } } @@ -109,7 +110,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) Options* opts = &pExecutor->getOptions(); // Parse the options - std::vector filenames = options::parse(*opts, argc, argv, progName); + std::vector filenames = main::parse(*solver, argc, argv, progName); auto limit = install_time_limit(*opts); @@ -120,7 +121,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) } else if (opts->base.languageHelp) { - options::printLanguageHelp(*opts->base.out); + main::printLanguageHelp(*opts->base.out); exit(1); } else if (opts->driver.version) diff --git a/src/main/main.h b/src/main/main.h index e76836600..5643588e1 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -65,6 +65,5 @@ extern bool segvSpin; /** Actual cvc5 driver functions **/ int runCvc5(int argc, char* argv[], std::unique_ptr&); -void printUsage(const cvc5::Options&, bool full = false); #endif /* CVC5__MAIN__MAIN_H */ diff --git a/src/main/options.h b/src/main/options.h new file mode 100644 index 000000000..a2c26273b --- /dev/null +++ b/src/main/options.h @@ -0,0 +1,64 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Options utilities used in the driver. + */ + +#ifndef CVC5__MAIN__OPTIONS_H +#define CVC5__MAIN__OPTIONS_H + +#include +#include +#include + +#include "api/cpp/cvc5.h" + +namespace cvc5::main { + +/** + * Print overall command-line option usage message, prefixed by + * "msg"---which could be an error message causing the usage + * output in the first place, e.g. "no such option --foo" + */ +void printUsage(const std::string& msg, std::ostream& os); + +/** + * Print command-line option usage message for only the most-commonly + * used options. The message is prefixed by "msg"---which could be + * an error message causing the usage output in the first place, e.g. + * "no such option --foo" + */ +void printShortUsage(const std::string& msg, std::ostream& os); + +/** Print help for the --lang command line option */ +void printLanguageHelp(std::ostream& os); + +/** + * Initialize the Options object options based on the given + * command-line arguments given in argc and argv. The return value + * is what's left of the command line (that is, the non-option + * arguments). + * + * This function uses getopt_long() and is not thread safe. + * + * Throws OptionException on failures. + * + * Preconditions: options and argv must be non-null. + */ +std::vector parse(api::Solver& solver, + int argc, + char* argv[], + std::string& binaryName); + +} // namespace cvc5::options + +#endif diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp new file mode 100644 index 000000000..87a5fc158 --- /dev/null +++ b/src/main/options_template.cpp @@ -0,0 +1,287 @@ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Gereon Kremer, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Options utilities used in the driver. + */ + +#include "main/options.h" + +#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) +// force use of optreset; mingw32 croaks on argv-switching otherwise +#include "base/cvc5config.h" +#define _BSD_SOURCE +#undef HAVE_DECL_OPTRESET +#define HAVE_DECL_OPTRESET 1 +#define CVC5_IS_NOT_REALLY_BSD +#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */ + +#ifdef __MINGW64__ +extern int optreset; +#endif /* __MINGW64__ */ + +#include + +// clean up +#ifdef CVC5_IS_NOT_REALLY_BSD +# undef _BSD_SOURCE +#endif /* CVC5_IS_NOT_REALLY_BSD */ + +#include "base/check.h" +#include "base/output.h" +#include "options/didyoumean.h" +#include "options/option_exception.h" + +#include +#include +#include + +namespace cvc5::main { + +// clang-format off +static const std::string commonOptionsDescription = + "Most commonly-used cvc5 options:\n" +${help_common}$ + ; + +static const std::string additionalOptionsDescription = + "Additional cvc5 options:\n" +${help_others}$; + +static const std::string optionsFootnote = "\n\ +[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ + sense of the option.\n\ +"; + +static const std::string languageDescription = + "\ +Languages currently supported as arguments to the -L / --lang option:\n\ + auto attempt to automatically determine language\n\ + cvc | presentation | pl CVC presentation language\n\ + smt | smtlib | smt2 |\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ + tptp TPTP format (cnf, fof and tff)\n\ + sygus | sygus2 SyGuS version 2.0\n\ +\n\ +Languages currently supported as arguments to the --output-lang option:\n\ + auto match output language to input language\n\ + cvc | presentation | pl CVC presentation language\n\ + smt | smtlib | smt2 |\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ + tptp TPTP format\n\ + ast internal format (simple syntax trees)\n\ +"; +// clang-format on + +void printUsage(const std::string& msg, std::ostream& os) { + os << msg << "\n" << commonOptionsDescription << "\n\n" << additionalOptionsDescription << std::endl + << optionsFootnote << std::endl << std::flush; +} + +void printShortUsage(const std::string& msg, std::ostream& os) { + os << msg << "\n" << commonOptionsDescription << std::endl + << optionsFootnote << std::endl + << "For full usage, please use --help." + << std::endl << std::endl << std::flush; +} + +void printLanguageHelp(std::ostream& os) { + os << languageDescription << std::flush; +} + +/** + * This is a table of long options. By policy, each short option + * should have an equivalent long option (but the reverse isn't the + * case), so this table should thus contain all command-line options. + * + * Each option in this array has four elements: + * + * 1. the long option string + * 2. argument behavior for the option: + * no_argument - no argument permitted + * required_argument - an argument is expected + * optional_argument - an argument is permitted but not required + * 3. this is a pointer to an int which is set to the 4th entry of the + * array if the option is present; or NULL, in which case + * getopt_long() returns the 4th entry + * 4. the return value for getopt_long() when this long option (or the + * value to set the 3rd entry to; see #3) + */ +// clang-format off +static struct option cmdlineOptions[] = { + ${cmdline_options}$ + {nullptr, no_argument, nullptr, '\0'} +}; +// clang-format on + +std::string suggestCommandLineOptions(const std::string& optionName) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { + didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); + } + + return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); +} + +void parseInternal(api::Solver& solver, int argc, + char* argv[], + std::vector& nonoptions) +{ + Assert(argv != nullptr); + if(Debug.isOn("options")) { + Debug("options") << "starting a new parseInternal with " + << argc << " arguments" << std::endl; + for( int i = 0; i < argc ; i++ ){ + Assert(argv[i] != NULL); + Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; + } + } + + // Reset getopt(), in the case of multiple calls to parse(). + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this +#endif /* HAVE_DECL_OPTRESET */ + + // We must parse the binary name, which is manually ignored below. Setting + // this to 1 leads to incorrect behavior on some platforms. + int main_optind = 0; + int old_optind; + + + while(true) { // Repeat Forever + + optopt = 0; + + optind = main_optind; + old_optind = main_optind; + + // If we encounter an element that is not at zero and does not start + // with a "-", this is a non-option. We consume this element as a + // non-option. + if (main_optind > 0 && main_optind < argc && + argv[main_optind][0] != '-') { + Debug("options") << "enqueueing " << argv[main_optind] + << " as a non-option." << std::endl; + nonoptions.push_back(argv[main_optind]); + ++main_optind; + continue; + } + + + Debug("options") << "[ before, main_optind == " << main_optind << " ]" + << std::endl; + Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; + Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" + << std::endl; + // clang-format off + int c = getopt_long(argc, argv, + "+:${options_short}$", + cmdlineOptions, NULL); + // clang-format on + + main_optind = optind; + + Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" + << "[ next option will be at pos: " << optind << " ]" + << std::endl; + + // The initial getopt_long call should always determine that argv[0] + // is not an option and returns -1. We always manually advance beyond + // this element. + if ( old_optind == 0 && c == -1 ) { + Assert(main_optind > 0); + continue; + } + + if ( c == -1 ) { + if(Debug.isOn("options")) { + Debug("options") << "done with option parsing" << std::endl; + for(int index = optind; index < argc; ++index) { + Debug("options") << "remaining " << argv[index] << std::endl; + } + } + break; + } + + std::string option = argv[old_optind == 0 ? 1 : old_optind]; + std::string optionarg = (optarg == nullptr) ? "" : optarg; + + Debug("preemptGetopt") << "processing option " << c + << " (`" << char(c) << "'), " << option << std::endl; + + // clang-format off + switch(c) + { + ${options_handler}$ + + case ':' : + // This can be a long or short option, and the way to get at the + // name of it is different. + throw OptionException(std::string("option `") + option + + "' missing its required argument"); + + case '?': + default: + throw OptionException(std::string("can't understand option `") + option + + "'" + suggestCommandLineOptions(option)); + } + } + // clang-format on + + Debug("options") << "got " << nonoptions.size() + << " non-option arguments." << std::endl; +} + +/** + * Parse argc/argv and put the result into a cvc5::Options. + * The return value is what's left of the command line (that is, the + * non-option arguments). + * + * Throws OptionException on failures. + */ +std::vector parse( + api::Solver& solver, int argc, char* argv[], std::string& binaryName) +{ + Assert(argv != nullptr); + + const char *progName = argv[0]; + + // To debug options parsing, you may prefer to simply uncomment this + // and recompile. Debug flags have not been parsed yet so these have + // not been set. + //DebugChannel.on("options"); + + Debug("options") << "argv == " << argv << std::endl; + + // Find the base name of the program. + const char *x = strrchr(progName, '/'); + if(x != nullptr) { + progName = x + 1; + } + binaryName = std::string(progName); + + std::vector nonoptions; + parseInternal(solver, argc, argv, nonoptions); + if (Debug.isOn("options")){ + for (const auto& no: nonoptions){ + Debug("options") << "nonoptions " << no << std::endl; + } + } + + return nonoptions; +} + +} // namespace cvc5::options diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h index c9949cd3e..e588dd36d 100644 --- a/src/options/didyoumean.h +++ b/src/options/didyoumean.h @@ -20,13 +20,15 @@ #pragma once +#include "cvc5_export.h" + #include #include #include namespace cvc5 { -class DidYouMean { +class CVC5_EXPORT DidYouMean { public: using Words = std::set; diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index a861b06eb..2ace926f0 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -70,25 +70,12 @@ g_getopt_long_start = 256 ### Source code templates -TPL_ASSIGN = ''' -void assign_{module}_{name}(Options& opts, const std::string& option, const std::string& optionarg) {{ - auto value = {handler}; - {predicates} - opts.{module}.{name} = value; - opts.{module}.{name}WasSetByUser = true; - Trace("options") << "user assigned option {name} = " << value << std::endl; -}}''' - -TPL_ASSIGN_BOOL = ''' -void assign_{module}_{name}(Options& opts, const std::string& option, bool value) {{ - {predicates} - opts.{module}.{name} = value; - opts.{module}.{name}WasSetByUser = true; - Trace("options") << "user assigned option {name} = " << value << std::endl; -}}''' - -TPL_CALL_ASSIGN_BOOL = ' assign_{module}_{name}(opts, {option}, {value});' -TPL_CALL_ASSIGN = ' assign_{module}_{name}(opts, {option}, optionarg);' +TPL_ASSIGN = ''' opts.{module}.{name} = {handler}; + opts.{module}.{name}WasSetByUser = true;''' +TPL_ASSIGN_PRED = ''' auto value = {handler}; + {predicates} + opts.{module}.{name} = value; + opts.{module}.{name}WasSetByUser = true;''' TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));' @@ -203,14 +190,12 @@ def get_handler(option): optname = option.long_name if option.long else "" if option.handler: if option.type == 'void': - return 'opts.handler().{}("{}", option)'.format(option.handler, optname) + return 'opts.handler().{}("{}", name)'.format(option.handler, optname) else: - return 'opts.handler().{}("{}", option, optionarg)'.format(option.handler, optname) + return 'opts.handler().{}("{}", name, optionarg)'.format(option.handler, optname) elif option.mode: return 'stringTo{}(optionarg)'.format(option.type) - elif option.type != 'bool': - return 'handleOption<{}>("{}", option, optionarg)'.format(option.type, optname) - return None + return 'handleOption<{}>("{}", name, optionarg)'.format(option.type, optname) def get_predicates(option): @@ -221,10 +206,10 @@ def get_predicates(option): assert option.type != 'void' res = [] if option.minimum: - res.append('opts.handler().checkMinimum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.minimum)) + res.append('opts.handler().checkMinimum("{}", name, value, static_cast<{}>({}));'.format(optname, option.type, option.minimum)) if option.maximum: - res.append('opts.handler().checkMaximum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.maximum)) - res += ['opts.handler().{}("{}", option, value);'.format(x, optname) + res.append('opts.handler().checkMaximum("{}", name, value, static_cast<{}>({}));'.format(optname, option.type, option.maximum)) + res += ['opts.handler().{}("{}", name, value);'.format(x, optname) for x in option.predicates] return res @@ -752,7 +737,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): # Generate options_handler and getopt_long cases = [] if option.short: - cases.append("case '{}':".format(option.short)) + cases.append("case '{0}': // -{0}".format(option.short)) getopt_short.append(option.short) if argument_req: @@ -773,22 +758,16 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): add_getopt_long(alias, argument_req, getopt_long) if cases: - if option.type == 'bool' and option.name: + if option.type == 'bool': + cases.append( + ' solver.setOption("{}", "true");'.format(option.long_name) + ) + elif option.type == 'void': cases.append( - TPL_CALL_ASSIGN_BOOL.format( - module=module.id, - name=option.name, - option='option', - value='true')) - elif option.type != 'void' and option.name and not mode_handler: + ' solver.setOption("{}", "");'.format(option.long_name)) + else: cases.append( - TPL_CALL_ASSIGN.format( - module=module.id, - name=option.name, - option='option', - value='optionarg')) - elif handler: - cases.append('{};'.format(handler)) + ' solver.setOption("{}", optionarg);'.format(option.long_name)) cases.append(' break;') @@ -809,20 +788,24 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): cond = ' || '.join( ['name == "{}"'.format(x) for x in sorted(names)]) - setoption_handlers.append(' if ({}) {{'.format(cond)) - if option.type == 'bool': - setoption_handlers.append( - TPL_CALL_ASSIGN_BOOL.format( - module=module.id, - name=option.name, - option='name', - value='optionarg == "true"')) - elif argument_req and option.name and not mode_handler: - setoption_handlers.append( - TPL_CALL_ASSIGN.format( - module=module.id, - name=option.name, - option='name')) + if setoption_handlers: + setoption_handlers.append(' }} else if ({}) {{'.format(cond)) + else: + setoption_handlers.append(' if ({}) {{'.format(cond)) + if option.name and not mode_handler: + if predicates: + setoption_handlers.append( + TPL_ASSIGN_PRED.format( + module=module.id, + name=option.name, + handler=handler, + predicates='\n '.join(predicates))) + else: + setoption_handlers.append( + TPL_ASSIGN.format( + module=module.id, + name=option.name, + handler=handler)) elif option.handler: h = ' opts.handler().{handler}("{smtname}", name' if argument_req: @@ -831,8 +814,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): setoption_handlers.append( h.format(handler=option.handler, smtname=option.long_name)) - setoption_handlers.append(' return;') - setoption_handlers.append(' }') if option.name: getoption_handlers.append( @@ -858,7 +839,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): if option.long and option.type == 'bool' and option.alternate: cases = [] cases.append( - 'case {}:// --no-{}'.format( + 'case {}: // --no-{}'.format( g_getopt_long_start + len(getopt_long), option.long)) @@ -867,16 +848,15 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): if option.alias: for alias in option.alias: cases.append( - 'case {}:// --no-{}'.format( + 'case {}: // --no-{}'.format( g_getopt_long_start + len(getopt_long), alias)) add_getopt_long('no-{}'.format(alias), argument_req, getopt_long) cases.append( - TPL_CALL_ASSIGN_BOOL.format( - module=module.id, - name=option.name, option='option', value='false')) + ' solver.setOption("{}", "false");'.format(option.long_name) + ) cases.append(' break;') options_handler.extend(cases) @@ -885,24 +865,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): if option.long_name: options_getall.append(get_getall(module, option)) - - # Define handler assign/assignBool - if not mode_handler: - if option.type == 'bool': - assign_impls.append(TPL_ASSIGN_BOOL.format( - module=module.id, - name=option.name, - handler=handler, - predicates='\n'.join(predicates) - )) - elif option.short or option.long: - assign_impls.append(TPL_ASSIGN.format( - module=module.id, - name=option.name, - handler=handler, - predicates='\n'.join(predicates) - )) - options_all_names = ', '.join(map(lambda s: '"' + s + '"', sorted(options_names))) options_all_names = '\n'.join(textwrap.wrap(options_all_names, width=80, break_on_hyphens=False)) @@ -920,7 +882,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): 'help_others': '\n'.join(help_others), 'options_handler': '\n '.join(options_handler), 'options_short': ''.join(getopt_short), - 'assigns': '\n'.join(assign_impls), 'options_getall': '\n '.join(options_getall), 'options_all_names': options_all_names, 'getoption_handlers': '\n'.join(getoption_handlers), @@ -1073,6 +1034,7 @@ def mkoptions_main(): {'input': 'options/options_template.h'}, {'input': 'options/options_template.cpp'}, {'input': 'options/options_public_template.cpp'}, + {'input': 'main/options_template.cpp'}, ] for tpl in module_tpls + global_tpls: diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 6d24e7c39..928b4c2f1 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -18,6 +18,7 @@ #ifndef CVC5__OPTION_EXCEPTION_H #define CVC5__OPTION_EXCEPTION_H +#include "cvc5_export.h" #include "base/exception.h" namespace cvc5 { @@ -26,7 +27,7 @@ namespace cvc5 { * Class representing an option-parsing exception such as badly-typed * or missing arguments, arguments out of bounds, etc. */ -class OptionException : public cvc5::Exception +class CVC5_EXPORT OptionException : public cvc5::Exception { public: OptionException(const std::string& s) : cvc5::Exception(s_errPrefix + s) {} diff --git a/src/options/options_public.h b/src/options/options_public.h index 06981a837..7b6767b58 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -29,47 +29,6 @@ namespace cvc5::options { bool getUfHo(const Options& opts) CVC5_EXPORT; -/** - * Get a description of the command-line flags accepted by - * parse. The returned string will be escaped so that it is - * suitable as an argument to printf. */ -const std::string& getDescription() CVC5_EXPORT; - -/** - * Print overall command-line option usage message, prefixed by - * "msg"---which could be an error message causing the usage - * output in the first place, e.g. "no such option --foo" - */ -void printUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT; - -/** - * Print command-line option usage message for only the most-commonly - * used options. The message is prefixed by "msg"---which could be - * an error message causing the usage output in the first place, e.g. - * "no such option --foo" - */ -void printShortUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT; - -/** Print help for the --lang command line option */ -void printLanguageHelp(std::ostream& os) CVC5_EXPORT; - -/** - * Initialize the Options object options based on the given - * command-line arguments given in argc and argv. The return value - * is what's left of the command line (that is, the non-option - * arguments). - * - * This function uses getopt_long() and is not thread safe. - * - * Throws OptionException on failures. - * - * Preconditions: options and argv must be non-null. - */ -std::vector parse(Options& opts, - int argc, - char* argv[], - std::string& binaryName) CVC5_EXPORT; - /** * Retrieve an option value by name (as given in key) from the Options object * opts as a string. diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index dc09c0618..7e892ff87 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -15,29 +15,9 @@ #include "options/options_public.h" -#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) -// force use of optreset; mingw32 croaks on argv-switching otherwise -#include "base/cvc5config.h" -#define _BSD_SOURCE -#undef HAVE_DECL_OPTRESET -#define HAVE_DECL_OPTRESET 1 -#define CVC5_IS_NOT_REALLY_BSD -#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */ - -#ifdef __MINGW64__ -extern int optreset; -#endif /* __MINGW64__ */ - -#include - -// clean up -#ifdef CVC5_IS_NOT_REALLY_BSD -# undef _BSD_SOURCE -#endif /* CVC5_IS_NOT_REALLY_BSD */ #include "base/check.h" #include "base/output.h" -#include "options/didyoumean.h" #include "options/options_handler.h" #include "options/options_listener.h" #include "options/options.h" @@ -53,63 +33,6 @@ namespace cvc5::options { bool getUfHo(const Options& opts) { return opts.uf.ufHo; } -// clang-format off -static const std::string mostCommonOptionsDescription = - "\ -Most commonly-used cvc5 options:\n" -${help_common}$ - ; - -static const std::string optionsDescription = - mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n" -${help_others}$; - -static const std::string optionsFootnote = "\n\ -[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ - sense of the option.\n\ -"; - -static const std::string languageDescription = - "\ -Languages currently supported as arguments to the -L / --lang option:\n\ - auto attempt to automatically determine language\n\ - cvc | presentation | pl CVC presentation language\n\ - smt | smtlib | smt2 |\n\ - smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format (cnf, fof and tff)\n\ - sygus | sygus2 SyGuS version 2.0\n\ -\n\ -Languages currently supported as arguments to the --output-lang option:\n\ - auto match output language to input language\n\ - cvc | presentation | pl CVC presentation language\n\ - smt | smtlib | smt2 |\n\ - smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format\n\ - ast internal format (simple syntax trees)\n\ -"; -// clang-format on - -const std::string& getDescription() -{ - return optionsDescription; -} - -void printUsage(const std::string& msg, std::ostream& os) { - os << msg << optionsDescription << std::endl - << optionsFootnote << std::endl << std::flush; -} - -void printShortUsage(const std::string& msg, std::ostream& os) { - os << msg << mostCommonOptionsDescription << std::endl - << optionsFootnote << std::endl - << "For full usage, please use --help." - << std::endl << std::endl << std::flush; -} - -void printLanguageHelp(std::ostream& os) { - os << languageDescription << std::flush; -} - /** Set a given Options* as "current" just for a particular scope. */ class OptionsGuard { Options** d_field; @@ -125,47 +48,6 @@ public: } };/* class OptionsGuard */ -/** - * This is a table of long options. By policy, each short option - * should have an equivalent long option (but the reverse isn't the - * case), so this table should thus contain all command-line options. - * - * Each option in this array has four elements: - * - * 1. the long option string - * 2. argument behavior for the option: - * no_argument - no argument permitted - * required_argument - an argument is expected - * optional_argument - an argument is permitted but not required - * 3. this is a pointer to an int which is set to the 4th entry of the - * array if the option is present; or NULL, in which case - * getopt_long() returns the 4th entry - * 4. the return value for getopt_long() when this long option (or the - * value to set the 3rd entry to; see #3) - * - * If you add something here, you should add it in src/main/usage.h - * also, to document it. - * - * If you add something that has a short option equivalent, you should - * add it to the getopt_long() call in parse(). - */ -// clang-format off -static struct option cmdlineOptions[] = { - ${cmdline_options}$ - {nullptr, no_argument, nullptr, '\0'}}; -// clang-format on - -std::string suggestCommandLineOptions(const std::string& optionName) -{ - DidYouMean didYouMean; - - const char* opt; - for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { - didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); - } - - return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); -} /** * This is a default handler for options of built-in C++ type. This @@ -337,165 +219,10 @@ template <> std::string handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) { return optionarg; } - -// clang-format off -${assigns}$ -// clang-format off - -void parseInternal(Options& opts, int argc, - char* argv[], - std::vector& nonoptions) -{ - Assert(argv != nullptr); - if(Debug.isOn("options")) { - Debug("options") << "starting a new parseInternal with " - << argc << " arguments" << std::endl; - for( int i = 0; i < argc ; i++ ){ - Assert(argv[i] != NULL); - Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; - } - } - - // Reset getopt(), in the case of multiple calls to parse(). - // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. - optind = 0; -#if HAVE_DECL_OPTRESET - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this -#endif /* HAVE_DECL_OPTRESET */ - - // We must parse the binary name, which is manually ignored below. Setting - // this to 1 leads to incorrect behavior on some platforms. - int main_optind = 0; - int old_optind; - - - while(true) { // Repeat Forever - - optopt = 0; - std::string option, optionarg; - - optind = main_optind; - old_optind = main_optind; - - // If we encounter an element that is not at zero and does not start - // with a "-", this is a non-option. We consume this element as a - // non-option. - if (main_optind > 0 && main_optind < argc && - argv[main_optind][0] != '-') { - Debug("options") << "enqueueing " << argv[main_optind] - << " as a non-option." << std::endl; - nonoptions.push_back(argv[main_optind]); - ++main_optind; - continue; - } - - - Debug("options") << "[ before, main_optind == " << main_optind << " ]" - << std::endl; - Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; - Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" - << std::endl; - // clang-format off - int c = getopt_long(argc, argv, - "+:${options_short}$", - cmdlineOptions, NULL); - // clang-format on - - main_optind = optind; - - Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" - << "[ next option will be at pos: " << optind << " ]" - << std::endl; - - // The initial getopt_long call should always determine that argv[0] - // is not an option and returns -1. We always manually advance beyond - // this element. - if ( old_optind == 0 && c == -1 ) { - Assert(main_optind > 0); - continue; - } - - if ( c == -1 ) { - if(Debug.isOn("options")) { - Debug("options") << "done with option parsing" << std::endl; - for(int index = optind; index < argc; ++index) { - Debug("options") << "remaining " << argv[index] << std::endl; - } - } - break; - } - - option = argv[old_optind == 0 ? 1 : old_optind]; - optionarg = (optarg == NULL) ? "" : optarg; - - Debug("preemptGetopt") << "processing option " << c - << " (`" << char(c) << "'), " << option << std::endl; - - // clang-format off - switch(c) - { -${options_handler}$ - - case ':' : - // This can be a long or short option, and the way to get at the - // name of it is different. - throw OptionException(std::string("option `") + option - + "' missing its required argument"); - - case '?': - default: - throw OptionException(std::string("can't understand option `") + option - + "'" + suggestCommandLineOptions(option)); - } - } - // clang-format on - - Debug("options") << "got " << nonoptions.size() - << " non-option arguments." << std::endl; -} - -/** - * Parse argc/argv and put the result into a cvc5::Options. - * The return value is what's left of the command line (that is, the - * non-option arguments). - * - * Throws OptionException on failures. - */ -std::vector parse( - Options & opts, int argc, char* argv[], std::string& binaryName) -{ - Assert(argv != nullptr); - - Options* cur = &Options::current(); - OptionsGuard guard(&cur, &opts); - - const char *progName = argv[0]; - - // To debug options parsing, you may prefer to simply uncomment this - // and recompile. Debug flags have not been parsed yet so these have - // not been set. - //DebugChannel.on("options"); - - Debug("options") << "options::parse == " << &opts << std::endl; - Debug("options") << "argv == " << argv << std::endl; - - // Find the base name of the program. - const char *x = strrchr(progName, '/'); - if(x != nullptr) { - progName = x + 1; - } - binaryName = std::string(progName); - - std::vector nonoptions; - parseInternal(opts, argc, argv, nonoptions); - if (Debug.isOn("options")){ - for(std::vector::const_iterator i = nonoptions.begin(), - iend = nonoptions.end(); i != iend; ++i){ - Debug("options") << "nonoptions " << *i << std::endl; - } - } - - return nonoptions; +template <> +bool handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) { + Assert(optionarg == "true" || optionarg == "false"); + return optionarg == "true"; } std::string get(const Options& options, const std::string& name) @@ -511,9 +238,14 @@ void setInternal(Options& opts, const std::string& name, const std::string& optionarg) { // clang-format off - ${setoption_handlers}$ +${setoption_handlers}$ // clang-format on - throw OptionException("Unrecognized option key or setting: " + name); + } + else + { + throw OptionException("Unrecognized option key or setting: " + name); + } + Trace("options") << "user assigned option " << name << " = " << optionarg << std::endl; } void set(Options& opts, const std::string& name, const std::string& optionarg) diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 787dd77ca..45801798b 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -27,6 +27,8 @@ #include "expr/node_manager.h" #include "expr/node_value.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" +#include "options/language.h" #include "options/options_public.h" #include "smt/smt_engine.h" #include "test_node.h" @@ -65,13 +67,8 @@ class TestNodeBlackNode : public TestNode TestNode::SetUp(); // setup an SMT engine so that options are in scope Options opts; - char* argv[2]; - argv[0] = strdup(""); - argv[1] = strdup("--output-lang=ast"); - std::string progName; - options::parse(opts, 2, argv, progName); - free(argv[0]); - free(argv[1]); + opts.base.outputLanguage = OutputLanguage::LANG_AST; + opts.base.outputLanguageWasSetByUser = true; d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts)); } -- 2.30.2