Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

11 files changed, 72 insertions, 70 deletions

diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 123d568cb..a957d6809 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -30,9 +30,12 @@ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) {
   return out << "@" << val.getIndex();
 }
 
-AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) :
-    d_index(index) {
-    PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
+AbstractValue::AbstractValue(Integer index) : d_index(index)
+{
+  PrettyCheckArgument(index >= 1,
+                      index,
+                      "index >= 1 required for abstract value, not `%s'",
+                      index.toString().c_str());
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 9c8e1cb37..2fbc26bec 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -27,36 +27,25 @@ namespace CVC4 {
 class CVC4_PUBLIC AbstractValue {
   const Integer d_index;
 
-public:
+ public:
+  AbstractValue(Integer index);
 
-  AbstractValue(Integer index) throw(IllegalArgumentException);
-
-  ~AbstractValue() throw() {}
-
-  const Integer& getIndex() const throw() {
-    return d_index;
-  }
-
-  bool operator==(const AbstractValue& val) const throw() {
+  const Integer& getIndex() const { return d_index; }
+  bool operator==(const AbstractValue& val) const
+  {
     return d_index == val.d_index;
   }
-  bool operator!=(const AbstractValue& val) const throw() {
-    return !(*this == val);
-  }
-
-  bool operator<(const AbstractValue& val) const throw() {
+  bool operator!=(const AbstractValue& val) const { return !(*this == val); }
+  bool operator<(const AbstractValue& val) const
+  {
     return d_index < val.d_index;
   }
-  bool operator<=(const AbstractValue& val) const throw() {
+  bool operator<=(const AbstractValue& val) const
+  {
     return d_index <= val.d_index;
   }
-  bool operator>(const AbstractValue& val) const throw() {
-    return !(*this <= val);
-  }
-  bool operator>=(const AbstractValue& val) const throw() {
-    return !(*this < val);
-  }
-
+  bool operator>(const AbstractValue& val) const { return !(*this <= val); }
+  bool operator>=(const AbstractValue& val) const { return !(*this < val); }
 };/* class AbstractValue */
 
 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
diff --git a/src/util/cache.h b/src/util/cache.h
index 38dc0fc99..4f9af98a6 100644
--- a/src/util/cache.h
+++ b/src/util/cache.h
@@ -58,9 +58,9 @@ public:
     bool d_fired;
 
   public:
-    Scope(Cache<T, U, Hasher>& cache, const T& elt) throw(AssertionException) :
-      d_cache(cache),
-      d_fired(d_cache.computing(elt)) {
+   Scope(Cache<T, U, Hasher>& cache, const T& elt)
+       : d_cache(cache), d_fired(d_cache.computing(elt))
+   {
     }
 
     ~Scope() {
@@ -69,21 +69,21 @@ public:
       }
     }
 
-    operator bool() throw() {
-      return d_fired;
-    }
-
-    const U& get() throw(AssertionException) {
+    operator bool() const { return d_fired; }
+    const U& get() const
+    {
       Assert(d_fired, "nothing in cache");
       return d_cache.get();
     }
 
-    U& operator()(U& computed) throw(AssertionException) {
+    U& operator()(U& computed)
+    {
       Assert(!d_fired, "can only cache a computation once");
       d_fired = true;
       return d_cache(computed);
     }
-    const U& operator()(const U& computed) throw(AssertionException) {
+    const U& operator()(const U& computed)
+    {
       Assert(!d_fired, "can only cache a computation once");
       d_fired = true;
       return d_cache(computed);
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 8f98d908f..c67277ad0 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -59,8 +59,8 @@ Integer Integer::exactQuotient(const Integer& y) const {
   return Integer( cln::exquo(d_value, y.d_value) );
 }
 
-
-void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
+void Integer::parseInt(const std::string& s, unsigned base)
+{
   cln::cl_read_flags flags;
   flags.syntax = cln::syntax_integer;
   flags.lsyntax = cln::lsyntax_standard;
@@ -86,7 +86,10 @@ void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_a
   readInt(flags, s, base);
 }
 
-void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
+void Integer::readInt(const cln::cl_read_flags& flags,
+                      const std::string& s,
+                      unsigned base)
+{
   try {
     // Removing leading zeroes, CLN has a bug for these inputs up to and
     // including CLN v1.3.2.
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 0433494cc..542333b1f 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -52,11 +52,13 @@ private:
    * Constructs an Integer by copying a CLN C++ primitive.
    */
   Integer(const cln::cl_I& val) : d_value(val) {}
+  // Throws a std::invalid_argument on invalid input `s` for the given base.
+  void readInt(const cln::cl_read_flags& flags,
+               const std::string& s,
+               unsigned base);
 
-  void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument);
-
-  void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
-
+  // Throws a std::invalid_argument on invalid inputs.
+  void parseInt(const std::string& s, unsigned base);
 
   // These constants are to help with CLN conversion in 32 bit.
   // See http://www.ginac.de/CLN/cln.html#Conversions
@@ -81,11 +83,13 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) {
+  explicit Integer(const char* sp, unsigned base = 10)
+  {
     parseInt(std::string(sp), base);
   }
 
-  explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) {
+  explicit Integer(const std::string& s, unsigned base = 10)
+  {
     parseInt(s, base);
   }
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 0b09bf1fd..2752971d2 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -84,14 +84,15 @@ public:
   /** Constructs a rational with the value 0/1. */
   Rational() : d_value(0){
   }
-
   /**
    * 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().
    */
-  explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
+  explicit Rational(const char* s, unsigned base = 10)
+  {
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
@@ -105,7 +106,8 @@ public:
       throw std::invalid_argument(ss.str());
     }
   }
-  Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
+  Rational(const std::string& s, unsigned base = 10)
+  {
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index b2adb4aba..9bcdcd96b 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -173,13 +173,14 @@ uint64_t ResourceManager::getTimeRemaining() const {
   return d_thisCallTimeBudget - time_passed;
 }
 
-void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) {
+void ResourceManager::spendResource(unsigned amount)
+{
   ++d_spendResourceCalls;
-  d_cumulativeResourceUsed += ammount;
+  d_cumulativeResourceUsed += amount;
   if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
-  d_thisCallResourceUsed += ammount;
+  d_thisCallResourceUsed += amount;
   if(out()) {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
     Trace("limit") << "          on call " << d_spendResourceCalls << std::endl;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 35315559f..e49b27286 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -151,8 +151,8 @@ public:
   uint64_t getResourceBudgetForThisCall() {
     return d_thisCallResourceBudget;
   }
-
-  void spendResource(unsigned ammount) throw(UnsafeInterruptException);
+  // Throws an UnsafeInterruptException if there are no remaining resources.
+  void spendResource(unsigned amount);
 
   void setHardLimit(bool value);
   void setResourceLimit(uint64_t units, bool cumulative = false);
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 016bd2184..11afb99ed 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -140,10 +140,8 @@ std::ostream& operator<<(std::ostream& os, const timespec& t) {
 
 
 /** Construct a statistics registry */
-StatisticsRegistry::StatisticsRegistry(const std::string& name)
-  throw(CVC4::IllegalArgumentException) :
-  Stat(name) {
-
+StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
+{
   d_prefix = name;
   if(__CVC4_USE_STATISTICS) {
     PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
@@ -152,7 +150,8 @@ StatisticsRegistry::StatisticsRegistry(const std::string& name)
   }
 }
 
-void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+void StatisticsRegistry::registerStat(Stat* s)
+{
 #ifdef CVC4_STATISTICS_ON
   PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
                 "Statistic `%s' was not registered with this registry.",
@@ -161,7 +160,8 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat_() */
 
-void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+void StatisticsRegistry::unregisterStat(Stat* s)
+{
 #ifdef CVC4_STATISTICS_ON
   PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s,
                 "Statistic `%s' was not registered with this registry.",
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3de001e32..73a545185 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -91,8 +91,8 @@ public:
    * will throw an assertion exception if the given name contains the
    * statistic delimiter string.
    */
-  Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
-    d_name(name) {
+  Stat(const std::string& name) : d_name(name)
+  {
     if(__CVC4_USE_STATISTICS) {
       CheckArgument(d_name.find(", ") == std::string::npos, name,
                     "Statistics names cannot include a comma (',')");
@@ -659,8 +659,7 @@ public:
   StatisticsRegistry() {}
 
   /** Construct a statistics registry */
-  StatisticsRegistry(const std::string& name)
-    throw(CVC4::IllegalArgumentException);
+  StatisticsRegistry(const std::string& name);
 
   /**
    * Set the name of this statistic registry, used as prefix during
@@ -689,10 +688,10 @@ public:
   }
 
   /** Register a new statistic */
-  void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
+  void registerStat(Stat* s);
 
   /** Unregister a new statistic */
-  void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
+  void unregisterStat(Stat* s);
 
 };/* class StatisticsRegistry */
 
diff --git a/src/util/tuple.h b/src/util/tuple.h
index e2440cc39..10da466de 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -28,11 +28,12 @@ namespace CVC4 {
 
 class CVC4_PUBLIC TupleUpdate {
   unsigned d_index;
-public:
-  TupleUpdate(unsigned index) throw() : d_index(index) { }
-  unsigned getIndex() const throw() { return d_index; }
-  bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; }
-  bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; }
+
+ public:
+  TupleUpdate(unsigned index) : d_index(index) {}
+  unsigned getIndex() const { return d_index; }
+  bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; }
+  bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; }
 };/* class TupleUpdate */
 
 struct CVC4_PUBLIC TupleUpdateHashFunction {