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

17 files changed, 132 insertions, 148 deletions

diff --git a/src/base/exception.h b/src/base/exception.h
index 01a054b19..04b155571 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -32,24 +32,24 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC Exception : public std::exception {
-protected:
+ protected:
   std::string d_msg;
 
-public:
+ public:
   // Constructors
-  Exception() throw() : d_msg("Unknown exception") {}
-  Exception(const std::string& msg) throw() : d_msg(msg) {}
-  Exception(const char* msg) throw() : d_msg(msg) {}
+  Exception() : d_msg("Unknown exception") {}
+  Exception(const std::string& msg) : d_msg(msg) {}
+  Exception(const char* msg) : d_msg(msg) {}
 
   // Destructor
-  virtual ~Exception() throw() {}
+  virtual ~Exception() {}
 
   // NON-VIRTUAL METHOD for setting and printing the error message
-  void setMessage(const std::string& msg) throw() { d_msg = msg; }
-  std::string getMessage() const throw() { return d_msg; }
+  void setMessage(const std::string& msg) { d_msg = msg; }
+  std::string getMessage() const { return d_msg; }
 
   // overridden from base class std::exception
-  virtual const char* what() const throw() { return d_msg.c_str(); }
+  const char* what() const noexcept override { return d_msg.c_str(); }
 
   /**
    * Get this exception as a string.  Note that
@@ -63,7 +63,8 @@ public:
    * toString(), there is no stream, so the parameters are default
    * and you'll get exprs and types printed using the AST language.
    */
-  std::string toString() const throw() {
+  std::string toString() const
+  {
     std::stringstream ss;
     toStream(ss);
     return ss.str();
@@ -74,7 +75,7 @@ public:
    * a derived class, it's recommended that this method print the
    * type of exception before the actual message.
    */
-  virtual void toStream(std::ostream& os) const throw() { os << d_msg; }
+  virtual void toStream(std::ostream& os) const { os << d_msg; }
 
 };/* class Exception */
 
@@ -116,8 +117,10 @@ public:
   static std::string formatVariadic(const char* format, ...);
 };/* class IllegalArgumentException */
 
-inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
+inline std::ostream& operator<<(std::ostream& os,
+                                const Exception& e) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const Exception& e)
+{
   e.toStream(os);
   return os;
 }
diff --git a/src/base/exception.i b/src/base/exception.i
index 083670567..429d13a63 100644
--- a/src/base/exception.i
+++ b/src/base/exception.i
@@ -2,8 +2,8 @@
 #include "base/exception.h"
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const Exception&) throw();
-%ignore CVC4::Exception::Exception(const char*) throw();
+%ignore CVC4::operator<<(std::ostream&, const Exception&);
+%ignore CVC4::Exception::Exception(const char*);
 %typemap(javabase) CVC4::Exception "java.lang.RuntimeException";
 
 %rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
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 */
 
 /**
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
index 4cea29592..12c69193e 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -30,9 +30,10 @@ namespace CVC4 {
  * class, below) should be used instead.
  */
 class CVC4_PUBLIC OptionException : public CVC4::Exception {
-public:
-  OptionException(const std::string& s) throw() :
-    CVC4::Exception("Error in option parsing: " + s) {
+ public:
+  OptionException(const std::string& s)
+      : CVC4::Exception("Error in option parsing: " + s)
+  {
   }
 };/* class OptionException */
 
@@ -41,7 +42,7 @@ public:
  * unrecognized or unsupported option key.
  */
 class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException {
-public:
+ public:
   UnrecognizedOptionException() :
     CVC4::OptionException("Unrecognized informational or option key or setting") {
   }
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 48eb43e33..5e1be70e8 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -29,40 +29,33 @@ namespace CVC4 {
 namespace parser {
 
 class CVC4_PUBLIC ParserException : public Exception {
-public:
+ public:
   // Constructors
-  ParserException() throw() :
-    d_filename(),
-    d_line(0),
-    d_column(0) {
-  }
+  ParserException() : d_filename(), d_line(0), d_column(0) {}
 
-  ParserException(const std::string& msg) throw() :
-    Exception(msg),
-    d_filename(),
-    d_line(0),
-    d_column(0) {
+  ParserException(const std::string& msg)
+      : Exception(msg), d_filename(), d_line(0), d_column(0)
+  {
   }
 
-  ParserException(const char* msg) throw() :
-    Exception(msg),
-    d_filename(),
-    d_line(0),
-    d_column(0) {
+  ParserException(const char* msg)
+      : Exception(msg), d_filename(), d_line(0), d_column(0)
+  {
   }
 
-  ParserException(const std::string& msg, const std::string& filename,
-                  unsigned long line, unsigned long column) throw() :
-    Exception(msg),
-    d_filename(filename),
-    d_line(line),
-    d_column(column) {
+  ParserException(const std::string& msg,
+                  const std::string& filename,
+                  unsigned long line,
+                  unsigned long column)
+      : Exception(msg), d_filename(filename), d_line(line), d_column(column)
+  {
   }
 
   // Destructor
-  virtual ~ParserException() throw() {}
+  ~ParserException() override {}
 
-  virtual void toStream(std::ostream& os) const throw() {
+  void toStream(std::ostream& os) const override
+  {
     if( d_line > 0 ) {
       os <<  "Parse Error: " << d_filename << ":" << d_line << "."
          << d_column << ": " << d_msg;
@@ -71,44 +64,34 @@ public:
     }
   }
 
-  std::string getFilename() const throw() {
-    return d_filename;
-  }
+  std::string getFilename() const { return d_filename; }
 
-  int getLine() const throw() {
-    return d_line;
-  }
+  int getLine() const { return d_line; }
 
-  int getColumn() const throw() {
-    return d_column;
-  }
+  int getColumn() const { return d_column; }
 
-protected:
+ protected:
   std::string d_filename;
   unsigned long d_line;
   unsigned long d_column;
 };/* class ParserException */
 
 class CVC4_PUBLIC ParserEndOfFileException : public ParserException {
-public:
-
+ public:
   // Constructors same as ParserException's
 
-  ParserEndOfFileException() throw() :
-    ParserException() {
-  }
+  ParserEndOfFileException() : ParserException() {}
 
-  ParserEndOfFileException(const std::string& msg) throw() :
-    ParserException(msg) {
-  }
+  ParserEndOfFileException(const std::string& msg) : ParserException(msg) {}
 
-  ParserEndOfFileException(const char* msg) throw() :
-    ParserException(msg) {
-  }
+  ParserEndOfFileException(const char* msg) : ParserException(msg) {}
 
-  ParserEndOfFileException(const std::string& msg, const std::string& filename,
-                           unsigned long line, unsigned long column) throw() :
-    ParserException(msg, filename, line, column) {
+  ParserEndOfFileException(const std::string& msg,
+                           const std::string& filename,
+                           unsigned long line,
+                           unsigned long column)
+      : ParserException(msg, filename, line, column)
+  {
   }
 
 };/* class ParserEndOfFileException */
diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
index 5d5b02162..86e386e9a 100644
--- a/src/smt/logic_exception.h
+++ b/src/smt/logic_exception.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC LogicException : public CVC4::Exception {
-public:
+ public:
   LogicException() :
     Exception("Feature used while operating in "
               "incorrect state") {
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index 467f868a3..fba7fdaf6 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -72,16 +72,17 @@ void DeltaRational::seperatingDelta(Rational& res, const DeltaRational& a, const
   }
 }
 
-
-DeltaRationalException::DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (){
-    std::stringstream ss;
-    ss << "Operation [" << op << "] between DeltaRational values ";
-    ss << a << " and " << b << " is not a DeltaRational.";
-    setMessage(ss.str());
+DeltaRationalException::DeltaRationalException(const char* op,
+                                               const DeltaRational& a,
+                                               const DeltaRational& b)
+{
+  std::stringstream ss;
+  ss << "Operation [" << op << "] between DeltaRational values ";
+  ss << a << " and " << b << " is not a DeltaRational.";
+  setMessage(ss.str());
 }
 
-DeltaRationalException::~DeltaRationalException() throw () { }
-
+DeltaRationalException::~DeltaRationalException() {}
 
 Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
   if(isIntegral() && y.isIntegral()){
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index b0ea8a9c1..7a1c18ea2 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -31,9 +31,11 @@ namespace CVC4 {
 class DeltaRational;
 
 class DeltaRationalException : public Exception {
-public:
-  DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw ();
-  virtual ~DeltaRationalException() throw ();
+ public:
+  DeltaRationalException(const char* op,
+                         const DeltaRational& a,
+                         const DeltaRational& b);
+  ~DeltaRationalException() override;
 };
 
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f281bdfcc..f05f47595 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -311,13 +311,13 @@ void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_congruenceManager.setMasterEqualityEngine(eq);
 }
 
-TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) throw (){
+TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg)
+{
   stringstream ss;
   ss << "Cannot construct a model for " << n << " as " << endl << msg;
   setMessage(ss.str());
 }
-TheoryArithPrivate::ModelException::~ModelException() throw (){ }
-
+TheoryArithPrivate::ModelException::~ModelException() {}
 
 TheoryArithPrivate::Statistics::Statistics()
   : d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0)
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index ff60e8436..912bae5e6 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -396,9 +396,9 @@ private:
   bool replayLog(ApproximateSimplex* approx);
 
   class ModelException : public Exception {
-  public:
-    ModelException(TNode n, const char* msg) throw ();
-    virtual ~ModelException() throw ();
+   public:
+    ModelException(TNode n, const char* msg);
+    ~ModelException() override;
   };
 
   /**
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 18ed6d661..f90a06833 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -29,8 +29,9 @@ namespace theory {
 
 class NoMoreValuesException : public Exception {
  public:
-  NoMoreValuesException(TypeNode n) throw() :
-    Exception("No more values for type `" + n.toString() + "'") {
+  NoMoreValuesException(TypeNode n)
+      : Exception("No more values for type `" + n.toString() + "'")
+  {
   }
 };/* class NoMoreValuesException */
 
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 6250cbccd..aa893517b 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -98,7 +98,6 @@ Maybe<Rational> Rational::fromDouble(double d)
   }catch(cln::floating_point_overflow_exception& fpoe){
     return Maybe<Rational>();
   }
-  Unreachable();
 }
 
 } /* namespace CVC4 */
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 7c17ead15..153b237d7 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -84,6 +84,7 @@ public:
 
   /**
    * Constructs a Rational from a C string in a given base (defaults to 10).
+   *
    * Throws std::invalid_argument if the string is not a valid rational.
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().