-/********************* */
-/*! \file options_template.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Contains code for handling command-line options.
- **
- ** Contains code for handling command-line options
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Tim King, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Contains code for handling command-line options.
+ */
#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
// force use of optreset; mingw32 croaks on argv-switching otherwise
-# include "cvc4autoconfig.h"
-# define _BSD_SOURCE
-# undef HAVE_DECL_OPTRESET
-# define HAVE_DECL_OPTRESET 1
-# define CVC4_IS_NOT_REALLY_BSD
+#include "base/cvc5config.h"
+#define _BSD_SOURCE
+#undef HAVE_DECL_OPTRESET
+#define HAVE_DECL_OPTRESET 1
+#define CVC5_IS_NOT_REALLY_BSD
#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
#ifdef __MINGW64__
#include <getopt.h>
// clean up
-#ifdef CVC4_IS_NOT_REALLY_BSD
+#ifdef CVC5_IS_NOT_REALLY_BSD
# undef _BSD_SOURCE
-#endif /* CVC4_IS_NOT_REALLY_BSD */
+#endif /* CVC5_IS_NOT_REALLY_BSD */
#include <unistd.h>
#include <string.h>
// clang-format off
${headers_module}$
-#include "options/options_holder.h"
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
#include "options/base_handlers.h"
${headers_handler}$
-using namespace CVC5;
-using namespace CVC5::options;
+using namespace cvc5;
+using namespace cvc5::options;
+// clang-format on
-namespace CVC5 {
+namespace cvc5 {
thread_local Options* Options::s_current = NULL;
}
Options::Options(OptionsListener* ol)
- : d_holder(new options::OptionsHolder()),
- d_handler(new options::OptionsHandler(this)),
+ : d_handler(new options::OptionsHandler(this)),
+// clang-format off
+${holder_mem_inits}$
+${holder_ref_inits}$
+// clang-format on
d_olisten(ol)
{}
Options::~Options() {
delete d_handler;
- delete d_holder;
}
void Options::copyValues(const Options& options){
if(this != &options) {
- delete d_holder;
- d_holder = new options::OptionsHolder(*options.d_holder);
+// clang-format off
+${holder_mem_copy}$
+// clang-format on
}
}
void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
+// clang-format off
${custom_handlers}$
+// clang-format on
-#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
-# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
-# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
-
-options::OptionsHolder::OptionsHolder() :
- ${module_defaults}$
-{
-}
-
-
-static const std::string mostCommonOptionsDescription = "\
-Most commonly-used CVC4 options:\n"
-${help_common}$;
-
+static const std::string mostCommonOptionsDescription =
+ "\
+Most commonly-used cvc5 options:\n"
+ // clang-format off
+${help_common}$
+ // clang-format on
+ ;
-static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
-\n\
-Additional CVC4 options:\n"
+// clang-format off
+static const std::string optionsDescription =
+ mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
${help_others}$;
-
+// clang-format on
static const std::string optionsFootnote = "\n\
[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
"\
Languages currently supported as arguments to the -L / --lang option:\n\
auto attempt to automatically determine language\n\
- cvc4 | presentation | pl CVC4 presentation language\n\
+ cvc | presentation | pl CVC presentation language\n\
smt | smtlib | smt2 |\n\
smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\
tptp TPTP format (cnf, fof and tff)\n\
\n\
Languages currently supported as arguments to the --output-lang option:\n\
auto match output language to input language\n\
- cvc4 | presentation | pl CVC4 presentation language\n\
- cvc3 CVC3 presentation language\n\
+ cvc | presentation | pl CVC presentation language\n\
smt | smtlib | smt2 |\n\
smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\
tptp TPTP format\n\
* If you add something that has a short option equivalent, you should
* add it to the getopt_long() call in parseOptions().
*/
+// clang-format off
static struct option cmdlineOptions[] = {
${cmdline_options}$
- { NULL, no_argument, NULL, '\0' }
-};/* cmdlineOptions */
+ {nullptr, no_argument, nullptr, '\0'}};
+// clang-format on
namespace options {
} // namespace options
/**
- * Parse argc/argv and put the result into a CVC5::Options.
+ * Parse argc/argv and put the result into a cvc5::Options.
* The return value is what's left of the command line (that is, the
* non-option arguments).
*
if(x != NULL) {
progName = x + 1;
}
- options->d_holder->binary_name = std::string(progName);
+ options->base.binary_name = std::string(progName);
std::vector<std::string> nonoptions;
- parseOptionsRecursive(options, argc, argv, &nonoptions);
+ options->parseOptionsRecursive(argc, argv, &nonoptions);
if(Debug.isOn("options")){
for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
iend = nonoptions.end(); i != iend; ++i){
return nonoptions;
}
-void Options::parseOptionsRecursive(Options* options,
- int argc,
+std::string suggestCommandLineOptions(const std::string& optionName)
+{
+ DidYouMean didYouMean;
+
+ const char* opt;
+ for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) {
+ didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
+ }
+
+ return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
+}
+
+void Options::parseOptionsRecursive(int argc,
char* argv[],
std::vector<std::string>* nonoptions)
{
}
}
- // Having this synonym simplifies the generation code in mkoptions.
- options::OptionsHandler* handler = options->d_handler;
-
// Reset getopt(), in the case of multiple calls to parseOptions().
// This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
optind = 0;
Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
<< std::endl;
+ // clang-format off
int c = getopt_long(argc, argv,
"+:${options_short}$",
cmdlineOptions, NULL);
+ // clang-format on
main_optind = optind;
Debug("preemptGetopt") << "processing option " << c
<< " (`" << char(c) << "'), " << option << std::endl;
+ // clang-format off
switch(c)
{
${options_handler}$
-
- case ':':
+ case ':' :
// This can be a long or short option, and the way to get at the
// name of it is different.
- throw OptionException(std::string("option `") + option +
- "' missing its required argument");
+ throw OptionException(std::string("option `") + option
+ + "' missing its required argument");
- case '?':
- default:
- throw OptionException(std::string("can't understand option `") + option +
- "'" + suggestCommandLineOptions(option));
+ case '?':
+ default:
+ throw OptionException(std::string("can't understand option `") + option
+ + "'" + suggestCommandLineOptions(option));
}
}
+ // clang-format on
Debug("options") << "got " << nonoptions->size()
<< " non-option arguments." << std::endl;
}
-std::string Options::suggestCommandLineOptions(const std::string& optionName)
-{
- DidYouMean didYouMean;
-
- const char* opt;
- for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
- didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
- }
-
- return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
-}
-
-static const char* smtOptions[] = {
- ${options_smt}$
- NULL
-};/* smtOptions[] */
-
-std::vector<std::string> Options::suggestSmtOptions(
- const std::string& optionName)
-{
- std::vector<std::string> suggestions;
-
- const char* opt;
- for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
- if(std::strstr(opt, optionName.c_str()) != NULL) {
- suggestions.push_back(opt);
- }
- }
-
- return suggestions;
-}
-
+// clang-format off
std::vector<std::vector<std::string> > Options::getOptions() const
{
std::vector< std::vector<std::string> > opts;
${options_getoptions}$
-
return opts;
}
+// clang-format on
void Options::setOption(const std::string& key, const std::string& optionarg)
{
}
}
+// clang-format off
void Options::setOptionInternal(const std::string& key,
const std::string& optionarg)
{
options::OptionsHandler* handler = d_handler;
- Options* options = this;
${setoption_handlers}$
throw UnrecognizedOptionException(key);
}
+// clang-format on
+// clang-format off
std::string Options::getOption(const std::string& key) const
{
Trace("options") << "Options::getOption(" << key << ")" << std::endl;
throw UnrecognizedOptionException(key);
}
+// clang-format on
-#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
-#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+} // namespace cvc5
-} // namespace CVC5
-// clang-format on
projects / cvc5.git / blobdiff