This PR adds a new API function api::Solver::getOptionNames() that exposes a list of all option names as strings. This PR will be followed by another that adds a method to further inspect a particular option by name, and thereby allows to inspect the solver options in a sensible way.
#include "options/main_options.h"
#include "options/option_exception.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "options/smt_options.h"
#include "proof/unsat_core.h"
#include "smt/model.h"
CVC5_API_TRY_CATCH_END;
}
+std::vector<std::string> Solver::getOptionNames() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
+ return options::getNames();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
std::vector<Term> Solver::getUnsatAssumptions(void) const
{
CVC5_API_TRY_CATCH_BEGIN;
*/
std::string getOption(const std::string& option) const;
+ /**
+ * Get all option names that can be used with `setOption`, `getOption` and
+ * `getOptionInfo`.
+ * @return all option names
+ */
+ std::vector<std::string> getOptionNames() const;
+
/**
* Get the set of unsat ("failed") assumptions.
* SMT-LIB:
options_getall = [] # options for options::getAll()
options_getoptions = [] # options for Options::getOptions()
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
# Generate handlers for setOption/getOption
if option.long:
# Make long and alias names available via set/get-option
- keys = set()
+ names = set()
if option.long:
- keys.add(long_get_option(option.long))
+ names.add(long_get_option(option.long))
if option.alias:
- keys.update(option.alias)
- assert keys
+ names.update(option.alias)
+ assert names
+ options_names.update(names)
cond = ' || '.join(
- ['key == "{}"'.format(x) for x in sorted(keys)])
+ ['name == "{}"'.format(x) for x in sorted(names)])
setoption_handlers.append(' if ({}) {{'.format(cond))
if option.type == 'bool':
TPL_CALL_ASSIGN_BOOL.format(
module=module.id,
name=option.name,
- option='key',
+ option='name',
value='optionarg == "true"'))
elif argument_req and option.name and not mode_handler:
setoption_handlers.append(
TPL_CALL_ASSIGN.format(
module=module.id,
name=option.name,
- option='key'))
+ option='name'))
elif option.handler:
- h = ' opts.handler().{handler}("{smtname}", key'
+ h = ' opts.handler().{handler}("{smtname}", name'
if argument_req:
h += ', optionarg'
h += ');'
predicates='\n'.join(predicates)
))
+ 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),
'options_short': ''.join(getopt_short),
'assigns': '\n'.join(assign_impls),
'options_getall': '\n '.join(options_getall),
+ 'options_all_names': options_all_names,
'getoption_handlers': '\n'.join(getoption_handlers),
'setoption_handlers': '\n'.join(setoption_handlers),
}
* Retrieve an option value by name (as given in key) from the Options object
* opts as a string.
*/
-std::string get(const Options& opts, const std::string& key) CVC5_EXPORT;
+std::string get(const Options& opts, const std::string& name) CVC5_EXPORT;
/**
* Update the Options object opts, set the value of the option specified by key
* to the value parsed from optionarg.
*/
void set(Options& opts,
- const std::string& key,
+ const std::string& name,
const std::string& optionarg) CVC5_EXPORT;
/**
*/
std::vector<std::vector<std::string> > getAll(const Options& opts) CVC5_EXPORT;
+/**
+ * Get a (sorted) list of all option names that are available.
+ */
+std::vector<std::string> getNames() CVC5_EXPORT;
+
} // namespace cvc5::options
#endif
return nonoptions;
}
-std::string get(const Options& options, const std::string& key)
+std::string get(const Options& options, const std::string& name)
{
- Trace("options") << "Options::getOption(" << key << ")" << std::endl;
+ Trace("options") << "Options::getOption(" << name << ")" << std::endl;
${getoption_handlers}$
- throw UnrecognizedOptionException(key);
+ throw UnrecognizedOptionException(name);
}
-void setInternal(Options& opts, const std::string& key,
+void setInternal(Options& opts, const std::string& name,
const std::string& optionarg)
{
- ${setoption_handlers}$
- throw UnrecognizedOptionException(key);
+${setoption_handlers}$
+ throw UnrecognizedOptionException(name);
}
-void set(Options& opts, const std::string& key, const std::string& optionarg)
+void set(Options& opts, const std::string& name, const std::string& optionarg)
{
- Trace("options") << "setOption(" << key << ", " << optionarg << ")"
+ Trace("options") << "setOption(" << name << ", " << optionarg << ")"
<< std::endl;
// first update this object
- setInternal(opts, key, optionarg);
+ setInternal(opts, name, optionarg);
// then, notify the provided listener
- opts.notifyListener(key);
+ opts.notifyListener(name);
}
std::vector<std::vector<std::string> > getAll(const Options& opts)
return res;
}
+std::vector<std::string> getNames()
+{
+ return {
+${options_all_names}$
+ };
+}
+
} // namespace cvc5::options
ASSERT_THROW(d_solver.getOption("asdf"), CVC5ApiException);
}
+TEST_F(TestApiBlackSolver, getOptionNames)
+{
+ std::vector<std::string> names = d_solver.getOptionNames();
+ ASSERT_TRUE(names.size() > 100);
+ ASSERT_NE(std::find(names.begin(), names.end(), "verbose"), names.end());
+ ASSERT_EQ(std::find(names.begin(), names.end(), "foobar"), names.end());
+}
+
TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
{
d_solver.setOption("incremental", "false");
projects / cvc5.git / commitdiff