diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-14 22:35:07 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-14 20:35:07 +0000 |
| commit | 485b3db20d182b0d621c002bb355c9d1ec2429e9 (patch) | |
| tree | 0796088bfe4b70055c298fa6a3d13f246c403ea2 /docs | |
| parent | 9f14a0d6feca8d8ba727f88ef7dda5268183bb56 (diff) | |
Improve documentation for API exceptions (#6340)
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/cpp.rst | 33 | ||||
| -rw-r--r-- | docs/cpp/exceptions.rst | 27 |
2 files changed, 32 insertions, 28 deletions
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: |