Removing throw specifiers from miscellaneous src/expr/ classes. (#1503)

11 files changed, 169 insertions, 173 deletions

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 65d16d9cc..c6c0d2bc0 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -57,8 +57,7 @@ ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other)
     : d_type(new ArrayType(other.getType())),
       d_expr(new Expr(other.getExpr())) {}
 
-ArrayStoreAll::~ArrayStoreAll() throw() {}
-
+ArrayStoreAll::~ArrayStoreAll() {}
 ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) {
   (*d_type) = other.getType();
   (*d_expr) = other.getExpr();
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index ce6401cd5..15a973d68 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -32,13 +32,16 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC AscriptionType {
   Type d_type;
-public:
-  AscriptionType(Type t) throw() : d_type(t) {}
-  Type getType() const throw() { return d_type; }
-  bool operator==(const AscriptionType& other) const throw() {
+
+ public:
+  AscriptionType(Type t) : d_type(t) {}
+  Type getType() const { return d_type; }
+  bool operator==(const AscriptionType& other) const
+  {
     return d_type == other.d_type;
   }
-  bool operator!=(const AscriptionType& other) const throw() {
+  bool operator!=(const AscriptionType& other) const
+  {
     return d_type != other.d_type;
   }
 };/* class AscriptionType */
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 8f5b503fe..bcd3a0784 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -106,8 +106,7 @@ void Datatype::resolve(ExprManager* em,
                        const std::vector<Type>& replacements,
                        const std::vector< SortConstructorType >& paramTypes,
                        const std::vector< DatatypeType >& paramReplacements)
-  throw(IllegalArgumentException, DatatypeResolutionException) {
-
+{
   PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
   PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
   PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
@@ -214,7 +213,8 @@ void Datatype::setRecord() {
   d_isRecord = true;
 }
 
-Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentException) {
+Cardinality Datatype::getCardinality(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
   std::vector< Type > processing;
@@ -222,12 +222,15 @@ Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentExcept
   return d_card;
 }
 
-Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
+Cardinality Datatype::getCardinality() const
+{
   PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric");
   return getCardinality( d_self );
 }
 
-Cardinality Datatype::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){
+Cardinality Datatype::computeCardinality(Type t,
+                                         std::vector<Type>& processing) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     d_card = Cardinality::INTEGERS;
@@ -243,7 +246,8 @@ Cardinality Datatype::computeCardinality( Type t, std::vector< Type >& processin
   return d_card;
 }
 
-bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentException) {
+bool Datatype::isRecursiveSingleton(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
   if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){
@@ -269,34 +273,42 @@ bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentExcepti
   return d_card_rec_singleton[t]==1;
 }
 
-bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
+bool Datatype::isRecursiveSingleton() const
+{
   PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric");
   return isRecursiveSingleton( d_self );
 }
 
-unsigned Datatype::getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException) {
+unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
+{
   Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() );
   Assert( isRecursiveSingleton( t ) );
   return d_card_u_assume[t].size();
 }
 
-unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) {
+unsigned Datatype::getNumRecursiveSingletonArgTypes() const
+{
   PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric");
   return getNumRecursiveSingletonArgTypes( d_self );
 }
 
-Type Datatype::getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException) {
+Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
+{
   Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() );
   Assert( isRecursiveSingleton( t ) );
   return d_card_u_assume[t][i];
 }
 
-Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) {
+Type Datatype::getRecursiveSingletonArgType(unsigned i) const
+{
   PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric");
   return getRecursiveSingletonArgType( d_self, i );
 }
 
-bool Datatype::computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){
+bool Datatype::computeCardinalityRecSingleton(Type t,
+                                              std::vector<Type>& processing,
+                                              std::vector<Type>& u_assume) const
+{
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     return true;
   }else{
@@ -343,7 +355,8 @@ bool Datatype::computeCardinalityRecSingleton( Type t, std::vector< Type >& proc
   }
 }
 
-bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) {
+bool Datatype::isFinite(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
 
@@ -365,12 +378,14 @@ bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) {
   self.setAttribute(DatatypeFiniteAttr(), true);
   return true;
 }
-bool Datatype::isFinite() const throw(IllegalArgumentException) {
+bool Datatype::isFinite() const
+{
   PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
   return isFinite( d_self );
 }
 
-bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
   // we're using some internals, so we have to set up this library context
@@ -392,12 +407,14 @@ bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentExceptio
   self.setAttribute(DatatypeUFiniteAttr(), true);
   return true;
 }
-bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite() const
+{
   PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
   return isInterpretedFinite( d_self );
 }
 
-bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
+bool Datatype::isWellFounded() const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( d_well_founded==0 ){
     // we're using some internals, so we have to set up this library context
@@ -412,7 +429,8 @@ bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
   return d_well_founded==1;
 }
 
-bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+bool Datatype::computeWellFounded(std::vector<Type>& processing) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     return d_isCo;
@@ -432,7 +450,8 @@ bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw
   }
 }
 
-Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
+Expr Datatype::mkGroundTerm(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   ExprManagerScope ems(d_self);
   Debug("datatypes") << "mkGroundTerm of type " << t << std::endl;
@@ -476,7 +495,8 @@ Expr getSubtermWithType( Expr e, Type t, bool isTop ){
   }
 }
 
-Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+Expr Datatype::computeGroundTerm(Type t, std::vector<Type>& processing) const
+{
   if( std::find( processing.begin(), processing.end(), t )==processing.end() ){
     processing.push_back( t );
     for( unsigned r=0; r<2; r++ ){
@@ -507,14 +527,15 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons
   return Expr();
 }
 
-DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
+DatatypeType Datatype::getDatatypeType() const
+{
   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
   PrettyCheckArgument(!d_self.isNull(), *this);
   return DatatypeType(d_self);
 }
 
-DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
-  const throw(IllegalArgumentException) {
+DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const
+{
   PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
   PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
   return DatatypeType(d_self).instantiate(params);
@@ -671,8 +692,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::vector<Type>& replacements,
                                   const std::vector< SortConstructorType >& paramTypes,
                                   const std::vector< DatatypeType >& paramReplacements, size_t cindex)
-  throw(IllegalArgumentException, DatatypeResolutionException) {
-
+{
   PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
   PrettyCheckArgument(!isResolved(),
                 "cannot resolve a Datatype constructor twice; "
@@ -902,7 +922,8 @@ std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback()
   return d_sygus_pc;
 }
 
-Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
+Cardinality DatatypeConstructor::getCardinality(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   Cardinality c = 1;
@@ -915,7 +936,9 @@ Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArg
 }
 
 /** compute the cardinality of this datatype */
-Cardinality DatatypeConstructor::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){
+Cardinality DatatypeConstructor::computeCardinality(
+    Type t, std::vector<Type>& processing) const
+{
   Cardinality c = 1;
   std::vector< Type > instTypes;
   std::vector< Type > paramTypes;
@@ -938,7 +961,9 @@ Cardinality DatatypeConstructor::computeCardinality( Type t, std::vector< Type >
   return c;
 }
 
-bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+bool DatatypeConstructor::computeWellFounded(
+    std::vector<Type>& processing) const
+{
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
     Type t = SelectorType((*i).getSelector().getType()).getRangeType();
     if( t.isDatatype() ){
@@ -951,8 +976,8 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing )
   return true;
 }
 
-
-bool DatatypeConstructor::isFinite( Type t ) const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isFinite(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -984,7 +1009,8 @@ bool DatatypeConstructor::isFinite( Type t ) const throw(IllegalArgumentExceptio
   return true;
 }
 
-bool DatatypeConstructor::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isInterpretedFinite(Type t) const
+{
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
@@ -1016,8 +1042,11 @@ bool DatatypeConstructor::isInterpretedFinite( Type t ) const throw(IllegalArgum
   return true;
 }
 
-Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) {
-// we're using some internals, so we have to set up this library context
+Expr DatatypeConstructor::computeGroundTerm(Type t,
+                                            std::vector<Type>& processing,
+                                            std::map<Type, Expr>& gt) const
+{
+  // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
 
   std::vector<Expr> groundTerms;
@@ -1306,10 +1335,7 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
   return os;
 }
 
-DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException) : d_index(index){
-
-}
-
+DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) : d_index(index) {}
 std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
   return out << "index_" << dic.getIndex();
 }
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 59941f174..9e3ad07f8 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -342,21 +342,21 @@ class CVC4_PUBLIC DatatypeConstructor {
    * Return the cardinality of this constructor (the product of the
    * cardinalities of its arguments).
    */
-  Cardinality getCardinality( Type t ) const throw(IllegalArgumentException);
+  Cardinality getCardinality(Type t) const;
 
   /**
    * Return true iff this constructor is finite (it is nullary or
    * each of its argument types are finite).  This function can
    * only be called for resolved constructors.
    */
-  bool isFinite( Type t ) const throw(IllegalArgumentException);
+  bool isFinite(Type t) const;
   /**
    * Return true iff this constructor is finite (it is nullary or
    * each of its argument types are finite) under assumption
    * uninterpreted sorts are finite.  This function can
    * only be called for resolved constructors.
    */
-  bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException);
+  bool isInterpretedFinite(Type t) const;
 
   /**
    * Returns true iff this Datatype constructor has already been
@@ -494,8 +494,7 @@ class CVC4_PUBLIC DatatypeConstructor {
                const std::vector<Type>& replacements,
                const std::vector<SortConstructorType>& paramTypes,
                const std::vector<DatatypeType>& paramReplacements,
-               size_t cindex) throw(IllegalArgumentException,
-                                    DatatypeResolutionException);
+               size_t cindex);
 
   /** Helper function for resolving parametric datatypes.
    *
@@ -518,16 +517,13 @@ class CVC4_PUBLIC DatatypeConstructor {
       const std::vector<DatatypeType>& paramReplacements);
 
   /** compute the cardinality of this datatype */
-  Cardinality computeCardinality(Type t, std::vector<Type>& processing) const
-      throw(IllegalArgumentException);
+  Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
   /** compute whether this datatype is well-founded */
-  bool computeWellFounded(std::vector<Type>& processing) const
-      throw(IllegalArgumentException);
+  bool computeWellFounded(std::vector<Type>& processing) const;
   /** compute ground term */
   Expr computeGroundTerm(Type t,
                          std::vector<Type>& processing,
-                         std::map<Type, Expr>& gt) const
-      throw(IllegalArgumentException);
+                         std::map<Type, Expr>& gt) const;
   /** compute shared selectors
    * This computes the maps d_shared_selectors and d_shared_selector_index.
    */
@@ -732,8 +728,8 @@ public:
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
    */
-  Cardinality getCardinality( Type t ) const throw(IllegalArgumentException);
-  Cardinality getCardinality() const throw(IllegalArgumentException);
+  Cardinality getCardinality(Type t) const;
+  Cardinality getCardinality() const;
 
   /**
    * Return true iff this Datatype has finite cardinality. If the
@@ -744,8 +740,8 @@ public:
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
    */
-  bool isFinite( Type t ) const throw(IllegalArgumentException);
-  bool isFinite() const throw(IllegalArgumentException);
+  bool isFinite(Type t) const;
+  bool isFinite() const;
 
   /**
    * Return true iff this  Datatype is finite (all constructors are
@@ -758,8 +754,8 @@ public:
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
    */
-  bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException);
-  bool isInterpretedFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite(Type t) const;
+  bool isInterpretedFinite() const;
 
   /** is well-founded
    *
@@ -767,7 +763,7 @@ public:
    * values of this type).
    * This datatype must be resolved or an exception is thrown.
    */
-  bool isWellFounded() const throw(IllegalArgumentException);
+  bool isWellFounded() const;
 
   /** is recursive singleton
    *
@@ -779,8 +775,8 @@ public:
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
    */
-  bool isRecursiveSingleton( Type t ) const throw(IllegalArgumentException);
-  bool isRecursiveSingleton() const throw(IllegalArgumentException);
+  bool isRecursiveSingleton(Type t) const;
+  bool isRecursiveSingleton() const;
 
   /** recursive single arguments
    *
@@ -795,10 +791,10 @@ public:
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
   */
-  unsigned getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException);
-  Type getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException);
-  unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException);
-  Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException);
+  unsigned getNumRecursiveSingletonArgTypes(Type t) const;
+  Type getRecursiveSingletonArgType(Type t, unsigned i) const;
+  unsigned getNumRecursiveSingletonArgTypes() const;
+  Type getRecursiveSingletonArgType(unsigned i) const;
 
   /**
    * Construct and return a ground term of this Datatype.  The
@@ -809,19 +805,19 @@ public:
    * datatype is this class, which may be an instantiated datatype
    * type if this datatype is parametric.
    */
-  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
+  Expr mkGroundTerm(Type t) const;
 
   /**
    * Get the DatatypeType associated to this Datatype.  Can only be
    * called post-resolution.
    */
-  DatatypeType getDatatypeType() const throw(IllegalArgumentException);
+  DatatypeType getDatatypeType() const;
 
   /**
    * Get the DatatypeType associated to this (parameterized) Datatype.  Can only be
    * called post-resolution.
    */
-  DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException);
+  DatatypeType getDatatypeType(const std::vector<Type>& params) const;
 
   /**
    * Return true iff the two Datatypes are the same.
@@ -1026,25 +1022,19 @@ public:
                const std::vector<Type>& placeholders,
                const std::vector<Type>& replacements,
                const std::vector<SortConstructorType>& paramTypes,
-               const std::vector<DatatypeType>&
-                   paramReplacements) throw(IllegalArgumentException,
-                                            DatatypeResolutionException);
+               const std::vector<DatatypeType>& paramReplacements);
   friend class ExprManager;  // for access to resolve()
 
   /** compute the cardinality of this datatype */
-  Cardinality computeCardinality(Type t, std::vector<Type>& processing) const
-      throw(IllegalArgumentException);
+  Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
   /** compute whether this datatype is a recursive singleton */
   bool computeCardinalityRecSingleton(Type t,
                                       std::vector<Type>& processing,
-                                      std::vector<Type>& u_assume) const
-      throw(IllegalArgumentException);
+                                      std::vector<Type>& u_assume) const;
   /** compute whether this datatype is well-founded */
-  bool computeWellFounded(std::vector<Type>& processing) const
-      throw(IllegalArgumentException);
+  bool computeWellFounded(std::vector<Type>& processing) const;
   /** compute ground term */
-  Expr computeGroundTerm(Type t, std::vector<Type>& processing) const
-      throw(IllegalArgumentException);
+  Expr computeGroundTerm(Type t, std::vector<Type>& processing) const;
   /** Get the shared selector
    *
    * This returns the index^th (constructor-agnostic)
@@ -1081,11 +1071,9 @@ struct CVC4_PUBLIC DatatypeHashFunction {
 
 /* stores an index to Datatype residing in NodeManager */
 class CVC4_PUBLIC DatatypeIndexConstant {
-public:
-
-  DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException);
+ public:
+  DatatypeIndexConstant(unsigned index);
 
-  ~DatatypeIndexConstant() {}
   const unsigned getIndex() const { return d_index; }
   bool operator==(const DatatypeIndexConstant& uc) const
   {
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index 42560fa11..10f03e279 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -49,38 +49,26 @@ EmptySet& EmptySet::operator=(const EmptySet& es) {
   return *this;
 }
 
-
-EmptySet::~EmptySet() throw() {
-  delete d_type;
-}
-
+EmptySet::~EmptySet() { delete d_type; }
 const SetType& EmptySet::getType() const {
   return *d_type;
 }
-
-bool EmptySet::operator==(const EmptySet& es) const throw() {
+bool EmptySet::operator==(const EmptySet& es) const
+{
   return getType() == es.getType();
 }
 
-bool EmptySet::operator!=(const EmptySet& es) const throw() {
-  return !(*this == es);
-}
-
-bool EmptySet::operator<(const EmptySet& es) const throw() {
+bool EmptySet::operator!=(const EmptySet& es) const { return !(*this == es); }
+bool EmptySet::operator<(const EmptySet& es) const
+{
   return getType() < es.getType();
 }
 
-bool EmptySet::operator<=(const EmptySet& es) const throw() {
+bool EmptySet::operator<=(const EmptySet& es) const
+{
   return getType() <= es.getType();
 }
 
-bool EmptySet::operator>(const EmptySet& es) const throw() {
-  return !(*this <= es);
-}
-
-bool EmptySet::operator>=(const EmptySet& es) const throw() {
-  return !(*this < es);
-}
-
-
+bool EmptySet::operator>(const EmptySet& es) const { return !(*this <= es); }
+bool EmptySet::operator>=(const EmptySet& es) const { return !(*this < es); }
 }/* CVC4 namespace */
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index 8cb2bbf41..9fcab7a55 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -33,25 +33,25 @@ namespace CVC4 {
 
 namespace CVC4 {
 class CVC4_PUBLIC EmptySet {
-public:
+ public:
   /**
    * Constructs an emptyset of the specified type. Note that the argument
    * is the type of the set itself, NOT the type of the elements.
    */
   EmptySet(const SetType& setType);
-  ~EmptySet() throw();
+  ~EmptySet();
   EmptySet(const EmptySet& other);
   EmptySet& operator=(const EmptySet& other);
 
   const SetType& getType() const;
-  bool operator==(const EmptySet& es) const throw();
-  bool operator!=(const EmptySet& es) const throw();
-  bool operator<(const EmptySet& es) const throw();
-  bool operator<=(const EmptySet& es) const throw();
-  bool operator>(const EmptySet& es) const throw() ;
-  bool operator>=(const EmptySet& es) const throw();
+  bool operator==(const EmptySet& es) const;
+  bool operator!=(const EmptySet& es) const;
+  bool operator<(const EmptySet& es) const;
+  bool operator<=(const EmptySet& es) const;
+  bool operator>(const EmptySet& es) const;
+  bool operator>=(const EmptySet& es) const;
 
-private:
+ private:
   /** Pointer to the SetType node. This is never NULL. */
   SetType* d_type;
 
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index c4bb633bd..db1680c7e 100644
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -58,10 +58,10 @@ public:
   }
 
   /* Helper functions for toPickle */
-  void toCaseNode(TNode n) throw(AssertionException, PicklingException);
-  void toCaseVariable(TNode n) throw(AssertionException, PicklingException);
+  void toCaseNode(TNode n);
+  void toCaseVariable(TNode n);
   void toCaseConstant(TNode n);
-  void toCaseOperator(TNode n) throw(AssertionException, PicklingException);
+  void toCaseOperator(TNode n);
   void toCaseString(Kind k, const std::string& s);
 
   /* Helper functions for toPickle */
@@ -127,7 +127,7 @@ Pickler::~Pickler() {
 }
 
 void Pickler::toPickle(Expr e, Pickle& p)
-  throw(PicklingException) {
+{
   Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
   Assert(d_private->atDefaultState());
 
@@ -145,7 +145,7 @@ void Pickler::toPickle(Expr e, Pickle& p)
 }
 
 void PicklerPrivate::toCaseNode(TNode n)
-  throw(AssertionException, PicklingException) {
+{
   Debug("pickler") << "toCaseNode: " << n << std::endl;
   Kind k = n.getKind();
   kind::MetaKind m = metaKindOf(k);
@@ -166,7 +166,7 @@ void PicklerPrivate::toCaseNode(TNode n)
 }
 
 void PicklerPrivate::toCaseOperator(TNode n)
-  throw(AssertionException, PicklingException) {
+{
   Kind k = n.getKind();
   kind::MetaKind m = metaKindOf(k);
   Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR);
@@ -180,7 +180,7 @@ void PicklerPrivate::toCaseOperator(TNode n)
 }
 
 void PicklerPrivate::toCaseVariable(TNode n)
-  throw(AssertionException, PicklingException) {
+{
   Kind k = n.getKind();
   Assert(metaKindOf(k) == kind::metakind::VARIABLE);
 
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index f9a3d07bd..652ca40c8 100644
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -64,14 +64,8 @@ class CVC4_PUBLIC Pickler {
   friend class PicklerPrivate;
 
 protected:
-  virtual uint64_t variableToMap(uint64_t x) const
-    throw(PicklingException) {
-    return x;
-  }
-  virtual uint64_t variableFromMap(uint64_t x) const {
-    return x;
-  }
-
+ virtual uint64_t variableToMap(uint64_t x) const { return x; }
+ virtual uint64_t variableFromMap(uint64_t x) const { return x; }
 public:
   Pickler(ExprManager* em);
   virtual ~Pickler();
@@ -85,7 +79,7 @@ public:
    *
    * @return the pickle, which should be dispose()'d when you're done with it
    */
-  void toPickle(Expr e, Pickle& p) throw(PicklingException);
+  void toPickle(Expr e, Pickle& p);
 
   /**
    * Constructs a node from a Pickle.
@@ -111,21 +105,21 @@ public:
     d_fromMap(from) {
   }
 
-  virtual ~MapPickler() throw() {}
-
 protected:
-
-  virtual uint64_t variableToMap(uint64_t x) const
-    throw(PicklingException) {
-    VarMap::const_iterator i = d_toMap.find(x);
-    if(i != d_toMap.end()) {
-      return i->second;
-    } else {
-      throw PicklingException();
-    }
+ uint64_t variableToMap(uint64_t x) const override
+ {
+   VarMap::const_iterator i = d_toMap.find(x);
+   if (i != d_toMap.end())
+   {
+     return i->second;
+   }
+   else
+   {
+     throw PicklingException();
+   }
   }
 
-  virtual uint64_t variableFromMap(uint64_t x) const; 
+  uint64_t variableFromMap(uint64_t x) const override;
 };/* class MapPickler */
 
 }/* CVC4::expr::pickle namespace */
diff --git a/src/expr/record.h b/src/expr/record.h
index ae03a7acd..774c07319 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -37,11 +37,12 @@ namespace CVC4 {
 // operators for record update
 class CVC4_PUBLIC RecordUpdate {
   std::string d_field;
-public:
-  RecordUpdate(const std::string& field) throw() : d_field(field) { }
-  std::string getField() const throw() { return d_field; }
-  bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; }
-  bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; }
+
+ public:
+  RecordUpdate(const std::string& field) : d_field(field) {}
+  std::string getField() const { return d_field; }
+  bool operator==(const RecordUpdate& t) const { return d_field == t.d_field; }
+  bool operator!=(const RecordUpdate& t) const { return d_field != t.d_field; }
 };/* class RecordUpdate */
 
 struct CVC4_PUBLIC RecordUpdateHashFunction {
@@ -54,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
 
 // now an actual record definition
 class CVC4_PUBLIC Record {
-public:
+ public:
   // Type must stay as incomplete types throughout this header!
   // Everything containing a Type must be a pointer or a reference.
   typedef std::vector< std::pair<std::string, Type> > FieldVector;
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index c823529be..062ea235d 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -26,9 +26,8 @@ using namespace std;
 
 namespace CVC4 {
 
-UninterpretedConstant::UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException)
-    : d_type(type)
-    , d_index(index)
+UninterpretedConstant::UninterpretedConstant(Type type, Integer index)
+    : d_type(type), d_index(index)
 {
   //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
   PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 06747e1af..16800391c 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -25,42 +25,40 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC UninterpretedConstant {
-public:
+ public:
+  UninterpretedConstant(Type type, Integer index);
 
-  UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException);
-
-  ~UninterpretedConstant() throw() { }
-
-  Type getType() const throw() {
-    return d_type;
-  }
-  const Integer& getIndex() const throw() {
-    return d_index;
-  }
-
-  bool operator==(const UninterpretedConstant& uc) const throw() {
+  Type getType() const { return d_type; }
+  const Integer& getIndex() const { return d_index; }
+  bool operator==(const UninterpretedConstant& uc) const
+  {
     return d_type == uc.d_type && d_index == uc.d_index;
   }
-  bool operator!=(const UninterpretedConstant& uc) const throw() {
+  bool operator!=(const UninterpretedConstant& uc) const
+  {
     return !(*this == uc);
   }
 
-  bool operator<(const UninterpretedConstant& uc) const throw() {
+  bool operator<(const UninterpretedConstant& uc) const
+  {
     return d_type < uc.d_type ||
            (d_type == uc.d_type && d_index < uc.d_index);
   }
-  bool operator<=(const UninterpretedConstant& uc) const throw() {
+  bool operator<=(const UninterpretedConstant& uc) const
+  {
     return d_type < uc.d_type ||
            (d_type == uc.d_type && d_index <= uc.d_index);
   }
-  bool operator>(const UninterpretedConstant& uc) const throw() {
+  bool operator>(const UninterpretedConstant& uc) const
+  {
     return !(*this <= uc);
   }
-  bool operator>=(const UninterpretedConstant& uc) const throw() {
+  bool operator>=(const UninterpretedConstant& uc) const
+  {
     return !(*this < uc);
   }
 
-private:
+ private:
   const Type d_type;
   const Integer d_index;
 };/* class UninterpretedConstant */