From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 30 Aug 2021 23:55:58 +0000 (-0700)
Subject: Add API function to obtain information about a single option (#6980)
X-Git-Tag: cvc5-1.0.0~1317
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=af1b3974022509e26fc14bfe6cb49cb73074b32e;p=cvc5.git

Add API function to obtain information about a single option (#6980)

This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
---

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 166003d69..103cfc005 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -211,7 +211,7 @@ jobs:
       run: |
         make -j${{ env.num_proc }} install
         echo -e "#include <cvc5/cvc5.h>\nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp
-        g++ -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc5
+        g++ -std=c++17 /tmp/test.cpp -I install/include -L install/lib -lcvc5
       working-directory: build
 
     - name: Python Install Check
diff --git a/docs/api/cpp/class_hierarchy.rst b/docs/api/cpp/class_hierarchy.rst
index 3fda2f348..b441106ff 100644
--- a/docs/api/cpp/class_hierarchy.rst
+++ b/docs/api/cpp/class_hierarchy.rst
@@ -24,6 +24,8 @@ C++ API Class Hierarchy
 
   * class :ref:`api/cpp/op:op`
 
+  * class :ref:`api/cpp/optioninfo:optioninfo`
+
   * class :ref:`api/cpp/result:result`
 
     * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>`
diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst
index 91e9f4619..c10ae7517 100644
--- a/docs/api/cpp/cpp.rst
+++ b/docs/api/cpp/cpp.rst
@@ -23,6 +23,7 @@ C++ API Documentation
     grammar
     kind
     op
+    optioninfo
     result
     roundingmode
     solver
diff --git a/docs/api/cpp/optioninfo.rst b/docs/api/cpp/optioninfo.rst
new file mode 100644
index 000000000..eb7848210
--- /dev/null
+++ b/docs/api/cpp/optioninfo.rst
@@ -0,0 +1,6 @@
+OptionInfo
+==========
+
+.. doxygenstruct:: cvc5::api::OptionInfo
+    :project: cvc5
+    :members:
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 076715f2e..86634bc0c 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -17,7 +17,7 @@ cmake_minimum_required(VERSION 3.4)
 
 project(cvc5-examples)
 
-set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD 17)
 
 enable_testing()
 
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 626edf7bb..6171c147b 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7046,6 +7046,124 @@ std::string Solver::getOption(const std::string& option) const
   CVC5_API_TRY_CATCH_END;
 }
 
+// Supports a visitor from a list of lambdas
+// Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
+template<class... Ts> struct overloaded : Ts... { using Ts::operator()...; };
+template<class... Ts> overloaded(Ts...) -> overloaded<Ts...>;
+
+bool OptionInfo::boolValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(std::holds_alternative<ValueInfo<bool>>(valueInfo))
+      << name << " is not a bool option";
+  //////// all checks before this line
+  return std::get<ValueInfo<bool>>(valueInfo).currentValue;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::string OptionInfo::stringValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(
+      std::holds_alternative<ValueInfo<std::string>>(valueInfo))
+      << name << " is not a string option";
+  //////// all checks before this line
+  return std::get<ValueInfo<std::string>>(valueInfo).currentValue;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+int64_t OptionInfo::intValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(
+      std::holds_alternative<NumberInfo<int64_t>>(valueInfo))
+      << name << " is not an int option";
+  //////// all checks before this line
+  return std::get<NumberInfo<int64_t>>(valueInfo).currentValue;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+uint64_t OptionInfo::uintValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(
+      std::holds_alternative<NumberInfo<uint64_t>>(valueInfo))
+      << name << " is not a uint option";
+  //////// all checks before this line
+  return std::get<NumberInfo<uint64_t>>(valueInfo).currentValue;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+double OptionInfo::doubleValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(
+      std::holds_alternative<NumberInfo<double>>(valueInfo))
+      << name << " is not a double option";
+  //////// all checks before this line
+  return std::get<NumberInfo<double>>(valueInfo).currentValue;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+std::ostream& operator<<(std::ostream& os, const OptionInfo& oi)
+{
+  os << "OptionInfo{ " << oi.name;
+  if (oi.setByUser)
+  {
+    os << " | set by user";
+  }
+  if (!oi.aliases.empty())
+  {
+    container_to_stream(os, oi.aliases, ", ", "", ", ");
+  }
+  auto printNum = [&os](const std::string& type, const auto& vi) {
+    os << " | " << type << " | " << vi.currentValue << " | default "
+       << vi.defaultValue;
+    if (vi.minimum || vi.maximum)
+    {
+      os << " |";
+      if (vi.minimum)
+      {
+        os << " " << *vi.minimum << " <=";
+      }
+      os << " x";
+      if (vi.maximum)
+      {
+        os << " <= " << *vi.maximum;
+      }
+    }
+  };
+  std::visit(overloaded{
+                 [&os](const OptionInfo::VoidInfo& vi) { os << " | void"; },
+                 [&os](const OptionInfo::ValueInfo<bool>& vi) {
+                   os << " | bool | " << vi.currentValue << " | default "
+                      << vi.defaultValue;
+                 },
+                 [&os](const OptionInfo::ValueInfo<std::string>& vi) {
+                   os << " | string | " << vi.currentValue << " | default "
+                      << vi.defaultValue;
+                 },
+                 [&printNum](const OptionInfo::NumberInfo<int64_t>& vi) {
+                   printNum("int64_t", vi);
+                 },
+                 [&printNum](const OptionInfo::NumberInfo<uint64_t>& vi) {
+                   printNum("uint64_t", vi);
+                 },
+                 [&printNum](const OptionInfo::NumberInfo<double>& vi) {
+                   printNum("double", vi);
+                 },
+                 [&os](const OptionInfo::ModeInfo& vi) {
+                   os << " | mode | " << vi.currentValue << " | default "
+                      << vi.defaultValue << " | modes: ";
+                   container_to_stream(os, vi.modes, "", "", ", ");
+                 },
+             },
+             oi.valueInfo);
+  os << " }";
+  return os;
+}
+
 std::vector<std::string> Solver::getOptionNames() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -7055,6 +7173,70 @@ std::vector<std::string> Solver::getOptionNames() const
   CVC5_API_TRY_CATCH_END;
 }
 
+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);
+  return std::visit(
+      overloaded{
+          [&info](const options::OptionInfo::VoidInfo& vi) {
+            return OptionInfo{info.name,
+                              info.aliases,
+                              info.setByUser,
+                              OptionInfo::VoidInfo{}};
+          },
+          [&info](const options::OptionInfo::ValueInfo<bool>& vi) {
+            return OptionInfo{
+                info.name,
+                info.aliases,
+                info.setByUser,
+                OptionInfo::ValueInfo<bool>{vi.defaultValue, vi.currentValue}};
+          },
+          [&info](const options::OptionInfo::ValueInfo<std::string>& vi) {
+            return OptionInfo{info.name,
+                              info.aliases,
+                              info.setByUser,
+                              OptionInfo::ValueInfo<std::string>{
+                                  vi.defaultValue, vi.currentValue}};
+          },
+          [&info](const options::OptionInfo::NumberInfo<int64_t>& vi) {
+            return OptionInfo{
+                info.name,
+                info.aliases,
+                info.setByUser,
+                OptionInfo::NumberInfo<int64_t>{
+                    vi.defaultValue, vi.currentValue, vi.minimum, vi.maximum}};
+          },
+          [&info](const options::OptionInfo::NumberInfo<uint64_t>& vi) {
+            return OptionInfo{
+                info.name,
+                info.aliases,
+                info.setByUser,
+                OptionInfo::NumberInfo<uint64_t>{
+                    vi.defaultValue, vi.currentValue, vi.minimum, vi.maximum}};
+          },
+          [&info](const options::OptionInfo::NumberInfo<double>& vi) {
+            return OptionInfo{
+                info.name,
+                info.aliases,
+                info.setByUser,
+                OptionInfo::NumberInfo<double>{
+                    vi.defaultValue, vi.currentValue, vi.minimum, vi.maximum}};
+          },
+          [&info](const options::OptionInfo::ModeInfo& vi) {
+            return OptionInfo{info.name,
+                              info.aliases,
+                              info.setByUser,
+                              OptionInfo::ModeInfo{
+                                  vi.defaultValue, vi.currentValue, vi.modes}};
+          },
+      },
+      info.valueInfo);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 DriverOptions Solver::getDriverOptions() const { return DriverOptions(*this); }
 
 std::vector<Term> Solver::getUnsatAssumptions(void) const
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 7a33210ed..5abcc578e 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -20,11 +20,13 @@
 
 #include <map>
 #include <memory>
+#include <optional>
 #include <set>
 #include <sstream>
 #include <string>
 #include <unordered_map>
 #include <unordered_set>
+#include <variant>
 #include <vector>
 
 #include "api/cpp/cvc5_kind.h"
@@ -2619,6 +2621,88 @@ class CVC5_EXPORT DriverOptions
   const Solver& d_solver;
 };
 
+/**
+ * Holds some description about a particular option, including its name, its
+ * aliases, whether the option was explcitly set by the user, and information
+ * concerning its value. The `valueInfo` member holds any of the following
+ * alternatives:
+ * - VoidInfo if the option holds no value (or the value has no native type)
+ * - ValueInfo<T> if the option is of type bool or std::string, holds the
+ *   current value and the default value.
+ * - NumberInfo<T> if the option is of type int64_t, uint64_t or double, holds
+ *   the current and default value, as well as the minimum and maximum.
+ * - ModeInfo if the option is a mode option, holds the current and default
+ *   values, as well as a list of valid modes.
+ * Additionally, this class provides convenience functions to obtain the
+ * current value of an option in a type-safe manner using boolValue(),
+ * stringValue(), intValue(), uintValue() and doubleValue(). They assert that
+ * the option has the respective type and return the current value.
+ */
+struct CVC5_EXPORT OptionInfo
+{
+  /** Has no value information */
+  struct VoidInfo {};
+  /** Has the current and the default value */
+  template <typename T>
+  struct ValueInfo
+  {
+    T defaultValue;
+    T currentValue;
+  };
+  /** Default value, current value, minimum and maximum of a numeric value */
+  template <typename T>
+  struct NumberInfo
+  {
+    T defaultValue;
+    T currentValue;
+    std::optional<T> minimum;
+    std::optional<T> maximum;
+  };
+  /** Default value, current value and choices of a mode option */
+  struct ModeInfo
+  {
+    std::string defaultValue;
+    std::string currentValue;
+    std::vector<std::string> modes;
+  };
+
+  /** The option name */
+  std::string name;
+  /** The option name aliases */
+  std::vector<std::string> aliases;
+  /** Whether the option was explicitly set by the user */
+  bool setByUser;
+  /** The option value information */
+  std::variant<VoidInfo,
+               ValueInfo<bool>,
+               ValueInfo<std::string>,
+               NumberInfo<int64_t>,
+               NumberInfo<uint64_t>,
+               NumberInfo<double>,
+               ModeInfo>
+      valueInfo;
+  /** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
+   */
+  bool boolValue() const;
+  /** Obtain the current value as a string. Asserts that valueInfo holds a
+   * string. */
+  std::string stringValue() const;
+  /** Obtain the current value as as int. Asserts that valueInfo holds an int.
+   */
+  int64_t intValue() const;
+  /** Obtain the current value as a uint. Asserts that valueInfo holds a uint.
+   */
+  uint64_t uintValue() const;
+  /** Obtain the current value as a double. Asserts that valueInfo holds a
+   * double. */
+  double doubleValue() const;
+};
+
+/**
+ * Print a `OptionInfo` object to an ``std::ostream``.
+ */
+std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT;
+
 /* -------------------------------------------------------------------------- */
 /* Statistics                                                                 */
 /* -------------------------------------------------------------------------- */
@@ -3775,6 +3859,13 @@ class CVC5_EXPORT Solver
    */
   std::vector<std::string> getOptionNames() const;
 
+  /**
+   * Get some information about the given option. Check the `OptionInfo` class
+   * for more details on which information is available.
+   * @return information about the given option
+   */
+  OptionInfo getOptionInfo(const std::string& option) const;
+
   /**
    * Get the driver options, which provide access to options that can not be
    * communicated properly via getOption() and getOptionInfo().
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index bf0134200..439a1beba 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -217,10 +217,13 @@ public = true
   short      = "o"
   long       = "output=TAG"
   type       = "OutputTag"
+  default    = "NONE"
   handler    = "enableOutputTag"
   category   = "regular"
   help       = "Enable output tag."
   help_mode  = "Output tags."
+[[option.mode.NONE]]
+  name = "none"
 [[option.mode.INST]]
   name = "inst"
   help = "print instantiations during solving"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 2ace926f0..41f2ef543 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -342,6 +342,8 @@ class SphinxGenerator:
             res.append(val.format(opt['help_mode']))
             res.append(val.format(''))
             for k, v in opt['modes'].items():
+                if v == '':
+                    continue
                 res.append(val.format(':{}: {}'.format(k, v)))
         res.append('    ')
 
@@ -506,12 +508,13 @@ def help_mode_format(option):
     for value, attrib in option.mode.items():
         assert len(attrib) == 1
         attrib = attrib[0]
+        if 'help' not in attrib:
+            continue
         if value == option.default and attrib['name'] != "default":
             text.append('+ {} (default)'.format(attrib['name']))
         else:
             text.append('+ {}'.format(attrib['name']))
-        if 'help' in attrib:
-            text.extend('  {}'.format(x) for x in wrapper.wrap(attrib['help']))
+        text.extend('  {}'.format(x) for x in wrapper.wrap(attrib['help']))
 
     return '\n         '.join('"{}\\n"'.format(x) for x in text)
 
@@ -698,7 +701,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
     getopt_short = []        # short options for getopt_long
     getopt_long = []         # long options for getopt_long
     options_getall = []      # options for options::getAll()
-    options_getoptions = []  # options for Options::getOptions()
+    options_get_info = []    # code for getOptionInfo()
     options_handler = []     # option handler calls
     options_names = set()    # option names
     help_common = []         # help text for all common options
@@ -788,6 +791,32 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
                 cond = ' || '.join(
                     ['name == "{}"'.format(x) for x in sorted(names)])
 
+                # Generate code for getOptionInfo
+                if option.name:
+                    constr = None
+                    fmt = {
+                        'type': option.type,
+                        'value': 'opts.{}.{}'.format(module.id, option.name),
+                        'default': option.default if option.default else '{}()'.format(option.type),
+                        'minimum': option.minimum if option.minimum else '{}',
+                        'maximum': option.maximum if option.maximum else '{}',
+                    }
+                    if option.type in ['bool', 'std::string']:
+                        constr = 'OptionInfo::ValueInfo<{type}>{{{default}, {value}}}'.format(**fmt)
+                    elif option.type == 'double' or is_numeric_cpp_type(option.type):
+                        constr = 'OptionInfo::NumberInfo<{type}>{{{default}, {value}, {minimum}, {maximum}}}'.format(**fmt)
+                    elif option.mode:
+                        values = ', '.join(map(lambda s: '"{}"'.format(s), option.mode.keys()))
+                        assert(option.default)
+                        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))
+
                 if setoption_handlers:
                     setoption_handlers.append('  }} else if ({}) {{'.format(cond))
                 else:
@@ -884,6 +913,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
         'options_short': ''.join(getopt_short),
         'options_getall': '\n  '.join(options_getall),
         '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),
     }
@@ -971,6 +1001,8 @@ def parse_module(filename, module):
             option = Option(attribs)
             if option.mode and not option.help_mode:
                 perr(filename, 'defines modes but no help_mode', option)
+            if option.mode and not option.default:
+                perr(filename, "mode option has no default", option)
             if option.mode and option.default and \
                     option.default not in option.mode.keys():
                 perr(filename,
diff --git a/src/options/options_public.h b/src/options/options_public.h
index 7b6767b58..17a70cadd 100644
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -19,7 +19,10 @@
 #define CVC5__OPTIONS__OPTIONS_PUBLIC_H
 
 #include <iosfwd>
+#include <optional>
+#include <sstream>
 #include <string>
+#include <variant>
 #include <vector>
 
 #include "cvc5_export.h"
@@ -53,6 +56,72 @@ std::vector<std::vector<std::string> > getAll(const Options& opts) CVC5_EXPORT;
  */
 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
+ * (if it is a mode option).
+ */
+struct CVC5_EXPORT OptionInfo
+{
+  std::string name;
+  std::vector<std::string> aliases;
+  bool setByUser;
+
+  /** No information about the options value */
+  struct VoidInfo
+  {
+  };
+  /** Default value and current value */
+  template <typename T>
+  struct ValueInfo
+  {
+    T defaultValue;
+    T currentValue;
+  };
+  /** Default value, current value, minimum and maximum of a numeric value */
+  template <typename T>
+  struct NumberInfo
+  {
+    T defaultValue;
+    T currentValue;
+    std::optional<T> minimum;
+    std::optional<T> maximum;
+  };
+  /** Default value, current value and choices of a mode option */
+  struct ModeInfo
+  {
+    std::string defaultValue;
+    std::string currentValue;
+    std::vector<std::string> modes;
+
+    template <typename T>
+    ModeInfo(const std::string& def, T cur, const std::vector<std::string>& m)
+        : defaultValue(def), modes(m)
+    {
+      std::stringstream ss;
+      ss << cur;
+      currentValue = ss.str();
+    }
+  };
+
+  /** A variant over all possible option value information */
+  std::variant<VoidInfo,
+               ValueInfo<bool>,
+               ValueInfo<std::string>,
+               NumberInfo<int64_t>,
+               NumberInfo<uint64_t>,
+               NumberInfo<double>,
+               ModeInfo>
+      valueInfo;
+};
+
+/**
+ * Retrieves information about an option specified by its name from an options
+ * object. Note that `opts` is only used to retrieve the current value.
+ */
+OptionInfo getInfo(const Options& opts, const std::string& name) CVC5_EXPORT;
+
 }  // namespace cvc5::options
 
 #endif
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index 7e892ff87..6269894b4 100644
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -260,17 +260,35 @@ void set(Options& opts, const std::string& name, const std::string& optionarg)
 std::vector<std::vector<std::string> > getAll(const Options& opts)
 {
   std::vector<std::vector<std::string>> res;
-
-${options_getall}$
-
+  // clang-format off
+  ${options_getall}$
+  // clang-format on
   return res;
 }
 
 std::vector<std::string> getNames()
 {
   return {
-${options_all_names}$
+    // 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 */
+#define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+
+OptionInfo getInfo(const Options& opts, const std::string& name)
+{
+  // clang-format off
+  ${options_get_info}$
+  // clang-format on
+  return OptionInfo{name, {}, false, OptionInfo::VoidInfo{}};
+}
+
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
 }  // namespace cvc5::options
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 312d57319..df4b42ca6 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1329,6 +1329,53 @@ TEST_F(TestApiBlackSolver, getOptionNames)
   ASSERT_EQ(std::find(names.begin(), names.end(), "foobar"), names.end());
 }
 
+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));
+  }
+  {
+    // int64 type with default
+    api::OptionInfo info = d_solver.getOptionInfo("verbosity");
+    EXPECT_EQ("verbosity", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(info.valueInfo));
+    auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo);
+    EXPECT_EQ(0, numInfo.defaultValue);
+    EXPECT_EQ(0, numInfo.currentValue);
+    EXPECT_FALSE(numInfo.minimum || numInfo.maximum);
+    ASSERT_EQ(info.intValue(), 0);
+  }
+  {
+    auto info = d_solver.getOptionInfo("random-freq");
+    ASSERT_EQ(info.name, "random-freq");
+    ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"});
+    ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(info.valueInfo));
+    auto ni = std::get<api::OptionInfo::NumberInfo<double>>(info.valueInfo);
+    ASSERT_EQ(ni.currentValue, 0.0);
+    ASSERT_EQ(ni.defaultValue, 0.0);
+    ASSERT_TRUE(ni.minimum && ni.maximum);
+    ASSERT_EQ(*ni.minimum, 0.0);
+    ASSERT_EQ(*ni.maximum, 1.0);
+    ASSERT_EQ(info.doubleValue(), 0.0);
+  }
+  {
+    // mode option
+    api::OptionInfo info = d_solver.getOptionInfo("output");
+    EXPECT_EQ("output", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
+    auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
+    EXPECT_EQ("NONE", modeInfo.defaultValue);
+    EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue);
+    std::vector<std::string> modes{"NONE", "INST", "SYGUS", "TRIGGER"};
+    EXPECT_EQ(modes, modeInfo.modes);
+  }
+}
+
 TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
 {
   d_solver.setOption("incremental", "false");