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_beforeSearchListeners()
 235     , d_tlimitListeners()
 236     , d_tlimitPerListeners()
 237     , d_rlimitListeners()
 238     , d_rlimitPerListeners()
 239 {}
 240
 241 Options::~Options() {
 242   delete d_handler;
 243   delete d_holder;
 244 }
 245
 246 void Options::copyValues(const Options& options){
 247   if(this != &options) {
 248     delete d_holder;
 249     d_holder = new options::OptionsHolder(*options.d_holder);
 250   }
 251 }
 252
 253 std::string Options::formatThreadOptionException(const std::string& option) {
 254   std::stringstream ss;
 255   ss << "can't understand option `" << option
 256      << "': expected something like --threadN=\"--option1 --option2\","
 257      << " where N is a nonnegative integer";
 258   return ss.str();
 259 }
 260
 261 ListenerCollection::Registration* Options::registerAndNotify(
 262     ListenerCollection& collection, Listener* listener, bool notify)
 263 {
 264   ListenerCollection::Registration* registration =
 265       collection.registerListener(listener);
 266   if(notify) {
 267     try
 268     {
 269       listener->notify();
 270     }
 271     catch (OptionException& e)
 272     {
 273       // It can happen that listener->notify() throws an OptionException. In
 274       // that case, we have to make sure that we delete the registration of our
 275       // listener before rethrowing the exception. Otherwise the
 276       // ListenerCollection deconstructor will complain that not all
 277       // registrations have been removed before invoking the deconstructor.
 278       delete registration;
 279       throw OptionException(e.getRawMessage());
 280     }
 281   }
 282   return registration;
 283 }
 284
 285 ListenerCollection::Registration* Options::registerBeforeSearchListener(
 286    Listener* listener)
 287 {
 288   return d_beforeSearchListeners.registerListener(listener);
 289 }
 290
 291 ListenerCollection::Registration* Options::registerTlimitListener(
 292    Listener* listener, bool notifyIfSet)
 293 {
 294   bool notify = notifyIfSet &&
 295       wasSetByUser(options::cumulativeMillisecondLimit);
 296   return registerAndNotify(d_tlimitListeners, listener, notify);
 297 }
 298
 299 ListenerCollection::Registration* Options::registerTlimitPerListener(
 300    Listener* listener, bool notifyIfSet)
 301 {
 302   bool notify = notifyIfSet && wasSetByUser(options::perCallMillisecondLimit);
 303   return registerAndNotify(d_tlimitPerListeners, listener, notify);
 304 }
 305
 306 ListenerCollection::Registration* Options::registerRlimitListener(
 307    Listener* listener, bool notifyIfSet)
 308 {
 309   bool notify = notifyIfSet && wasSetByUser(options::cumulativeResourceLimit);
 310   return registerAndNotify(d_rlimitListeners, listener, notify);
 311 }
 312
 313 ListenerCollection::Registration* Options::registerRlimitPerListener(
 314    Listener* listener, bool notifyIfSet)
 315 {
 316   bool notify = notifyIfSet && wasSetByUser(options::perCallResourceLimit);
 317   return registerAndNotify(d_rlimitPerListeners, listener, notify);
 318 }
 319
 320 ListenerCollection::Registration* Options::registerUseTheoryListListener(
 321    Listener* listener, bool notifyIfSet)
 322 {
 323   bool notify = notifyIfSet && wasSetByUser(options::useTheoryList);
 324   return registerAndNotify(d_useTheoryListListeners, listener, notify);
 325 }
 326
 327 ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
 328     Listener* listener, bool notifyIfSet)
 329 {
 330   bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth);
 331   return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify);
 332 }
 333
 334 ListenerCollection::Registration* Options::registerSetDefaultExprDagListener(
 335     Listener* listener, bool notifyIfSet)
 336 {
 337   bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh);
 338   return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify);
 339 }
 340
 341 ListenerCollection::Registration* Options::registerSetPrintExprTypesListener(
 342     Listener* listener, bool notifyIfSet)
 343 {
 344   bool notify = notifyIfSet && wasSetByUser(options::printExprTypes);
 345   return registerAndNotify(d_setPrintExprTypesListeners, listener, notify);
 346 }
 347
 348 ListenerCollection::Registration* Options::registerSetDumpModeListener(
 349     Listener* listener, bool notifyIfSet)
 350 {
 351   bool notify = notifyIfSet && wasSetByUser(options::dumpModeString);
 352   return registerAndNotify(d_setDumpModeListeners, listener, notify);
 353 }
 354
 355 ListenerCollection::Registration* Options::registerSetPrintSuccessListener(
 356     Listener* listener, bool notifyIfSet)
 357 {
 358   bool notify = notifyIfSet && wasSetByUser(options::printSuccess);
 359   return registerAndNotify(d_setPrintSuccessListeners, listener, notify);
 360 }
 361
 362 ListenerCollection::Registration* Options::registerDumpToFileNameListener(
 363     Listener* listener, bool notifyIfSet)
 364 {
 365   bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName);
 366   return registerAndNotify(d_dumpToFileListeners, listener, notify);
 367 }
 368
 369 ListenerCollection::Registration*
 370 Options::registerSetRegularOutputChannelListener(
 371     Listener* listener, bool notifyIfSet)
 372 {
 373   bool notify = notifyIfSet && wasSetByUser(options::regularChannelName);
 374   return registerAndNotify(d_setRegularChannelListeners, listener, notify);
 375 }
 376
 377 ListenerCollection::Registration*
 378 Options::registerSetDiagnosticOutputChannelListener(
 379     Listener* listener, bool notifyIfSet)
 380 {
 381   bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName);
 382   return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
 383 }
 384
 385 ListenerCollection::Registration*
 386 Options::registerSetReplayLogFilename(
 387     Listener* listener, bool notifyIfSet)
 388 {
 389   bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename);
 390   return registerAndNotify(d_setReplayFilenameListeners, listener, notify);
 391 }
 392
 393 ${custom_handlers}$
 394
 395
 396 #ifdef CVC4_DEBUG
 397 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
 398 #else /* CVC4_DEBUG */
 399 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
 400 #endif /* CVC4_DEBUG */
 401
 402 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
 403 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
 404 #else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 405 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
 406 #endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 407
 408 options::OptionsHolder::OptionsHolder() :
 409   ${module_defaults}$
 410 {
 411 }
 412
 413
 414 static const std::string mostCommonOptionsDescription = "\
 415 Most commonly-used CVC4 options:\n"
 416 ${help_common}$;
 417
 418
 419 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 420 \n\
 421 Additional CVC4 options:\n"
 422 ${help_others}$;
 423
 424
 425 static const std::string optionsFootnote = "\n\
 426 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
 427     sense of the option.\n\
 428 ";
 429
 430 static const std::string languageDescription =
 431     "\
 432 Languages currently supported as arguments to the -L / --lang option:\n\
 433   auto                           attempt to automatically determine language\n\
 434   cvc4 | presentation | pl       CVC4 presentation language\n\
 435   smt1 | smtlib1                 SMT-LIB format 1.2\n\
 436   smt | smtlib | smt2 |\n\
 437   smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
 438   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
 439   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
 440   smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
 441   tptp                           TPTP format (cnf, fof and tff)\n\
 442   sygus                          SyGuS format\n\
 443 \n\
 444 Languages currently supported as arguments to the --output-lang option:\n\
 445   auto                           match output language to input language\n\
 446   cvc4 | presentation | pl       CVC4 presentation language\n\
 447   cvc3                           CVC3 presentation language\n\
 448   smt | smtlib | smt2 |\n\
 449   smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
 450   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
 451   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
 452   smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
 453   tptp                           TPTP format\n\
 454   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
 455   ast                            internal format (simple syntax trees)\n\
 456 ";
 457
 458 std::string Options::getDescription() const {
 459   return optionsDescription;
 460 }
 461
 462 void Options::printUsage(const std::string msg, std::ostream& out) {
 463   out << msg << optionsDescription << std::endl
 464       << optionsFootnote << std::endl << std::flush;
 465 }
 466
 467 void Options::printShortUsage(const std::string msg, std::ostream& out) {
 468   out << msg << mostCommonOptionsDescription << std::endl
 469       << optionsFootnote << std::endl
 470       << "For full usage, please use --help."
 471       << std::endl << std::endl << std::flush;
 472 }
 473
 474 void Options::printLanguageHelp(std::ostream& out) {
 475   out << languageDescription << std::flush;
 476 }
 477
 478 /**
 479  * This is a table of long options.  By policy, each short option
 480  * should have an equivalent long option (but the reverse isn't the
 481  * case), so this table should thus contain all command-line options.
 482  *
 483  * Each option in this array has four elements:
 484  *
 485  * 1. the long option string
 486  * 2. argument behavior for the option:
 487  *    no_argument - no argument permitted
 488  *    required_argument - an argument is expected
 489  *    optional_argument - an argument is permitted but not required
 490  * 3. this is a pointer to an int which is set to the 4th entry of the
 491  *    array if the option is present; or NULL, in which case
 492  *    getopt_long() returns the 4th entry
 493  * 4. the return value for getopt_long() when this long option (or the
 494  *    value to set the 3rd entry to; see #3)
 495  *
 496  * If you add something here, you should add it in src/main/usage.h
 497  * also, to document it.
 498  *
 499  * If you add something that has a short option equivalent, you should
 500  * add it to the getopt_long() call in parseOptions().
 501  */
 502 static struct option cmdlineOptions[] = {
 503   ${cmdline_options}$
 504   { NULL, no_argument, NULL, '\0' }
 505 };/* cmdlineOptions */
 506
 507
 508 // static void preemptGetopt(int& argc, char**& argv, const char* opt) {
 509
 510 //   Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
 511
 512 //   AlwaysAssert(opt != NULL && *opt != '\0');
 513 //   AlwaysAssert(strlen(opt) <= maxoptlen);
 514
 515 //   ++argc;
 516 //   unsigned i = 1;
 517 //   while(argv[i] != NULL && argv[i][0] != '\0') {
 518 //     ++i;
 519 //   }
 520
 521 //   if(argv[i] == NULL) {
 522 //     argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
 523 //     for(unsigned j = i; j < i + 5; ++j) {
 524 //       argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
 525 //       argv[j][0] = '\0';
 526 //     }
 527 //     argv[i + 5] = NULL;
 528 //   }
 529
 530 //   strncpy(argv[i], opt, maxoptlen - 1);
 531 //   argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
 532 // }
 533
 534 namespace options {
 535
 536 /** Set a given Options* as "current" just for a particular scope. */
 537 class OptionsGuard {
 538   Options** d_field;
 539   Options* d_old;
 540 public:
 541   OptionsGuard(Options** field, Options* opts) :
 542     d_field(field),
 543     d_old(*field) {
 544     *field = opts;
 545   }
 546   ~OptionsGuard() {
 547     *d_field = d_old;
 548   }
 549 };/* class OptionsGuard */
 550
 551 }/* CVC4::options namespace */
 552
 553 /**
 554  * Parse argc/argv and put the result into a CVC4::Options.
 555  * The return value is what's left of the command line (that is, the
 556  * non-option arguments).
 557  *
 558  * Throws OptionException on failures.
 559  */
 560 std::vector<std::string> Options::parseOptions(Options* options,
 561                                                int argc,
 562                                                char* argv[])
 563 {
 564   Assert(options != NULL);
 565   Assert(argv != NULL);
 566
 567   options::OptionsGuard guard(&s_current, options);
 568
 569   const char *progName = argv[0];
 570
 571   // To debug options parsing, you may prefer to simply uncomment this
 572   // and recompile. Debug flags have not been parsed yet so these have
 573   // not been set.
 574   //DebugChannel.on("options");
 575
 576   Debug("options") << "Options::parseOptions == " << options << std::endl;
 577   Debug("options") << "argv == " << argv << std::endl;
 578
 579   // Find the base name of the program.
 580   const char *x = strrchr(progName, '/');
 581   if(x != NULL) {
 582     progName = x + 1;
 583   }
 584   options->d_holder->binary_name = std::string(progName);
 585
 586   ArgumentExtender* argumentExtender = new ArgumentExtenderImplementation();
 587   for(int position = 1; position < argc; position++) {
 588     argumentExtender->pushBackArgument(argv[position]);
 589   }
 590
 591   std::vector<std::string> nonoptions;
 592   parseOptionsRecursive(options, argumentExtender, &nonoptions);
 593   if(Debug.isOn("options")){
 594     for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
 595           iend = nonoptions.end(); i != iend; ++i){
 596       Debug("options") << "nonoptions " << *i << std::endl;
 597     }
 598   }
 599
 600   delete argumentExtender;
 601   return nonoptions;
 602 }
 603
 604 void Options::parseOptionsRecursive(Options* options,
 605                                     ArgumentExtender* extender,
 606                                     std::vector<std::string>* nonoptions)
 607 {
 608   int argc;
 609   char** argv;
 610
 611   extender->movePreemptionsToArguments();
 612   extender->pushFrontArgument("");
 613   extender->getArguments(&argc, &argv);
 614
 615   if(Debug.isOn("options")) {
 616     Debug("options") << "starting a new parseOptionsRecursive with "
 617                      << argc << " arguments" << std::endl;
 618     for( int i = 0; i < argc ; i++ ){
 619       Assert(argv[i] != NULL);
 620       Debug("options") << "  argv[" << i << "] = " << argv[i] << std::endl;
 621     }
 622   }
 623
 624   // Having this synonym simplifies the generation code in mkoptions.
 625   options::OptionsHandler* handler = options->d_handler;
 626   options::OptionsHolder* holder = options->d_holder;
 627
 628   // Reset getopt(), in the case of multiple calls to parseOptions().
 629   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
 630   optind = 0;
 631 #if HAVE_DECL_OPTRESET
 632   optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 633 #endif /* HAVE_DECL_OPTRESET */
 634
 635
 636   int main_optind = 0;
 637   int old_optind;
 638
 639
 640   while(true) { // Repeat Forever
 641
 642     if(extender->hasPreemptions()){
 643       // Stop this round of parsing. We now parse recursively
 644       // to start on a new character array for argv.
 645       parseOptionsRecursive(options, extender, nonoptions);
 646       break;
 647     }
 648
 649     optopt = 0;
 650     std::string option, optionarg;
 651
 652     optind = main_optind;
 653     old_optind = main_optind;
 654     //optind_ref = &main_optind;
 655     //argv = main_argv;
 656
 657     // If we encounter an element that is not at zero and does not start
 658     // with a "-", this is a non-option. We consume this element as a
 659     // non-option.
 660     if (main_optind > 0 && main_optind < argc &&
 661         argv[main_optind][0] != '-') {
 662       Debug("options") << "enqueueing " << argv[main_optind]
 663                        << " as a non-option." << std::endl;
 664       nonoptions->push_back(argv[main_optind]);
 665       ++main_optind;
 666       extender->popFrontArgument();
 667       continue;
 668     }
 669
 670
 671     Debug("options") << "[ before, main_optind == " << main_optind << " ]"
 672                      << std::endl;
 673     Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
 674     Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
 675                      << std::endl;
 676     int c = getopt_long(argc, argv,
 677                         "+:${options_short}$",
 678                         cmdlineOptions, NULL);
 679
 680     while(main_optind < optind) {
 681       main_optind++;
 682       extender->popFrontArgument();
 683     }
 684
 685     Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
 686                      << "[ next option will be at pos: " << optind << " ]"
 687                      << std::endl;
 688
 689     // The initial getopt_long call should always determine that argv[0]
 690     // is not an option and returns -1. We always manually advance beyond
 691     // this element.
 692     //
 693     // We have to reinitialize optind to 0 instead of 1 as we need to support
 694     // changing the argv array passed to getopt.
 695     // This is needed as are using GNU extensions.
 696     // From: http://man7.org/linux/man-pages/man3/getopt.3.html
 697     // A program that scans multiple argument vectors, or rescans the same
 698     // vector more than once, and wants to make use of GNU extensions such
 699     // as '+' and '-' at the start of optstring, or changes the value of
 700     //  POSIXLY_CORRECT between scans, must reinitialize getopt() by
 701     //  resetting optind to 0, rather than the traditional value of 1.
 702     //  (Resetting to 0 forces the invocation of an internal initialization
 703     //  routine that rechecks POSIXLY_CORRECT and checks for GNU extensions
 704     //  in optstring.)
 705     if ( old_optind == 0  && c == -1 ) {
 706       Assert(main_optind > 0);
 707       continue;
 708     }
 709
 710     if ( c == -1 ) {
 711       if(Debug.isOn("options")) {
 712         Debug("options") << "done with option parsing" << std::endl;
 713         for(int index = optind; index < argc; ++index) {
 714           Debug("options") << "remaining " << argv[index] << std::endl;
 715         }
 716       }
 717       break;
 718     }
 719
 720     option = argv[old_optind == 0 ? 1 : old_optind];
 721     optionarg = (optarg == NULL) ? "" : optarg;
 722
 723     Debug("preemptGetopt") << "processing option " << c
 724                            << " (`" << char(c) << "'), " << option << std::endl;
 725
 726     switch(c) {
 727 ${options_handler}$
 728
 729
 730     case ':':
 731       // This can be a long or short option, and the way to get at the
 732       // name of it is different.
 733       throw OptionException(std::string("option `") + option +
 734                             "' missing its required argument");
 735
 736     case '?':
 737     default:
 738       if( ( optopt == 0 ||
 739             ( optopt >= ${option_value_begin}$ &&
 740               optopt <= ${option_value_end}$ )
 741           ) && !strncmp(argv[optind - 1], "--thread", 8) &&
 742           strlen(argv[optind - 1]) > 8 )
 743       {
 744         if(! isdigit(argv[optind - 1][8])) {
 745           throw OptionException(formatThreadOptionException(option));
 746         }
 747         std::vector<std::string>& threadArgv = holder->threadArgv;
 748         char *end;
 749         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
 750         if(tnum < 0 || (*end != '\0' && *end != '=')) {
 751           throw OptionException(formatThreadOptionException(option));
 752         }
 753         if(threadArgv.size() <= size_t(tnum)) {
 754           threadArgv.resize(tnum + 1);
 755         }
 756         if(threadArgv[tnum] != "") {
 757           threadArgv[tnum] += " ";
 758         }
 759         if(*end == '\0') { // e.g., we have --thread0 "foo"
 760           if(argc <= optind) {
 761             throw OptionException(std::string("option `") + option +
 762                                   "' missing its required argument");
 763           }
 764           Debug("options") << "thread " << tnum << " gets option "
 765                            << argv[optind] << std::endl;
 766           threadArgv[tnum] += argv[main_optind];
 767           main_optind++;
 768         } else { // e.g., we have --thread0="foo"
 769           if(end[1] == '\0') {
 770             throw OptionException(std::string("option `") + option +
 771                                   "' missing its required argument");
 772           }
 773           Debug("options") << "thread " << tnum << " gets option "
 774                            << (end + 1) << std::endl;
 775           threadArgv[tnum] += end + 1;
 776         }
 777         Debug("options") << "thread " << tnum << " now has "
 778                          << threadArgv[tnum] << std::endl;
 779         break;
 780       }
 781
 782       throw OptionException(std::string("can't understand option `") + option +
 783                             "'" + suggestCommandLineOptions(option));
 784     }
 785   }
 786
 787   Debug("options") << "got " << nonoptions->size()
 788                    << " non-option arguments." << std::endl;
 789
 790   free(argv);
 791 }
 792
 793 std::string Options::suggestCommandLineOptions(const std::string& optionName)
 794 {
 795   DidYouMean didYouMean;
 796
 797   const char* opt;
 798   for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
 799     didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
 800   }
 801
 802   return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
 803 }
 804
 805 static const char* smtOptions[] = {
 806   ${options_smt}$
 807   NULL
 808 };/* smtOptions[] */
 809
 810 std::vector<std::string> Options::suggestSmtOptions(
 811     const std::string& optionName)
 812 {
 813   std::vector<std::string> suggestions;
 814
 815   const char* opt;
 816   for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
 817     if(std::strstr(opt, optionName.c_str()) != NULL) {
 818       suggestions.push_back(opt);
 819     }
 820   }
 821
 822   return suggestions;
 823 }
 824
 825 std::vector<std::vector<std::string> > Options::getOptions() const
 826 {
 827   std::vector< std::vector<std::string> > opts;
 828
 829   ${options_getoptions}$
 830
 831
 832   return opts;
 833 }
 834
 835 void Options::setOption(const std::string& key, const std::string& optionarg)
 836 {
 837   options::OptionsHandler* handler = d_handler;
 838   Options *options = Options::current();
 839   Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")"
 840                    << std::endl;
 841
 842   ${setoption_handlers}$
 843
 844
 845   throw UnrecognizedOptionException(key);
 846 }
 847
 848 std::string Options::getOption(const std::string& key) const
 849 {
 850   Trace("options") << "SMT getOption(" << key << ")" << std::endl;
 851
 852   ${getoption_handlers}$
 853
 854
 855   throw UnrecognizedOptionException(key);
 856 }
 857
 858 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 859 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 860
 861 }  // namespace CVC4