summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/mkoptions.py123
-rw-r--r--src/options/options_public.h10
-rw-r--r--src/options/options_public_template.cpp52
3 files changed, 122 insertions, 63 deletions
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 51a353597..bb5de4dea 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -62,6 +62,38 @@ OPTION_ATTR_ALL = OPTION_ATTR_REQ + [
CATEGORY_VALUES = ['common', 'expert', 'regular', 'undocumented']
+################################################################################
+################################################################################
+# utility functions
+
+
+def wrap_line(s, indent, **kwargs):
+ """Wrap and indent text and forward all other kwargs to textwrap.wrap()."""
+ return ('\n' + ' ' * indent).join(
+ textwrap.wrap(s, width=80 - indent, **kwargs))
+
+
+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 all_options(modules, sorted=False):
+ """Helper to iterate all options from all modules."""
+ if sorted:
+ options = []
+ for m in modules:
+ options = options + [(m, o) for o in m.options]
+ options.sort(key=lambda t: t[1])
+ yield from options
+ else:
+ for module in modules:
+ if not module.options:
+ continue
+ for option in module.options:
+ yield module, option
+
+
### Other globals
g_long_cache = dict() # maps long options to filename/fileno
@@ -145,10 +177,6 @@ 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_module_headers(modules):
"""Render includes for module headers"""
@@ -252,6 +280,60 @@ class Option(object):
self.long_name = r[0]
if len(r) > 1:
self.long_opt = r[1]
+ self.names = set()
+ if self.long_name:
+ self.names.add(self.long_name)
+ if self.alias:
+ self.names.update(self.alias)
+
+ def __lt__(self, other):
+ if self.long_name and other.long_name:
+ return self.long_name < other.long_name
+ if self.long_name: return True
+ return False
+
+################################################################################
+# stuff for options/options_public.cpp
+
+
+def generate_public_includes(modules):
+ """Generates the list of includes for options_public.cpp."""
+ headers = set()
+ for _, option in all_options(modules):
+ headers.update([format_include(x) for x in option.includes])
+ return '\n'.join(headers)
+
+
+def generate_getnames_impl(modules):
+ """Generates the implementation for options::getNames()."""
+ names = set()
+ for _, option in all_options(modules):
+ names.update(option.names)
+ res = ', '.join(map(lambda s: '"' + s + '"', sorted(names)))
+ return wrap_line(res, 4, break_on_hyphens=False)
+
+
+def generate_get_impl(modules):
+ """Generates the implementation for options::get()."""
+ res = []
+ for module, option in all_options(modules, True):
+ if not option.name or not option.long:
+ continue
+ cond = ' || '.join(['name == "{}"'.format(x) for x in option.names])
+ ret = None
+ if option.type == 'bool':
+ ret = 'return options.{}.{} ? "true" : "false";'.format(
+ module.id, option.name)
+ elif option.type == 'std::string':
+ ret = 'return options.{}.{};'.format(module.id, option.name)
+ elif is_numeric_cpp_type(option.type):
+ ret = 'return std::to_string(options.{}.{});'.format(
+ module.id, option.name)
+ else:
+ ret = '{{ std::stringstream s; s << options.{}.{}; return s.str(); }}'.format(
+ module.id, option.name)
+ res.append('if ({}) {}'.format(cond, ret))
+ return '\n '.join(res)
class SphinxGenerator:
@@ -680,11 +762,9 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
getopt_long = [] # long options for getopt_long
options_get_info = [] # code for getOptionInfo()
options_handler = [] # option handler calls
- options_names = set() # option names
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 = []
@@ -763,7 +843,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
if option.alias:
names.update(option.alias)
assert names
- options_names.update(names)
cond = ' || '.join(
['name == "{}"'.format(x) for x in sorted(names)])
@@ -822,27 +901,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
setoption_handlers.append(
h.format(handler=option.handler, smtname=option.long_name))
-
- if option.name:
- getoption_handlers.append(
- 'if ({}) {{'.format(cond))
- if option.type == 'bool':
- getoption_handlers.append(
- 'return options.{}.{} ? "true" : "false";'.format(module.id, option.name))
- elif option.type == 'std::string':
- getoption_handlers.append(
- 'return options.{}.{};'.format(module.id, option.name))
- elif is_numeric_cpp_type(option.type):
- getoption_handlers.append(
- 'return std::to_string(options.{}.{});'.format(module.id, option.name))
- else:
- getoption_handlers.append('std::stringstream ss;')
- getoption_handlers.append(
- 'ss << options.{}.{};'.format(module.id, option.name))
- getoption_handlers.append('return ss.str();')
- getoption_handlers.append('}')
-
-
# Add --no- alternative options for boolean options
if option.long and option.type == 'bool' and option.alternate:
cases = []
@@ -868,9 +926,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
cases.append(' break;')
options_handler.extend(cases)
- options_all_names = ', '.join(map(lambda s: '"' + s + '"', sorted(options_names)))
- options_all_names = '\n'.join(textwrap.wrap(options_all_names, width=80, break_on_hyphens=False))
-
data = {
'holder_fwd_decls': get_holder_fwd_decls(modules),
'holder_mem_decls': get_holder_mem_decls(modules),
@@ -880,14 +935,16 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
'holder_mem_inits': get_holder_mem_inits(modules),
'holder_ref_inits': get_holder_ref_inits(modules),
'holder_mem_copy': get_holder_mem_copy(modules),
+ # options/options_public.cpp
+ 'options_includes': generate_public_includes(modules),
+ 'getnames_impl': generate_getnames_impl(modules),
+ 'get_impl': generate_get_impl(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),
- 'options_all_names': options_all_names,
'options_get_info': '\n '.join(sorted(options_get_info)),
- 'getoption_handlers': '\n'.join(getoption_handlers),
'setoption_handlers': '\n'.join(setoption_handlers),
}
for tpl in tpls:
diff --git a/src/options/options_public.h b/src/options/options_public.h
index a5a223517..a6246a894 100644
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -35,6 +35,11 @@
namespace cvc5::options {
/**
+ * Get a (sorted) list of all option names that are available.
+ */
+std::vector<std::string> getNames() CVC5_EXPORT;
+
+/**
* Retrieve an option value by name (as given in key) from the Options object
* opts as a string.
*/
@@ -49,11 +54,6 @@ void set(Options& opts,
const std::string& optionarg) CVC5_EXPORT;
/**
- * Get a (sorted) list of all option names that are available.
- */
-std::vector<std::string> getNames() CVC5_EXPORT;
-
-/**
* Represents information we can provide about a particular option. It contains
* its name and aliases, the current value and the default value as well as
* type-specific information like its range (if it is a number) or the choices
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index c21fdee97..5b56933b5 100644
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -13,23 +13,25 @@
* Global (command-line, set-option, ...) parameters for SMT.
*/
-#include "options/options_public.h"
-
-
#include "base/check.h"
#include "base/output.h"
+#include "options/options.h"
#include "options/options_handler.h"
#include "options/options_listener.h"
-#include "options/options.h"
+#include "options/options_public.h"
#include "options/uf_options.h"
+
+// clang-format off
${headers_module}$
-${headers_handler}$
+${options_includes}$
+// clang-format on
#include <cstring>
#include <iostream>
#include <limits>
-namespace cvc5::options {
+namespace cvc5::options
+{
// Contains the default option handlers (i.e. parsers)
namespace handlers {
@@ -191,17 +193,26 @@ namespace cvc5::options {
}
}
-std::string get(const Options& options, const std::string& name)
-{
- Trace("options") << "Options::getOption(" << name << ")" << std::endl;
- // clang-format off
- ${getoption_handlers}$
- // clang-format on
- throw OptionException("Unrecognized option key or setting: " + name);
-}
+ std::vector<std::string> getNames()
+ {
+ return {
+ // clang-format off
+ ${getnames_impl}$
+ // clang-format on
+ };
+ }
-void setInternal(Options& opts, const std::string& name,
- const std::string& optionarg)
+ std::string get(const Options& options, const std::string& name)
+ {
+ Trace("options") << "Options::getOption(" << name << ")" << std::endl;
+ // clang-format off
+ ${get_impl}$
+ // clang-format on
+ throw OptionException("Unrecognized option key or setting: " + name);
+ }
+
+void setInternal(Options & opts, const std::string& name,
+ const std::string& optionarg)
{
// clang-format off
${setoption_handlers}$
@@ -223,15 +234,6 @@ void set(Options& opts, const std::string& name, const std::string& optionarg)
setInternal(opts, name, optionarg);
}
-std::vector<std::string> getNames()
-{
- return {
- // clang-format off
- ${options_all_names}$
- // clang-format on
- };
-}
-
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
#define DO_SEMANTIC_CHECKS_BY_DEFAULT false
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback