summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/CMakeLists.txt9
-rw-r--r--src/options/mkoptions.py106
-rw-r--r--src/options/module_template.cpp1
-rw-r--r--src/options/module_template.h27
-rw-r--r--src/options/options_handler.cpp16
-rw-r--r--src/options/options_holder_template.h45
-rw-r--r--src/options/options_public_functions.cpp2
-rw-r--r--src/options/options_template.cpp15
-rw-r--r--src/options/options_template.h (renamed from src/options/options.h)13
-rw-r--r--src/options/resource_manager_options.toml2
10 files changed, 128 insertions, 108 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 38f68461b..078c2ad31 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -27,7 +27,6 @@ libcvc5_add_sources(
open_ostream.h
option_exception.cpp
option_exception.h
- options.h
options_handler.cpp
options_handler.h
options_listener.h
@@ -67,13 +66,13 @@ 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.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}
@@ -86,14 +85,14 @@ add_custom_command(
${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}
)
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 74e8d690d..a9ef65899 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -79,8 +79,6 @@ g_getopt_long_start = 256
### Source code templates
-TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER'
-
TPL_IMPL_ASSIGN = \
"""template <> void Options::assign(
options::{name}__option_t,
@@ -89,8 +87,8 @@ TPL_IMPL_ASSIGN = \
{{
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;
}}"""
@@ -101,8 +99,8 @@ TPL_IMPL_ASSIGN_BOOL = \
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;
}}"""
@@ -117,13 +115,10 @@ TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},'
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 = \
@@ -141,7 +136,7 @@ TPL_DECL_SET = \
TPL_IMPL_SET = TPL_DECL_SET[:-1] + \
"""
{{
- return d_holder->{name};
+ return {module}().{name};
}}"""
@@ -152,7 +147,7 @@ TPL_DECL_OP_BRACKET = \
TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \
"""
{{
- return d_holder->{name};
+ return {module}().{name};
}}"""
@@ -162,7 +157,7 @@ TPL_DECL_WAS_SET_BY_USER = \
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
@@ -225,6 +220,42 @@ TPL_MODE_HANDLER_CASE = \
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.
@@ -432,8 +463,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
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:
@@ -447,9 +476,9 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
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
@@ -482,9 +511,9 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
### 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))
@@ -593,14 +622,13 @@ def add_getopt_long(long_name, argument_req, getopt_long):
'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
@@ -615,7 +643,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
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(
@@ -780,14 +807,14 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
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)
@@ -799,6 +826,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
tpl = TPL_IMPL_ASSIGN
if tpl:
custom_handlers.append(tpl.format(
+ module=module.id,
name=option.name,
handler=handler,
predicates='\n'.join(predicates)
@@ -812,14 +840,18 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder):
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),
@@ -977,8 +1009,8 @@ 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 = 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 = []
@@ -1002,7 +1034,7 @@ def mkoptions_main():
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)
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index 0a4d594b2..c79656e4b 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -21,7 +21,6 @@
#include "base/check.h"
#include "options/option_exception.h"
-#include "options/options_holder.h"
// clang-format off
namespace cvc5 {
diff --git a/src/options/module_template.h b/src/options/module_template.h
index b668a1e3f..4e031d843 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -25,25 +25,46 @@
// 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
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index dd555ab56..ee5396dff 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -33,7 +33,7 @@
#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"
@@ -83,7 +83,7 @@ unsigned long OptionsHandler::limitHandler(std::string option,
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
@@ -258,24 +258,24 @@ void OptionsHandler::setStats(const std::string& option, bool value)
{
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;
}
}
}
diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h
deleted file mode 100644
index 04e5eba53..000000000
--- a/src/options/options_holder_template.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/******************************************************************************
- * 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
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 8c55a19eb..d1cae6d64 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -23,7 +23,7 @@
#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"
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 49a35ab38..9419e9914 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -57,7 +57,6 @@ extern int optreset;
// clang-format off
${headers_module}$
-#include "options/options_holder.h"
#include "base/cvc5config.h"
#include "options/base_handlers.h"
@@ -223,8 +222,10 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* 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)
{}
@@ -234,10 +235,14 @@ Options::~Options() {
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
@@ -390,7 +395,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
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);
diff --git a/src/options/options.h b/src/options/options_template.h
index 324850c43..a25ddc58c 100644
--- a/src/options/options.h
+++ b/src/options/options_template.h
@@ -36,6 +36,9 @@ class Solver;
namespace options {
struct OptionsHolder;
class OptionsHandler;
+// clang-format off
+${holder_fwd_decls}$
+// clang-format on
} // namespace options
class OptionsListener;
@@ -43,12 +46,14 @@ 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;
+// clang-format off
+${holder_mem_decls}$
+// clang-format on
+
/** The current Options in effect */
static thread_local Options* s_current;
@@ -104,6 +109,10 @@ public:
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.
diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
index 85cdf1bef..96bc30aaa 100644
--- a/src/options/resource_manager_options.toml
+++ b/src/options/resource_manager_options.toml
@@ -1,4 +1,4 @@
-id = "resource_manager"
+id = "RESMAN"
name = "Resource Manager options"
[[option]]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback