Removing miscellaneous throw specifiers. (#1474)

5 files changed, 32 insertions, 44 deletions

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index ff026057c..65d16d9cc 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -65,33 +65,39 @@ ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) {
   return *this;
 }
 
-const ArrayType& ArrayStoreAll::getType() const throw() { return *d_type; }
+const ArrayType& ArrayStoreAll::getType() const { return *d_type; }
 
-const Expr& ArrayStoreAll::getExpr() const throw() { return *d_expr; }
+const Expr& ArrayStoreAll::getExpr() const { return *d_expr; }
 
-bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const
+{
   return getType() == asa.getType() && getExpr() == asa.getExpr();
 }
 
-bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const
+{
   return !(*this == asa);
 }
 
-bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const
+{
   return (getType() < asa.getType()) ||
          (getType() == asa.getType() && getExpr() < asa.getExpr());
 }
 
-bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const
+{
   return (getType() < asa.getType()) ||
          (getType() == asa.getType() && getExpr() <= asa.getExpr());
 }
 
-bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const
+{
   return !(*this <= asa);
 }
 
-bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const throw() {
+bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const
+{
   return !(*this < asa);
 }
 
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 308794f48..6b265d740 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -40,20 +40,20 @@ class CVC4_PUBLIC ArrayStoreAll {
    * not a constant of type `type`.
    */
   ArrayStoreAll(const ArrayType& type, const Expr& expr);
-  ~ArrayStoreAll() throw();
+  ~ArrayStoreAll();
 
   ArrayStoreAll(const ArrayStoreAll& other);
   ArrayStoreAll& operator=(const ArrayStoreAll& other);
 
-  const ArrayType& getType() const throw();
-  const Expr& getExpr() const throw();
+  const ArrayType& getType() const;
+  const Expr& getExpr() const;
 
-  bool operator==(const ArrayStoreAll& asa) const throw();
-  bool operator!=(const ArrayStoreAll& asa) const throw();
-  bool operator<(const ArrayStoreAll& asa) const throw();
-  bool operator<=(const ArrayStoreAll& asa) const throw();
-  bool operator>(const ArrayStoreAll& asa) const throw();
-  bool operator>=(const ArrayStoreAll& asa) const throw();
+  bool operator==(const ArrayStoreAll& asa) const;
+  bool operator!=(const ArrayStoreAll& asa) const;
+  bool operator<(const ArrayStoreAll& asa) const;
+  bool operator<=(const ArrayStoreAll& asa) const;
+  bool operator>(const ArrayStoreAll& asa) const;
+  bool operator>=(const ArrayStoreAll& asa) const;
 
  private:
   std::unique_ptr<ArrayType> d_type;
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d6249d6fd..bc4205217 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -93,7 +93,8 @@ ExprManager::ExprManager(const Options& options) :
 #endif
 }
 
-ExprManager::~ExprManager() throw() {
+ExprManager::~ExprManager()
+{
   NodeManagerScope nms(d_nodeManager);
 
   try {
@@ -128,7 +129,8 @@ const Options& ExprManager::getOptions() const {
   return d_nodeManager->getOptions();
 }
 
-ResourceManager* ExprManager::getResourceManager() throw() {
+ResourceManager* ExprManager::getResourceManager()
+{
   return d_nodeManager->getResourceManager();
 }
 
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index a12c68791..35a3b6a6e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -109,13 +109,13 @@ public:
    * any expression references that used to be managed by this expression
    * manager and are left-over are bad.
    */
-  ~ExprManager() throw();
+  ~ExprManager();
 
   /** Get this expr manager's options */
   const Options& getOptions() const;
 
   /** Get this expr manager's resource manager */
-  ResourceManager* getResourceManager() throw();
+  ResourceManager* getResourceManager();
 
   /** Get the type for booleans */
   BooleanType booleanType() const;
@@ -436,27 +436,6 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingException can be thrown if lambda is
-   * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
-   * the resulting predicate subtype is inhabited.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda)
-  //  throw(TypeCheckingException);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingException can be thrown if lambda is not
-   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
-   * ill-typed.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda, Expr witness)
-  //  throw(TypeCheckingException);
-
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
     throw(TypeCheckingException);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0b1773114..d9345a5f5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -391,10 +391,11 @@ public:
   }
 
   /** Get this node manager's resource manager */
-  ResourceManager* getResourceManager() throw() { return d_resourceManager; }
+  ResourceManager* getResourceManager() { return d_resourceManager; }
 
   /** Get this node manager's statistics registry */
-  StatisticsRegistry* getStatisticsRegistry() const throw() {
+  StatisticsRegistry* getStatisticsRegistry() const
+  {
     return d_statisticsRegistry;
   }