From: Gereon Kremer Date: Wed, 4 Aug 2021 18:17:42 +0000 (-0700) Subject: Add API function to get list of option names (#6971) X-Git-Tag: cvc5-1.0.0~1411 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f2e127061ee03db1ba8ff56d9dfb42fbe9d60b1;p=cvc5.git Add API function to get list of option names (#6971) 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. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 05f8bd073..aca5fa981 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -59,6 +59,7 @@ #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" @@ -7047,6 +7048,15 @@ std::string Solver::getOption(const std::string& option) const CVC5_API_TRY_CATCH_END; } +std::vector Solver::getOptionNames() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return options::getNames(); + //////// + CVC5_API_TRY_CATCH_END; +} + std::vector Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3b6ba7069..0d8a268ae 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3718,6 +3718,13 @@ class CVC5_EXPORT Solver */ 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 getOptionNames() const; + /** * Get the set of unsat ("failed") assumptions. * SMT-LIB: diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 7231106d5..02087d6a0 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -741,6 +741,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, 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 @@ -823,15 +824,16 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, # 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': @@ -839,16 +841,16 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, 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 += ');' @@ -927,6 +929,9 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_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), @@ -943,6 +948,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, '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), } diff --git a/src/options/options_public.h b/src/options/options_public.h index 03d7ec41a..06981a837 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -74,14 +74,14 @@ std::vector parse(Options& opts, * 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; /** @@ -89,6 +89,11 @@ void set(Options& opts, */ std::vector > getAll(const Options& opts) CVC5_EXPORT; +/** + * Get a (sorted) list of all option names that are available. + */ +std::vector getNames() CVC5_EXPORT; + } // namespace cvc5::options #endif diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index 70c6f420a..220445327 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -458,30 +458,30 @@ std::vector parse( 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 > getAll(const Options& opts) @@ -493,4 +493,11 @@ ${options_getall}$ return res; } +std::vector getNames() +{ + return { +${options_all_names}$ + }; +} + } // namespace cvc5::options diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index ce989c9ea..08f5596c5 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1301,6 +1301,14 @@ TEST_F(TestApiBlackSolver, getOption) ASSERT_THROW(d_solver.getOption("asdf"), CVC5ApiException); } +TEST_F(TestApiBlackSolver, getOptionNames) +{ + std::vector 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");