From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 1 Apr 2022 22:53:53 +0000 (-0700)
Subject: docs: Document UnknownExplanation. (#8508)
X-Git-Tag: cvc5-1.0.0~50
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5982baed871b6bef18a352a3bb31186f4a364932;p=cvc5.git

docs: Document UnknownExplanation. (#8508)
---

diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst
index 6b17d1222..65704ed56 100644
--- 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 6626157eb..6edad90a7 100644
--- 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
index 000000000..20091596d
--- /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 bb4e3fbdf..8a3848bd4 100644
--- 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 db99cf3c8..c05ce0698 100644
--- 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
 };