Exceptions 

The cvc5 API communicates certain errors using exceptions. We broadly distinguish two types of exceptions: CVC5ApiException and CVC5ApiRecoverableException (which is derived from CVC5ApiException ).

If any method fails with a CVC5ApiRecoverableException , 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 CVC5ApiException , the associated object may be in an unsafe state and it should no longer be used.

class CVC5ApiException : public exception 

Base class for all API exceptions. If thrown, all API objects may be in an unsafe state.

Subclassed by cvc5::CVC5ApiRecoverableException , cvc5::parser::ParserException

Public Functions

inline CVC5ApiException ( const std :: string & str ) 

Construct with message from a string.

Parameters :

str – The error message.

inline CVC5ApiException ( const std :: stringstream & stream ) 

Construct with message from a string stream.

Parameters :

stream – The error message.

inline const std :: string & getMessage ( ) const 

Retrieve the message from this exception.

Returns :

The error message.

inline const char * what ( ) const noexcept override 

Retrieve the message as a C-style array.

Returns :

The error message.

inline virtual void toStream ( std :: ostream & os ) const 

Printing: feel free to redefine toStream() . When overridden in a derived class, it’s recommended that this method print the type of exception before the actual message.

class CVC5ApiRecoverableException : public cvc5 :: CVC5ApiException 

A recoverable API exception. If thrown, API objects can still be used.

Subclassed by cvc5::CVC5ApiOptionException, cvc5::CVC5ApiUnsupportedException

Public Functions

inline CVC5ApiRecoverableException ( const std :: string & str ) 

Construct with message from a string.

Parameters :

str – The error message.

inline CVC5ApiRecoverableException ( const std :: stringstream & stream ) 

Construct with message from a string stream.

Parameters :

stream – The error message.