Improve documentation for API exceptions (#6340)

diff --git a/docs/cpp.rst b/docs/cpp.rst
index b9bc5f07732447f20a0ef47dff7f0eb6bf583d0a..41352407888e9c89eb2bc0ee802407155f3e760a 100644 (file)
--- a/docs/cpp.rst
+++ b/docs/cpp.rst
@@ -8,9 +8,9 @@ Class Hierarchy
 
   * namespace ``api``
 
-    * class :ref:`CVC4ApiException<exceptions>`
+    * class :cpp:class:`cvc5::api::CVC4ApiException`
 
-    * class :ref:`CVC4ApiRecoverableException<exceptions>`
+    * class :cpp:class:`cvc5::api::CVC4ApiRecoverableException`
 
     * class :doc:`cpp/datatype`
 
@@ -48,36 +48,11 @@ Class Hierarchy
 
     * struct :ref:`SortHashFunction<sort>`
 
-    * struct :ref:`TermHashFunction<term>`
 
 
 Full API Documentation
 ----------------------
 
-Exceptions
-^^^^^^^^^^
-.. doxygenclass:: cvc5::api::CVC4ApiException
-    :project: cvc5
-    :members:
-
-.. doxygenclass:: cvc5::api::CVC4ApiRecoverableException
-    :project: cvc5
-    :members:
-
-
-Enums
-^^^^^
-
-.. toctree::
-   :maxdepth: 2
-
-   cpp/kind
-   cpp/roundingmode
-
-
-Classes
-^^^^^^^
-
 .. toctree::
    :maxdepth: 2
 
@@ -86,10 +61,12 @@ Classes
    cpp/datatypeconstructordecl
    cpp/datatypedecl
    cpp/datatypeselector
+   cpp/exceptions
    cpp/grammar
+   cpp/kind
    cpp/op
    cpp/result
+   cpp/roundingmode
    cpp/solver
    cpp/sort
    cpp/term
-

diff --git a/docs/cpp/exceptions.rst b/docs/cpp/exceptions.rst
new file mode 100644 (file)
index 0000000..93a6805
--- /dev/null
+++ b/docs/cpp/exceptions.rst
@@ -0,0 +1,27 @@
+Exceptions
+==========
+
+The CVC5 API communicates certain errors using exceptions. We broadly
+distinguish two types of exceptions: :cpp:class:`CVC4ApiException
+<cvc5::api::CVC4ApiException>` and :cpp:class:`CVC4ApiRecoverableException
+<cvc5::api::CVC4ApiRecoverableException>` (which is derived from
+:cpp:class:`CVC4ApiException <cvc5::api::CVC4ApiException>`).
+
+If any method fails with a :cpp:class:`CVC4ApiRecoverableException
+<cvc5::api::CVC4ApiRecoverableException>`, the solver behaves as if the failing
+method was not called. The solver can still be used safely.
+
+If, however, a method fails with a :cpp:class:`CVC4ApiException
+<cvc5::api::CVC4ApiException>`, the associated object may be in an unsafe state
+and it should no longer be used.
+
+
+.. doxygenclass:: cvc5::api::CVC4ApiException
+    :project: cvc5
+    :members:
+    :undoc-members:
+
+.. doxygenclass:: cvc5::api::CVC4ApiRecoverableException
+    :project: cvc5
+    :members:
+    :undoc-members:

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 1e0e17e529694a25f1b80baef9e5277166bd66ed..b541c742e7f14cf0f89a32f654233ae3f79157aa 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -59,22 +59,55 @@ struct APIStatistics;
 /* Exception                                                                  */
 /* -------------------------------------------------------------------------- */
 
+/**
+ * Base class for all API exceptions.
+ * If thrown, all API objects may be in an unsafe state.
+ */
 class CVC4_EXPORT CVC4ApiException : public std::exception
 {
  public:
+  /**
+   * Construct with message from a string.
+   * @param str The error message.
+   */
   CVC4ApiException(const std::string& str) : d_msg(str) {}
+  /**
+   * Construct with message from a string stream.
+   * @param stream The error message.
+   */
   CVC4ApiException(const std::stringstream& stream) : d_msg(stream.str()) {}
-  std::string getMessage() const { return d_msg; }
+  /**
+   * Retrieve the message from this exception.
+   * @return The error message.
+   */
+  const std::string& getMessage() const { return d_msg; }
+  /**
+   * Retrieve the message as a C-style array.
+   * @return The error message.
+   */
   const char* what() const noexcept override { return d_msg.c_str(); }
 
  private:
+  /** The stored error message. */
   std::string d_msg;
 };
 
+/**
+ * A recoverable API exception.
+ * If thrown, API objects can still be used.
+ */
 class CVC4_EXPORT CVC4ApiRecoverableException : public CVC4ApiException
 {
  public:
+  /**
+   * Construct with message from a string.
+   * @param str The error message.
+   */
   CVC4ApiRecoverableException(const std::string& str) : CVC4ApiException(str) {}
+  /**
+   * Construct with message from a string stream.
+   * @param stream The error message.
+   */
   CVC4ApiRecoverableException(const std::stringstream& stream)
       : CVC4ApiException(stream.str())
   {