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
  19 #include "base/check.h"
  20 #include "base/output.h"
  21 #include "options/options_handler.h"
  22 #include "options/options_listener.h"
  23 #include "options/options.h"
  24 #include "options/uf_options.h"
  25 ${headers_module}$
  26 ${headers_handler}$
  27
  28 #include <cstring>
  29 #include <iostream>
  30 #include <limits>
  31
  32 namespace cvc5::options {
  33
  34 bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
  35
  36 /** Set a given Options* as "current" just for a particular scope. */
  37 class OptionsGuard {
  38   Options** d_field;
  39   Options* d_old;
  40 public:
  41   OptionsGuard(Options** field, Options* opts) :
  42     d_field(field),
  43     d_old(*field) {
  44     *field = opts;
  45   }
  46   ~OptionsGuard() {
  47     *d_field = d_old;
  48   }
  49 };/* class OptionsGuard */
  50
  51
  52 /**
  53  * This is a default handler for options of built-in C++ type.  This
  54  * template is really just a helper for the handleOption() template,
  55  * below.  Variants of this template handle numeric and non-numeric,
  56  * integral and non-integral, signed and unsigned C++ types.
  57  * handleOption() makes sure to instantiate the right one.
  58  *
  59  * This implements default behavior when e.g. an option is
  60  * unsigned but the user specifies a negative argument; etc.
  61  */
  62 template <class T, bool is_numeric, bool is_integer>
  63 struct OptionHandler {
  64   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg);
  65 };/* struct OptionHandler<> */
  66
  67 /** Variant for integral C++ types */
  68 template <class T>
  69 struct OptionHandler<T, true, true> {
  70   static bool stringToInt(T& t, const std::string& str) {
  71     std::istringstream ss(str);
  72     ss >> t;
  73     char tmp;
  74     return !(ss.fail() || ss.get(tmp));
  75   }
  76
  77   static bool containsMinus(const std::string& str) {
  78     return str.find('-') != std::string::npos;
  79   }
  80
  81   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
  82     try {
  83       T i;
  84       bool success = stringToInt(i, optionarg);
  85
  86       if(!success){
  87         throw OptionException(flag + ": failed to parse "+ optionarg +
  88                               " as an integer of the appropriate type.");
  89       }
  90
  91       // Depending in the platform unsigned numbers with '-' signs may parse.
  92       // Reject these by looking for any minus if it is not signed.
  93       if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
  94         // unsigned type but user gave negative argument
  95         throw OptionException(flag + " requires a nonnegative argument");
  96       } else if(i < std::numeric_limits<T>::min()) {
  97         // negative overflow for type
  98         std::stringstream ss;
  99         ss << flag << " requires an argument >= "
 100            << std::numeric_limits<T>::min();
 101         throw OptionException(ss.str());
 102       } else if(i > std::numeric_limits<T>::max()) {
 103         // positive overflow for type
 104         std::stringstream ss;
 105         ss << flag << " requires an argument <= "
 106            << std::numeric_limits<T>::max();
 107         throw OptionException(ss.str());
 108       }
 109
 110       return i;
 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(flag + " 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(const std::string& option, const std::string& flag, const std::string& optionarg) {
 128     std::stringstream inss(optionarg);
 129     long double r;
 130     inss >> r;
 131     if(! inss.eof()) {
 132       // we didn't consume the whole string (junk at end)
 133       throw OptionException(flag + " 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(flag + " requires a nonnegative argument");
 139     } else if(r < -std::numeric_limits<T>::max()) {
 140       // negative overflow for type
 141       std::stringstream ss;
 142       ss << flag << " requires an argument >= "
 143          << -std::numeric_limits<T>::max();
 144       throw OptionException(ss.str());
 145     } else if(r > std::numeric_limits<T>::max()) {
 146       // positive overflow for type
 147       std::stringstream ss;
 148       ss << flag << " requires an argument <= "
 149          << std::numeric_limits<T>::max();
 150       throw OptionException(ss.str());
 151     }
 152
 153     return T(r);
 154   }
 155 };/* struct OptionHandler<T, true, false> */
 156
 157 /** Variant for non-numeric C++ types */
 158 template <class T>
 159 struct OptionHandler<T, false, false> {
 160   static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
 161     T::unsupported_handleOption_call___please_write_me;
 162     // The above line causes a compiler error if this version of the template
 163     // is ever instantiated (meaning that a specialization is missing).  So
 164     // don't worry about the segfault in the next line, the "return" is only
 165     // there to keep the compiler from giving additional, distracting errors
 166     // and warnings.
 167     return *(T*)0;
 168   }
 169 };/* struct OptionHandler<T, false, false> */
 170
 171 /** Specialization for ManagedErr */
 172 template <>
 173 struct OptionHandler<ManagedErr, false, false>
 174 {
 175   static ManagedErr handle(const std::string& option,
 176                            const std::string& flag,
 177                            const std::string& optionarg)
 178   {
 179     ManagedErr res;
 180     res.open(optionarg);
 181     return res;
 182   }
 183 };
 184 /** Specialization for ManagedIn */
 185 template <>
 186 struct OptionHandler<ManagedIn, false, false>
 187 {
 188   static ManagedIn handle(const std::string& option,
 189                           const std::string& flag,
 190                           const std::string& optionarg)
 191   {
 192     ManagedIn res;
 193     res.open(optionarg);
 194     return res;
 195   }
 196 };
 197 /** Specialization for ManagedOut */
 198 template <>
 199 struct OptionHandler<ManagedOut, false, false>
 200 {
 201   static ManagedOut handle(const std::string& option,
 202                            const std::string& flag,
 203                            const std::string& optionarg)
 204   {
 205     ManagedOut res;
 206     res.open(optionarg);
 207     return res;
 208   }
 209 };
 210
 211 /** Handle an option of type T in the default way. */
 212 template <class T>
 213 T handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) {
 214   return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, flag, optionarg);
 215 }
 216
 217 /** Handle an option of type std::string in the default way. */
 218 template <>
 219 std::string handleOption<std::string>(const std::string& option, const std::string& flag, const std::string& optionarg) {
 220   return optionarg;
 221 }
 222 template <>
 223 bool handleOption<bool>(const std::string& option, const std::string& flag, const std::string& optionarg) {
 224   Assert(optionarg == "true" || optionarg == "false");
 225   return optionarg == "true";
 226 }
 227
 228 std::string get(const Options& options, const std::string& name)
 229 {
 230   Trace("options") << "Options::getOption(" << name << ")" << std::endl;
 231   // clang-format off
 232   ${getoption_handlers}$
 233   // clang-format on
 234   throw OptionException("Unrecognized option key or setting: " + name);
 235 }
 236
 237 void setInternal(Options& opts, const std::string& name,
 238                                 const std::string& optionarg)
 239 {
 240   // clang-format off
 241 ${setoption_handlers}$
 242   // clang-format on
 243   }
 244   else
 245   {
 246     throw OptionException("Unrecognized option key or setting: " + name);
 247   }
 248   Trace("options") << "user assigned option " << name << " = " << optionarg << std::endl;
 249 }
 250
 251 void set(Options& opts, const std::string& name, const std::string& optionarg)
 252 {
 253
 254   Trace("options") << "setOption(" << name << ", " << optionarg << ")"
 255                    << std::endl;
 256   // first update this object
 257   setInternal(opts, name, optionarg);
 258 }
 259
 260 std::vector<std::vector<std::string> > getAll(const Options& opts)
 261 {
 262   std::vector<std::vector<std::string>> res;
 263   // clang-format off
 264   ${options_getall}$
 265   // clang-format on
 266   return res;
 267 }
 268
 269 std::vector<std::string> getNames()
 270 {
 271   return {
 272     // clang-format off
 273     ${options_all_names}$
 274     // clang-format on
 275   };
 276 }
 277
 278 #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
 279 #define DO_SEMANTIC_CHECKS_BY_DEFAULT false
 280 #else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
 281 #define DO_SEMANTIC_CHECKS_BY_DEFAULT true
 282 #endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
 283
 284 OptionInfo getInfo(const Options& opts, const std::string& name)
 285 {
 286   // clang-format off
 287   ${options_get_info}$
 288   // clang-format on
 289   return OptionInfo{name, {}, false, OptionInfo::VoidInfo{}};
 290 }
 291
 292 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 293
 294 }  // namespace cvc5::options