Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

7 files changed, 36 insertions, 34 deletions

diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h
index b036c7e93..874516265 100644
--- a/src/options/base_handlers.h
+++ b/src/options/base_handlers.h
@@ -35,11 +35,10 @@ class comparator {
   double d_dbound;
   bool d_hasLbound;
 
-public:
-  comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
-  comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
-  comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
-
+ public:
+  comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
+  comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
+  comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
   template <class T>
   void operator()(std::string option, const T& value) {
     if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) ||
@@ -52,33 +51,33 @@ public:
 };/* class comparator */
 
 struct greater : public comparator<std::greater> {
-  greater(int i) throw() : comparator<std::greater>(i) {}
-  greater(long l) throw() : comparator<std::greater>(l) {}
-  greater(double d) throw() : comparator<std::greater>(d) {}
+  greater(int i) : comparator<std::greater>(i) {}
+  greater(long l) : comparator<std::greater>(l) {}
+  greater(double d) : comparator<std::greater>(d) {}
 };/* struct greater */
 
 struct greater_equal : public comparator<std::greater_equal> {
-  greater_equal(int i) throw() : comparator<std::greater_equal>(i) {}
-  greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
-  greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
+  greater_equal(int i) : comparator<std::greater_equal>(i) {}
+  greater_equal(long l) : comparator<std::greater_equal>(l) {}
+  greater_equal(double d) : comparator<std::greater_equal>(d) {}
 };/* struct greater_equal */
 
 struct less : public comparator<std::less> {
-  less(int i) throw() : comparator<std::less>(i) {}
-  less(long l) throw() : comparator<std::less>(l) {}
-  less(double d) throw() : comparator<std::less>(d) {}
+  less(int i) : comparator<std::less>(i) {}
+  less(long l) : comparator<std::less>(l) {}
+  less(double d) : comparator<std::less>(d) {}
 };/* struct less */
 
 struct less_equal : public comparator<std::less_equal> {
-  less_equal(int i) throw() : comparator<std::less_equal>(i) {}
-  less_equal(long l) throw() : comparator<std::less_equal>(l) {}
-  less_equal(double d) throw() : comparator<std::less_equal>(d) {}
+  less_equal(int i) : comparator<std::less_equal>(i) {}
+  less_equal(long l) : comparator<std::less_equal>(l) {}
+  less_equal(double d) : comparator<std::less_equal>(d) {}
 };/* struct less_equal */
 
 struct not_equal : public comparator<std::not_equal_to> {
-  not_equal(int i) throw() : comparator<std::not_equal_to>(i) {}
-  not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
-  not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
+  not_equal(int i) : comparator<std::not_equal_to>(i) {}
+  not_equal(long l) : comparator<std::not_equal_to>(l) {}
+  not_equal(double d) : comparator<std::not_equal_to>(d) {}
 };/* struct not_equal_to */
 
 }/* CVC4::options namespace */
diff --git a/src/options/options.h b/src/options/options.h
index 474ef0f96..ce0e3c347 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -302,7 +302,7 @@ public:
    * to the given name.  Returns an empty string if there are no
    * suggestions.
    */
-  static std::string suggestCommandLineOptions(const std::string& optionName) throw();
+  static std::string suggestCommandLineOptions(const std::string& optionName);
 
   /**
    * Look up SMT option names that bear some similarity to
@@ -310,7 +310,8 @@ public:
    * useful in case of typos.  Can return an empty vector if there are
    * no suggestions.
    */
-  static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
+  static std::vector<std::string> suggestSmtOptions(
+      const std::string& optionName);
 
   /**
    * Initialize the Options object options based on the given
@@ -329,8 +330,7 @@ public:
   /**
    * Get the setting for all options.
    */
-  std::vector< std::vector<std::string> > getOptions() const throw();
-
+  std::vector<std::vector<std::string> > getOptions() const;
 
   /**
    * Registers a listener for the notification, notifyBeforeSearch.
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 4fb6357bd..583f79d2d 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1361,7 +1361,8 @@ SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
   }
 }
 
-void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
+void OptionsHandler::setProduceAssertions(std::string option, bool value)
+{
   options::produceAssertions.set(value);
   options::interactiveMode.set(value);
 }
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9d5f8cc6e..eef4c9b61 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -146,7 +146,7 @@ public:
   SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
   SygusSolutionOutMode stringToSygusSolutionOutMode(
       std::string option, std::string optarg) throw(OptionException);
-  void setProduceAssertions(std::string option, bool value) throw();
+  void setProduceAssertions(std::string option, bool value);
   void proofEnabledBuild(std::string option, bool value) throw(OptionException);
   void LFSCEnabledBuild(std::string option, bool value);
   void notifyDumpToFile(std::string option);
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index a48b22625..9de47b388 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -787,7 +787,8 @@ ${all_modules_option_handlers}
   free(argv);
 }
 
-std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
+std::string Options::suggestCommandLineOptions(const std::string& optionName)
+{
   DidYouMean didYouMean;
 
   const char* opt;
@@ -804,7 +805,9 @@ static const char* smtOptions[] = {
   NULL
 };/* smtOptions[] */
 
-std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
+std::vector<std::string> Options::suggestSmtOptions(
+    const std::string& optionName)
+{
   std::vector<std::string> suggestions;
 
   const char* opt;
@@ -817,7 +820,8 @@ std::vector<std::string> Options::suggestSmtOptions(const std::string& optionNam
   return suggestions;
 }
 
-std::vector< std::vector<std::string> > Options::getOptions() const throw() {
+std::vector<std::vector<std::string> > Options::getOptions() const
+{
   std::vector< std::vector<std::string> > opts;
 
   ${all_modules_get_options}
diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp
index 9eb2be178..3fe7db532 100644
--- a/src/options/theoryof_mode.cpp
+++ b/src/options/theoryof_mode.cpp
@@ -19,19 +19,17 @@
 #include "options/theoryof_mode.h"
 
 #include <ostream>
-#include "base/cvc4_assert.h"
 
 namespace CVC4 {
 namespace theory {
 
-std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() {
+std::ostream& operator<<(std::ostream& out, TheoryOfMode m)
+{
   switch(m) {
   case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED";
   case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED";
   default: return out << "TheoryOfMode!UNKNOWN";
   }
-
-  Unreachable();
 }
 
 }/* CVC4::theory namespace */
diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h
index f999a6081..d1306defd 100644
--- a/src/options/theoryof_mode.h
+++ b/src/options/theoryof_mode.h
@@ -31,7 +31,7 @@ enum TheoryOfMode {
   THEORY_OF_TERM_BASED
 };/* enum TheoryOfMode */
 
-std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, TheoryOfMode m) CVC4_PUBLIC;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */