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
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"""
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:
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 = []
if option.alias:
names.update(option.alias)
assert names
- options_names.update(names)
cond = ' || '.join(
['name == "{}"'.format(x) for x in sorted(names)])
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 = []
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),
'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:
* 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 {
}
}
-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}$
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 */
projects / cvc5.git / commitdiff