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 "base/check.h"
  17 #include "base/output.h"
  18 #include "options/options.h"
  19 #include "options/options_handler.h"
  20 #include "options/options_listener.h"
  21 #include "options/options_public.h"
  22 #include "options/uf_options.h"
  23
  24 // clang-format off
  25 ${headers_module}$
  26 ${options_includes}$
  27 // clang-format on
  28
  29 #include <cstring>
  30 #include <iostream>
  31 #include <limits>
  32
  33 namespace cvc5::options
  34 {
  35   // Contains the default option handlers (i.e. parsers)
  36   namespace handlers {
  37
  38   /**
  39    * Utility function for handling numeric options. Takes care of checking for
  40    * unsignedness, parsing and handling parsing exceptions. Expects `conv` to be
  41    * a conversion function like `std::stod`, accepting a `std::string` and a
  42    * `size_t*`. The argument `type` is only used to generate proper error
  43    * messages and should be the string representation of `T`. If `T` is
  44    * unsigned, checks that `optionarg` contains no minus. Then `conv` is called
  45    * and the error conditions are handled: `conv` may throw an exception or
  46    * `pos` may be smaller than the size of `optionarg`, indicating that not the
  47    * entirety of `optionarg` was parsed.
  48    */
  49   template <typename T, typename FF>
  50   T parseNumber(const std::string& flag,
  51                 const std::string& optionarg,
  52                 FF&& conv,
  53                 const std::string& type)
  54   {
  55     if (!std::numeric_limits<T>::is_signed
  56         && (optionarg.find('-') != std::string::npos))
  57     {
  58       std::stringstream ss;
  59       ss << "Argument '" << optionarg << "' for " << type << " option " << flag
  60          << " is negative";
  61       throw OptionException(ss.str());
  62     }
  63     size_t pos = 0;
  64     T res;
  65     try
  66     {
  67       res = conv(optionarg, &pos);
  68     }
  69     catch (const std::exception& e)
  70     {
  71       std::stringstream ss;
  72       ss << "Argument '" << optionarg << "' for " << type << " option " << flag
  73          << " did not parse as " << type;
  74       throw OptionException(ss.str());
  75     }
  76     if (pos < optionarg.size())
  77     {
  78       std::stringstream ss;
  79       ss << "Argument '" << optionarg << "' for " << type << " option " << flag
  80          << " did parse only partially as " << type << ", leaving '"
  81          << optionarg.substr(pos) << "'";
  82       throw OptionException(ss.str());
  83     }
  84     return res;
  85   }
  86
  87   /** Default handler that triggers a compiler error */
  88   template <typename T>
  89   T handleOption(const std::string& option,
  90                  const std::string& flag,
  91                  const std::string& optionarg)
  92   {
  93     T::unsupported_handleOption_specialization;
  94     return *static_cast<T*>(nullptr);
  95   }
  96
  97   /** Handle a string option by returning it as is. */
  98   template <>
  99   std::string handleOption<std::string>(const std::string& option,
 100                                         const std::string& flag,
 101                                         const std::string& optionarg)
 102   {
 103     return optionarg;
 104   }
 105   /** Handle a bool option, recognizing "true" or "false". */
 106   template <>
 107   bool handleOption<bool>(const std::string& option,
 108                           const std::string& flag,
 109                           const std::string& optionarg)
 110   {
 111     if (optionarg == "true")
 112     {
 113       return true;
 114     }
 115     if (optionarg == "false")
 116     {
 117       return false;
 118     }
 119     throw OptionException("Argument '" + optionarg + "' for bool option " + flag
 120                           + " is not a bool constant");
 121   }
 122
 123   /** Handle a double option, using `parseNumber` with `std::stod`. */
 124   template <>
 125   double handleOption<double>(const std::string& option,
 126                               const std::string& flag,
 127                               const std::string& optionarg)
 128   {
 129     return parseNumber<double>(
 130         flag,
 131         optionarg,
 132         [](const auto& s, auto p) { return std::stod(s, p); },
 133         "double");
 134   }
 135
 136   /** Handle a int64_t option, using `parseNumber` with `std::stoll`. */
 137   template <>
 138   int64_t handleOption<int64_t>(const std::string& option,
 139                                 const std::string& flag,
 140                                 const std::string& optionarg)
 141   {
 142     return parseNumber<int64_t>(
 143         flag,
 144         optionarg,
 145         [](const auto& s, auto p) { return std::stoll(s, p); },
 146         "int64_t");
 147   }
 148
 149   /** Handle a uint64_t option, using `parseNumber` with `std::stoull`. */
 150   template <>
 151   uint64_t handleOption<uint64_t>(const std::string& option,
 152                                   const std::string& flag,
 153                                   const std::string& optionarg)
 154   {
 155     return parseNumber<uint64_t>(
 156         flag,
 157         optionarg,
 158         [](const auto& s, auto p) { return std::stoull(s, p); },
 159         "uint64_t");
 160   }
 161
 162   /** Handle a ManagedIn option. */
 163   template <>
 164   ManagedIn handleOption<ManagedIn>(const std::string& option,
 165                                     const std::string& flag,
 166                                     const std::string& optionarg)
 167   {
 168     ManagedIn res;
 169     res.open(optionarg);
 170     return res;
 171   }
 172
 173   /** Handle a ManagedErr option. */
 174   template <>
 175   ManagedErr handleOption<ManagedErr>(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   /** Handle a ManagedOut option. */
 185   template <>
 186   ManagedOut handleOption<ManagedOut>(const std::string& option,
 187                                       const std::string& flag,
 188                                       const std::string& optionarg)
 189   {
 190     ManagedOut res;
 191     res.open(optionarg);
 192     return res;
 193   }
 194   }
 195
 196   std::vector<std::string> getNames()
 197   {
 198     return {
 199         // clang-format off
 200     ${getnames_impl}$
 201         // clang-format on
 202     };
 203   }
 204
 205   std::string get(const Options& options, const std::string& name)
 206   {
 207     Trace("options") << "Options::getOption(" << name << ")" << std::endl;
 208     // clang-format off
 209   ${get_impl}$
 210     // clang-format on
 211     throw OptionException("Unrecognized option key or setting: " + name);
 212   }
 213
 214   void set(
 215       Options & opts, const std::string& name, const std::string& optionarg)
 216   {
 217     Trace("options") << "set option " << name << " = " << optionarg
 218                      << std::endl;
 219     // clang-format off
 220   ${set_impl}$
 221     // clang-format on
 222   }
 223   else
 224   {
 225     throw OptionException("Unrecognized option key or setting: " + name);
 226   }
 227 }
 228
 229 #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
 230 #define DO_SEMANTIC_CHECKS_BY_DEFAULT false
 231 #else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
 232 #define DO_SEMANTIC_CHECKS_BY_DEFAULT true
 233 #endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
 234
 235 OptionInfo getInfo(const Options& opts, const std::string& name)
 236 {
 237   // clang-format off
 238   ${options_get_info}$
 239   // clang-format on
 240   return OptionInfo{"", {}, false, OptionInfo::VoidInfo{}};
 241 }
 242
 243 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 244
 245 }  // namespace cvc5::options