diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.h | 2 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 30 | ||||
-rw-r--r-- | src/expr/expr_template.h | 34 | ||||
-rw-r--r-- | src/expr/node.cpp | 26 | ||||
-rw-r--r-- | src/expr/node.h | 21 |
5 files changed, 53 insertions, 60 deletions
diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 9e3ad07f8..fffabac77 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -88,7 +88,7 @@ public: * An exception that is thrown when a datatype resolution fails. */ class CVC4_PUBLIC DatatypeResolutionException : public Exception { -public: + public: inline DatatypeResolutionException(std::string msg); };/* class DatatypeResolutionException */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 6dbc2256c..0ed3601fc 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -54,31 +54,33 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { } } -TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() : - Exception(t.d_msg), d_expr(new Expr(t.getExpression())) { +TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) + : Exception(t.d_msg), d_expr(new Expr(t.getExpression())) +{ } -TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() : - Exception(message), d_expr(new Expr(expr)) { +TypeCheckingException::TypeCheckingException(const Expr& expr, + std::string message) + : Exception(message), d_expr(new Expr(expr)) +{ } -TypeCheckingException::TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc) throw() : - Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) { +TypeCheckingException::TypeCheckingException( + ExprManager* em, const TypeCheckingExceptionPrivate* exc) + : Exception(exc->getMessage()), + d_expr(new Expr(em, new Node(exc->getNode()))) +{ } -TypeCheckingException::~TypeCheckingException() throw() { - delete d_expr; -} +TypeCheckingException::~TypeCheckingException() { delete d_expr; } -void TypeCheckingException::toStream(std::ostream& os) const throw() { +void TypeCheckingException::toStream(std::ostream& os) const +{ os << "Error during type checking: " << d_msg << endl << "The ill-typed expression: " << *d_expr; } -Expr TypeCheckingException::getExpression() const throw() { - return *d_expr; -} +Expr TypeCheckingException::getExpression() const { return *d_expr; } Expr::Expr() : d_node(new Node), diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index ead50c1ab..9656781a8 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -83,44 +83,40 @@ namespace expr { * Exception thrown in the case of type-checking errors. */ class CVC4_PUBLIC TypeCheckingException : public Exception { - + private: friend class SmtEngine; friend class smt::SmtEnginePrivate; -private: - /** The expression responsible for the error */ Expr* d_expr; -protected: - - TypeCheckingException() throw() : Exception() {} + protected: + TypeCheckingException() : Exception() {} TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc) throw(); + const TypeCheckingExceptionPrivate* exc); -public: - - TypeCheckingException(const Expr& expr, std::string message) throw(); + public: + TypeCheckingException(const Expr& expr, std::string message); /** Copy constructor */ - TypeCheckingException(const TypeCheckingException& t) throw(); + TypeCheckingException(const TypeCheckingException& t); /** Destructor */ - ~TypeCheckingException() throw(); + ~TypeCheckingException() override; /** * Get the Expr that caused the type-checking to fail. * * @return the expr */ - Expr getExpression() const throw(); + Expr getExpression() const; /** * 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. */ - void toStream(std::ostream& out) const throw(); + void toStream(std::ostream& out) const override; friend class ExprManager; };/* class TypeCheckingException */ @@ -129,13 +125,9 @@ public: * Exception thrown in case of failure to export */ class CVC4_PUBLIC ExportUnsupportedException : public Exception { -public: - ExportUnsupportedException() throw(): - Exception("export unsupported") { - } - ExportUnsupportedException(const char* msg) throw(): - Exception(msg) { - } + public: + ExportUnsupportedException() : Exception("export unsupported") {} + ExportUnsupportedException(const char* msg) : Exception(msg) {} };/* class DatatypeExportUnsupportedException */ std::ostream& operator<<(std::ostream& out, diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 126feadd8..110925f41 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -27,9 +27,9 @@ using namespace std; namespace CVC4 { TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, - std::string message) throw() : - Exception(message), - d_node(new Node(node)) { + std::string message) + : Exception(message), d_node(new Node(node)) +{ #ifdef CVC4_DEBUG LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); if(current != NULL){ @@ -38,21 +38,25 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, #endif /* CVC4_DEBUG */ } -TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { - delete d_node; -} +TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; } -void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() { +void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const +{ os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node; } -NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() { +NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const +{ return *d_node; } -UnknownTypeException::UnknownTypeException(TNode n) throw() : - TypeCheckingExceptionPrivate(n, "this expression contains an element of unknown type (such as an abstract value);" - " its type cannot be computed until it is substituted away") { +UnknownTypeException::UnknownTypeException(TNode n) + : TypeCheckingExceptionPrivate( + n, + "this expression contains an element of unknown type (such as an " + "abstract value);" + " its type cannot be computed until it is substituted away") +{ } /** Is this node constant? (and has that been computed yet?) */ diff --git a/src/expr/node.h b/src/expr/node.h index 66f8b0a47..fd3d20afa 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -66,44 +66,39 @@ class NodeTemplate; * thrown by node.getType(). */ class TypeCheckingExceptionPrivate : public Exception { - -private: - + private: /** The node responsible for the failure */ NodeTemplate<true>* d_node; -public: - + public: /** * Construct the exception with the problematic node and the message * @param node the problematic node * @param message the message explaining the failure */ - TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw(); + TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message); /** Destructor */ - ~TypeCheckingExceptionPrivate() throw (); + ~TypeCheckingExceptionPrivate() override; /** * Get the Node that caused the type-checking to fail. * @return the node */ - NodeTemplate<true> getNode() const throw(); + NodeTemplate<true> getNode() const; /** * 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. */ - void toStream(std::ostream& out) const throw(); + void toStream(std::ostream& out) const override; };/* class TypeCheckingExceptionPrivate */ class UnknownTypeException : public TypeCheckingExceptionPrivate { -public: - - UnknownTypeException(NodeTemplate<false> node) throw(); - + public: + UnknownTypeException(NodeTemplate<false> node); };/* class UnknownTypeException */ /** |