src/options/options_public_template.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Gereon Kremer, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Global (command-line, set-option, ...) parameters for SMT.
  14  */
  15
  16 #include "options/options_public.h"
  17
  18 #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
  19 // force use of optreset; mingw32 croaks on argv-switching otherwise
  20 #include "base/cvc5config.h"
  21 #define _BSD_SOURCE
  22 #undef HAVE_DECL_OPTRESET
  23 #define HAVE_DECL_OPTRESET 1
  24 #define CVC5_IS_NOT_REALLY_BSD
  25 #endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
  26
  27 #ifdef __MINGW64__
  28 extern int optreset;
  29 #endif /* __MINGW64__ */
  30
  31 #include <getopt.h>
  32
  33 // clean up
  34 #ifdef CVC5_IS_NOT_REALLY_BSD
  35 #  undef _BSD_SOURCE
  36 #endif /* CVC5_IS_NOT_REALLY_BSD */
  37
  38 #include "base/check.h"
  39 #include "base/output.h"
  40 #include "options/didyoumean.h"
  41 #include "options/options_handler.h"
  42 #include "options/options_listener.h"
  43 #include "options/options.h"
  44 #include "options/uf_options.h"
  45 ${headers_module}$
  46 ${headers_handler}$
  47
  48 #include <cstring>
  49 #include <iostream>
  50 #include <limits>
  51
  52 namespace cvc5::options {
  53
  54 bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
  55
  56 // clang-format off
  57 static const std::string mostCommonOptionsDescription =
  58     "\
  59 Most commonly-used cvc5 options:\n"
  60 ${help_common}$
  61     ;
  62
  63 static const std::string optionsDescription =
  64     mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
  65 ${help_others}$;
  66
  67 static const std::string optionsFootnote = "\n\
  68 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
  69     sense of the option.\n\
  70 ";
  71
  72 static const std::string languageDescription =
  73     "\
  74 Languages currently supported as arguments to the -L / --lang option:\n\
  75   auto                           attempt to automatically determine language\n\
  76   cvc | presentation | pl        CVC presentation language\n\
  77   smt | smtlib | smt2 |\n\
  78   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
  79   tptp                           TPTP format (cnf, fof and tff)\n\
  80   sygus | sygus2                 SyGuS version 2.0\n\
  81 \n\
  82 Languages currently supported as arguments to the --output-lang option:\n\
  83   auto                           match output language to input language\n\
  84   cvc | presentation | pl        CVC presentation language\n\
  85   smt | smtlib | smt2 |\n\
  86   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
  87   tptp                           TPTP format\n\
  88   ast                            internal format (simple syntax trees)\n\
  89 ";
  90 // clang-format on
  91
  92 const std::string& getDescription()
  93 {
  94   return optionsDescription;
  95 }
  96
  97 void printUsage(const std::string& msg, std::ostream& os) {
  98   os << msg << optionsDescription << std::endl
  99       << optionsFootnote << std::endl << std::flush;
 100 }
 101
 102 void printShortUsage(const std::string& msg, std::ostream& os) {
 103   os << msg << mostCommonOptionsDescription << std::endl
 104       << optionsFootnote << std::endl
 105       << "For full usage, please use --help."
 106       << std::endl << std::endl << std::flush;
 107 }
 108
 109 void printLanguageHelp(std::ostream& os) {
 110   os << languageDescription << std::flush;
 111 }
 112
 113 /** Set a given Options* as "current" just for a particular scope. */
 114 class OptionsGuard {
 115   Options** d_field;
 116   Options* d_old;
 117 public:
 118   OptionsGuard(Options** field, Options* opts) :
 119     d_field(field),
 120     d_old(*field) {
 121     *field = opts;
 122   }
 123   ~OptionsGuard() {
 124     *d_field = d_old;
 125   }
 126 };/* class OptionsGuard */
 127
 128 /**
 129  * This is a table of long options.  By policy, each short option
 130  * should have an equivalent long option (but the reverse isn't the
 131  * case), so this table should thus contain all command-line options.
 132  *
 133  * Each option in this array has four elements:
 134  *
 135  * 1. the long option string
 136  * 2. argument behavior for the option:
 137  *    no_argument - no argument permitted
 138  *    required_argument - an argument is expected
 139  *    optional_argument - an argument is permitted but not required
 140  * 3. this is a pointer to an int which is set to the 4th entry of the
 141  *    array if the option is present; or NULL, in which case
 142  *    getopt_long() returns the 4th entry
 143  * 4. the return value for getopt_long() when this long option (or the
 144  *    value to set the 3rd entry to; see #3)
 145  *
 146  * If you add something here, you should add it in src/main/usage.h
 147  * also, to document it.
 148  *
 149  * If you add something that has a short option equivalent, you should
 150  * add it to the getopt_long() call in parse().
 151  */
 152 // clang-format off
 153 static struct option cmdlineOptions[] = {
 154   ${cmdline_options}$
 155   {nullptr, no_argument, nullptr, '\0'}};
 156 // clang-format on
 157
 158 std::string suggestCommandLineOptions(const std::string& optionName)
 159 {
 160   DidYouMean didYouMean;
 161
 162   const char* opt;
 163   for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) {
 164     didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
 165   }
 166
 167   return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
 168 }
 169
 170 /**
 171  * This is a default handler for options of built-in C++ type.  This
 172  * template is really just a helper for the handleOption() template,
 173  * below.  Variants of this template handle numeric and non-numeric,
 174  * integral and non-integral, signed and unsigned C++ types.
 175  * handleOption() makes sure to instantiate the right one.
 176  *
 177  * This implements default behavior when e.g. an option is
 178  * unsigned but the user specifies a negative argument; etc.
 179  */
 180 template <class T, bool is_numeric, bool is_integer>
 181 struct OptionHandler {
 182   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg);
 183 };/* struct OptionHandler<> */
 184
 185 /** Variant for integral C++ types */
 186 template <class T>
 187 struct OptionHandler<T, true, true> {
 188   static bool stringToInt(T& t, const std::string& str) {
 189     std::istringstream ss(str);
 190     ss >> t;
 191     char tmp;
 192     return !(ss.fail() || ss.get(tmp));
 193   }
 194
 195   static bool containsMinus(const std::string& str) {
 196     return str.find('-') != std::string::npos;
 197   }
 198
 199   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
 200     try {
 201       T i;
 202       bool success = stringToInt(i, optionarg);
 203
 204       if(!success){
 205         throw OptionException(flag + ": failed to parse "+ optionarg +
 206                               " as an integer of the appropriate type.");
 207       }
 208
 209       // Depending in the platform unsigned numbers with '-' signs may parse.
 210       // Reject these by looking for any minus if it is not signed.
 211       if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
 212         // unsigned type but user gave negative argument
 213         throw OptionException(flag + " requires a nonnegative argument");
 214       } else if(i < std::numeric_limits<T>::min()) {
 215         // negative overflow for type
 216         std::stringstream ss;
 217         ss << flag << " requires an argument >= "
 218            << std::numeric_limits<T>::min();
 219         throw OptionException(ss.str());
 220       } else if(i > std::numeric_limits<T>::max()) {
 221         // positive overflow for type
 222         std::stringstream ss;
 223         ss << flag << " requires an argument <= "
 224            << std::numeric_limits<T>::max();
 225         throw OptionException(ss.str());
 226       }
 227
 228       return i;
 229
 230       // if(std::numeric_limits<T>::is_signed) {
 231       //   return T(i.getLong());
 232       // } else {
 233       //   return T(i.getUnsignedLong());
 234       // }
 235     } catch(std::invalid_argument&) {
 236       // user gave something other than an integer
 237       throw OptionException(flag + " requires an integer argument");
 238     }
 239   }
 240 };/* struct OptionHandler<T, true, true> */
 241
 242 /** Variant for numeric but non-integral C++ types */
 243 template <class T>
 244 struct OptionHandler<T, true, false> {
 245   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
 246     std::stringstream inss(optionarg);
 247     long double r;
 248     inss >> r;
 249     if(! inss.eof()) {
 250       // we didn't consume the whole string (junk at end)
 251       throw OptionException(flag + " requires a numeric argument");
 252     }
 253
 254     if(! std::numeric_limits<T>::is_signed && r < 0.0) {
 255       // unsigned type but user gave negative value
 256       throw OptionException(flag + " requires a nonnegative argument");
 257     } else if(r < -std::numeric_limits<T>::max()) {
 258       // negative overflow for type
 259       std::stringstream ss;
 260       ss << flag << " requires an argument >= "
 261          << -std::numeric_limits<T>::max();
 262       throw OptionException(ss.str());
 263     } else if(r > std::numeric_limits<T>::max()) {
 264       // positive overflow for type
 265       std::stringstream ss;
 266       ss << flag << " requires an argument <= "
 267          << std::numeric_limits<T>::max();
 268       throw OptionException(ss.str());
 269     }
 270
 271     return T(r);
 272   }
 273 };/* struct OptionHandler<T, true, false> */
 274
 275 /** Variant for non-numeric C++ types */
 276 template <class T>
 277 struct OptionHandler<T, false, false> {
 278   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
 279     T::unsupported_handleOption_call___please_write_me;
 280     // The above line causes a compiler error if this version of the template
 281     // is ever instantiated (meaning that a specialization is missing).  So
 282     // don't worry about the segfault in the next line, the "return" is only
 283     // there to keep the compiler from giving additional, distracting errors
 284     // and warnings.
 285     return *(T*)0;
 286   }
 287 };/* struct OptionHandler<T, false, false> */
 288
 289 /** Handle an option of type T in the default way. */
 290 template <class T>
 291 T handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) {
 292   return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, flag, optionarg);
 293 }
 294
 295 /** Handle an option of type std::string in the default way. */
 296 template <>
 297 std::string handleOption<std::string>(const std::string& option, const std::string& flag, const std::string& optionarg) {
 298   return optionarg;
 299 }
 300
 301 // clang-format off
 302 ${assigns}$
 303 // clang-format off
 304
 305 void parseInternal(Options& opts, int argc,
 306                                     char* argv[],
 307                                     std::vector<std::string>& nonoptions)
 308 {
 309   Assert(argv != nullptr);
 310   if(Debug.isOn("options")) {
 311     Debug("options") << "starting a new parseInternal with "
 312                      << argc << " arguments" << std::endl;
 313     for( int i = 0; i < argc ; i++ ){
 314       Assert(argv[i] != NULL);
 315       Debug("options") << "  argv[" << i << "] = " << argv[i] << std::endl;
 316     }
 317   }
 318
 319   // Reset getopt(), in the case of multiple calls to parse().
 320   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
 321   optind = 0;
 322 #if HAVE_DECL_OPTRESET
 323   optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 324 #endif /* HAVE_DECL_OPTRESET */
 325
 326   // We must parse the binary name, which is manually ignored below. Setting
 327   // this to 1 leads to incorrect behavior on some platforms.
 328   int main_optind = 0;
 329   int old_optind;
 330
 331
 332   while(true) { // Repeat Forever
 333
 334     optopt = 0;
 335     std::string option, optionarg;
 336
 337     optind = main_optind;
 338     old_optind = main_optind;
 339
 340     // If we encounter an element that is not at zero and does not start
 341     // with a "-", this is a non-option. We consume this element as a
 342     // non-option.
 343     if (main_optind > 0 && main_optind < argc &&
 344         argv[main_optind][0] != '-') {
 345       Debug("options") << "enqueueing " << argv[main_optind]
 346                        << " as a non-option." << std::endl;
 347       nonoptions.push_back(argv[main_optind]);
 348       ++main_optind;
 349       continue;
 350     }
 351
 352
 353     Debug("options") << "[ before, main_optind == " << main_optind << " ]"
 354                      << std::endl;
 355     Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
 356     Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
 357                      << std::endl;
 358     // clang-format off
 359     int c = getopt_long(argc, argv,
 360                         "+:${options_short}$",
 361                         cmdlineOptions, NULL);
 362     // clang-format on
 363
 364     main_optind = optind;
 365
 366     Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
 367                      << "[ next option will be at pos: " << optind << " ]"
 368                      << std::endl;
 369
 370     // The initial getopt_long call should always determine that argv[0]
 371     // is not an option and returns -1. We always manually advance beyond
 372     // this element.
 373     if ( old_optind == 0  && c == -1 ) {
 374       Assert(main_optind > 0);
 375       continue;
 376     }
 377
 378     if ( c == -1 ) {
 379       if(Debug.isOn("options")) {
 380         Debug("options") << "done with option parsing" << std::endl;
 381         for(int index = optind; index < argc; ++index) {
 382           Debug("options") << "remaining " << argv[index] << std::endl;
 383         }
 384       }
 385       break;
 386     }
 387
 388     option = argv[old_optind == 0 ? 1 : old_optind];
 389     optionarg = (optarg == NULL) ? "" : optarg;
 390
 391     Debug("preemptGetopt") << "processing option " << c
 392                            << " (`" << char(c) << "'), " << option << std::endl;
 393
 394     // clang-format off
 395     switch(c)
 396     {
 397 ${options_handler}$
 398
 399       case ':' :
 400       // This can be a long or short option, and the way to get at the
 401       // name of it is different.
 402       throw OptionException(std::string("option `") + option
 403                             + "' missing its required argument");
 404
 405       case '?':
 406       default:
 407         throw OptionException(std::string("can't understand option `") + option
 408                               + "'" + suggestCommandLineOptions(option));
 409     }
 410   }
 411   // clang-format on
 412
 413   Debug("options") << "got " << nonoptions.size()
 414                    << " non-option arguments." << std::endl;
 415 }
 416
 417 /**
 418  * Parse argc/argv and put the result into a cvc5::Options.
 419  * The return value is what's left of the command line (that is, the
 420  * non-option arguments).
 421  *
 422  * Throws OptionException on failures.
 423  */
 424 std::vector<std::string> parse(
 425     Options & opts, int argc, char* argv[], std::string& binaryName)
 426 {
 427   Assert(argv != nullptr);
 428
 429   Options* cur = &Options::current();
 430   OptionsGuard guard(&cur, &opts);
 431
 432   const char *progName = argv[0];
 433
 434   // To debug options parsing, you may prefer to simply uncomment this
 435   // and recompile. Debug flags have not been parsed yet so these have
 436   // not been set.
 437   //DebugChannel.on("options");
 438
 439   Debug("options") << "options::parse == " << &opts << std::endl;
 440   Debug("options") << "argv == " << argv << std::endl;
 441
 442   // Find the base name of the program.
 443   const char *x = strrchr(progName, '/');
 444   if(x != nullptr) {
 445     progName = x + 1;
 446   }
 447   binaryName = std::string(progName);
 448
 449   std::vector<std::string> nonoptions;
 450   parseInternal(opts, argc, argv, nonoptions);
 451   if (Debug.isOn("options")){
 452     for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
 453           iend = nonoptions.end(); i != iend; ++i){
 454       Debug("options") << "nonoptions " << *i << std::endl;
 455     }
 456   }
 457
 458   return nonoptions;
 459 }
 460
 461 std::string get(const Options& options, const std::string& key)
 462 {
 463   Trace("options") << "Options::getOption(" << key << ")" << std::endl;
 464   ${getoption_handlers}$
 465
 466   throw UnrecognizedOptionException(key);
 467 }
 468
 469 void setInternal(Options& opts, const std::string& key,
 470                                 const std::string& optionarg)
 471                                 {
 472   ${setoption_handlers}$
 473   throw UnrecognizedOptionException(key);
 474 }
 475
 476 void set(Options& opts, const std::string& key, const std::string& optionarg)
 477 {
 478
 479   Trace("options") << "setOption(" << key << ", " << optionarg << ")"
 480                    << std::endl;
 481   // first update this object
 482   setInternal(opts, key, optionarg);
 483   // then, notify the provided listener
 484   opts.notifyListener(key);
 485 }
 486
 487 std::vector<std::vector<std::string> > getAll(const Options& opts)
 488 {
 489   std::vector<std::vector<std::string>> res;
 490
 491 ${options_getall}$
 492
 493   return res;
 494 }
 495
 496 }  // namespace cvc5::options