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   smt | smtlib | smt2 |\n\
 436   smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
 437   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
 438   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
 439   smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
 440   tptp                           TPTP format (cnf, fof and tff)\n\
 441   sygus                          SyGuS format\n\
 442 \n\
 443 Languages currently supported as arguments to the --output-lang option:\n\
 444   auto                           match output language to input language\n\
 445   cvc4 | presentation | pl       CVC4 presentation language\n\
 446   cvc3                           CVC3 presentation language\n\
 447   smt | smtlib | smt2 |\n\
 448   smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
 449   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
 450   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
 451   smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
 452   tptp                           TPTP format\n\
 453   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
 454   ast                            internal format (simple syntax trees)\n\
 455 ";
 456
 457 std::string Options::getDescription() const {
 458   return optionsDescription;
 459 }
 460
 461 void Options::printUsage(const std::string msg, std::ostream& out) {
 462   out << msg << optionsDescription << std::endl
 463       << optionsFootnote << std::endl << std::flush;
 464 }
 465
 466 void Options::printShortUsage(const std::string msg, std::ostream& out) {
 467   out << msg << mostCommonOptionsDescription << std::endl
 468       << optionsFootnote << std::endl
 469       << "For full usage, please use --help."
 470       << std::endl << std::endl << std::flush;
 471 }
 472
 473 void Options::printLanguageHelp(std::ostream& out) {
 474   out << languageDescription << std::flush;
 475 }
 476
 477 /**
 478  * This is a table of long options.  By policy, each short option
 479  * should have an equivalent long option (but the reverse isn't the
 480  * case), so this table should thus contain all command-line options.
 481  *
 482  * Each option in this array has four elements:
 483  *
 484  * 1. the long option string
 485  * 2. argument behavior for the option:
 486  *    no_argument - no argument permitted
 487  *    required_argument - an argument is expected
 488  *    optional_argument - an argument is permitted but not required
 489  * 3. this is a pointer to an int which is set to the 4th entry of the
 490  *    array if the option is present; or NULL, in which case
 491  *    getopt_long() returns the 4th entry
 492  * 4. the return value for getopt_long() when this long option (or the
 493  *    value to set the 3rd entry to; see #3)
 494  *
 495  * If you add something here, you should add it in src/main/usage.h
 496  * also, to document it.
 497  *
 498  * If you add something that has a short option equivalent, you should
 499  * add it to the getopt_long() call in parseOptions().
 500  */
 501 static struct option cmdlineOptions[] = {
 502   ${cmdline_options}$
 503   { NULL, no_argument, NULL, '\0' }
 504 };/* cmdlineOptions */
 505
 506
 507 // static void preemptGetopt(int& argc, char**& argv, const char* opt) {
 508
 509 //   Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
 510
 511 //   AlwaysAssert(opt != NULL && *opt != '\0');
 512 //   AlwaysAssert(strlen(opt) <= maxoptlen);
 513
 514 //   ++argc;
 515 //   unsigned i = 1;
 516 //   while(argv[i] != NULL && argv[i][0] != '\0') {
 517 //     ++i;
 518 //   }
 519
 520 //   if(argv[i] == NULL) {
 521 //     argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
 522 //     for(unsigned j = i; j < i + 5; ++j) {
 523 //       argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
 524 //       argv[j][0] = '\0';
 525 //     }
 526 //     argv[i + 5] = NULL;
 527 //   }
 528
 529 //   strncpy(argv[i], opt, maxoptlen - 1);
 530 //   argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
 531 // }
 532
 533 namespace options {
 534
 535 /** Set a given Options* as "current" just for a particular scope. */
 536 class OptionsGuard {
 537   Options** d_field;
 538   Options* d_old;
 539 public:
 540   OptionsGuard(Options** field, Options* opts) :
 541     d_field(field),
 542     d_old(*field) {
 543     *field = opts;
 544   }
 545   ~OptionsGuard() {
 546     *d_field = d_old;
 547   }
 548 };/* class OptionsGuard */
 549
 550 }/* CVC4::options namespace */
 551
 552 /**
 553  * Parse argc/argv and put the result into a CVC4::Options.
 554  * The return value is what's left of the command line (that is, the
 555  * non-option arguments).
 556  *
 557  * Throws OptionException on failures.
 558  */
 559 std::vector<std::string> Options::parseOptions(Options* options,
 560                                                int argc,
 561                                                char* argv[])
 562 {
 563   Assert(options != NULL);
 564   Assert(argv != NULL);
 565
 566   options::OptionsGuard guard(&s_current, options);
 567
 568   const char *progName = argv[0];
 569
 570   // To debug options parsing, you may prefer to simply uncomment this
 571   // and recompile. Debug flags have not been parsed yet so these have
 572   // not been set.
 573   //DebugChannel.on("options");
 574
 575   Debug("options") << "Options::parseOptions == " << options << std::endl;
 576   Debug("options") << "argv == " << argv << std::endl;
 577
 578   // Find the base name of the program.
 579   const char *x = strrchr(progName, '/');
 580   if(x != NULL) {
 581     progName = x + 1;
 582   }
 583   options->d_holder->binary_name = std::string(progName);
 584
 585   ArgumentExtender* argumentExtender = new ArgumentExtenderImplementation();
 586   for(int position = 1; position < argc; position++) {
 587     argumentExtender->pushBackArgument(argv[position]);
 588   }
 589
 590   std::vector<std::string> nonoptions;
 591   parseOptionsRecursive(options, argumentExtender, &nonoptions);
 592   if(Debug.isOn("options")){
 593     for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
 594           iend = nonoptions.end(); i != iend; ++i){
 595       Debug("options") << "nonoptions " << *i << std::endl;
 596     }
 597   }
 598
 599   delete argumentExtender;
 600   return nonoptions;
 601 }
 602
 603 void Options::parseOptionsRecursive(Options* options,
 604                                     ArgumentExtender* extender,
 605                                     std::vector<std::string>* nonoptions)
 606 {
 607   int argc;
 608   char** argv;
 609
 610   extender->movePreemptionsToArguments();
 611   extender->pushFrontArgument("");
 612   extender->getArguments(&argc, &argv);
 613
 614   if(Debug.isOn("options")) {
 615     Debug("options") << "starting a new parseOptionsRecursive with "
 616                      << argc << " arguments" << std::endl;
 617     for( int i = 0; i < argc ; i++ ){
 618       Assert(argv[i] != NULL);
 619       Debug("options") << "  argv[" << i << "] = " << argv[i] << std::endl;
 620     }
 621   }
 622
 623   // Having this synonym simplifies the generation code in mkoptions.
 624   options::OptionsHandler* handler = options->d_handler;
 625   options::OptionsHolder* holder = options->d_holder;
 626
 627   // Reset getopt(), in the case of multiple calls to parseOptions().
 628   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
 629   optind = 0;
 630 #if HAVE_DECL_OPTRESET
 631   optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 632 #endif /* HAVE_DECL_OPTRESET */
 633
 634
 635   int main_optind = 0;
 636   int old_optind;
 637
 638
 639   while(true) { // Repeat Forever
 640
 641     if(extender->hasPreemptions()){
 642       // Stop this round of parsing. We now parse recursively
 643       // to start on a new character array for argv.
 644       parseOptionsRecursive(options, extender, nonoptions);
 645       break;
 646     }
 647
 648     optopt = 0;
 649     std::string option, optionarg;
 650
 651     optind = main_optind;
 652     old_optind = main_optind;
 653     //optind_ref = &main_optind;
 654     //argv = main_argv;
 655
 656     // If we encounter an element that is not at zero and does not start
 657     // with a "-", this is a non-option. We consume this element as a
 658     // non-option.
 659     if (main_optind > 0 && main_optind < argc &&
 660         argv[main_optind][0] != '-') {
 661       Debug("options") << "enqueueing " << argv[main_optind]
 662                        << " as a non-option." << std::endl;
 663       nonoptions->push_back(argv[main_optind]);
 664       ++main_optind;
 665       extender->popFrontArgument();
 666       continue;
 667     }
 668
 669
 670     Debug("options") << "[ before, main_optind == " << main_optind << " ]"
 671                      << std::endl;
 672     Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
 673     Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
 674                      << std::endl;
 675     int c = getopt_long(argc, argv,
 676                         "+:${options_short}$",
 677                         cmdlineOptions, NULL);
 678
 679     while(main_optind < optind) {
 680       main_optind++;
 681       extender->popFrontArgument();
 682     }
 683
 684     Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
 685                      << "[ next option will be at pos: " << optind << " ]"
 686                      << std::endl;
 687
 688     // The initial getopt_long call should always determine that argv[0]
 689     // is not an option and returns -1. We always manually advance beyond
 690     // this element.
 691     //
 692     // We have to reinitialize optind to 0 instead of 1 as we need to support
 693     // changing the argv array passed to getopt.
 694     // This is needed as are using GNU extensions.
 695     // From: http://man7.org/linux/man-pages/man3/getopt.3.html
 696     // A program that scans multiple argument vectors, or rescans the same
 697     // vector more than once, and wants to make use of GNU extensions such
 698     // as '+' and '-' at the start of optstring, or changes the value of
 699     //  POSIXLY_CORRECT between scans, must reinitialize getopt() by
 700     //  resetting optind to 0, rather than the traditional value of 1.
 701     //  (Resetting to 0 forces the invocation of an internal initialization
 702     //  routine that rechecks POSIXLY_CORRECT and checks for GNU extensions
 703     //  in optstring.)
 704     if ( old_optind == 0  && c == -1 ) {
 705       Assert(main_optind > 0);
 706       continue;
 707     }
 708
 709     if ( c == -1 ) {
 710       if(Debug.isOn("options")) {
 711         Debug("options") << "done with option parsing" << std::endl;
 712         for(int index = optind; index < argc; ++index) {
 713           Debug("options") << "remaining " << argv[index] << std::endl;
 714         }
 715       }
 716       break;
 717     }
 718
 719     option = argv[old_optind == 0 ? 1 : old_optind];
 720     optionarg = (optarg == NULL) ? "" : optarg;
 721
 722     Debug("preemptGetopt") << "processing option " << c
 723                            << " (`" << char(c) << "'), " << option << std::endl;
 724
 725     switch(c) {
 726 ${options_handler}$
 727
 728
 729     case ':':
 730       // This can be a long or short option, and the way to get at the
 731       // name of it is different.
 732       throw OptionException(std::string("option `") + option +
 733                             "' missing its required argument");
 734
 735     case '?':
 736     default:
 737       if( ( optopt == 0 ||
 738             ( optopt >= ${option_value_begin}$ &&
 739               optopt <= ${option_value_end}$ )
 740           ) && !strncmp(argv[optind - 1], "--thread", 8) &&
 741           strlen(argv[optind - 1]) > 8 )
 742       {
 743         if(! isdigit(argv[optind - 1][8])) {
 744           throw OptionException(formatThreadOptionException(option));
 745         }
 746         std::vector<std::string>& threadArgv = holder->threadArgv;
 747         char *end;
 748         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
 749         if(tnum < 0 || (*end != '\0' && *end != '=')) {
 750           throw OptionException(formatThreadOptionException(option));
 751         }
 752         if(threadArgv.size() <= size_t(tnum)) {
 753           threadArgv.resize(tnum + 1);
 754         }
 755         if(threadArgv[tnum] != "") {
 756           threadArgv[tnum] += " ";
 757         }
 758         if(*end == '\0') { // e.g., we have --thread0 "foo"
 759           if(argc <= optind) {
 760             throw OptionException(std::string("option `") + option +
 761                                   "' missing its required argument");
 762           }
 763           Debug("options") << "thread " << tnum << " gets option "
 764                            << argv[optind] << std::endl;
 765           threadArgv[tnum] += argv[main_optind];
 766           main_optind++;
 767         } else { // e.g., we have --thread0="foo"
 768           if(end[1] == '\0') {
 769             throw OptionException(std::string("option `") + option +
 770                                   "' missing its required argument");
 771           }
 772           Debug("options") << "thread " << tnum << " gets option "
 773                            << (end + 1) << std::endl;
 774           threadArgv[tnum] += end + 1;
 775         }
 776         Debug("options") << "thread " << tnum << " now has "
 777                          << threadArgv[tnum] << std::endl;
 778         break;
 779       }
 780
 781       throw OptionException(std::string("can't understand option `") + option +
 782                             "'" + suggestCommandLineOptions(option));
 783     }
 784   }
 785
 786   Debug("options") << "got " << nonoptions->size()
 787                    << " non-option arguments." << std::endl;
 788
 789   free(argv);
 790 }
 791
 792 std::string Options::suggestCommandLineOptions(const std::string& optionName)
 793 {
 794   DidYouMean didYouMean;
 795
 796   const char* opt;
 797   for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
 798     didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
 799   }
 800
 801   return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
 802 }
 803
 804 static const char* smtOptions[] = {
 805   ${options_smt}$
 806   NULL
 807 };/* smtOptions[] */
 808
 809 std::vector<std::string> Options::suggestSmtOptions(
 810     const std::string& optionName)
 811 {
 812   std::vector<std::string> suggestions;
 813
 814   const char* opt;
 815   for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
 816     if(std::strstr(opt, optionName.c_str()) != NULL) {
 817       suggestions.push_back(opt);
 818     }
 819   }
 820
 821   return suggestions;
 822 }
 823
 824 std::vector<std::vector<std::string> > Options::getOptions() const
 825 {
 826   std::vector< std::vector<std::string> > opts;
 827
 828   ${options_getoptions}$
 829
 830
 831   return opts;
 832 }
 833
 834 void Options::setOption(const std::string& key, const std::string& optionarg)
 835 {
 836   options::OptionsHandler* handler = d_handler;
 837   Options *options = Options::current();
 838   Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")"
 839                    << std::endl;
 840
 841   ${setoption_handlers}$
 842
 843
 844   throw UnrecognizedOptionException(key);
 845 }
 846
 847 std::string Options::getOption(const std::string& key) const
 848 {
 849   Trace("options") << "SMT getOption(" << key << ")" << std::endl;
 850
 851   ${getoption_handlers}$
 852
 853
 854   throw UnrecognizedOptionException(key);
 855 }
 856
 857 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 858 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 859
 860 }  // namespace CVC4