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