From 0a531a383e7281bc6ca1bf6610d067f1cc34a8b8 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 31 Mar 2022 23:09:38 -0700
Subject: [PATCH] docs: Add documentation for modes. (#8509)

---
 docs/api/cpp/cpp.rst     | 3 +++
 docs/api/cpp/modes.rst   | 5 +++++
 src/api/cpp/cvc5.h       | 7 +++----
 src/api/cpp/cvc5_types.h | 6 ++++++
 4 files changed, 17 insertions(+), 4 deletions(-)
 create mode 100644 docs/api/cpp/modes.rst

diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst
index 6001b2a86..6b17d1222 100644
--- 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
index 000000000..be93dac47
--- /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 9f4113fb6..b8bab4bcc 100644
--- 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 cf694cd3f..909efc650 100644
--- 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. */
-- 
2.30.2