docs: Document UnknownExplanation. (#8508)

diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst
index 6b17d122222d2be92bdc1b0ba4803310b213493f..65704ed563c29359421783ddfdcf94eaa29617a9 100644 (file)
--- a/docs/api/cpp/cpp.rst
+++ b/docs/api/cpp/cpp.rst
@@ -30,6 +30,7 @@ For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main
     statistics
     synthresult
     term
+    unknownexplanation
 
 
 Class hierarchy
@@ -52,14 +53,9 @@ Class hierarchy
   * 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`
   * class :ref:`api/cpp/optioninfo:optioninfo`
   * class :ref:`api/cpp/result:result`
-
-    * enum :cpp:enum:`UnknownExplanation <cvc5::Result::UnknownExplanation>`
-
-  * class :ref:`api/cpp/roundingmode:roundingmode`
   * class :ref:`api/cpp/solver:solver`
   * class :ref:`api/cpp/sort:sort`
   * class :cpp:class:`Stat <cvc5::Stat>`
@@ -69,6 +65,9 @@ Class hierarchy
 
     * class :cpp:class:`const_iterator <cvc5::Term::const_iterator>`
 
+  * enum :ref:`api/cpp/kind:kind`
+  * enum :ref:`api/cpp/roundingmode:roundingmode`
+  * enum :ref:`api/cpp/unknownexplanation:unknownexplanation`
   * modes enums :ref:`api/cpp/modes:modes`
 
 ``}``

diff --git a/docs/api/cpp/roundingmode.rst b/docs/api/cpp/roundingmode.rst
index 6626157eb166ed65ddff72eec53283f338c59fa1..6edad90a7f9eae4f6ae17dbacb62fafe7e161e1d 100644 (file)
--- a/docs/api/cpp/roundingmode.rst
+++ b/docs/api/cpp/roundingmode.rst
@@ -3,8 +3,3 @@ RoundingMode
 
 .. doxygenenum:: cvc5::RoundingMode
     :project: cvc5
-
-.. doxygenstruct:: std::hash< cvc5::RoundingMode >
-    :project: std
-    :members:
-    :undoc-members:

diff --git a/docs/api/cpp/unknownexplanation.rst b/docs/api/cpp/unknownexplanation.rst
new file mode 100644 (file)
index 0000000..2009159
--- /dev/null
+++ b/docs/api/cpp/unknownexplanation.rst
@@ -0,0 +1,6 @@
+UnknownExplanation
+==================
+
+.. doxygenenum:: cvc5::UnknownExplanation
+    :project: cvc5
+

diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst
index bb4e3fbdfea3edbf1aab805ff849595fb446d370..8a3848bd43ca9efbdd1b9201b222776685552ed6 100644 (file)
--- a/docs/resource-limits.rst
+++ b/docs/resource-limits.rst
@@ -31,8 +31,8 @@ All other limits are enforced centrally by the resource manager as follows.
 Whenever certain parts of the solver execute, they instruct the resource manager to *spend* a resource.
 As soon as the resource manager realizes that some limit is exhausted (either the resource limit or the per-check time limit is reached), it asynchronously instructs the core solver to interrupt the check.
 To not invalidate the internal state of the solver, and allow to use it again after an interrupt, the solver continues its work until it reaches a safe point in one of the core solving components.
-Then, it returns `unknown` (with an :cpp:enum:`explanation <cvc5::Result::UnknownExplanation>`).
+Then, it returns `unknown` (with an :cpp:enum:`explanation <cvc5::UnknownExplanation>`).
 
 The intention of a resource limit is to be a deterministic measure that grows (linearly, if possible) with actual running time.
 Resources are spent when lemmas are generated and during a few select events like preprocessing, rewriting, decisions and restarts in the SAT solver, or theory checks.
-In case the resource spending does not properly reflect the running time, the weights of the individual resources can be modified using the :ref:`rweight <lbl-option-rweight>` option, for example with ``--rweight=RestartStep=5``.
\ No newline at end of file
+In case the resource spending does not properly reflect the running time, the weights of the individual resources can be modified using the :ref:`rweight <lbl-option-rweight>` option, for example with ``--rweight=RestartStep=5``.

diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h
index db99cf3c8df57a585366c460815498e8388b396d..c05ce06985fd870dbbf302e2e9adec4a7ed8ae34 100644 (file)
--- a/src/api/cpp/cvc5_types.h
+++ b/src/api/cpp/cvc5_types.h
@@ -28,14 +28,26 @@ namespace cvc5 {
  */
 enum UnknownExplanation
 {
+  /**
+   * Full satisfiability check required (e.g., if only preprocessing was
+   * performed).
+   */
   REQUIRES_FULL_CHECK,
+  /** Incomplete theory solver. */
   INCOMPLETE,
+  /** Time limit reached. */
   TIMEOUT,
+  /** Resource limit reached. */
   RESOURCEOUT,
+  /** Memory limit reached. */
   MEMOUT,
+  /** Solver was interrupted. */
   INTERRUPTED,
+  /** Unsupported feature encountered. */
   UNSUPPORTED,
+  /** Other reason. */
   OTHER,
+  /** No specific reason given. */
   UNKNOWN_REASON
 };