-/********************* */
-/*! \file options_template.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Contains code for handling command-line options.
- **
- ** Contains code for handling command-line options
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Tim King, 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.
+ * ****************************************************************************
+ *
+ * Contains code for handling command-line options.
+ */
#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
// force use of optreset; mingw32 croaks on argv-switching otherwise
-# include "cvc4autoconfig.h"
-# define _BSD_SOURCE
-# undef HAVE_DECL_OPTRESET
-# define HAVE_DECL_OPTRESET 1
-# define CVC4_IS_NOT_REALLY_BSD
+#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__
#include <getopt.h>
// clean up
-#ifdef CVC4_IS_NOT_REALLY_BSD
+#ifdef CVC5_IS_NOT_REALLY_BSD
# undef _BSD_SOURCE
-#endif /* CVC4_IS_NOT_REALLY_BSD */
+#endif /* CVC5_IS_NOT_REALLY_BSD */
#include <unistd.h>
#include <string.h>
-#include <stdint.h>
#include <time.h>
#include <cstdio>
#include <sstream>
#include <limits>
-#include "base/cvc4_assert.h"
+#include "base/check.h"
#include "base/exception.h"
#include "base/output.h"
-#include "base/tls.h"
-#include "options/argument_extender.h"
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/options_handler.h"
+#include "options/options_listener.h"
-${include_all_option_headers}
-
-#line 63 "${template}"
+// clang-format off
+${headers_module}$
-#include "options/options_holder.h"
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
#include "options/base_handlers.h"
-${option_handler_includes}
-
-#line 71 "${template}"
+${headers_handler}$
-using namespace CVC4;
-using namespace CVC4::options;
-
-namespace CVC4 {
-
-CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
+using namespace cvc5;
+using namespace cvc5::options;
+// clang-format on
+namespace cvc5 {
+thread_local Options* Options::s_current = NULL;
/**
* This is a default handler for options of built-in C++ type. This
if(!success){
throw OptionException(option + ": failed to parse "+ optionarg +
- " as an integer of the appropraite type.");
+ " as an integer of the appropriate type.");
}
// Depending in the platform unsigned numbers with '-' signs may parse.
// that can throw exceptions.
}
-
-Options::Options()
- : d_holder(new options::OptionsHolder())
- , d_handler(new options::OptionsHandler(this))
- , d_forceLogicListeners()
- , d_beforeSearchListeners()
- , d_tlimitListeners()
- , d_tlimitPerListeners()
- , d_rlimitListeners()
- , d_rlimitPerListeners()
+Options::Options(OptionsListener* ol)
+ : d_handler(new options::OptionsHandler(this)),
+// clang-format off
+${holder_mem_inits}$
+${holder_ref_inits}$
+// clang-format on
+ d_olisten(ol)
{}
Options::~Options() {
delete d_handler;
- delete d_holder;
}
void Options::copyValues(const Options& options){
if(this != &options) {
- delete d_holder;
- d_holder = new options::OptionsHolder(*options.d_holder);
+// clang-format off
+${holder_mem_copy}$
+// clang-format on
}
}
return ss.str();
}
-ListenerCollection::Registration* Options::registerAndNotify(
- ListenerCollection& collection, Listener* listener, bool notify)
-{
- ListenerCollection::Registration* registration =
- collection.registerListener(listener);
- if(notify) {
- listener->notify();
- }
- return registration;
-}
-
-ListenerCollection::Registration* Options::registerForceLogicListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::forceLogicString);
- return registerAndNotify(d_forceLogicListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerBeforeSearchListener(
- Listener* listener)
-{
- return d_beforeSearchListeners.registerListener(listener);
-}
-
-ListenerCollection::Registration* Options::registerTlimitListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet &&
- wasSetByUser(options::cumulativeMillisecondLimit);
- return registerAndNotify(d_tlimitListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerTlimitPerListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::perCallMillisecondLimit);
- return registerAndNotify(d_tlimitPerListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerRlimitListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::cumulativeResourceLimit);
- return registerAndNotify(d_rlimitListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerRlimitPerListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::perCallResourceLimit);
- return registerAndNotify(d_rlimitPerListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerUseTheoryListListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::useTheoryList);
- return registerAndNotify(d_useTheoryListListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth);
- return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDagListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh);
- return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintExprTypesListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::printExprTypes);
- return registerAndNotify(d_setPrintExprTypesListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDumpModeListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::dumpModeString);
- return registerAndNotify(d_setDumpModeListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintSuccessListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::printSuccess);
- return registerAndNotify(d_setPrintSuccessListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerDumpToFileNameListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName);
- return registerAndNotify(d_dumpToFileListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetRegularOutputChannelListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::regularChannelName);
- return registerAndNotify(d_setRegularChannelListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetDiagnosticOutputChannelListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName);
- return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetReplayLogFilename(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename);
- return registerAndNotify(d_setReplayFilenameListeners, listener, notify);
-}
-
-${all_custom_handlers}
-
-#line 393 "${template}"
-
-#ifdef CVC4_DEBUG
-# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
-#else /* CVC4_DEBUG */
-# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
-#endif /* CVC4_DEBUG */
-
-#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
-# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
-# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
-
-options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
-{
-}
-
-#line 411 "${template}"
+void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
-static const std::string mostCommonOptionsDescription = "\
-Most commonly-used CVC4 options:${common_documentation}";
+// clang-format off
+${custom_handlers}$
+// clang-format on
-#line 416 "${template}"
+static const std::string mostCommonOptionsDescription =
+ "\
+Most commonly-used cvc5 options:\n"
+ // clang-format off
+${help_common}$
+ // clang-format on
+ ;
-static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
-\n\
-Additional CVC4 options:${remaining_documentation}";
-
-#line 422 "${template}"
+// clang-format off
+static const std::string optionsDescription =
+ mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
+${help_others}$;
+// clang-format on
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 = "\
+static const std::string languageDescription =
+ "\
Languages currently supported as arguments to the -L / --lang option:\n\
auto attempt to automatically determine language\n\
- cvc4 | presentation | pl CVC4 presentation language\n\
- smt1 | smtlib1 SMT-LIB format 1.2\n\
+ cvc | presentation | pl CVC presentation language\n\
smt | smtlib | smt2 |\n\
- smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
- smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\
- tptp TPTP format (cnf and fof)\n\
- sygus SyGuS format\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\
- cvc4 | presentation | pl CVC4 presentation language\n\
- cvc3 CVC3 presentation language\n\
- smt1 | smtlib1 SMT-LIB format 1.2\n\
+ cvc | presentation | pl CVC presentation language\n\
smt | smtlib | smt2 |\n\
- smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\
- smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\
+ smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\
tptp TPTP format\n\
- z3str SMT-LIB 2.0 with Z3-str string constraints\n\
ast internal format (simple syntax trees)\n\
";
* If you add something that has a short option equivalent, you should
* add it to the getopt_long() call in parseOptions().
*/
-static struct option cmdlineOptions[] = {${all_modules_long_options}
- { NULL, no_argument, NULL, '\0' }
-};/* cmdlineOptions */
-
-#line 501 "${template}"
-
-// static void preemptGetopt(int& argc, char**& argv, const char* opt) {
-
-// Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
-
-// AlwaysAssert(opt != NULL && *opt != '\0');
-// AlwaysAssert(strlen(opt) <= maxoptlen);
-
-// ++argc;
-// unsigned i = 1;
-// while(argv[i] != NULL && argv[i][0] != '\0') {
-// ++i;
-// }
-
-// if(argv[i] == NULL) {
-// argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
-// for(unsigned j = i; j < i + 5; ++j) {
-// argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
-// argv[j][0] = '\0';
-// }
-// argv[i + 5] = NULL;
-// }
-
-// strncpy(argv[i], opt, maxoptlen - 1);
-// argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
-// }
+// clang-format off
+static struct option cmdlineOptions[] = {
+ ${cmdline_options}$
+ {nullptr, no_argument, nullptr, '\0'}};
+// clang-format on
namespace options {
/** Set a given Options* as "current" just for a particular scope. */
class OptionsGuard {
- CVC4_THREADLOCAL_TYPE(Options*)* d_field;
+ Options** d_field;
Options* d_old;
public:
- OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) :
+ OptionsGuard(Options** field, Options* opts) :
d_field(field),
d_old(*field) {
*field = opts;
}
};/* class OptionsGuard */
-}/* CVC4::options namespace */
+} // namespace options
/**
- * Parse argc/argv and put the result into a CVC4::Options.
+ * 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<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
- options::OptionsGuard guard(&s_current, this);
+std::vector<std::string> Options::parseOptions(Options* options,
+ int argc,
+ char* argv[])
+{
+ Assert(options != NULL);
+ Assert(argv != NULL);
- // Having this synonym simplifies the generation code in mkoptions.
- options::OptionsHandler* handler = d_handler;
+ options::OptionsGuard guard(&s_current, options);
- const char *progName = main_argv[0];
+ const char *progName = argv[0];
- ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen);
- std::vector<char*> allocated;
+ // 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") << "main_argv == " << main_argv << std::endl;
+ Debug("options") << "Options::parseOptions == " << options << std::endl;
+ Debug("options") << "argv == " << argv << std::endl;
+
+ // Find the base name of the program.
+ const char *x = strrchr(progName, '/');
+ if(x != NULL) {
+ progName = x + 1;
+ }
+ options->base.binary_name = std::string(progName);
+
+ std::vector<std::string> nonoptions;
+ options->parseOptionsRecursive(argc, argv, &nonoptions);
+ if(Debug.isOn("options")){
+ for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
+ iend = nonoptions.end(); i != iend; ++i){
+ Debug("options") << "nonoptions " << *i << std::endl;
+ }
+ }
+
+ return nonoptions;
+}
+
+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 Options::parseOptionsRecursive(int argc,
+ char* argv[],
+ std::vector<std::string>* nonoptions)
+{
+
+ if(Debug.isOn("options")) {
+ Debug("options") << "starting a new parseOptionsRecursive 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 parseOptions().
// This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
#endif /* HAVE_DECL_OPTRESET */
- // find the base name of the program
- const char *x = strrchr(progName, '/');
- if(x != NULL) {
- progName = x + 1;
- }
- d_holder->binary_name = std::string(progName);
-
- int extra_argc = 1;
- char **extra_argv = (char**) malloc(2 * sizeof(char*));
- extra_argv[0] = NULL;
- extra_argv[1] = NULL;
-
- int extra_optind = 0, main_optind = 0;
+ // 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;
- int *optind_ref = &main_optind;
- char** argv = main_argv;
- std::vector<std::string> nonOptions;
+ while(true) { // Repeat Forever
- 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
- if(optind_ref != &extra_optind) {
- optreset = 1; // on BSD getopt() (e.g. Mac OS), might 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}",
- 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;
- while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') {
- extra_argv[i][0] = '\0';
- ++i;
- }
- extra_argc = 1;
- extra_optind = 0;
- } else {
- Debug("preemptGetopt") << "-- more preempt args" << std::endl;
- extra_optind = optind;
- }
+
+ 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;
}
- if(c == -1) {
-#if HAVE_DECL_OPTRESET
- if(optind_ref != &main_optind) {
- optreset = 1; // on BSD getopt() (e.g. Mac OS), might 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;
- }
- Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
-#if defined(__MINGW32__) || defined(__MINGW64__)
- if(optreset == 1 && optind > 1) {
- // on mingw, optreset will reset the optind, so we have to
- // manually advance argc, argv
- main_argv[optind - 1] = main_argv[0];
- argv = main_argv += optind - 1;
- argc -= optind - 1;
- old_optind = optind = main_optind = 1;
- if(argc > 0) {
- Debug("options") << "looking at : " << argv[0] << std::endl;
- }
- /*c = getopt_long(argc, main_argv,
- "+:${all_modules_short_options}",
+
+
+ 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);
- Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl;
- Debug("options") << "optind was reset to " << optind << std::endl;
- optind = main_optind;
- Debug("options") << "I restored optind to " << optind << std::endl;*/
- }
-#endif /* __MINGW32__ || __MINGW64__ */
- Debug("options") << "[ argc == " << argc
- << ", main_argv == " << main_argv << " ]" << std::endl;
- c = getopt_long(argc, main_argv,
- "+:${all_modules_short_options}",
- cmdlineOptions, NULL);
- main_optind = optind;
- Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
- << std::endl;
- Debug("options") << "[ next option will be at pos: " << optind << " ]"
- << std::endl;
- if(c == -1) {
+ // 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;
- break;
+ for(int index = optind; index < argc; ++index) {
+ Debug("options") << "remaining " << argv[index] << std::endl;
+ }
}
- option = argv[old_optind == 0 ? 1 : old_optind];
- optionarg = (optarg == NULL) ? "" : optarg;
+ break;
}
+ option = argv[old_optind == 0 ? 1 : old_optind];
+ optionarg = (optarg == NULL) ? "" : optarg;
+
Debug("preemptGetopt") << "processing option " << c
<< " (`" << char(c) << "'), " << option << std::endl;
- switch(c) {
-${all_modules_option_handlers}
-
-#line 709 "${template}"
+ // clang-format off
+ switch(c)
+ {
+${options_handler}$
- case ':':
+ 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:
- 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(formatThreadOptionException(option));
- }
- 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(formatThreadOptionException(option));
- }
- if(threadArgv.size() <= size_t(tnum)) {
- threadArgv.resize(tnum + 1);
- }
- if(threadArgv[tnum] != "") {
- threadArgv[tnum] += " ";
- }
- if(*end == '\0') { // e.g., we have --thread0 "foo"
- if(argc <= optind) {
- 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 `") + option +
- "' 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;
- }
+ throw OptionException(std::string("option `") + option
+ + "' missing its required argument");
- throw OptionException(std::string("can't understand option `") + option +
- "'" + suggestCommandLineOptions(option));
+ case '?':
+ default:
+ throw OptionException(std::string("can't understand option `") + option
+ + "'" + suggestCommandLineOptions(option));
}
}
+ // clang-format on
- Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
-
- free(extra_argv);
- for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end();
- i != iend; ++i)
- {
- char* current = *i;
- #warning "TODO: Unit tests fail if garbage collection is done here."
- //free(current);
- }
- allocated.clear();
-
- return nonOptions;
+ Debug("options") << "got " << nonoptions->size()
+ << " non-option arguments." << std::endl;
}
-std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
- DidYouMean didYouMean;
+// clang-format off
+std::vector<std::vector<std::string> > Options::getOptions() const
+{
+ std::vector< std::vector<std::string> > opts;
- const char* opt;
- for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
- didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
- }
+ ${options_getoptions}$
- return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
+ return opts;
}
+// clang-format on
-static const char* smtOptions[] = {
- ${all_modules_smt_options},
-#line 790 "${template}"
- NULL
-};/* smtOptions[] */
-
-std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
- std::vector<std::string> suggestions;
-
- const char* opt;
- for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
- if(std::strstr(opt, optionName.c_str()) != NULL) {
- suggestions.push_back(opt);
- }
+void Options::setOption(const std::string& key, const std::string& optionarg)
+{
+ Trace("options") << "setOption(" << key << ", " << optionarg << ")"
+ << std::endl;
+ // first update this object
+ setOptionInternal(key, optionarg);
+ // then, notify the provided listener
+ if (d_olisten != nullptr)
+ {
+ d_olisten->notifySetOption(key);
}
-
- return suggestions;
}
-std::vector< std::vector<std::string> > Options::getOptions() const throw() {
- std::vector< std::vector<std::string> > opts;
-
- ${all_modules_get_options}
+// clang-format off
+void Options::setOptionInternal(const std::string& key,
+ const std::string& optionarg)
+{
+ options::OptionsHandler* handler = d_handler;
+ ${setoption_handlers}$
+ throw UnrecognizedOptionException(key);
+}
+// clang-format on
-#line 813 "${template}"
+// clang-format off
+std::string Options::getOption(const std::string& key) const
+{
+ Trace("options") << "Options::getOption(" << key << ")" << std::endl;
+ ${getoption_handlers}$
- return opts;
+ throw UnrecognizedOptionException(key);
}
+// clang-format on
+} // namespace cvc5
-#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
-#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
-
-}/* CVC4 namespace */