This PR splits the OptionsHolder class into separate holder classes for every options module and makes them directly accessible via appropriate Options::<module>() methods. We forward declare these new holder classes and thereby retain that we only need to recompile when we change an option module that is explicitly included.
All (generated) methods that previously accessed the old holder object are changed to instead use the new holder objects.
This PR does the bare minimum to do this change, further PRs will eventually get rid of all template specializations that currently surround our options class.
open_ostream.h
option_exception.cpp
option_exception.h
- options.h
options_handler.cpp
options_handler.h
options_listener.h
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.cpp ${options_gen_cpp_files})
+libcvc5_add_sources(GENERATED options.h options.cpp ${options_gen_cpp_files})
list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
add_custom_command(
OUTPUT
- options.cpp options_holder.h
+ options.h options.cpp
${options_gen_cpp_files} ${options_gen_h_files}
COMMAND
${PYTHON_EXECUTABLE}
${options_toml_files}
module_template.h
module_template.cpp
- options_holder_template.h
+ options_template.h
options_template.cpp
)
add_custom_target(gen-options
DEPENDS
+ options.h
options.cpp
- options_holder.h
${options_gen_cpp_files}
${options_gen_h_files}
)
### Source code templates
-TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER'
-
TPL_IMPL_ASSIGN = \
"""template <> void Options::assign(
options::{name}__option_t,
{{
auto parsedval = {handler};
{predicates}
- d_holder->{name} = parsedval;
- d_holder->{name}__setByUser__ = true;
+ {module}().{name} = parsedval;
+ {module}().{name}__setByUser__ = true;
Trace("options") << "user assigned option {name}" << std::endl;
}}"""
bool value)
{{
{predicates}
- d_holder->{name} = value;
- d_holder->{name}__setByUser__ = true;
+ {module}().{name} = value;
+ {module}().{name}__setByUser__ = true;
Trace("options") << "user assigned option {name}" << std::endl;
}}"""
TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});'
-
-TPL_HOLDER_MACRO = '#define ' + TPL_HOLDER_MACRO_NAME
-
-TPL_HOLDER_MACRO_ATTR = " {name}__option_t::type {name};\\\n"
+TPL_HOLDER_MACRO_ATTR = " {type} {name};\\\n"
TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__ = false;"
-TPL_HOLDER_MACRO_ATTR_DEF = " {name}__option_t::type {name} = {default};\\\n"
+TPL_HOLDER_MACRO_ATTR_DEF = " {type} {name} = {default};\\\n"
TPL_HOLDER_MACRO_ATTR_DEF += " bool {name}__setByUser__ = false;"
TPL_OPTION_STRUCT_RW = \
TPL_IMPL_SET = TPL_DECL_SET[:-1] + \
"""
{{
- return d_holder->{name};
+ return {module}().{name};
}}"""
TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \
"""
{{
- return d_holder->{name};
+ return {module}().{name};
}}"""
TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
"""
{{
- return d_holder->{name}__setByUser__;
+ return {module}().{name}__setByUser__;
}}"""
# Option specific methods
return {type}::{enum};
}}"""
+def concat_format(s, objs):
+ """Helper method to render a string for a list of object"""
+ return '\n'.join([s.format(**o.__dict__) for o in objs])
+
+
+def get_holder_fwd_decls(modules):
+ """Render forward declaration of holder structs"""
+ return concat_format(' struct Holder{id_cap};', modules)
+
+
+def get_holder_mem_decls(modules):
+ """Render declarations of holder members of the Option class"""
+ return concat_format(' std::unique_ptr<options::Holder{id_cap}> d_{id};', modules)
+
+
+def get_holder_mem_inits(modules):
+ """Render initializations of holder members of the Option class"""
+ return concat_format(' d_{id}(std::make_unique<options::Holder{id_cap}>()),', modules)
+
+
+def get_holder_mem_copy(modules):
+ """Render copy operation of holder members of the Option class"""
+ return concat_format(' *d_{id} = *options.d_{id};', modules)
+
+
+def get_holder_getter_decls(modules):
+ """Render getter declarations for holder members of the Option class"""
+ return concat_format(''' const options::Holder{id_cap}& {id}() const;
+ options::Holder{id_cap}& {id}();''', modules)
+
+
+def get_holder_getter_impl(modules):
+ """Render getter implementations for holder members of the Option class"""
+ return concat_format('''const options::Holder{id_cap}& Options::{id}() const {{ return *d_{id}; }}
+options::Holder{id_cap}& Options::{id}() {{ return *d_{id}; }}''', modules)
+
class Module(object):
"""Options module.
accs = []
defs = []
- holder_specs.append(TPL_HOLDER_MACRO.format(id=module.id))
-
for option in \
sorted(module.options, key=lambda x: x.long if x.long else x.name):
if option.name is None:
default = option.default
if option.mode and option.type not in default:
default = '{}::{}'.format(option.type, default)
- holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(name=option.name, default=default))
+ holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(type=option.type, name=option.name, default=default))
else:
- holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name))
+ holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(type=option.type, name=option.name))
# Generate module declaration
tpl_decl = TPL_OPTION_STRUCT_RW
### Generate code for {module.name}_options.cpp
# Accessors
- accs.append(TPL_IMPL_SET.format(name=option.name))
- accs.append(TPL_IMPL_OP_BRACKET.format(name=option.name))
- accs.append(TPL_IMPL_WAS_SET_BY_USER.format(name=option.name))
+ accs.append(TPL_IMPL_SET.format(module=module.id, name=option.name))
+ accs.append(TPL_IMPL_OP_BRACKET.format(module=module.id, name=option.name))
+ accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name))
# Global definitions
defs.append('thread_local struct {name}__option_t {name};'.format(name=option.name))
'required' if argument_req else 'no', value))
-def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
+def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
"""
Generate code for all option modules (options.cpp, options_holder.h).
"""
headers_module = [] # generated *_options.h header includes
headers_handler = set() # option includes (for handlers, predicates, ...)
- macros_module = [] # option holder macro for options_holder.h
getopt_short = [] # short options for getopt_long
getopt_long = [] # long options for getopt_long
options_smt = [] # all options names accessible via {set,get}-option
for module in modules:
headers_module.append(format_include(module.header))
- macros_module.append(TPL_HOLDER_MACRO_NAME.format(id=module.id))
if module.options:
help_others.append(
options_smt.append('"{}",'.format(optname))
if option.type == 'bool':
- s = 'opts.push_back({{"{}", d_holder->{} ? "true" : "false"}});'.format(
- optname, option.name)
+ 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(d_holder->{})}});'.format(
- optname, option.name)
+ s = 'opts.push_back({{"{}", std::to_string({}().{})}});'.format(
+ optname, module.id, option.name)
else:
- s = '{{ std::stringstream ss; ss << d_holder->{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
- option.name, optname)
+ s = '{{ std::stringstream ss; ss << {}().{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
+ module.id, option.name, optname)
options_getoptions.append(s)
tpl = TPL_IMPL_ASSIGN
if tpl:
custom_handlers.append(tpl.format(
+ module=module.id,
name=option.name,
handler=handler,
predicates='\n'.join(predicates)
defaults.append('{}({})'.format(option.name, default))
defaults.append('{}__setByUser__(false)'.format(option.name))
- write_file(dst_dir, 'options_holder.h', tpl_options_holder.format(
- headers_module='\n'.join(headers_module),
- macros_module='\n '.join(macros_module)
+ write_file(dst_dir, 'options.h', tpl_options_h.format(
+ holder_fwd_decls=get_holder_fwd_decls(modules),
+ holder_getter_decls=get_holder_getter_decls(modules),
+ holder_mem_decls=get_holder_mem_decls(modules),
))
- write_file(dst_dir, 'options.cpp', tpl_options.format(
+ 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_getter_impl=get_holder_getter_impl(modules),
+ holder_mem_copy=get_holder_mem_copy(modules),
+ holder_mem_inits=get_holder_mem_inits(modules),
custom_handlers='\n'.join(custom_handlers),
module_defaults=',\n '.join(defaults),
help_common='\n'.join(help_common),
# 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 = read_tpl(src_dir, 'options_template.cpp')
- tpl_options_holder = read_tpl(src_dir, 'options_holder_template.h')
+ tpl_options_h = read_tpl(src_dir, 'options_template.h')
+ tpl_options_cpp = read_tpl(src_dir, 'options_template.cpp')
# Parse files, check attributes and create module/option objects
modules = []
codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp)
# Create options.cpp and options_holder.h in destination directory
- codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder)
+ codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp)
#include "base/check.h"
#include "options/option_exception.h"
-#include "options/options_holder.h"
// clang-format off
namespace cvc5 {
// clang-format off
${includes}$
-
-${holder_spec}$
+// clang-format on
namespace cvc5 {
namespace options {
+// clang-format off
${modes}$
+// clang-format on
+#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
+# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+
+struct Holder${id_cap}$
+{
+// clang-format off
+${holder_spec}$
+// clang-format on
+};
+
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
+// clang-format off
${decls}$
+// clang-format on
} // namespace options
+// clang-format off
${specs}$
+// clang-format on
namespace options {
+// clang-format off
${inls}$
+// clang-format on
} // namespace options
} // namespace cvc5
#endif /* CVC5__OPTIONS__${id_cap}$_H */
-//clang-format on
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Tim King, Morgan Deters, Paul Meng
- *
- * 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 "cvc5_public.h"
-
-#ifndef CVC5__OPTIONS__OPTIONS_H
-#define CVC5__OPTIONS__OPTIONS_H
-
-#include <iosfwd>
-#include <memory>
-#include <string>
-#include <vector>
-
-#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;
- } // namespace options
-
-class OptionsListener;
-
-class CVC5_EXPORT Options
-{
- friend api::Solver;
- /** The struct that holds all option values. */
- std::unique_ptr<options::OptionsHolder> d_holder;
-
- /** The handler for the options of the theory. */
- options::OptionsHandler* d_handler;
-
- /** The current Options in effect */
- static thread_local Options* s_current;
-
- /** Low-level assignment function for options */
- template <class T>
- void assign(T, std::string option, std::string value);
- /** Low-level assignment function for bool-valued options */
- template <class T>
- void assignBool(T, std::string option, bool value);
-
- friend class options::OptionsHandler;
-
- /**
- * Options cannot be copied as they are given an explicit list of
- * Listeners to respond to.
- */
- Options(const Options& options) = delete;
-
- /**
- * Options cannot be assigned as they are given an explicit list of
- * Listeners to respond to.
- */
- Options& operator=(const Options& options) = delete;
-
- static std::string formatThreadOptionException(const std::string& option);
-
-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;
- }
- };
-
- /** Return true if current Options are null */
- static inline bool isCurrentNull() {
- return s_current == NULL;
- }
-
- /** Get the current Options in effect */
- static inline Options& current() {
- return *s_current;
- }
-
- Options(OptionsListener* ol = nullptr);
- ~Options();
-
- /**
- * Copies the value of the options stored in OptionsHolder into the current
- * Options object.
- * This does not copy the listeners in the Options object.
- */
- void copyValues(const Options& options);
-
- /**
- * Set the value of the given option. Uses `ref()`, which causes a
- * compile-time error if the given option is read-only.
- */
- template <class T>
- void set(T t, const typename T::type& val) {
- ref(t) = val;
- }
-
- /**
- * Set the default value of the given option. Is equivalent to calling `set()`
- * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time
- * error if the given option is read-only.
- */
- template <class T>
- void setDefault(T t, const typename T::type& val)
- {
- if (!wasSetByUser(t))
- {
- ref(t) = val;
- }
- }
-
- /**
- * Get a non-const reference to the value of the given option. Causes a
- * compile-time error if the given option is read-only. Writeable options
- * specialize this template with a real implementation.
- */
- template <class T>
- typename T::type& ref(T) {
- // Flag a compile-time error.
- T::you_are_trying_to_get_nonconst_access_to_a_read_only_option;
- // Ensure the compiler does not complain about the return value.
- return *static_cast<typename T::type*>(nullptr);
- }
-
- /**
- * 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);
-
- /** Get the value of the given option. Const access only. */
- template <class T>
- const typename T::type& operator[](T) const;
-
- /**
- * 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;
-
- // Get accessor functions.
- InputLanguage getInputLanguage() const;
- options::InstFormatMode getInstFormatMode() const;
- OutputLanguage getOutputLanguage() const;
- bool getUfHo() const;
- bool getDumpInstantiations() const;
- bool getDumpModels() const;
- bool getDumpProofs() const;
- bool getDumpUnsatCores() const;
- bool getEarlyExit() const;
- bool getFilesystemAccess() const;
- bool getForceNoLimitCpuWhileDump() const;
- bool getHelp() const;
- bool getIncrementalSolving() const;
- bool getInteractive() const;
- bool getInteractivePrompt() const;
- bool getLanguageHelp() const;
- bool getMemoryMap() const;
- bool getParseOnly() const;
- bool getProduceModels() const;
- bool getSegvSpin() const;
- bool getSemanticChecks() const;
- bool getStatistics() const;
- bool getStatsEveryQuery() const;
- bool getStrictParsing() const;
- int getTearDownIncremental() const;
- uint64_t getCumulativeTimeLimit() const;
- bool getVersion() const;
- const std::string& getForceLogicString() const;
- int getVerbosity() const;
- std::istream* getIn() const;
- std::ostream* getErr();
- std::ostream* getOut();
- std::ostream* getOutConst() const; // TODO: Remove this.
- std::string getBinaryName() const;
-
- // TODO: Document these.
- void setInputLanguage(InputLanguage);
- void setInteractive(bool);
- void setOut(std::ostream*);
- void setOutputLanguage(OutputLanguage);
-
- bool wasSetByUserEarlyExit() const;
- bool wasSetByUserForceLogicString() const;
- bool wasSetByUserIncrementalSolving() const;
- bool wasSetByUserInteractive() const;
-
- // Static accessor functions.
- // TODO: Document these.
- static std::ostream* currentGetOut();
-
- /**
- * Returns true iff the value of the given option was set
- * by the user via a command-line option or SmtEngine::setOption().
- * (Options::set() is low-level and doesn't count.) Returns false
- * otherwise.
- */
- template <class T>
- bool wasSetByUser(T) const;
-
- /**
- * 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[]);
-
- /**
- * 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();
-
- 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);
-}; /* class Options */
-
-} // namespace cvc5
-
-#endif /* CVC5__OPTIONS__OPTIONS_H */
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/option_exception.h"
-#include "options/options_holder.h"
+#include "options/resource_manager_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
{
- d_options->d_holder->resourceWeightHolder.emplace_back(optarg);
+ d_options->resman().resourceWeightHolder.emplace_back(optarg);
}
// theory/quantifiers/options_handlers.h
{
if (opt == options::statisticsAll.name)
{
- d_options->d_holder->statistics = true;
+ d_options->base().statistics = true;
}
else if (opt == options::statisticsEveryQuery.name)
{
- d_options->d_holder->statistics = true;
+ d_options->base().statistics = true;
}
else if (opt == options::statisticsExpert.name)
{
- d_options->d_holder->statistics = true;
+ d_options->base().statistics = true;
}
}
else
{
if (opt == options::statistics.name)
{
- d_options->d_holder->statisticsAll = false;
- d_options->d_holder->statisticsEveryQuery = false;
- d_options->d_holder->statisticsExpert = false;
+ d_options->base().statisticsAll = false;
+ d_options->base().statisticsEveryQuery = false;
+ d_options->base().statisticsExpert = false;
}
}
}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mathias Preiner, Aina Niemetz, Morgan Deters
- *
- * 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 "cvc5_private.h"
-
-#ifndef CVC5__OPTIONS__OPTIONS_HOLDER_H
-#define CVC5__OPTIONS__OPTIONS_HOLDER_H
-
-// clang-format off
-${headers_module}$
-
-namespace cvc5 {
-namespace options {
-
-#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
-# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
-# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
-
-struct OptionsHolder
-{
- ${macros_module}$
-
-}; /* struct OptionsHolder */
-
-#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
-
-} // namespace options
-} // namespace cvc5
-
-#endif /* CVC5__OPTIONS__OPTIONS_HOLDER_H */
-// clang-format on
#include "base/listener.h"
#include "base/modal_exception.h"
-#include "options.h"
+#include "options/options.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/main_options.h"
// clang-format off
${headers_module}$
-#include "options/options_holder.h"
#include "base/cvc5config.h"
#include "options/base_handlers.h"
}
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}$
+// clang-format on
d_olisten(ol)
{}
void Options::copyValues(const Options& options){
if(this != &options) {
- *d_holder = *options.d_holder;
+// clang-format off
+${holder_mem_copy}$
+// clang-format on
}
}
+${holder_getter_impl}$
+
std::string Options::formatThreadOptionException(const std::string& option) {
std::stringstream ss;
ss << "can't understand option `" << option
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;
options->parseOptionsRecursive(argc, argv, &nonoptions);
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Morgan Deters, Paul Meng
+ *
+ * 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 "cvc5_public.h"
+
+#ifndef CVC5__OPTIONS__OPTIONS_H
+#define CVC5__OPTIONS__OPTIONS_H
+
+#include <iosfwd>
+#include <memory>
+#include <string>
+#include <vector>
+
+#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
+
+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
+
+ /** The current Options in effect */
+ static thread_local Options* s_current;
+
+ /** Low-level assignment function for options */
+ template <class T>
+ void assign(T, std::string option, std::string value);
+ /** Low-level assignment function for bool-valued options */
+ template <class T>
+ void assignBool(T, std::string option, bool value);
+
+ friend class options::OptionsHandler;
+
+ /**
+ * Options cannot be copied as they are given an explicit list of
+ * Listeners to respond to.
+ */
+ Options(const Options& options) = delete;
+
+ /**
+ * Options cannot be assigned as they are given an explicit list of
+ * Listeners to respond to.
+ */
+ Options& operator=(const Options& options) = delete;
+
+ static std::string formatThreadOptionException(const std::string& option);
+
+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;
+ }
+ };
+
+ /** Return true if current Options are null */
+ static inline bool isCurrentNull() {
+ return s_current == NULL;
+ }
+
+ /** Get the current Options in effect */
+ static inline Options& current() {
+ return *s_current;
+ }
+
+ Options(OptionsListener* ol = nullptr);
+ ~Options();
+
+// clang-format off
+${holder_getter_decls}$
+// clang-format on
+
+ /**
+ * Copies the value of the options stored in OptionsHolder into the current
+ * Options object.
+ * This does not copy the listeners in the Options object.
+ */
+ void copyValues(const Options& options);
+
+ /**
+ * Set the value of the given option. Uses `ref()`, which causes a
+ * compile-time error if the given option is read-only.
+ */
+ template <class T>
+ void set(T t, const typename T::type& val) {
+ ref(t) = val;
+ }
+
+ /**
+ * Set the default value of the given option. Is equivalent to calling `set()`
+ * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time
+ * error if the given option is read-only.
+ */
+ template <class T>
+ void setDefault(T t, const typename T::type& val)
+ {
+ if (!wasSetByUser(t))
+ {
+ ref(t) = val;
+ }
+ }
+
+ /**
+ * Get a non-const reference to the value of the given option. Causes a
+ * compile-time error if the given option is read-only. Writeable options
+ * specialize this template with a real implementation.
+ */
+ template <class T>
+ typename T::type& ref(T) {
+ // Flag a compile-time error.
+ T::you_are_trying_to_get_nonconst_access_to_a_read_only_option;
+ // Ensure the compiler does not complain about the return value.
+ return *static_cast<typename T::type*>(nullptr);
+ }
+
+ /**
+ * 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);
+
+ /** Get the value of the given option. Const access only. */
+ template <class T>
+ const typename T::type& operator[](T) const;
+
+ /**
+ * 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;
+
+ // Get accessor functions.
+ InputLanguage getInputLanguage() const;
+ options::InstFormatMode getInstFormatMode() const;
+ OutputLanguage getOutputLanguage() const;
+ bool getUfHo() const;
+ bool getDumpInstantiations() const;
+ bool getDumpModels() const;
+ bool getDumpProofs() const;
+ bool getDumpUnsatCores() const;
+ bool getEarlyExit() const;
+ bool getFilesystemAccess() const;
+ bool getForceNoLimitCpuWhileDump() const;
+ bool getHelp() const;
+ bool getIncrementalSolving() const;
+ bool getInteractive() const;
+ bool getInteractivePrompt() const;
+ bool getLanguageHelp() const;
+ bool getMemoryMap() const;
+ bool getParseOnly() const;
+ bool getProduceModels() const;
+ bool getSegvSpin() const;
+ bool getSemanticChecks() const;
+ bool getStatistics() const;
+ bool getStatsEveryQuery() const;
+ bool getStrictParsing() const;
+ int getTearDownIncremental() const;
+ uint64_t getCumulativeTimeLimit() const;
+ bool getVersion() const;
+ const std::string& getForceLogicString() const;
+ int getVerbosity() const;
+ std::istream* getIn() const;
+ std::ostream* getErr();
+ std::ostream* getOut();
+ std::ostream* getOutConst() const; // TODO: Remove this.
+ std::string getBinaryName() const;
+
+ // TODO: Document these.
+ void setInputLanguage(InputLanguage);
+ void setInteractive(bool);
+ void setOut(std::ostream*);
+ void setOutputLanguage(OutputLanguage);
+
+ bool wasSetByUserEarlyExit() const;
+ bool wasSetByUserForceLogicString() const;
+ bool wasSetByUserIncrementalSolving() const;
+ bool wasSetByUserInteractive() const;
+
+ // Static accessor functions.
+ // TODO: Document these.
+ static std::ostream* currentGetOut();
+
+ /**
+ * Returns true iff the value of the given option was set
+ * by the user via a command-line option or SmtEngine::setOption().
+ * (Options::set() is low-level and doesn't count.) Returns false
+ * otherwise.
+ */
+ template <class T>
+ bool wasSetByUser(T) const;
+
+ /**
+ * 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[]);
+
+ /**
+ * 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();
+
+ 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);
+}; /* class Options */
+
+} // namespace cvc5
+
+#endif /* CVC5__OPTIONS__OPTIONS_H */
-id = "resource_manager"
+id = "RESMAN"
name = "Resource Manager options"
[[option]]
projects / cvc5.git / commitdiff