docs: Add documentation for modes. (#8509)

diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst
index 6001b2a865fe5207333dc10448149cb0931b24f4..6b17d122222d2be92bdc1b0ba4803310b213493f 100644 (file)
--- a/docs/api/cpp/cpp.rst
+++ b/docs/api/cpp/cpp.rst
@@ -20,6 +20,7 @@ For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main
     driveroptions
     grammar
     kind
+    modes
     op
     optioninfo
     result
@@ -68,4 +69,6 @@ Class hierarchy
 
     * class :cpp:class:`const_iterator <cvc5::Term::const_iterator>`
 
+  * modes enums :ref:`api/cpp/modes:modes`
+
 ``}``

diff --git a/docs/api/cpp/modes.rst b/docs/api/cpp/modes.rst
new file mode 100644 (file)
index 0000000..be93dac
--- /dev/null
+++ b/docs/api/cpp/modes.rst
@@ -0,0 +1,5 @@
+Modes
+======
+
+.. doxygennamespace:: cvc5::modes
+    :project: cvc5

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 9f4113fb6471a64ec035f41431b7aac44ec117b2..b8bab4bcc9231c59e2d7dac913737aa547155ead 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4499,9 +4499,9 @@ class CVC5_EXPORT Solver
    *     (block-model)
    *
    * Requires enabling option
-   * :ref:`produce-models <lbl-option-produce-models>`.
-   * 'produce-models' and setting option
-   * :ref:`block-models <lbl-option-block-models>`.
+   * :ref:`produce-models <lbl-option-produce-models>`
+   * and setting option
+   * :ref:`block-models <lbl-option-block-models>`
    * to a mode other than ``none``.
    * \endverbatim
    *
@@ -4522,7 +4522,6 @@ class CVC5_EXPORT Solver
    *
    * Requires enabling option
    * :ref:`produce-models <lbl-option-produce-models>`.
-   * 'produce-models'.
    * \endverbatim
    *
    * @warning This method is experimental and may change in future versions.

diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h
index cf694cd3f278c57e026295ade7257bcd2dac2acb..909efc650b113417cb04abbd3e9415478fccdd8b 100644 (file)
--- a/src/api/cpp/cvc5_types.h
+++ b/src/api/cpp/cvc5_types.h
@@ -102,6 +102,12 @@ enum RoundingMode
 
 namespace cvc5::modes {
 
+/**
+ * Mode for blocking models.
+ *
+ * Specifies how models are blocked in Solver::blockModel and
+ * Solver::blockModelValues.
+ */
 enum BlockModelsMode
 {
   /** Block models based on the SAT skeleton. */