src/options/options_template.cpp

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