Add API check whether option in getOptionInfo() exists (#7093)

This PR adds a missing check in the API for getOptionInfo().

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d6c0a58ee26bfe7b3f67666ad82143e9a1c56067..d41af938a7dc090a409f43ee717f18e0cd8e8ed6 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7178,6 +7178,8 @@ OptionInfo Solver::getOptionInfo(const std::string& option) const
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   auto info = options::getInfo(d_smtEngine->getOptions(), option);
+  CVC5_API_CHECK(info.name != "")
+      << "Querying invalid or unknown option " << option;
   return std::visit(
       overloaded{
           [&info](const options::OptionInfo::VoidInfo& vi) {

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 62e70214d21161a87f9c71f40b666f1029eac100..d2881cc949ff158eaaf591c14c91ae4f3711ef88 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -769,6 +769,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
                     ['name == "{}"'.format(x) for x in sorted(names)])
 
                 # Generate code for getOptionInfo
+                if option.alias:
+                    alias = ', '.join(map(lambda s: '"{}"'.format(s), option.alias))
+                else:
+                    alias = ''
                 if option.name:
                     constr = None
                     fmt = {
@@ -788,11 +792,9 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
                         constr = 'OptionInfo::ModeInfo{{"{default}", {value}, {{ {modes} }}}}'.format(**fmt, modes=values)
                     else:
                         constr = 'OptionInfo::VoidInfo{}'
-                    if option.alias:
-                        alias = ', '.join(map(lambda s: '"{}"'.format(s), option.alias))
-                    else:
-                        alias = ''
                     options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, opts.{}.{}WasSetByUser, {}}};'.format(cond, long_get_option(option.long), module.id, option.name, constr, alias=alias))
+                else:
+                    options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, false, OptionInfo::VoidInfo{{}}}};'.format(cond, long_get_option(option.long), alias=alias))
 
                 if setoption_handlers:
                     setoption_handlers.append('  }} else if ({}) {{'.format(cond))

diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index 4beb47e0fdb91c736ee5ad8999b51aab9b5d504c..9c44dacbaf52546629d83831fa8a8f0606940a35 100644 (file)
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -277,7 +277,7 @@ OptionInfo getInfo(const Options& opts, const std::string& name)
   // clang-format off
   ${options_get_info}$
   // clang-format on
-  return OptionInfo{name, {}, false, OptionInfo::VoidInfo{}};
+  return OptionInfo{"", {}, false, OptionInfo::VoidInfo{}};
 }
 
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 5ca96f0352ce87424df309cf15baa27f8d1355df..e7d7c0bb4d8c6570e52e996247b951a0803bad18 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1332,10 +1332,13 @@ TEST_F(TestApiBlackSolver, getOptionNames)
 TEST_F(TestApiBlackSolver, getOptionInfo)
 {
   {
-    auto info = d_solver.getOptionInfo("verbose");
-    ASSERT_EQ(info.name, "verbose");
-    ASSERT_EQ(info.aliases, std::vector<std::string>{});
-    ASSERT_TRUE(std::holds_alternative<api::OptionInfo::VoidInfo>(info.valueInfo));
+    EXPECT_THROW(d_solver.getOptionInfo("asdf-invalid"), CVC5ApiException);
+  }
+  {
+    api::OptionInfo info = d_solver.getOptionInfo("verbose");
+    EXPECT_EQ("verbose", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(info.valueInfo));
   }
   {
     // int64 type with default