From: Gereon Kremer Date: Thu, 31 Mar 2022 04:40:10 +0000 (+0200) Subject: Improve documentation for OptionInfo (#8474) X-Git-Tag: cvc5-1.0.0~100 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=078ea64696c3ce3f7267e7f7bee6fb0158871e1c;p=cvc5.git Improve documentation for OptionInfo (#8474) This PR improves the documentation for OptionInfo and adds documentation for the DriverOptions class. --- diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index f51f55756..6001b2a86 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -17,6 +17,7 @@ For most applications, the :cpp:class:`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 index 000000000..cc22c560d --- /dev/null +++ b/docs/api/cpp/driveroptions.rst @@ -0,0 +1,6 @@ +DriverOptions +============= + +.. doxygenclass:: cvc5::DriverOptions + :project: cvc5 + :members: diff --git a/docs/options.rst b/docs/options.rst index 06567fbc3..3f1a2b8d0 100644 --- a/docs/options.rst +++ b/docs/options.rst @@ -14,6 +14,10 @@ Also, options can be set and inspected using the respective commands of the inpu :py:func:`getOption() `, :py:func:`getOptionNames() `, :py:func:`getOptionInfo() ` +- Pythonic API: :py:func:`setOption() `, + :py:func:`getOption() `, + :py:func:`getOptionNames() `, + :py:func:`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 `) that require special treatment internally. diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 2f6161112..0416f1a2d 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -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() ` or + * :cpp:func:`Solver::getOptionInfo() ` methods. + * This includes, e.g., the input and output streams that can be configured via + * :ref:`err `, :ref:`in ` and :ref:`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` if the option is of type `bool` or `std::string`, holds the - * current value and the default value. - * - `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. - * - `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() ` and + * allows for a more detailed inspection of options than + * :cpp:func:`Solver::getOption() `. The + * :cpp:member:`valueInfo ` member holds any of the + * following alternatives: + * + * - :cpp:class:`VoidInfo ` if the option holds no + * value (or the value has no native type) + * - :cpp:class:`ValueInfo ` if the option is of + * type ``bool`` or ``std::string``, holds the current value and the default + * value. + * - :cpp:class:`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 ` 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() + * `, :cpp:func:`stringValue() + * `, :cpp:func:`intValue() + * `, :cpp:func:`uintValue() + * ` and :cpp:func:`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 ` holds + * a :cpp:class:`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() + * `. \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 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 struct NumberInfo { + /** The default value. */ T defaultValue; + /** The current value. */ T currentValue; + /** The optional minimum value. */ std::optional minimum; + /** The optional maximum value. */ std::optional 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 modes; }; @@ -2801,7 +2839,7 @@ struct CVC5_EXPORT OptionInfo std::vector aliases; /** Whether the option was explicitly set by the user */ bool setByUser; - /** The option value information */ + /** Possible types for ``valueInfo``. */ using OptionInfoVariant = std::variant, ValueInfo, @@ -2809,26 +2847,30 @@ struct CVC5_EXPORT OptionInfo NumberInfo, NumberInfo, 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;