Cleaning up throw specifiers on Exception and subclasses. (#1475)

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 */
 
 /**