diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/CMakeLists.txt | 9 | ||||
-rw-r--r-- | src/options/mkoptions.py | 106 | ||||
-rw-r--r-- | src/options/module_template.cpp | 1 | ||||
-rw-r--r-- | src/options/module_template.h | 27 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 16 | ||||
-rw-r--r-- | src/options/options_holder_template.h | 45 | ||||
-rw-r--r-- | src/options/options_public_functions.cpp | 2 | ||||
-rw-r--r-- | src/options/options_template.cpp | 15 | ||||
-rw-r--r-- | src/options/options_template.h (renamed from src/options/options.h) | 13 | ||||
-rw-r--r-- | src/options/resource_manager_options.toml | 2 |
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]] |