Improve documentation for OptionInfo (#8474)
authorGereon Kremer <gkremer@cs.stanford.edu>
Thu, 31 Mar 2022 04:40:10 +0000 (06:40 +0200)
committerGitHub <noreply@github.com>
Thu, 31 Mar 2022 04:40:10 +0000 (04:40 +0000)
This PR improves the documentation for OptionInfo and adds documentation for the DriverOptions class.

docs/api/cpp/cpp.rst
docs/api/cpp/driveroptions.rst [new file with mode: 0644]
docs/options.rst
src/api/cpp/cvc5.h

index f51f55756be55351cf6233fd9b3b851a8afc7d8e..6001b2a865fe5207333dc10448149cb0931b24f4 100644 (file)
@@ -17,6 +17,7 @@ For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main
     datatypeconstructordecl
     datatypedecl
     datatypeselector
+    driveroptions
     grammar
     kind
     op
@@ -48,6 +49,7 @@ Class hierarchy
   * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl`
   * class :ref:`api/cpp/datatypedecl:datatypedecl`
   * class :ref:`api/cpp/datatypeselector:datatypeselector`
+  * class :ref:`api/cpp/driveroptions:driveroptions`
   * class :ref:`api/cpp/grammar:grammar`
   * class :ref:`api/cpp/kind:kind`
   * class :ref:`api/cpp/op:op`
diff --git a/docs/api/cpp/driveroptions.rst b/docs/api/cpp/driveroptions.rst
new file mode 100644 (file)
index 0000000..cc22c56
--- /dev/null
@@ -0,0 +1,6 @@
+DriverOptions
+=============
+
+.. doxygenclass:: cvc5::DriverOptions
+    :project: cvc5
+    :members:
index 06567fbc3e6ff7fe24e5cf449f7dbbe0fed1ce6f..3f1a2b8d0331271480aac2e4bdd95949cb611b94 100644 (file)
@@ -14,6 +14,10 @@ Also, options can be set and inspected using the respective commands of the inpu
   :py:func:`getOption() <cvc5.Solver.getOption()>`,
   :py:func:`getOptionNames() <cvc5.Solver.getOptionNames()>`,
   :py:func:`getOptionInfo() <cvc5.Solver.getOptionInfo()>`
+- Pythonic API: :py:func:`setOption() <cvc5.pythonic.Solver.setOption()>`,
+  :py:func:`getOption() <cvc5.pythonic.Solver.getOption()>`,
+  :py:func:`getOptionNames() <cvc5.pythonic.Solver.getOptionNames()>`,
+  :py:func:`getOptionInfo() <cvc5.pythonic.Solver.getOptionInfo()>`
 
 Generally, all options are identified by a name, and they can additionally have one or more aliases (that can be used instead of their name anywhere) and a short name (a single letter).
 Internally, options are strongly typed and must be either Boolean, (signed or unsigned) integers, floating-point numbers, strings, or an enumeration type. Values for options with a numeric type may be restricted to an interval. A few options have custom types (for example :ref:`err <lbl-option-err>`) that require special treatment internally.
index 2f6161112d4772fdddd976bc12a00c0a6bbe1acb..0416f1a2d518c960d5ed58e6f7108fd41a6cb4c9 100644 (file)
@@ -2727,21 +2727,27 @@ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT;
 /* -------------------------------------------------------------------------- */
 
 /**
- * Provides access to options that can not be communicated via the regular
- * getOption() or getOptionInfo() methods. This class does not store the options
- * itself, but only acts as a wrapper to the solver object. It can thus no
- * longer be used after the solver object has been destroyed.
+ * \verbatim embed:rst:leading-asterisk
+ * This class provides type-safe access to a few options that frontends are
+ * likely to use, but can not be not be communicated appropriately via the
+ * regular :cpp:func:`Solver::getOption() <cvc5::Solver::getOption()>` or
+ * :cpp:func:`Solver::getOptionInfo() <cvc5::Solver::getOptionInfo()>` methods.
+ * This includes, e.g., the input and output streams that can be configured via
+ * :ref:`err <lbl-option-err>`, :ref:`in <lbl-option-in>` and :ref:`out
+ * <lbl-option-out>`. This class does not store the options itself, but only
+ * acts as a wrapper to the solver object. It can thus no longer be used after
+ * the solver object has been destroyed. \endverbatim
  */
 class CVC5_EXPORT DriverOptions
 {
   friend class Solver;
 
  public:
-  /** Access the solvers input stream */
+  /** Access the solver's input stream */
   std::istream& in() const;
-  /** Access the solvers error output stream */
+  /** Access the solver's error output stream */
   std::ostream& err() const;
-  /** Access the solvers output stream */
+  /** Access the solver's output stream */
   std::ostream& out() const;
 
  private:
@@ -2750,48 +2756,80 @@ class CVC5_EXPORT DriverOptions
 };
 
 /**
+ * \verbatim embed:rst:leading-asterisk
  * Holds some description about a particular option, including its name, its
  * aliases, whether the option was explicitly 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.
+ * concerning its value. It can be obtained via
+ * :cpp:func:`Solver::getOptionInfo() <cvc5::Solver::getOptionInfo()>` and
+ * allows for a more detailed inspection of options than
+ * :cpp:func:`Solver::getOption() <cvc5::Solver::getOption()>`. The
+ * :cpp:member:`valueInfo <cvc5::OptionInfo::valueInfo>` member holds any of the
+ * following alternatives:
+ *
+ * - :cpp:class:`VoidInfo <cvc5::OptionInfo::VoidInfo>` if the option holds no
+ *   value (or the value has no native type)
+ * - :cpp:class:`ValueInfo <cvc5::OptionInfo::ValueInfo>` if the option is of
+ *   type ``bool`` or ``std::string``, holds the current value and the default
+ *   value.
+ * - :cpp:class:`NumberInfo <cvc5::OptionInfo::NumberInfo>` 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.
+ * - :cpp:class:`ModeInfo <cvc5::OptionInfo::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.
+ * current value of an option in a type-safe manner using :cpp:func:`boolValue()
+ * <cvc5::OptionInfo::boolValue()>`, :cpp:func:`stringValue()
+ * <cvc5::OptionInfo::stringValue()>`, :cpp:func:`intValue()
+ * <cvc5::OptionInfo::intValue()>`, :cpp:func:`uintValue()
+ * <cvc5::OptionInfo::uintValue()>` and :cpp:func:`doubleValue()
+ * <cvc5::OptionInfo::doubleValue()>`. They assert that the option has the
+ * respective type and return the current value.
+ *
+ * If the option has a special type that is not covered by the above
+ * alternatives, the :cpp:member:`valueInfo <cvc5::OptionInfo::valueInfo>` holds
+ * a :cpp:class:`VoidInfo <cvc5::OptionInfo::VoidInfo>`. Some options, that are
+ * expected to be used by frontends (e.g., input and output streams) can also
+ * be accessed using :cpp:func:`Solver::getDriverOptions()
+ * <cvc5::Solver::getDriverOptions()>`. \endverbatim
  */
 struct CVC5_EXPORT OptionInfo
 {
-  /** Has no value information */
+  /** Has no value information. */
   struct VoidInfo {};
-  /** Has the current and the default value */
+  /** Basic information for option values. ``T`` can be ``bool`` or
+   * ``std::string``. */
   template <typename T>
   struct ValueInfo
   {
+    /** The default value. */
     T defaultValue;
+    /** The current value. */
     T currentValue;
   };
-  /** Default value, current value, minimum and maximum of a numeric value */
+  /** Information for numeric values. ``T`` can be ``int64_t``, ``uint64_t`` or
+   * ``double``. */
   template <typename T>
   struct NumberInfo
   {
+    /** The default value. */
     T defaultValue;
+    /** The current value. */
     T currentValue;
+    /** The optional minimum value. */
     std::optional<T> minimum;
+    /** The optional maximum value. */
     std::optional<T> maximum;
   };
-  /** Default value, current value and choices of a mode option */
+  /** Information for mode option values. */
   struct ModeInfo
   {
+    /** The default value. */
     std::string defaultValue;
+    /** The current value. */
     std::string currentValue;
+    /** The possible modes. */
     std::vector<std::string> modes;
   };
 
@@ -2801,7 +2839,7 @@ struct CVC5_EXPORT OptionInfo
   std::vector<std::string> aliases;
   /** Whether the option was explicitly set by the user */
   bool setByUser;
-  /** The option value information */
+  /** Possible types for ``valueInfo``. */
   using OptionInfoVariant = std::variant<VoidInfo,
                                          ValueInfo<bool>,
                                          ValueInfo<std::string>,
@@ -2809,26 +2847,30 @@ struct CVC5_EXPORT OptionInfo
                                          NumberInfo<uint64_t>,
                                          NumberInfo<double>,
                                          ModeInfo>;
+  /** The option value information */
   OptionInfoVariant valueInfo;
-  /** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
+  /** 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. */
+  /** Obtain the current value as a `std::string`. Asserts that `valueInfo`
+   * holds a `std::string`. */
   std::string stringValue() const;
-  /** Obtain the current value as as int. Asserts that valueInfo holds an int.
+  /** Obtain the current value as an `int64_t`. Asserts that `valueInfo` holds
+   * an `int64_t`.
    */
   int64_t intValue() const;
-  /** Obtain the current value as a uint. Asserts that valueInfo holds a uint.
+  /** Obtain the current value as a `uint64_t`. Asserts that `valueInfo` holds a
+   * `uint64_t`.
    */
   uint64_t uintValue() const;
-  /** Obtain the current value as a double. Asserts that valueInfo holds a
-   * double. */
+  /** Obtain the current value as a `double`. Asserts that `valueInfo` holds a
+   * `double`. */
   double doubleValue() const;
 };
 
 /**
- * Print a `OptionInfo` object to an ``std::ostream``.
+ * Print an `OptionInfo` object to an ``std::ostream``.
  */
 std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT;