This PR moves the code responsible for parsing the command line to the main folder. Note that the options themselves, and converting strings to the options proper types, calling predicates etc, stays in libcvc5. The PR also slightly refactors the options code to get rid of the assign_* functions.
interactive_shell.cpp
interactive_shell.h
main.h
+ options.h
signal_handlers.cpp
signal_handlers.h
time_limit.cpp
time_limit.h
)
+set(libmain_gen_src_files
+ ${CMAKE_CURRENT_BINARY_DIR}/options.cpp
+)
+set_source_files_properties(${libmain_gen_src_files} PROPERTIES GENERATED TRUE)
#-----------------------------------------------------------------------------#
# Build object library since we will use the object files for cvc5-bin and
# main-test library.
-add_library(main OBJECT ${libmain_src_files})
+add_library(main OBJECT ${libmain_src_files} ${libmain_gen_src_files})
target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER)
if(ENABLE_SHARED)
set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
#include "main/command_executor.h"
#include "main/interactive_shell.h"
#include "main/main.h"
+#include "main/options.h"
#include "main/signal_handlers.h"
#include "main/time_limit.h"
#include "options/base_options.h"
<< endl
<< "cvc5 options:" << endl;
if(full) {
- options::printUsage(ss.str(), *opts.base.out);
+ main::printUsage(ss.str(), *opts.base.out);
} else {
- options::printShortUsage(ss.str(), *opts.base.out);
+ main::printShortUsage(ss.str(), *opts.base.out);
}
}
Options* opts = &pExecutor->getOptions();
// Parse the options
- std::vector<string> filenames = options::parse(*opts, argc, argv, progName);
+ std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
auto limit = install_time_limit(*opts);
}
else if (opts->base.languageHelp)
{
- options::printLanguageHelp(*opts->base.out);
+ main::printLanguageHelp(*opts->base.out);
exit(1);
}
else if (opts->driver.version)
/** Actual cvc5 driver functions **/
int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::api::Solver>&);
-void printUsage(const cvc5::Options&, bool full = false);
#endif /* CVC5__MAIN__MAIN_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Options utilities used in the driver.
+ */
+
+#ifndef CVC5__MAIN__OPTIONS_H
+#define CVC5__MAIN__OPTIONS_H
+
+#include <iosfwd>
+#include <string>
+#include <vector>
+
+#include "api/cpp/cvc5.h"
+
+namespace cvc5::main {
+
+/**
+ * Print overall command-line option usage message, prefixed by
+ * "msg"---which could be an error message causing the usage
+ * output in the first place, e.g. "no such option --foo"
+ */
+void printUsage(const std::string& msg, std::ostream& os);
+
+/**
+ * Print command-line option usage message for only the most-commonly
+ * used options. The message is prefixed by "msg"---which could be
+ * an error message causing the usage output in the first place, e.g.
+ * "no such option --foo"
+ */
+void printShortUsage(const std::string& msg, std::ostream& os);
+
+/** Print help for the --lang command line option */
+void printLanguageHelp(std::ostream& os);
+
+/**
+ * Initialize the Options object options based on the given
+ * command-line arguments given in argc and argv. The return value
+ * is what's left of the command line (that is, the non-option
+ * arguments).
+ *
+ * This function uses getopt_long() and is not thread safe.
+ *
+ * Throws OptionException on failures.
+ *
+ * Preconditions: options and argv must be non-null.
+ */
+std::vector<std::string> parse(api::Solver& solver,
+ int argc,
+ char* argv[],
+ std::string& binaryName);
+
+} // namespace cvc5::options
+
+#endif
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * Options utilities used in the driver.
+ */
+
+#include "main/options.h"
+
+#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
+// force use of optreset; mingw32 croaks on argv-switching otherwise
+#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__
+extern int optreset;
+#endif /* __MINGW64__ */
+
+#include <getopt.h>
+
+// clean up
+#ifdef CVC5_IS_NOT_REALLY_BSD
+# undef _BSD_SOURCE
+#endif /* CVC5_IS_NOT_REALLY_BSD */
+
+#include "base/check.h"
+#include "base/output.h"
+#include "options/didyoumean.h"
+#include "options/option_exception.h"
+
+#include <cstring>
+#include <iostream>
+#include <limits>
+
+namespace cvc5::main {
+
+// clang-format off
+static const std::string commonOptionsDescription =
+ "Most commonly-used cvc5 options:\n"
+${help_common}$
+ ;
+
+static const std::string additionalOptionsDescription =
+ "Additional cvc5 options:\n"
+${help_others}$;
+
+static const std::string optionsFootnote = "\n\
+[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
+ sense of the option.\n\
+";
+
+static const std::string languageDescription =
+ "\
+Languages currently supported as arguments to the -L / --lang option:\n\
+ auto attempt to automatically determine 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\
+ sygus | sygus2 SyGuS version 2.0\n\
+\n\
+Languages currently supported as arguments to the --output-lang option:\n\
+ auto match output language to input 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\
+ ast internal format (simple syntax trees)\n\
+";
+// clang-format on
+
+void printUsage(const std::string& msg, std::ostream& os) {
+ os << msg << "\n" << commonOptionsDescription << "\n\n" << additionalOptionsDescription << std::endl
+ << optionsFootnote << std::endl << std::flush;
+}
+
+void printShortUsage(const std::string& msg, std::ostream& os) {
+ os << msg << "\n" << commonOptionsDescription << std::endl
+ << optionsFootnote << std::endl
+ << "For full usage, please use --help."
+ << std::endl << std::endl << std::flush;
+}
+
+void printLanguageHelp(std::ostream& os) {
+ os << languageDescription << std::flush;
+}
+
+/**
+ * This is a table of long options. By policy, each short option
+ * should have an equivalent long option (but the reverse isn't the
+ * case), so this table should thus contain all command-line options.
+ *
+ * Each option in this array has four elements:
+ *
+ * 1. the long option string
+ * 2. argument behavior for the option:
+ * no_argument - no argument permitted
+ * required_argument - an argument is expected
+ * optional_argument - an argument is permitted but not required
+ * 3. this is a pointer to an int which is set to the 4th entry of the
+ * array if the option is present; or NULL, in which case
+ * getopt_long() returns the 4th entry
+ * 4. the return value for getopt_long() when this long option (or the
+ * value to set the 3rd entry to; see #3)
+ */
+// clang-format off
+static struct option cmdlineOptions[] = {
+ ${cmdline_options}$
+ {nullptr, no_argument, nullptr, '\0'}
+};
+// clang-format on
+
+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 parseInternal(api::Solver& solver, int argc,
+ char* argv[],
+ std::vector<std::string>& nonoptions)
+{
+ Assert(argv != nullptr);
+ if(Debug.isOn("options")) {
+ Debug("options") << "starting a new parseInternal with "
+ << argc << " arguments" << std::endl;
+ for( int i = 0; i < argc ; i++ ){
+ Assert(argv[i] != NULL);
+ Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl;
+ }
+ }
+
+ // Reset getopt(), in the case of multiple calls to parse().
+ // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
+ optind = 0;
+#if HAVE_DECL_OPTRESET
+ optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
+#endif /* HAVE_DECL_OPTRESET */
+
+ // We must parse the binary name, which is manually ignored below. Setting
+ // this to 1 leads to incorrect behavior on some platforms.
+ int main_optind = 0;
+ int old_optind;
+
+
+ while(true) { // Repeat Forever
+
+ optopt = 0;
+
+ optind = main_optind;
+ old_optind = main_optind;
+
+ // If we encounter an element that is not at zero and does not start
+ // with a "-", this is a non-option. We consume this element as a
+ // non-option.
+ if (main_optind > 0 && main_optind < argc &&
+ argv[main_optind][0] != '-') {
+ Debug("options") << "enqueueing " << argv[main_optind]
+ << " as a non-option." << std::endl;
+ nonoptions.push_back(argv[main_optind]);
+ ++main_optind;
+ continue;
+ }
+
+
+ Debug("options") << "[ before, main_optind == " << main_optind << " ]"
+ << std::endl;
+ 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("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
+ << "[ next option will be at pos: " << optind << " ]"
+ << std::endl;
+
+ // The initial getopt_long call should always determine that argv[0]
+ // is not an option and returns -1. We always manually advance beyond
+ // this element.
+ if ( old_optind == 0 && c == -1 ) {
+ Assert(main_optind > 0);
+ continue;
+ }
+
+ if ( c == -1 ) {
+ if(Debug.isOn("options")) {
+ Debug("options") << "done with option parsing" << std::endl;
+ for(int index = optind; index < argc; ++index) {
+ Debug("options") << "remaining " << argv[index] << std::endl;
+ }
+ }
+ break;
+ }
+
+ std::string option = argv[old_optind == 0 ? 1 : old_optind];
+ std::string optionarg = (optarg == nullptr) ? "" : optarg;
+
+ Debug("preemptGetopt") << "processing option " << c
+ << " (`" << char(c) << "'), " << option << std::endl;
+
+ // clang-format off
+ switch(c)
+ {
+ ${options_handler}$
+
+ 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");
+
+ 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;
+}
+
+/**
+ * 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).
+ *
+ * Throws OptionException on failures.
+ */
+std::vector<std::string> parse(
+ api::Solver& solver, int argc, char* argv[], std::string& binaryName)
+{
+ Assert(argv != nullptr);
+
+ const char *progName = argv[0];
+
+ // To debug options parsing, you may prefer to simply uncomment this
+ // and recompile. Debug flags have not been parsed yet so these have
+ // not been set.
+ //DebugChannel.on("options");
+
+ Debug("options") << "argv == " << argv << std::endl;
+
+ // Find the base name of the program.
+ const char *x = strrchr(progName, '/');
+ if(x != nullptr) {
+ progName = x + 1;
+ }
+ binaryName = std::string(progName);
+
+ std::vector<std::string> nonoptions;
+ parseInternal(solver, argc, argv, nonoptions);
+ if (Debug.isOn("options")){
+ for (const auto& no: nonoptions){
+ Debug("options") << "nonoptions " << no << std::endl;
+ }
+ }
+
+ return nonoptions;
+}
+
+} // namespace cvc5::options
#pragma once
+#include "cvc5_export.h"
+
#include <set>
#include <string>
#include <vector>
namespace cvc5 {
-class DidYouMean {
+class CVC5_EXPORT DidYouMean {
public:
using Words = std::set<std::string>;
### Source code templates
-TPL_ASSIGN = '''
-void assign_{module}_{name}(Options& opts, const std::string& option, const std::string& optionarg) {{
- auto value = {handler};
- {predicates}
- opts.{module}.{name} = value;
- opts.{module}.{name}WasSetByUser = true;
- Trace("options") << "user assigned option {name} = " << value << std::endl;
-}}'''
-
-TPL_ASSIGN_BOOL = '''
-void assign_{module}_{name}(Options& opts, const std::string& option, bool value) {{
- {predicates}
- opts.{module}.{name} = value;
- opts.{module}.{name}WasSetByUser = true;
- Trace("options") << "user assigned option {name} = " << value << std::endl;
-}}'''
-
-TPL_CALL_ASSIGN_BOOL = ' assign_{module}_{name}(opts, {option}, {value});'
-TPL_CALL_ASSIGN = ' assign_{module}_{name}(opts, {option}, optionarg);'
+TPL_ASSIGN = ''' opts.{module}.{name} = {handler};
+ opts.{module}.{name}WasSetByUser = true;'''
+TPL_ASSIGN_PRED = ''' auto value = {handler};
+ {predicates}
+ opts.{module}.{name} = value;
+ opts.{module}.{name}WasSetByUser = true;'''
TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));'
optname = option.long_name if option.long else ""
if option.handler:
if option.type == 'void':
- return 'opts.handler().{}("{}", option)'.format(option.handler, optname)
+ return 'opts.handler().{}("{}", name)'.format(option.handler, optname)
else:
- return 'opts.handler().{}("{}", option, optionarg)'.format(option.handler, optname)
+ return 'opts.handler().{}("{}", name, optionarg)'.format(option.handler, optname)
elif option.mode:
return 'stringTo{}(optionarg)'.format(option.type)
- elif option.type != 'bool':
- return 'handleOption<{}>("{}", option, optionarg)'.format(option.type, optname)
- return None
+ return 'handleOption<{}>("{}", name, optionarg)'.format(option.type, optname)
def get_predicates(option):
assert option.type != 'void'
res = []
if option.minimum:
- res.append('opts.handler().checkMinimum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.minimum))
+ res.append('opts.handler().checkMinimum("{}", name, value, static_cast<{}>({}));'.format(optname, option.type, option.minimum))
if option.maximum:
- res.append('opts.handler().checkMaximum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.maximum))
- res += ['opts.handler().{}("{}", option, value);'.format(x, optname)
+ res.append('opts.handler().checkMaximum("{}", name, value, static_cast<{}>({}));'.format(optname, option.type, option.maximum))
+ res += ['opts.handler().{}("{}", name, value);'.format(x, optname)
for x in option.predicates]
return res
# Generate options_handler and getopt_long
cases = []
if option.short:
- cases.append("case '{}':".format(option.short))
+ cases.append("case '{0}': // -{0}".format(option.short))
getopt_short.append(option.short)
if argument_req:
add_getopt_long(alias, argument_req, getopt_long)
if cases:
- if option.type == 'bool' and option.name:
+ if option.type == 'bool':
+ cases.append(
+ ' solver.setOption("{}", "true");'.format(option.long_name)
+ )
+ elif option.type == 'void':
cases.append(
- TPL_CALL_ASSIGN_BOOL.format(
- module=module.id,
- name=option.name,
- option='option',
- value='true'))
- elif option.type != 'void' and option.name and not mode_handler:
+ ' solver.setOption("{}", "");'.format(option.long_name))
+ else:
cases.append(
- TPL_CALL_ASSIGN.format(
- module=module.id,
- name=option.name,
- option='option',
- value='optionarg'))
- elif handler:
- cases.append('{};'.format(handler))
+ ' solver.setOption("{}", optionarg);'.format(option.long_name))
cases.append(' break;')
cond = ' || '.join(
['name == "{}"'.format(x) for x in sorted(names)])
- setoption_handlers.append(' if ({}) {{'.format(cond))
- if option.type == 'bool':
- setoption_handlers.append(
- TPL_CALL_ASSIGN_BOOL.format(
- module=module.id,
- name=option.name,
- option='name',
- value='optionarg == "true"'))
- elif argument_req and option.name and not mode_handler:
- setoption_handlers.append(
- TPL_CALL_ASSIGN.format(
- module=module.id,
- name=option.name,
- option='name'))
+ if setoption_handlers:
+ setoption_handlers.append(' }} else if ({}) {{'.format(cond))
+ else:
+ setoption_handlers.append(' if ({}) {{'.format(cond))
+ if option.name and not mode_handler:
+ if predicates:
+ setoption_handlers.append(
+ TPL_ASSIGN_PRED.format(
+ module=module.id,
+ name=option.name,
+ handler=handler,
+ predicates='\n '.join(predicates)))
+ else:
+ setoption_handlers.append(
+ TPL_ASSIGN.format(
+ module=module.id,
+ name=option.name,
+ handler=handler))
elif option.handler:
h = ' opts.handler().{handler}("{smtname}", name'
if argument_req:
setoption_handlers.append(
h.format(handler=option.handler, smtname=option.long_name))
- setoption_handlers.append(' return;')
- setoption_handlers.append(' }')
if option.name:
getoption_handlers.append(
if option.long and option.type == 'bool' and option.alternate:
cases = []
cases.append(
- 'case {}:// --no-{}'.format(
+ 'case {}: // --no-{}'.format(
g_getopt_long_start + len(getopt_long),
option.long))
if option.alias:
for alias in option.alias:
cases.append(
- 'case {}:// --no-{}'.format(
+ 'case {}: // --no-{}'.format(
g_getopt_long_start + len(getopt_long),
alias))
add_getopt_long('no-{}'.format(alias), argument_req,
getopt_long)
cases.append(
- TPL_CALL_ASSIGN_BOOL.format(
- module=module.id,
- name=option.name, option='option', value='false'))
+ ' solver.setOption("{}", "false");'.format(option.long_name)
+ )
cases.append(' break;')
options_handler.extend(cases)
if option.long_name:
options_getall.append(get_getall(module, option))
-
- # Define handler assign/assignBool
- if not mode_handler:
- if option.type == 'bool':
- assign_impls.append(TPL_ASSIGN_BOOL.format(
- module=module.id,
- name=option.name,
- handler=handler,
- predicates='\n'.join(predicates)
- ))
- elif option.short or option.long:
- assign_impls.append(TPL_ASSIGN.format(
- module=module.id,
- name=option.name,
- handler=handler,
- predicates='\n'.join(predicates)
- ))
-
options_all_names = ', '.join(map(lambda s: '"' + s + '"', sorted(options_names)))
options_all_names = '\n'.join(textwrap.wrap(options_all_names, width=80, break_on_hyphens=False))
'help_others': '\n'.join(help_others),
'options_handler': '\n '.join(options_handler),
'options_short': ''.join(getopt_short),
- 'assigns': '\n'.join(assign_impls),
'options_getall': '\n '.join(options_getall),
'options_all_names': options_all_names,
'getoption_handlers': '\n'.join(getoption_handlers),
{'input': 'options/options_template.h'},
{'input': 'options/options_template.cpp'},
{'input': 'options/options_public_template.cpp'},
+ {'input': 'main/options_template.cpp'},
]
for tpl in module_tpls + global_tpls:
#ifndef CVC5__OPTION_EXCEPTION_H
#define CVC5__OPTION_EXCEPTION_H
+#include "cvc5_export.h"
#include "base/exception.h"
namespace cvc5 {
* Class representing an option-parsing exception such as badly-typed
* or missing arguments, arguments out of bounds, etc.
*/
-class OptionException : public cvc5::Exception
+class CVC5_EXPORT OptionException : public cvc5::Exception
{
public:
OptionException(const std::string& s) : cvc5::Exception(s_errPrefix + s) {}
bool getUfHo(const Options& opts) CVC5_EXPORT;
-/**
- * Get a description of the command-line flags accepted by
- * parse. The returned string will be escaped so that it is
- * suitable as an argument to printf. */
-const std::string& getDescription() CVC5_EXPORT;
-
-/**
- * Print overall command-line option usage message, prefixed by
- * "msg"---which could be an error message causing the usage
- * output in the first place, e.g. "no such option --foo"
- */
-void printUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT;
-
-/**
- * Print command-line option usage message for only the most-commonly
- * used options. The message is prefixed by "msg"---which could be
- * an error message causing the usage output in the first place, e.g.
- * "no such option --foo"
- */
-void printShortUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT;
-
-/** Print help for the --lang command line option */
-void printLanguageHelp(std::ostream& os) CVC5_EXPORT;
-
-/**
- * Initialize the Options object options based on the given
- * command-line arguments given in argc and argv. The return value
- * is what's left of the command line (that is, the non-option
- * arguments).
- *
- * This function uses getopt_long() and is not thread safe.
- *
- * Throws OptionException on failures.
- *
- * Preconditions: options and argv must be non-null.
- */
-std::vector<std::string> parse(Options& opts,
- int argc,
- char* argv[],
- std::string& binaryName) CVC5_EXPORT;
-
/**
* Retrieve an option value by name (as given in key) from the Options object
* opts as a string.
#include "options/options_public.h"
-#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
-// force use of optreset; mingw32 croaks on argv-switching otherwise
-#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__
-extern int optreset;
-#endif /* __MINGW64__ */
-
-#include <getopt.h>
-
-// clean up
-#ifdef CVC5_IS_NOT_REALLY_BSD
-# undef _BSD_SOURCE
-#endif /* CVC5_IS_NOT_REALLY_BSD */
#include "base/check.h"
#include "base/output.h"
-#include "options/didyoumean.h"
#include "options/options_handler.h"
#include "options/options_listener.h"
#include "options/options.h"
bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
-// clang-format off
-static const std::string mostCommonOptionsDescription =
- "\
-Most commonly-used cvc5 options:\n"
-${help_common}$
- ;
-
-static const std::string optionsDescription =
- mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
-${help_others}$;
-
-static const std::string optionsFootnote = "\n\
-[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
- sense of the option.\n\
-";
-
-static const std::string languageDescription =
- "\
-Languages currently supported as arguments to the -L / --lang option:\n\
- auto attempt to automatically determine 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\
- sygus | sygus2 SyGuS version 2.0\n\
-\n\
-Languages currently supported as arguments to the --output-lang option:\n\
- auto match output language to input 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\
- ast internal format (simple syntax trees)\n\
-";
-// clang-format on
-
-const std::string& getDescription()
-{
- return optionsDescription;
-}
-
-void printUsage(const std::string& msg, std::ostream& os) {
- os << msg << optionsDescription << std::endl
- << optionsFootnote << std::endl << std::flush;
-}
-
-void printShortUsage(const std::string& msg, std::ostream& os) {
- os << msg << mostCommonOptionsDescription << std::endl
- << optionsFootnote << std::endl
- << "For full usage, please use --help."
- << std::endl << std::endl << std::flush;
-}
-
-void printLanguageHelp(std::ostream& os) {
- os << languageDescription << std::flush;
-}
-
/** Set a given Options* as "current" just for a particular scope. */
class OptionsGuard {
Options** d_field;
}
};/* class OptionsGuard */
-/**
- * This is a table of long options. By policy, each short option
- * should have an equivalent long option (but the reverse isn't the
- * case), so this table should thus contain all command-line options.
- *
- * Each option in this array has four elements:
- *
- * 1. the long option string
- * 2. argument behavior for the option:
- * no_argument - no argument permitted
- * required_argument - an argument is expected
- * optional_argument - an argument is permitted but not required
- * 3. this is a pointer to an int which is set to the 4th entry of the
- * array if the option is present; or NULL, in which case
- * getopt_long() returns the 4th entry
- * 4. the return value for getopt_long() when this long option (or the
- * value to set the 3rd entry to; see #3)
- *
- * If you add something here, you should add it in src/main/usage.h
- * also, to document it.
- *
- * If you add something that has a short option equivalent, you should
- * add it to the getopt_long() call in parse().
- */
-// clang-format off
-static struct option cmdlineOptions[] = {
- ${cmdline_options}$
- {nullptr, no_argument, nullptr, '\0'}};
-// clang-format on
-
-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('=')));
-}
/**
* This is a default handler for options of built-in C++ type. This
std::string handleOption<std::string>(const std::string& option, const std::string& flag, const std::string& optionarg) {
return optionarg;
}
-
-// clang-format off
-${assigns}$
-// clang-format off
-
-void parseInternal(Options& opts, int argc,
- char* argv[],
- std::vector<std::string>& nonoptions)
-{
- Assert(argv != nullptr);
- if(Debug.isOn("options")) {
- Debug("options") << "starting a new parseInternal with "
- << argc << " arguments" << std::endl;
- for( int i = 0; i < argc ; i++ ){
- Assert(argv[i] != NULL);
- Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl;
- }
- }
-
- // Reset getopt(), in the case of multiple calls to parse().
- // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
- optind = 0;
-#if HAVE_DECL_OPTRESET
- optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
-#endif /* HAVE_DECL_OPTRESET */
-
- // We must parse the binary name, which is manually ignored below. Setting
- // this to 1 leads to incorrect behavior on some platforms.
- int main_optind = 0;
- int old_optind;
-
-
- while(true) { // Repeat Forever
-
- optopt = 0;
- std::string option, optionarg;
-
- optind = main_optind;
- old_optind = main_optind;
-
- // If we encounter an element that is not at zero and does not start
- // with a "-", this is a non-option. We consume this element as a
- // non-option.
- if (main_optind > 0 && main_optind < argc &&
- argv[main_optind][0] != '-') {
- Debug("options") << "enqueueing " << argv[main_optind]
- << " as a non-option." << std::endl;
- nonoptions.push_back(argv[main_optind]);
- ++main_optind;
- continue;
- }
-
-
- Debug("options") << "[ before, main_optind == " << main_optind << " ]"
- << std::endl;
- 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("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
- << "[ next option will be at pos: " << optind << " ]"
- << std::endl;
-
- // The initial getopt_long call should always determine that argv[0]
- // is not an option and returns -1. We always manually advance beyond
- // this element.
- if ( old_optind == 0 && c == -1 ) {
- Assert(main_optind > 0);
- continue;
- }
-
- if ( c == -1 ) {
- if(Debug.isOn("options")) {
- Debug("options") << "done with option parsing" << std::endl;
- for(int index = optind; index < argc; ++index) {
- Debug("options") << "remaining " << argv[index] << std::endl;
- }
- }
- break;
- }
-
- option = argv[old_optind == 0 ? 1 : old_optind];
- optionarg = (optarg == NULL) ? "" : optarg;
-
- Debug("preemptGetopt") << "processing option " << c
- << " (`" << char(c) << "'), " << option << std::endl;
-
- // clang-format off
- switch(c)
- {
-${options_handler}$
-
- 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");
-
- 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;
-}
-
-/**
- * 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).
- *
- * Throws OptionException on failures.
- */
-std::vector<std::string> parse(
- Options & opts, int argc, char* argv[], std::string& binaryName)
-{
- Assert(argv != nullptr);
-
- Options* cur = &Options::current();
- OptionsGuard guard(&cur, &opts);
-
- const char *progName = argv[0];
-
- // To debug options parsing, you may prefer to simply uncomment this
- // and recompile. Debug flags have not been parsed yet so these have
- // not been set.
- //DebugChannel.on("options");
-
- Debug("options") << "options::parse == " << &opts << std::endl;
- Debug("options") << "argv == " << argv << std::endl;
-
- // Find the base name of the program.
- const char *x = strrchr(progName, '/');
- if(x != nullptr) {
- progName = x + 1;
- }
- binaryName = std::string(progName);
-
- std::vector<std::string> nonoptions;
- parseInternal(opts, argc, argv, nonoptions);
- if (Debug.isOn("options")){
- for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
- iend = nonoptions.end(); i != iend; ++i){
- Debug("options") << "nonoptions " << *i << std::endl;
- }
- }
-
- return nonoptions;
+template <>
+bool handleOption<bool>(const std::string& option, const std::string& flag, const std::string& optionarg) {
+ Assert(optionarg == "true" || optionarg == "false");
+ return optionarg == "true";
}
std::string get(const Options& options, const std::string& name)
const std::string& optionarg)
{
// clang-format off
- ${setoption_handlers}$
+${setoption_handlers}$
// clang-format on
- throw OptionException("Unrecognized option key or setting: " + name);
+ }
+ else
+ {
+ throw OptionException("Unrecognized option key or setting: " + name);
+ }
+ Trace("options") << "user assigned option " << name << " = " << optionarg << std::endl;
}
void set(Options& opts, const std::string& name, const std::string& optionarg)
#include "expr/node_manager.h"
#include "expr/node_value.h"
#include "expr/skolem_manager.h"
+#include "options/base_options.h"
+#include "options/language.h"
#include "options/options_public.h"
#include "smt/smt_engine.h"
#include "test_node.h"
TestNode::SetUp();
// setup an SMT engine so that options are in scope
Options opts;
- char* argv[2];
- argv[0] = strdup("");
- argv[1] = strdup("--output-lang=ast");
- std::string progName;
- options::parse(opts, 2, argv, progName);
- free(argv[0]);
- free(argv[1]);
+ opts.base.outputLanguage = OutputLanguage::LANG_AST;
+ opts.base.outputLanguageWasSetByUser = true;
d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
}
projects / cvc5.git / commitdiff