cvc4-1.4
CVC4::TypeCheckingException Class Reference

Exception thrown in the case of type-checking errors. More...

#include <expr.h>

Inheritance diagram for CVC4::TypeCheckingException:
CVC4::Exception

Public Member Functions

 TypeCheckingException (const Expr &expr, std::string message) throw ()
 
 TypeCheckingException (const TypeCheckingException &t) throw ()
 Copy constructor. More...
 
 ~TypeCheckingException () throw ()
 Destructor. More...
 
Expr getExpression () const throw ()
 Get the Expr that caused the type-checking to fail. More...
 
void toStream (std::ostream &out) const throw ()
 Returns the message corresponding to the type-checking failure. More...
 
void setMessage (const std::string &msg) throw ()
 
std::string getMessage () const throw ()
 
virtual const char * what () const throw ()
 
std::string toString () const throw ()
 Get this exception as a string. More...
 

Protected Member Functions

 TypeCheckingException () throw ()
 
 TypeCheckingException (ExprManager *em, const TypeCheckingExceptionPrivate *exc) throw ()
 

Protected Attributes

std::string d_msg
 

Friends

class SmtEngine
 
class smt::SmtEnginePrivate
 
class ExprManager
 

Detailed Description

Exception thrown in the case of type-checking errors.

Definition at line 151 of file expr.h.

Constructor & Destructor Documentation

CVC4::TypeCheckingException::TypeCheckingException ( )
throw (
)
inlineprotected

Definition at line 163 of file expr.h.

CVC4::TypeCheckingException::TypeCheckingException ( ExprManager em,
const TypeCheckingExceptionPrivate *  exc 
)
throw (
)
protected
CVC4::TypeCheckingException::TypeCheckingException ( const Expr expr,
std::string  message 
)
throw (
)
CVC4::TypeCheckingException::TypeCheckingException ( const TypeCheckingException t)
throw (
)

Copy constructor.

CVC4::TypeCheckingException::~TypeCheckingException ( )
throw (
)

Destructor.

Member Function Documentation

Expr CVC4::TypeCheckingException::getExpression ( ) const
throw (
)

Get the Expr that caused the type-checking to fail.

Returns
the expr
std::string CVC4::Exception::getMessage ( ) const
throw (
)
inlineinherited

Definition at line 47 of file exception.h.

void CVC4::Exception::setMessage ( const std::string &  msg)
throw (
)
inlineinherited

Definition at line 46 of file exception.h.

void CVC4::TypeCheckingException::toStream ( std::ostream &  out) const
throw (
)
virtual

Returns the message corresponding to the type-checking failure.

We prefer toStream() to toString() because that keeps the expr-depth and expr-language settings present in the stream.

Reimplemented from CVC4::Exception.

std::string CVC4::Exception::toString ( ) const
throw (
)
inlineinherited

Get this exception as a string.

Note that cout << ex.toString(); is subtly different from cout << ex; which is equivalent to ex.toStream(cout); That is because with the latter two, the output language (and other preferences) for exprs on the stream is respected. In toString(), there is no stream, so the parameters are default and you'll get exprs and types printed using the AST language.

Definition at line 64 of file exception.h.

virtual const char* CVC4::Exception::what ( ) const
throw (
)
inlinevirtualinherited

Definition at line 50 of file exception.h.

Friends And Related Function Documentation

friend class ExprManager
friend

Definition at line 191 of file expr.h.

friend class smt::SmtEnginePrivate
friend

Definition at line 154 of file expr.h.

friend class SmtEngine
friend

Definition at line 153 of file expr.h.

Field Documentation

std::string CVC4::Exception::d_msg
protectedinherited

Definition at line 34 of file exception.h.


The documentation for this class was generated from the following file: