diff options
Diffstat (limited to 'docs/cpp')
| -rw-r--r-- | docs/cpp/exceptions.rst | 27 |
1 files changed, 27 insertions, 0 deletions
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: |