src/options/options_template.cpp

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