summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.style.yapf5
-rw-r--r--src/main/driver_unified.cpp10
-rw-r--r--src/options/CMakeLists.txt7
-rw-r--r--src/options/base_options.toml6
-rw-r--r--src/options/mkoptions.py123
-rw-r--r--src/options/options_handler.cpp10
-rw-r--r--src/options/options_public.cpp26
-rw-r--r--src/options/options_public.h72
-rw-r--r--src/options/options_public_template.cpp496
-rw-r--r--src/options/options_template.cpp534
-rw-r--r--src/options/options_template.h172
-rw-r--r--src/smt/smt_engine.cpp8
-rw-r--r--test/unit/node/node_black.cpp3
13 files changed, 700 insertions, 772 deletions
diff --git a/.style.yapf b/.style.yapf
new file mode 100644
index 000000000..f9f97e806
--- /dev/null
+++ b/.style.yapf
@@ -0,0 +1,5 @@
+[style]
+based_on_style = pep8
+split_before_arithmetic_operator = true
+split_before_bitwise_operator = true
+split_before_logical_operator = true
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9d221450b..8c86f03cb 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -35,6 +35,7 @@
#include "main/time_limit.h"
#include "options/base_options.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "options/parser_options.h"
#include "options/main_options.h"
#include "options/set_language.h"
@@ -87,9 +88,9 @@ void printUsage(const Options& opts, bool full) {
<< endl
<< "cvc5 options:" << endl;
if(full) {
- Options::printUsage(ss.str(), *opts.base.out);
+ options::printUsage(ss.str(), *opts.base.out);
} else {
- Options::printShortUsage(ss.str(), *opts.base.out);
+ options::printShortUsage(ss.str(), *opts.base.out);
}
}
@@ -103,8 +104,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
progPath = argv[0];
// Parse the options
- std::vector<string> filenames =
- Options::parseOptions(&opts, argc, argv, progName);
+ std::vector<string> filenames = options::parse(opts, argc, argv, progName);
auto limit = install_time_limit(opts);
@@ -115,7 +115,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
}
else if (opts.base.languageHelp)
{
- Options::printLanguageHelp(*opts.base.out);
+ options::printLanguageHelp(*opts.base.out);
exit(1);
}
else if (opts.driver.version)
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 926693185..a548717f3 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -29,7 +29,6 @@ libcvc5_add_sources(
options_handler.cpp
options_handler.h
options_listener.h
- options_public.cpp
options_public.h
outputc.cpp
outputc.h
@@ -67,7 +66,7 @@ set(options_toml_files
string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files})
-libcvc5_add_sources(GENERATED options.h options.cpp ${options_gen_cpp_files})
+libcvc5_add_sources(GENERATED options.h options.cpp options_public.cpp ${options_gen_cpp_files})
list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
@@ -82,7 +81,7 @@ endif()
add_custom_command(
OUTPUT
- options.h options.cpp
+ options.h options.cpp options_public.cpp
${options_gen_cpp_files} ${options_gen_h_files}
${options_gen_doc_files}
COMMAND
@@ -97,6 +96,7 @@ add_custom_command(
${options_toml_files}
module_template.h
module_template.cpp
+ options_public_template.cpp
options_template.h
options_template.cpp
)
@@ -105,6 +105,7 @@ add_custom_target(gen-options
DEPENDS
options.h
options.cpp
+ options_public.cpp
${options_gen_cpp_files}
${options_gen_h_files}
)
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 2223664d1..a766dce67 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -7,21 +7,21 @@ public = true
category = "undocumented"
type = "std::istream*"
default = "&std::cin"
- includes = ["<iosfwd>"]
+ includes = ["<iostream>"]
[[option]]
name = "out"
category = "undocumented"
type = "std::ostream*"
default = "&std::cout"
- includes = ["<iosfwd>"]
+ includes = ["<iostream>"]
[[option]]
name = "err"
category = "undocumented"
type = "std::ostream*"
default = "&std::cerr"
- includes = ["<iosfwd>"]
+ includes = ["<iostream>"]
[[option]]
name = "inputLanguage"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 45b1db4d6..aeff832b5 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -27,6 +27,7 @@
Directory <tpl-src> must contain:
- options_template.cpp
+ - options_public_template.cpp
- module_template.cpp
- module_template.h
@@ -183,6 +184,11 @@ def concat_format(s, objs):
return '\n'.join([s.format(**o.__dict__) for o in objs])
+def get_module_headers(modules):
+ """Render includes for module headers"""
+ return concat_format('#include "{header}"', modules)
+
+
def get_holder_fwd_decls(modules):
"""Render forward declaration of holder structs"""
return concat_format(' struct Holder{id_cap};', modules)
@@ -237,6 +243,19 @@ def get_predicates(option):
return ['opts.handler().{}("{}", option, value);'.format(x, optname)
for x in option.predicates]
+
+def get_getall(module, option):
+ """Render snippet to add option to result of getAll()"""
+ if option.type == 'bool':
+ return 'res.push_back({{"{}", opts.{}.{} ? "true" : "false"}});'.format(
+ option.long_name, module.id, option.name)
+ elif is_numeric_cpp_type(option.type):
+ return 'res.push_back({{"{}", std::to_string(opts.{}.{})}});'.format(
+ option.long_name, module.id, option.name)
+ else:
+ return '{{ std::stringstream ss; ss << opts.{}.{}; res.push_back({{"{}", ss.str()}}); }}'.format(
+ module.id, option.name, option.long_name)
+
class Module(object):
"""Options module.
@@ -705,25 +724,26 @@ def add_getopt_long(long_name, argument_req, getopt_long):
'required' if argument_req else 'no', value))
-def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp):
+def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h,
+ tpl_options_cpp, tpl_options_public):
"""
- Generate code for all option modules (options.cpp, options_holder.h).
+ Generate code for all option modules (options.cpp).
"""
headers_module = [] # generated *_options.h header includes
headers_handler = set() # option includes (for handlers, predicates, ...)
getopt_short = [] # short options for getopt_long
getopt_long = [] # long options for getopt_long
- options_smt = [] # all options names accessible via {set,get}-option
+ options_getall = [] # options for options::getAll()
options_getoptions = [] # options for Options::getOptions()
options_handler = [] # option handler calls
- defaults = [] # default values
- custom_handlers = [] # custom handler implementations assign/assignBool
help_common = [] # help text for all common options
help_others = [] # help text for all non-common options
setoption_handlers = [] # handlers for set-option command
getoption_handlers = [] # handlers for get-option command
+ assign_impls = []
+
sphinxgen = SphinxGenerator()
for module in modules:
@@ -809,7 +829,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
cond = ' || '.join(
['key == "{}"'.format(x) for x in sorted(keys)])
- setoption_handlers.append('if({}) {{'.format(cond))
+ setoption_handlers.append(' if ({}) {{'.format(cond))
if option.type == 'bool':
setoption_handlers.append(
TPL_CALL_ASSIGN_BOOL.format(
@@ -824,15 +844,15 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
name=option.name,
option='key'))
elif option.handler:
- h = 'handler->{handler}("{smtname}", key'
+ h = ' opts.handler().{handler}("{smtname}", key'
if argument_req:
h += ', optionarg'
h += ');'
setoption_handlers.append(
h.format(handler=option.handler, smtname=option.long_name))
- setoption_handlers.append('return;')
- setoption_handlers.append('}')
+ setoption_handlers.append(' return;')
+ setoption_handlers.append(' }')
if option.name:
getoption_handlers.append(
@@ -880,80 +900,51 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
cases.append(' break;')
options_handler.extend(cases)
- optname = option.long
- # collect options available to the SMT-frontend
- if optname:
- options_smt.append('"{}",'.format(optname))
-
if option.name:
# Build options for options::getOptions()
- if optname:
- # collect SMT option names
- options_smt.append('"{}",'.format(optname))
-
- if option.type == 'bool':
- s = 'opts.push_back({{"{}", {}.{} ? "true" : "false"}});'.format(
- optname, module.id, option.name)
- elif is_numeric_cpp_type(option.type):
- s = 'opts.push_back({{"{}", std::to_string({}.{})}});'.format(
- optname, module.id, option.name)
- else:
- s = '{{ std::stringstream ss; ss << {}.{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
- module.id, option.name, optname)
- options_getoptions.append(s)
+ if option.long_name:
+ options_getall.append(get_getall(module, option))
# Define handler assign/assignBool
if not mode_handler:
if option.type == 'bool':
- custom_handlers.append(TPL_ASSIGN_BOOL.format(
+ 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:
- custom_handlers.append(TPL_ASSIGN.format(
+ assign_impls.append(TPL_ASSIGN.format(
module=module.id,
name=option.name,
handler=handler,
predicates='\n'.join(predicates)
))
- # Default option values
- default = option.default if option.default else ''
- # Prepend enum name
- if option.mode and option.type not in default:
- default = '{}::{}'.format(option.type, default)
- defaults.append('{}({})'.format(option.name, default))
- defaults.append('{}WasSetByUser(false)'.format(option.name))
-
- write_file(dst_dir, 'options.h', tpl_options_h.format(
- holder_fwd_decls=get_holder_fwd_decls(modules),
- holder_mem_decls=get_holder_mem_decls(modules),
- holder_ref_decls=get_holder_ref_decls(modules),
- ))
-
- write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(
- headers_module='\n'.join(headers_module),
- headers_handler='\n'.join(sorted(list(headers_handler))),
- holder_mem_copy=get_holder_mem_copy(modules),
- holder_mem_inits=get_holder_mem_inits(modules),
- holder_ref_inits=get_holder_ref_inits(modules),
- custom_handlers='\n'.join(custom_handlers),
- module_defaults=',\n '.join(defaults),
- help_common='\n'.join(help_common),
- help_others='\n'.join(help_others),
- cmdline_options='\n '.join(getopt_long),
- options_short=''.join(getopt_short),
- options_handler='\n '.join(options_handler),
- option_value_begin=g_getopt_long_start,
- option_value_end=g_getopt_long_start + len(getopt_long),
- options_smt='\n '.join(options_smt),
- options_getoptions='\n '.join(options_getoptions),
- setoption_handlers='\n'.join(setoption_handlers),
- getoption_handlers='\n'.join(getoption_handlers)
- ))
+ data = {
+ 'holder_fwd_decls': get_holder_fwd_decls(modules),
+ 'holder_mem_decls': get_holder_mem_decls(modules),
+ 'holder_ref_decls': get_holder_ref_decls(modules),
+ 'headers_module': get_module_headers(modules),
+ 'headers_handler': '\n'.join(sorted(list(headers_handler))),
+ 'holder_mem_inits': get_holder_mem_inits(modules),
+ 'holder_ref_inits': get_holder_ref_inits(modules),
+ 'holder_mem_copy': get_holder_mem_copy(modules),
+ 'cmdline_options': '\n '.join(getopt_long),
+ 'help_common': '\n'.join(help_common),
+ '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),
+ 'getoption_handlers': '\n'.join(getoption_handlers),
+ 'setoption_handlers': '\n'.join(setoption_handlers),
+ }
+ write_file(dst_dir, 'options.h', tpl_options_h.format(**data))
+ write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(**data))
+ write_file(dst_dir, 'options_public.cpp', tpl_options_public.format(**data))
if os.path.isdir('{}/docs/'.format(build_dir)):
sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst')
@@ -1093,6 +1084,7 @@ def mkoptions_main():
# Read source code template files from source directory.
tpl_module_h = read_tpl(src_dir, 'module_template.h')
tpl_module_cpp = read_tpl(src_dir, 'module_template.cpp')
+ tpl_options_public = read_tpl(src_dir, 'options_public_template.cpp')
tpl_options_h = read_tpl(src_dir, 'options_template.h')
tpl_options_cpp = read_tpl(src_dir, 'options_template.cpp')
@@ -1113,8 +1105,7 @@ def mkoptions_main():
codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp)
# Create options.cpp in destination directory
- codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp)
-
+ codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp, tpl_options_public)
if __name__ == "__main__":
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e423dc149..7a80c4d7a 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -155,11 +155,11 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
throw OptionException(ss.str());
}
- if (options::bvSolver() != options::BVSolver::BITBLAST
+ if (d_options->bv.bvSolver != options::BVSolver::BITBLAST
&& (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
|| m == SatSolverMode::KISSAT))
{
- if (options::bitblastMode() == options::BitblastMode::LAZY
+ if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
&& d_options->bv.bitblastModeWasSetByUser)
{
throwLazyBBUnsupported(m);
@@ -178,9 +178,9 @@ void OptionsHandler::checkBitblastMode(const std::string& option,
options::bv::setDefaultBitvectorEqualitySolver(*d_options, true);
options::bv::setDefaultBitvectorInequalitySolver(*d_options, true);
options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true);
- if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
+ if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT)
{
- throwLazyBBUnsupported(options::bvSatSolver());
+ throwLazyBBUnsupported(d_options->bv.bvSatSolver);
}
}
else if (m == BitblastMode::EAGER)
@@ -195,7 +195,7 @@ void OptionsHandler::setBitblastAig(const std::string& option,
{
if(arg) {
if (d_options->bv.bitblastModeWasSetByUser) {
- if (options::bitblastMode() != options::BitblastMode::EAGER)
+ if (d_options->bv.bitblastMode != options::BitblastMode::EAGER)
{
throw OptionException("bitblast-aig must be used with eager bitblaster");
}
diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
deleted file mode 100644
index 552058312..000000000
--- a/src/options/options_public.cpp
+++ /dev/null
@@ -1,26 +0,0 @@
-/******************************************************************************
- * 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.
- * ****************************************************************************
- *
- * Definitions of public facing interface functions for Options.
- *
- * These are all one line wrappers for accessing the internal option data.
- */
-
-#include "options_public.h"
-
-#include "options/uf_options.h"
-
-namespace cvc5::options {
-
-bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
-
-} // namespace cvc5::options
diff --git a/src/options/options_public.h b/src/options/options_public.h
index 60929c96c..03d7ec41a 100644
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -10,12 +10,7 @@
* directory for licensing information.
* ****************************************************************************
*
- * Public facing functions for options that need to be accessed from the
- * outside.
- *
- * These are all one line wrappers for accessing the internal option data so
- * that external code (including parser/ and main/) does not need to include
- * the option modules (*_options.h).
+ * Global (command-line, set-option, ...) parameters for SMT.
*/
#include "cvc5_public.h"
@@ -23,12 +18,77 @@
#ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H
#define CVC5__OPTIONS__OPTIONS_PUBLIC_H
+#include <iosfwd>
+#include <string>
+#include <vector>
+
+#include "cvc5_export.h"
#include "options/options.h"
namespace cvc5::options {
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.
+ */
+std::string get(const Options& opts, const std::string& key) CVC5_EXPORT;
+
+/**
+ * Update the Options object opts, set the value of the option specified by key
+ * to the value parsed from optionarg.
+ */
+void set(Options& opts,
+ const std::string& key,
+ const std::string& optionarg) CVC5_EXPORT;
+
+/**
+ * Get the setting for all options.
+ */
+std::vector<std::vector<std::string> > getAll(const Options& opts) CVC5_EXPORT;
+
} // namespace cvc5::options
#endif
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
new file mode 100644
index 000000000..70c6f420a
--- /dev/null
+++ b/src/options/options_public_template.cpp
@@ -0,0 +1,496 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Global (command-line, set-option, ...) parameters for SMT.
+ */
+
+#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"
+#include "options/uf_options.h"
+${headers_module}$
+${headers_handler}$
+
+#include <cstring>
+#include <iostream>
+#include <limits>
+
+namespace cvc5::options {
+
+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;
+ Options* d_old;
+public:
+ OptionsGuard(Options** field, Options* opts) :
+ d_field(field),
+ d_old(*field) {
+ *field = opts;
+ }
+ ~OptionsGuard() {
+ *d_field = d_old;
+ }
+};/* 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
+ * template is really just a helper for the handleOption() template,
+ * below. Variants of this template handle numeric and non-numeric,
+ * integral and non-integral, signed and unsigned C++ types.
+ * handleOption() makes sure to instantiate the right one.
+ *
+ * This implements default behavior when e.g. an option is
+ * unsigned but the user specifies a negative argument; etc.
+ */
+template <class T, bool is_numeric, bool is_integer>
+struct OptionHandler {
+ static T handle(const std::string& option, const std::string& flag, const std::string& optionarg);
+};/* struct OptionHandler<> */
+
+/** Variant for integral C++ types */
+template <class T>
+struct OptionHandler<T, true, true> {
+ static bool stringToInt(T& t, const std::string& str) {
+ std::istringstream ss(str);
+ ss >> t;
+ char tmp;
+ return !(ss.fail() || ss.get(tmp));
+ }
+
+ static bool containsMinus(const std::string& str) {
+ return str.find('-') != std::string::npos;
+ }
+
+ static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
+ try {
+ T i;
+ bool success = stringToInt(i, optionarg);
+
+ if(!success){
+ throw OptionException(flag + ": failed to parse "+ optionarg +
+ " as an integer of the appropriate type.");
+ }
+
+ // Depending in the platform unsigned numbers with '-' signs may parse.
+ // Reject these by looking for any minus if it is not signed.
+ if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
+ // unsigned type but user gave negative argument
+ throw OptionException(flag + " requires a nonnegative argument");
+ } else if(i < std::numeric_limits<T>::min()) {
+ // negative overflow for type
+ std::stringstream ss;
+ ss << flag << " requires an argument >= "
+ << std::numeric_limits<T>::min();
+ throw OptionException(ss.str());
+ } else if(i > std::numeric_limits<T>::max()) {
+ // positive overflow for type
+ std::stringstream ss;
+ ss << flag << " requires an argument <= "
+ << std::numeric_limits<T>::max();
+ throw OptionException(ss.str());
+ }
+
+ return i;
+
+ // if(std::numeric_limits<T>::is_signed) {
+ // return T(i.getLong());
+ // } else {
+ // return T(i.getUnsignedLong());
+ // }
+ } catch(std::invalid_argument&) {
+ // user gave something other than an integer
+ throw OptionException(flag + " requires an integer argument");
+ }
+ }
+};/* struct OptionHandler<T, true, true> */
+
+/** Variant for numeric but non-integral C++ types */
+template <class T>
+struct OptionHandler<T, true, false> {
+ static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
+ std::stringstream inss(optionarg);
+ long double r;
+ inss >> r;
+ if(! inss.eof()) {
+ // we didn't consume the whole string (junk at end)
+ throw OptionException(flag + " requires a numeric argument");
+ }
+
+ if(! std::numeric_limits<T>::is_signed && r < 0.0) {
+ // unsigned type but user gave negative value
+ throw OptionException(flag + " requires a nonnegative argument");
+ } else if(r < -std::numeric_limits<T>::max()) {
+ // negative overflow for type
+ std::stringstream ss;
+ ss << flag << " requires an argument >= "
+ << -std::numeric_limits<T>::max();
+ throw OptionException(ss.str());
+ } else if(r > std::numeric_limits<T>::max()) {
+ // positive overflow for type
+ std::stringstream ss;
+ ss << flag << " requires an argument <= "
+ << std::numeric_limits<T>::max();
+ throw OptionException(ss.str());
+ }
+
+ return T(r);
+ }
+};/* struct OptionHandler<T, true, false> */
+
+/** Variant for non-numeric C++ types */
+template <class T>
+struct OptionHandler<T, false, false> {
+ static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
+ T::unsupported_handleOption_call___please_write_me;
+ // The above line causes a compiler error if this version of the template
+ // is ever instantiated (meaning that a specialization is missing). So
+ // don't worry about the segfault in the next line, the "return" is only
+ // there to keep the compiler from giving additional, distracting errors
+ // and warnings.
+ return *(T*)0;
+ }
+};/* struct OptionHandler<T, false, false> */
+
+/** Handle an option of type T in the default way. */
+template <class T>
+T handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) {
+ return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, flag, optionarg);
+}
+
+/** Handle an option of type std::string in the default way. */
+template <>
+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;
+}
+
+std::string get(const Options& options, const std::string& key)
+{
+ Trace("options") << "Options::getOption(" << key << ")" << std::endl;
+ ${getoption_handlers}$
+
+ throw UnrecognizedOptionException(key);
+}
+
+void setInternal(Options& opts, const std::string& key,
+ const std::string& optionarg)
+ {
+ ${setoption_handlers}$
+ throw UnrecognizedOptionException(key);
+}
+
+void set(Options& opts, const std::string& key, const std::string& optionarg)
+{
+
+ Trace("options") << "setOption(" << key << ", " << optionarg << ")"
+ << std::endl;
+ // first update this object
+ setInternal(opts, key, optionarg);
+ // then, notify the provided listener
+ opts.notifyListener(key);
+}
+
+std::vector<std::vector<std::string> > getAll(const Options& opts)
+{
+ std::vector<std::vector<std::string>> res;
+
+${options_getall}$
+
+ return res;
+}
+
+} // namespace cvc5::options
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 2c22065c2..db58c3a4a 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -13,43 +13,11 @@
* 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 "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 <unistd.h>
-#include <string.h>
-#include <time.h>
-
-#include <cstdio>
-#include <cstdlib>
-#include <cstring>
-#include <iomanip>
-#include <new>
-#include <string>
-#include <sstream>
-#include <limits>
+#include "options/options.h"
#include "base/check.h"
#include "base/exception.h"
#include "base/output.h"
-#include "options/didyoumean.h"
#include "options/language.h"
#include "options/options_handler.h"
#include "options/options_listener.h"
@@ -65,175 +33,22 @@ using namespace cvc5;
using namespace cvc5::options;
// clang-format on
-namespace cvc5 {
-
-thread_local Options* Options::s_current = NULL;
-
-/**
- * This is a default handler for options of built-in C++ type. This
- * template is really just a helper for the handleOption() template,
- * below. Variants of this template handle numeric and non-numeric,
- * integral and non-integral, signed and unsigned C++ types.
- * handleOption() makes sure to instantiate the right one.
- *
- * This implements default behavior when e.g. an option is
- * unsigned but the user specifies a negative argument; etc.
- */
-template <class T, bool is_numeric, bool is_integer>
-struct OptionHandler {
- static T handle(const std::string& option,
- const std::string& flag,
- const std::string& optionarg);
-};/* struct OptionHandler<> */
-
-/** Variant for integral C++ types */
-template <class T>
-struct OptionHandler<T, true, true> {
- static bool stringToInt(T& t, const std::string& str) {
- std::istringstream ss(str);
- ss >> t;
- char tmp;
- return !(ss.fail() || ss.get(tmp));
- }
-
- static bool containsMinus(const std::string& str) {
- return str.find('-') != std::string::npos;
- }
-
- static T handle(const std::string& option,
- const std::string& flag,
- const std::string& optionarg)
- {
- try {
- T i;
- bool success = stringToInt(i, optionarg);
-
- if(!success){
- throw OptionException(flag + ": failed to parse " + optionarg
- + " as an integer of the appropriate type.");
- }
-
- // Depending in the platform unsigned numbers with '-' signs may parse.
- // Reject these by looking for any minus if it is not signed.
- if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
- // unsigned type but user gave negative argument
- throw OptionException(flag + " requires a nonnegative argument");
- } else if(i < std::numeric_limits<T>::min()) {
- // negative overflow for type
- std::stringstream ss;
- ss << flag
- << " requires an argument >= " << std::numeric_limits<T>::min();
- throw OptionException(ss.str());
- } else if(i > std::numeric_limits<T>::max()) {
- // positive overflow for type
- std::stringstream ss;
- ss << flag
- << " requires an argument <= " << std::numeric_limits<T>::max();
- throw OptionException(ss.str());
- }
-
- return i;
-
- // if(std::numeric_limits<T>::is_signed) {
- // return T(i.getLong());
- // } else {
- // return T(i.getUnsignedLong());
- // }
- } catch(std::invalid_argument&) {
- // user gave something other than an integer
- throw OptionException(flag + " requires an integer argument");
- }
- }
-};/* struct OptionHandler<T, true, true> */
-
-/** Variant for numeric but non-integral C++ types */
-template <class T>
-struct OptionHandler<T, true, false> {
- static T handle(const std::string& option,
- const std::string& flag,
- const std::string& optionarg)
- {
- std::stringstream inss(optionarg);
- long double r;
- inss >> r;
- if (!inss.eof())
- {
- // we didn't consume the whole string (junk at end)
- throw OptionException(flag + " requires a numeric argument");
- }
-
- if(! std::numeric_limits<T>::is_signed && r < 0.0) {
- // unsigned type but user gave negative value
- throw OptionException(flag + " requires a nonnegative argument");
- } else if(r < -std::numeric_limits<T>::max()) {
- // negative overflow for type
- std::stringstream ss;
- ss << flag
- << " requires an argument >= " << -std::numeric_limits<T>::max();
- throw OptionException(ss.str());
- } else if(r > std::numeric_limits<T>::max()) {
- // positive overflow for type
- std::stringstream ss;
- ss << flag
- << " requires an argument <= " << std::numeric_limits<T>::max();
- throw OptionException(ss.str());
- }
-
- return T(r);
- }
-};/* struct OptionHandler<T, true, false> */
-
-/** Variant for non-numeric C++ types */
-template <class T>
-struct OptionHandler<T, false, false> {
- static T handle(const std::string& option,
- const std::string& flag,
- const std::string& optionarg)
- {
- T::unsupported_handleOption_call___please_write_me;
- // The above line causes a compiler error if this version of the template
- // is ever instantiated (meaning that a specialization is missing). So
- // don't worry about the segfault in the next line, the "return" is only
- // there to keep the compiler from giving additional, distracting errors
- // and warnings.
- return *(T*)0;
- }
-};/* struct OptionHandler<T, false, false> */
-
-/** Handle an option of type T in the default way. */
-template <class T>
-T handleOption(const std::string& option,
- const std::string& flag,
- const std::string& optionarg)
-{
- return OptionHandler<T,
- std::numeric_limits<T>::is_specialized,
- std::numeric_limits<T>::is_integer>::handle(option,
- flag,
- optionarg);
-}
-
-/** Handle an option of type std::string in the default way. */
-template <>
-std::string handleOption<std::string>(const std::string& option,
- const std::string& flag,
- const std::string& optionarg)
+namespace cvc5
{
- return optionarg;
-}
+ thread_local Options* Options::s_current = nullptr;
-Options::Options(OptionsListener* ol)
- : d_handler(new options::OptionsHandler(this)),
+ Options::Options(OptionsListener * ol)
+ :
+ d_olisten(ol),
// clang-format off
${holder_mem_inits}$
${holder_ref_inits}$
// clang-format on
- d_olisten(ol)
-{}
+ d_handler(std::make_unique<options::OptionsHandler>(this))
+ {
+ }
-Options::~Options() {
- delete d_handler;
-}
+ Options::~Options() {}
void Options::copyValues(const Options& options){
if(this != &options) {
@@ -244,333 +59,14 @@ ${holder_mem_copy}$
}
void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
-
-// clang-format off
-${custom_handlers}$
-// clang-format on
-
-static const std::string mostCommonOptionsDescription =
- "\
-Most commonly-used cvc5 options:\n"
- // clang-format off
-${help_common}$
- // clang-format on
- ;
-
-// 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\
- 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\
-";
-
-std::string Options::getDescription() const {
- return optionsDescription;
-}
-
-void Options::printUsage(const std::string msg, std::ostream& out) {
- out << msg << optionsDescription << std::endl
- << optionsFootnote << std::endl << std::flush;
-}
-
-void Options::printShortUsage(const std::string msg, std::ostream& out) {
- out << msg << mostCommonOptionsDescription << std::endl
- << optionsFootnote << std::endl
- << "For full usage, please use --help."
- << std::endl << std::endl << std::flush;
-}
-
-void Options::printLanguageHelp(std::ostream& out) {
- out << 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)
- *
- * 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 parseOptions().
- */
-// clang-format off
-static struct option cmdlineOptions[] = {
- ${cmdline_options}$
- {nullptr, no_argument, nullptr, '\0'}};
-// clang-format on
-
-namespace options {
-
-/** Set a given Options* as "current" just for a particular scope. */
-class OptionsGuard {
- Options** d_field;
- Options* d_old;
-public:
- OptionsGuard(Options** field, Options* opts) :
- d_field(field),
- d_old(*field) {
- *field = opts;
- }
- ~OptionsGuard() {
- *d_field = d_old;
- }
-};/* class OptionsGuard */
-
-} // namespace 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).
- *
- * Throws OptionException on failures.
- */
-std::vector<std::string> Options::parseOptions(Options* options,
- int argc,
- char* argv[],
- std::string& binaryName)
-{
- Assert(options != NULL);
- Assert(argv != NULL);
-
- options::OptionsGuard guard(&s_current, options);
-
- 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::parseOptions == " << options << std::endl;
- Debug("options") << "argv == " << argv << std::endl;
-
- // Find the base name of the program.
- const char *x = strrchr(progName, '/');
- if(x != NULL) {
- progName = x + 1;
- }
- binaryName = std::string(progName);
-
- std::vector<std::string> 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){
- Debug("options") << "nonoptions " << *i << std::endl;
- }
- }
-
- return nonoptions;
-}
-
-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)
-{
- Options& opts = *this;
- if(Debug.isOn("options")) {
- Debug("options") << "starting a new parseOptionsRecursive 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 parseOptions().
- // 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)
+
+void Options::notifyListener(const std::string& key)
+ {
+ if (d_olisten != nullptr)
{
-${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));
+ d_olisten->notifySetOption(key);
}
}
- // clang-format on
-
- Debug("options") << "got " << nonoptions->size()
- << " non-option arguments." << std::endl;
-}
-
-// 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)
-{
- Trace("options") << "setOption(" << key << ", " << optionarg << ")"
- << std::endl;
- // first update this object
- setOptionInternal(key, optionarg);
- // then, notify the provided listener
- if (d_olisten != nullptr)
- {
- d_olisten->notifySetOption(key);
- }
-}
-
-// clang-format off
-void Options::setOptionInternal(const std::string& key,
- const std::string& optionarg)
-{
- options::OptionsHandler* handler = d_handler;
- Options& opts = *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;
- const Options& options = *this;
- ${getoption_handlers}$
-
- throw UnrecognizedOptionException(key);
-}
-// clang-format on
} // namespace cvc5
diff --git a/src/options/options_template.h b/src/options/options_template.h
index e9a4a6999..a4e595f0d 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -25,46 +25,20 @@
#include "base/listener.h"
#include "cvc5_export.h"
-#include "options/language.h"
-#include "options/printer_modes.h"
namespace cvc5 {
-
-namespace api {
-class Solver;
-}
namespace options {
- struct OptionsHolder;
class OptionsHandler;
// clang-format off
${holder_fwd_decls}$
// clang-format on
- } // namespace options
+} // namespace options
class OptionsListener;
class CVC5_EXPORT Options
{
- friend api::Solver;
-
- /** The handler for the options of the theory. */
- options::OptionsHandler* d_handler;
-
-// clang-format off
-${holder_mem_decls}$
-// clang-format on
- public:
-// clang-format off
-${holder_ref_decls}$
-// clang-format on
-
- private:
-
- /** The current Options in effect */
- static thread_local Options* s_current;
-
- friend class options::OptionsHandler;
-
+ public:
/**
* Options cannot be copied as they are given an explicit list of
* Listeners to respond to.
@@ -77,25 +51,25 @@ ${holder_ref_decls}$
*/
Options& operator=(const Options& options) = delete;
-public:
- class OptionsScope
- {
- private:
- Options* d_oldOptions;
- public:
- OptionsScope(Options* newOptions) :
- d_oldOptions(Options::s_current)
- {
- Options::s_current = newOptions;
- }
- ~OptionsScope(){
- Options::s_current = d_oldOptions;
- }
- };
+ class OptionsScope
+ {
+ private:
+ Options* d_oldOptions;
+ public:
+ OptionsScope(Options* newOptions) :
+ d_oldOptions(Options::s_current)
+ {
+ Options::s_current = newOptions;
+ }
+ ~OptionsScope(){
+ Options::s_current = d_oldOptions;
+ }
+ };
+ friend class OptionsScope;
/** Return true if current Options are null */
static inline bool isCurrentNull() {
- return s_current == NULL;
+ return s_current == nullptr;
}
/** Get the current Options in effect */
@@ -117,103 +91,31 @@ public:
*/
void copyValues(const Options& options);
- /**
- * Set the value of the given option by key.
- *
- * Throws OptionException or ModalException on failures.
- */
- void setOption(const std::string& key, const std::string& optionarg);
-
- /**
- * Gets the value of the given option by key and returns value as a string.
- *
- * Throws OptionException on failures, such as key not being the name of an
- * option.
- */
- std::string getOption(const std::string& key) const;
-
- // Static accessor functions.
- // TODO: Document these.
- static std::ostream* currentGetOut();
-
- /**
- * Get a description of the command-line flags accepted by
- * parseOptions. The returned string will be escaped so that it is
- * suitable as an argument to printf. */
- std::string getDescription() const;
-
- /**
- * 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"
- */
- static void printUsage(const std::string msg, std::ostream& out);
-
- /**
- * 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"
- */
- static void printShortUsage(const std::string msg, std::ostream& out);
-
- /** Print help for the --lang command line option */
- static void printLanguageHelp(std::ostream& out);
-
- /**
- * 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.
- */
- static std::vector<std::string> parseOptions(Options* options,
- int argc,
- char* argv[],
- std::string& binaryName);
-
- /**
- * Get the setting for all options.
- */
- std::vector<std::vector<std::string> > getOptions() const;
-
/** Set the generic listener associated with this class to ol */
void setListener(OptionsListener* ol);
- /** Sends a std::flush to getErr(). */
- void flushErr();
-
- /** Sends a std::flush to getOut(). */
- void flushOut();
+ void notifyListener(const std::string& key);
private:
/** Pointer to the options listener, if one exists */
- OptionsListener* d_olisten;
- /**
- * Helper method for setOption, updates this object for setting the given
- * option.
- */
- void setOptionInternal(const std::string& key, const std::string& optionarg);
- /**
- * Internal procedure for implementing the parseOptions function.
- * Initializes the options object based on the given command-line
- * arguments. The command line arguments are stored in argc/argv.
- * Nonoptions are stored into nonoptions.
- *
- * This is not thread safe.
- *
- * Throws OptionException on failures.
- *
- * Preconditions: options, extender and nonoptions are non-null.
- */
- void parseOptionsRecursive(int argc,
- char* argv[],
- std::vector<std::string>* nonoptions);
+ OptionsListener* d_olisten = nullptr;
+
+// clang-format off
+${holder_mem_decls}$
+// clang-format on
+ public:
+// clang-format off
+${holder_ref_decls}$
+// clang-format on
+
+ private:
+ /** The handler for the options of the theory. */
+ std::unique_ptr<options::OptionsHandler> d_handler;
+
+ /** The current Options in effect */
+ static thread_local Options* s_current;
+
+
}; /* class Options */
} // namespace cvc5
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b09fdb4d7..bbd65c24f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -27,6 +27,8 @@
#include "options/language.h"
#include "options/main_options.h"
#include "options/option_exception.h"
+#include "options/options_public.h"
+#include "options/parser_options.h"
#include "options/printer_options.h"
#include "options/proof_options.h"
#include "options/smt_options.h"
@@ -549,7 +551,7 @@ std::string SmtEngine::getInfo(const std::string& key) const
}
Assert(key == "all-options");
// get the options, like all-statistics
- return toSExpr(Options::current().getOptions());
+ return toSExpr(options::getAll(getOptions()));
}
void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
@@ -1978,7 +1980,7 @@ void SmtEngine::setOption(const std::string& key, const std::string& value)
}
std::string optionarg = value;
- getOptions().setOption(key, optionarg);
+ options::set(getOptions(), key, optionarg);
}
void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
@@ -2043,7 +2045,7 @@ std::string SmtEngine::getOption(const std::string& key) const
return nm->mkNode(Kind::SEXPR, result).toString();
}
- std::string atom = getOptions().getOption(key);
+ std::string atom = options::get(getOptions(), key);
if (atom != "true" && atom != "false")
{
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 522270de4..787dd77ca 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -27,6 +27,7 @@
#include "expr/node_manager.h"
#include "expr/node_value.h"
#include "expr/skolem_manager.h"
+#include "options/options_public.h"
#include "smt/smt_engine.h"
#include "test_node.h"
#include "theory/rewriter.h"
@@ -68,7 +69,7 @@ class TestNodeBlackNode : public TestNode
argv[0] = strdup("");
argv[1] = strdup("--output-lang=ast");
std::string progName;
- Options::parseOptions(&opts, 2, argv, progName);
+ options::parse(opts, 2, argv, progName);
free(argv[0]);
free(argv[1]);
d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback