From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 14 Apr 2021 20:35:07 +0000 (+0200)
Subject: Improve documentation for API exceptions (#6340)
X-Git-Tag: cvc5-1.0.0~1902
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=485b3db20d182b0d621c002bb355c9d1ec2429e9;p=cvc5.git

Improve documentation for API exceptions (#6340)
---

diff --git a/docs/cpp.rst b/docs/cpp.rst
index b9bc5f077..413524078 100644
--- 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
index 000000000..93a680533
--- /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 1e0e17e52..b541c742e 100644
--- 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())
   {