src/options/options_template.cpp

   1 /*********************                                                        */
   2 /*! \file options_template.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Kshitij Bansal
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Contains code for handling command-line options.
  13  **
  14  ** Contains code for handling command-line options
  15  **/
  16
  17 #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
  18 // force use of optreset; mingw32 croaks on argv-switching otherwise
  19 #  include "cvc4autoconfig.h"
  20 #  define _BSD_SOURCE
  21 #  undef HAVE_DECL_OPTRESET
  22 #  define HAVE_DECL_OPTRESET 1
  23 #  define CVC4_IS_NOT_REALLY_BSD
  24 #endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
  25
  26 #ifdef __MINGW64__
  27 extern int optreset;
  28 #endif /* __MINGW64__ */
  29
  30 #include <getopt.h>
  31
  32 // clean up
  33 #ifdef CVC4_IS_NOT_REALLY_BSD
  34 #  undef _BSD_SOURCE
  35 #endif /* CVC4_IS_NOT_REALLY_BSD */
  36
  37 #include <unistd.h>
  38 #include <string.h>
  39 #include <stdint.h>
  40 #include <time.h>
  41
  42 #include <cstdio>
  43 #include <cstdlib>
  44 #include <cstring>
  45 #include <iomanip>
  46 #include <new>
  47 #include <string>
  48 #include <sstream>
  49 #include <limits>
  50
  51 #include "base/cvc4_assert.h"
  52 #include "base/exception.h"
  53 #include "base/output.h"
  54 #include "base/tls.h"
  55 #include "options/argument_extender.h"
  56 #include "options/didyoumean.h"
  57 #include "options/language.h"
  58 #include "options/options_handler.h"
  59
  60 ${include_all_option_headers}
  61
  62 #line 63 "${template}"
  63
  64 #include "options/options_holder.h"
  65 #include "cvc4autoconfig.h"
  66 #include "options/base_handlers.h"
  67
  68 ${option_handler_includes}
  69
  70 #line 71 "${template}"
  71
  72 using namespace CVC4;
  73 using namespace CVC4::options;
  74
  75 namespace CVC4 {
  76
  77 CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
  78
  79
  80
  81 /**
  82  * This is a default handler for options of built-in C++ type.  This
  83  * template is really just a helper for the handleOption() template,
  84  * below.  Variants of this template handle numeric and non-numeric,
  85  * integral and non-integral, signed and unsigned C++ types.
  86  * handleOption() makes sure to instantiate the right one.
  87  *
  88  * This implements default behavior when e.g. an option is
  89  * unsigned but the user specifies a negative argument; etc.
  90  */
  91 template <class T, bool is_numeric, bool is_integer>
  92 struct OptionHandler {
  93   static T handle(std::string option, std::string optionarg);
  94 };/* struct OptionHandler<> */
  95
  96 /** Variant for integral C++ types */
  97 template <class T>
  98 struct OptionHandler<T, true, true> {
  99   static bool stringToInt(T& t, const std::string& str) {
 100     std::istringstream ss(str);
 101     ss >> t;
 102     char tmp;
 103     return !(ss.fail() || ss.get(tmp));
 104   }
 105
 106   static bool containsMinus(const std::string& str) {
 107     return str.find('-') != std::string::npos;
 108   }
 109
 110   static T handle(const std::string& option, const std::string& optionarg) {
 111     try {
 112       T i;
 113       bool success = stringToInt(i, optionarg);
 114
 115       if(!success){
 116         throw OptionException(option + ": failed to parse "+ optionarg +
 117                               " as an integer of the appropraite type.");
 118       }
 119
 120       // Depending in the platform unsigned numbers with '-' signs may parse.
 121       // Reject these by looking for any minus if it is not signed.
 122       if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
 123         // unsigned type but user gave negative argument
 124         throw OptionException(option + " requires a nonnegative argument");
 125       } else if(i < std::numeric_limits<T>::min()) {
 126         // negative overflow for type
 127         std::stringstream ss;
 128         ss << option << " requires an argument >= "
 129            << std::numeric_limits<T>::min();
 130         throw OptionException(ss.str());
 131       } else if(i > std::numeric_limits<T>::max()) {
 132         // positive overflow for type
 133         std::stringstream ss;
 134         ss << option << " requires an argument <= "
 135            << std::numeric_limits<T>::max();
 136         throw OptionException(ss.str());
 137       }
 138
 139       return i;
 140
 141       // if(std::numeric_limits<T>::is_signed) {
 142       //   return T(i.getLong());
 143       // } else {
 144       //   return T(i.getUnsignedLong());
 145       // }
 146     } catch(std::invalid_argument&) {
 147       // user gave something other than an integer
 148       throw OptionException(option + " requires an integer argument");
 149     }
 150   }
 151 };/* struct OptionHandler<T, true, true> */
 152
 153 /** Variant for numeric but non-integral C++ types */
 154 template <class T>
 155 struct OptionHandler<T, true, false> {
 156   static T handle(std::string option, std::string optionarg) {
 157     std::stringstream in(optionarg);
 158     long double r;
 159     in >> r;
 160     if(! in.eof()) {
 161       // we didn't consume the whole string (junk at end)
 162       throw OptionException(option + " requires a numeric argument");
 163     }
 164
 165     if(! std::numeric_limits<T>::is_signed && r < 0.0) {
 166       // unsigned type but user gave negative value
 167       throw OptionException(option + " requires a nonnegative argument");
 168     } else if(r < -std::numeric_limits<T>::max()) {
 169       // negative overflow for type
 170       std::stringstream ss;
 171       ss << option << " requires an argument >= "
 172          << -std::numeric_limits<T>::max();
 173       throw OptionException(ss.str());
 174     } else if(r > std::numeric_limits<T>::max()) {
 175       // positive overflow for type
 176       std::stringstream ss;
 177       ss << option << " requires an argument <= "
 178          << std::numeric_limits<T>::max();
 179       throw OptionException(ss.str());
 180     }
 181
 182     return T(r);
 183   }
 184 };/* struct OptionHandler<T, true, false> */
 185
 186 /** Variant for non-numeric C++ types */
 187 template <class T>
 188 struct OptionHandler<T, false, false> {
 189   static T handle(std::string option, std::string optionarg) {
 190     T::unsupported_handleOption_call___please_write_me;
 191     // The above line causes a compiler error if this version of the template
 192     // is ever instantiated (meaning that a specialization is missing).  So
 193     // don't worry about the segfault in the next line, the "return" is only
 194     // there to keep the compiler from giving additional, distracting errors
 195     // and warnings.
 196     return *(T*)0;
 197   }
 198 };/* struct OptionHandler<T, false, false> */
 199
 200 /** Handle an option of type T in the default way. */
 201 template <class T>
 202 T handleOption(std::string option, std::string optionarg) {
 203   return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
 204 }
 205
 206 /** Handle an option of type std::string in the default way. */
 207 template <>
 208 std::string handleOption<std::string>(std::string option, std::string optionarg) {
 209   return optionarg;
 210 }
 211
 212 /**
 213  * Run handler, and any user-given predicates, for option T.
 214  * If a user specifies a :handler or :predicates, it overrides this.
 215  */
 216 template <class T>
 217 typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) {
 218   // By default, parse the option argument in a way appropriate for its type.
 219   // E.g., for "unsigned int" options, ensure that the provided argument is
 220   // a nonnegative integer that fits in the unsigned int type.
 221
 222   return handleOption<typename T::type>(option, optionarg);
 223 }
 224
 225 template <class T>
 226 void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) {
 227   // By default, nothing to do for bool.  Users add things with
 228   // :predicate in options files to provide custom checking routines
 229   // that can throw exceptions.
 230 }
 231
 232
 233 Options::Options()
 234     : d_holder(new options::OptionsHolder())
 235     , d_handler(new options::OptionsHandler(this))
 236     , d_forceLogicListeners()
 237     , d_beforeSearchListeners()
 238     , d_tlimitListeners()
 239     , d_tlimitPerListeners()
 240     , d_rlimitListeners()
 241     , d_rlimitPerListeners()
 242 {}
 243
 244 Options::~Options() {
 245   delete d_handler;
 246   delete d_holder;
 247 }
 248
 249 void Options::copyValues(const Options& options){
 250   if(this != &options) {
 251     delete d_holder;
 252     d_holder = new options::OptionsHolder(*options.d_holder);
 253   }
 254 }
 255
 256 std::string Options::formatThreadOptionException(const std::string& option) {
 257   std::stringstream ss;
 258   ss << "can't understand option `" << option
 259      << "': expected something like --threadN=\"--option1 --option2\","
 260      << " where N is a nonnegative integer";
 261   return ss.str();
 262 }
 263
 264 ListenerCollection::Registration* Options::registerAndNotify(
 265     ListenerCollection& collection, Listener* listener, bool notify)
 266 {
 267   ListenerCollection::Registration* registration =
 268       collection.registerListener(listener);
 269   if(notify) {
 270     listener->notify();
 271   }
 272   return registration;
 273 }
 274
 275 ListenerCollection::Registration* Options::registerForceLogicListener(
 276     Listener* listener, bool notifyIfSet)
 277 {
 278   bool notify = notifyIfSet && wasSetByUser(options::forceLogicString);
 279   return registerAndNotify(d_forceLogicListeners, listener, notify);
 280 }
 281
 282 ListenerCollection::Registration* Options::registerBeforeSearchListener(
 283    Listener* listener)
 284 {
 285   return d_beforeSearchListeners.registerListener(listener);
 286 }
 287
 288 ListenerCollection::Registration* Options::registerTlimitListener(
 289    Listener* listener, bool notifyIfSet)
 290 {
 291   bool notify = notifyIfSet &&
 292       wasSetByUser(options::cumulativeMillisecondLimit);
 293   return registerAndNotify(d_tlimitListeners, listener, notify);
 294 }
 295
 296 ListenerCollection::Registration* Options::registerTlimitPerListener(
 297    Listener* listener, bool notifyIfSet)
 298 {
 299   bool notify = notifyIfSet && wasSetByUser(options::perCallMillisecondLimit);
 300   return registerAndNotify(d_tlimitPerListeners, listener, notify);
 301 }
 302
 303 ListenerCollection::Registration* Options::registerRlimitListener(
 304    Listener* listener, bool notifyIfSet)
 305 {
 306   bool notify = notifyIfSet && wasSetByUser(options::cumulativeResourceLimit);
 307   return registerAndNotify(d_rlimitListeners, listener, notify);
 308 }
 309
 310 ListenerCollection::Registration* Options::registerRlimitPerListener(
 311    Listener* listener, bool notifyIfSet)
 312 {
 313   bool notify = notifyIfSet && wasSetByUser(options::perCallResourceLimit);
 314   return registerAndNotify(d_rlimitPerListeners, listener, notify);
 315 }
 316
 317 ListenerCollection::Registration* Options::registerUseTheoryListListener(
 318    Listener* listener, bool notifyIfSet)
 319 {
 320   bool notify = notifyIfSet && wasSetByUser(options::useTheoryList);
 321   return registerAndNotify(d_useTheoryListListeners, listener, notify);
 322 }
 323
 324 ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
 325     Listener* listener, bool notifyIfSet)
 326 {
 327   bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth);
 328   return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify);
 329 }
 330
 331 ListenerCollection::Registration* Options::registerSetDefaultExprDagListener(
 332     Listener* listener, bool notifyIfSet)
 333 {
 334   bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh);
 335   return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify);
 336 }
 337
 338 ListenerCollection::Registration* Options::registerSetPrintExprTypesListener(
 339     Listener* listener, bool notifyIfSet)
 340 {
 341   bool notify = notifyIfSet && wasSetByUser(options::printExprTypes);
 342   return registerAndNotify(d_setPrintExprTypesListeners, listener, notify);
 343 }
 344
 345 ListenerCollection::Registration* Options::registerSetDumpModeListener(
 346     Listener* listener, bool notifyIfSet)
 347 {
 348   bool notify = notifyIfSet && wasSetByUser(options::dumpModeString);
 349   return registerAndNotify(d_setDumpModeListeners, listener, notify);
 350 }
 351
 352 ListenerCollection::Registration* Options::registerSetPrintSuccessListener(
 353     Listener* listener, bool notifyIfSet)
 354 {
 355   bool notify = notifyIfSet && wasSetByUser(options::printSuccess);
 356   return registerAndNotify(d_setPrintSuccessListeners, listener, notify);
 357 }
 358
 359 ListenerCollection::Registration* Options::registerDumpToFileNameListener(
 360     Listener* listener, bool notifyIfSet)
 361 {
 362   bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName);
 363   return registerAndNotify(d_dumpToFileListeners, listener, notify);
 364 }
 365
 366 ListenerCollection::Registration*
 367 Options::registerSetRegularOutputChannelListener(
 368     Listener* listener, bool notifyIfSet)
 369 {
 370   bool notify = notifyIfSet && wasSetByUser(options::regularChannelName);
 371   return registerAndNotify(d_setRegularChannelListeners, listener, notify);
 372 }
 373
 374 ListenerCollection::Registration*
 375 Options::registerSetDiagnosticOutputChannelListener(
 376     Listener* listener, bool notifyIfSet)
 377 {
 378   bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName);
 379   return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
 380 }
 381
 382 ListenerCollection::Registration*
 383 Options::registerSetReplayLogFilename(
 384     Listener* listener, bool notifyIfSet)
 385 {
 386   bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename);
 387   return registerAndNotify(d_setReplayFilenameListeners, listener, notify);
 388 }
 389
 390 ${all_custom_handlers}
 391
 392 #line 393 "${template}"
 393
 394 #ifdef CVC4_DEBUG
 395 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
 396 #else /* CVC4_DEBUG */
 397 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
 398 #endif /* CVC4_DEBUG */
 399
 400 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
 401 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
 402 #else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 403 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
 404 #endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 405
 406 options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 407 {
 408 }
 409
 410 #line 411 "${template}"
 411
 412 static const std::string mostCommonOptionsDescription = "\
 413 Most commonly-used CVC4 options:${common_documentation}";
 414
 415 #line 416 "${template}"
 416
 417 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 418 \n\
 419 Additional CVC4 options:${remaining_documentation}";
 420
 421 #line 422 "${template}"
 422
 423 static const std::string optionsFootnote = "\n\
 424 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
 425     sense of the option.\n\
 426 ";
 427
 428 static const std::string languageDescription = "\
 429 Languages currently supported as arguments to the -L / --lang option:\n\
 430   auto                           attempt to automatically determine language\n\
 431   cvc4 | presentation | pl       CVC4 presentation language\n\
 432   smt1 | smtlib1                 SMT-LIB format 1.2\n\
 433   smt | smtlib | smt2 |\n\
 434     smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
 435   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
 436   tptp                           TPTP format (cnf and fof)\n\
 437   sygus                          SyGuS format\n\
 438 \n\
 439 Languages currently supported as arguments to the --output-lang option:\n\
 440   auto                           match output language to input language\n\
 441   cvc4 | presentation | pl       CVC4 presentation language\n\
 442   cvc3                           CVC3 presentation language\n\
 443   smt1 | smtlib1                 SMT-LIB format 1.2\n\
 444   smt | smtlib | smt2 |\n\
 445     smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
 446   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
 447   tptp                           TPTP format\n\
 448   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
 449   ast                            internal format (simple syntax trees)\n\
 450 ";
 451
 452 std::string Options::getDescription() const {
 453   return optionsDescription;
 454 }
 455
 456 void Options::printUsage(const std::string msg, std::ostream& out) {
 457   out << msg << optionsDescription << std::endl
 458       << optionsFootnote << std::endl << std::flush;
 459 }
 460
 461 void Options::printShortUsage(const std::string msg, std::ostream& out) {
 462   out << msg << mostCommonOptionsDescription << std::endl
 463       << optionsFootnote << std::endl
 464       << "For full usage, please use --help."
 465       << std::endl << std::endl << std::flush;
 466 }
 467
 468 void Options::printLanguageHelp(std::ostream& out) {
 469   out << languageDescription << std::flush;
 470 }
 471
 472 /**
 473  * This is a table of long options.  By policy, each short option
 474  * should have an equivalent long option (but the reverse isn't the
 475  * case), so this table should thus contain all command-line options.
 476  *
 477  * Each option in this array has four elements:
 478  *
 479  * 1. the long option string
 480  * 2. argument behavior for the option:
 481  *    no_argument - no argument permitted
 482  *    required_argument - an argument is expected
 483  *    optional_argument - an argument is permitted but not required
 484  * 3. this is a pointer to an int which is set to the 4th entry of the
 485  *    array if the option is present; or NULL, in which case
 486  *    getopt_long() returns the 4th entry
 487  * 4. the return value for getopt_long() when this long option (or the
 488  *    value to set the 3rd entry to; see #3)
 489  *
 490  * If you add something here, you should add it in src/main/usage.h
 491  * also, to document it.
 492  *
 493  * If you add something that has a short option equivalent, you should
 494  * add it to the getopt_long() call in parseOptions().
 495  */
 496 static struct option cmdlineOptions[] = {${all_modules_long_options}
 497   { NULL, no_argument, NULL, '\0' }
 498 };/* cmdlineOptions */
 499
 500 #line 501 "${template}"
 501
 502 // static void preemptGetopt(int& argc, char**& argv, const char* opt) {
 503
 504 //   Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
 505
 506 //   AlwaysAssert(opt != NULL && *opt != '\0');
 507 //   AlwaysAssert(strlen(opt) <= maxoptlen);
 508
 509 //   ++argc;
 510 //   unsigned i = 1;
 511 //   while(argv[i] != NULL && argv[i][0] != '\0') {
 512 //     ++i;
 513 //   }
 514
 515 //   if(argv[i] == NULL) {
 516 //     argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
 517 //     for(unsigned j = i; j < i + 5; ++j) {
 518 //       argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
 519 //       argv[j][0] = '\0';
 520 //     }
 521 //     argv[i + 5] = NULL;
 522 //   }
 523
 524 //   strncpy(argv[i], opt, maxoptlen - 1);
 525 //   argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
 526 // }
 527
 528 namespace options {
 529
 530 /** Set a given Options* as "current" just for a particular scope. */
 531 class OptionsGuard {
 532   CVC4_THREADLOCAL_TYPE(Options*)* d_field;
 533   Options* d_old;
 534 public:
 535   OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) :
 536     d_field(field),
 537     d_old(*field) {
 538     *field = opts;
 539   }
 540   ~OptionsGuard() {
 541     *d_field = d_old;
 542   }
 543 };/* class OptionsGuard */
 544
 545 }/* CVC4::options namespace */
 546
 547 /**
 548  * Parse argc/argv and put the result into a CVC4::Options.
 549  * The return value is what's left of the command line (that is, the
 550  * non-option arguments).
 551  */
 552 std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
 553   options::OptionsGuard guard(&s_current, this);
 554
 555   // Having this synonym simplifies the generation code in mkoptions.
 556   options::OptionsHandler* handler = d_handler;
 557
 558   const char *progName = main_argv[0];
 559
 560   ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen);
 561   std::vector<char*> allocated;
 562
 563   Debug("options") << "main_argv == " << main_argv << std::endl;
 564
 565   // Reset getopt(), in the case of multiple calls to parseOptions().
 566   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
 567   optind = 0;
 568 #if HAVE_DECL_OPTRESET
 569   optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 570 #endif /* HAVE_DECL_OPTRESET */
 571
 572   // find the base name of the program
 573   const char *x = strrchr(progName, '/');
 574   if(x != NULL) {
 575     progName = x + 1;
 576   }
 577   d_holder->binary_name = std::string(progName);
 578
 579   int extra_argc = 1;
 580   char **extra_argv = (char**) malloc(2 * sizeof(char*));
 581   extra_argv[0] = NULL;
 582   extra_argv[1] = NULL;
 583
 584   int extra_optind = 0, main_optind = 0;
 585   int old_optind;
 586   int *optind_ref = &main_optind;
 587
 588   char** argv = main_argv;
 589
 590   std::vector<std::string> nonOptions;
 591
 592   for(;;) {
 593     int c = -1;
 594     optopt = 0;
 595     std::string option, optionarg;
 596     Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind
 597                            << ", extra_argc == " << extra_argc << std::endl;
 598     if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
 599 #if HAVE_DECL_OPTRESET
 600       if(optind_ref != &extra_optind) {
 601         optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 602       }
 603 #endif /* HAVE_DECL_OPTRESET */
 604       old_optind = optind = extra_optind;
 605       optind_ref = &extra_optind;
 606       argv = extra_argv;
 607       Debug("preemptGetopt") << "in preempt code, next arg is "
 608                              << extra_argv[optind == 0 ? 1 : optind]
 609                              << std::endl;
 610       if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') {
 611         InternalError(
 612             "preempted args cannot give non-options command-line args (found `%s')",
 613             extra_argv[extra_optind == 0 ? 1 : extra_optind]);
 614       }
 615       c = getopt_long(extra_argc, extra_argv,
 616                       "+:${all_modules_short_options}",
 617                       cmdlineOptions, NULL);
 618       Debug("preemptGetopt") << "in preempt code"
 619                              << ", c == " << c << " (`" << char(c) << "')"
 620                              << " optind == " << optind << std::endl;
 621       if(optopt == 0 ||
 622          ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
 623         // long option
 624         option = argv[old_optind == 0 ? 1 : old_optind];
 625         optionarg = (optarg == NULL) ? "" : optarg;
 626       } else {
 627         // short option
 628         option = std::string("-") + char(optopt);
 629         optionarg = (optarg == NULL) ? "" : optarg;
 630       }
 631       if(optind >= extra_argc) {
 632         Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
 633         unsigned i = 1;
 634         while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') {
 635           extra_argv[i][0] = '\0';
 636           ++i;
 637         }
 638         extra_argc = 1;
 639         extra_optind = 0;
 640       } else {
 641         Debug("preemptGetopt") << "-- more preempt args" << std::endl;
 642         extra_optind = optind;
 643       }
 644     }
 645     if(c == -1) {
 646 #if HAVE_DECL_OPTRESET
 647       if(optind_ref != &main_optind) {
 648         optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 649       }
 650 #endif /* HAVE_DECL_OPTRESET */
 651       old_optind = optind = main_optind;
 652       optind_ref = &main_optind;
 653       argv = main_argv;
 654       if(main_optind < argc && main_argv[main_optind][0] != '-') {
 655         do {
 656           if(main_optind != 0) {
 657             nonOptions.push_back(main_argv[main_optind]);
 658           }
 659           ++main_optind;
 660         } while(main_optind < argc && main_argv[main_optind][0] != '-');
 661         continue;
 662       }
 663       Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
 664 #if defined(__MINGW32__) || defined(__MINGW64__)
 665       if(optreset == 1 && optind > 1) {
 666         // on mingw, optreset will reset the optind, so we have to
 667         // manually advance argc, argv
 668         main_argv[optind - 1] = main_argv[0];
 669         argv = main_argv += optind - 1;
 670         argc -= optind - 1;
 671         old_optind = optind = main_optind = 1;
 672         if(argc > 0) {
 673           Debug("options") << "looking at : " << argv[0] << std::endl;
 674         }
 675         /*c = getopt_long(argc, main_argv,
 676                         "+:${all_modules_short_options}",
 677                         cmdlineOptions, NULL);
 678         Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl;
 679         Debug("options") << "optind was reset to " << optind << std::endl;
 680         optind = main_optind;
 681         Debug("options") << "I restored optind to " << optind << std::endl;*/
 682       }
 683 #endif /* __MINGW32__ || __MINGW64__ */
 684       Debug("options") << "[ argc == " << argc
 685                        << ", main_argv == " << main_argv << " ]" << std::endl;
 686       c = getopt_long(argc, main_argv,
 687                       "+:${all_modules_short_options}",
 688                       cmdlineOptions, NULL);
 689       main_optind = optind;
 690       Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
 691                        << std::endl;
 692       Debug("options") << "[ next option will be at pos: " << optind << " ]"
 693                        << std::endl;
 694       if(c == -1) {
 695         Debug("options") << "done with option parsing" << std::endl;
 696         break;
 697       }
 698       option = argv[old_optind == 0 ? 1 : old_optind];
 699       optionarg = (optarg == NULL) ? "" : optarg;
 700     }
 701
 702     Debug("preemptGetopt") << "processing option " << c
 703                            << " (`" << char(c) << "'), " << option << std::endl;
 704
 705     switch(c) {
 706 ${all_modules_option_handlers}
 707
 708 #line 709 "${template}"
 709
 710     case ':':
 711       // This can be a long or short option, and the way to get at the
 712       // name of it is different.
 713       throw OptionException(std::string("option `") + option + "' missing its required argument");
 714
 715     case '?':
 716     default:
 717       if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) &&
 718           !strncmp(argv[optind - 1], "--thread", 8) &&
 719           strlen(argv[optind - 1]) > 8 ) {
 720         if(! isdigit(argv[optind - 1][8])) {
 721           throw OptionException(formatThreadOptionException(option));
 722         }
 723         std::vector<std::string>& threadArgv = d_holder->threadArgv;
 724         char *end;
 725         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
 726         if(tnum < 0 || (*end != '\0' && *end != '=')) {
 727           throw OptionException(formatThreadOptionException(option));
 728         }
 729         if(threadArgv.size() <= size_t(tnum)) {
 730           threadArgv.resize(tnum + 1);
 731         }
 732         if(threadArgv[tnum] != "") {
 733           threadArgv[tnum] += " ";
 734         }
 735         if(*end == '\0') { // e.g., we have --thread0 "foo"
 736           if(argc <= optind) {
 737             throw OptionException(std::string("option `") + option
 738                                   + "' missing its required argument");
 739           }
 740           Debug("options") << "thread " << tnum << " gets option "
 741                            << argv[optind] << std::endl;
 742           threadArgv[tnum] += argv[(*optind_ref)++];
 743         } else { // e.g., we have --thread0="foo"
 744           if(end[1] == '\0') {
 745             throw OptionException(std::string("option `") + option +
 746                                   "' missing its required argument");
 747           }
 748           Debug("options") << "thread " << tnum << " gets option " << (end + 1)
 749                            << std::endl;
 750           threadArgv[tnum] += end + 1;
 751         }
 752         Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum]
 753                          << std::endl;
 754         break;
 755       }
 756
 757       throw OptionException(std::string("can't understand option `") + option +
 758                             "'" + suggestCommandLineOptions(option));
 759     }
 760   }
 761
 762   Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
 763
 764   free(extra_argv);
 765   for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end();
 766       i != iend; ++i)
 767   {
 768     char* current = *i;
 769     #warning "TODO: Unit tests fail if garbage collection is done here."
 770     //free(current);
 771   }
 772   allocated.clear();
 773
 774   return nonOptions;
 775 }
 776
 777 std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
 778   DidYouMean didYouMean;
 779
 780   const char* opt;
 781   for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
 782     didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
 783   }
 784
 785   return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
 786 }
 787
 788 static const char* smtOptions[] = {
 789   ${all_modules_smt_options},
 790 #line 790 "${template}"
 791   NULL
 792 };/* smtOptions[] */
 793
 794 std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
 795   std::vector<std::string> suggestions;
 796
 797   const char* opt;
 798   for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
 799     if(std::strstr(opt, optionName.c_str()) != NULL) {
 800       suggestions.push_back(opt);
 801     }
 802   }
 803
 804   return suggestions;
 805 }
 806
 807 std::vector< std::vector<std::string> > Options::getOptions() const throw() {
 808   std::vector< std::vector<std::string> > opts;
 809
 810   ${all_modules_get_options}
 811
 812 #line 813 "${template}"
 813
 814   return opts;
 815 }
 816
 817
 818 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 819 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 820
 821 }/* CVC4 namespace */