From: Tim King <taking@cs.nyu.edu>
Date: Sun, 14 Jan 2018 08:59:54 +0000 (-0800)
Subject: Removing throw specifiers from OptionsHandler. (#1510)
X-Git-Tag: cvc5-1.0.0~5356
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43c0aaae5bf43f385b1faa598812a238810c4486;p=cvc5.git

Removing throw specifiers from OptionsHandler. (#1510)
---

diff --git a/src/options/options.h b/src/options/options.h
index ce0e3c347..608b9906a 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -321,11 +321,13 @@ public:
    *
    * This function uses getopt_long() and is not thread safe.
    *
+   * Throws OptionException on failures.
+   *
    * Preconditions: options and argv must be non-null.
    */
   static std::vector<std::string> parseOptions(Options* options,
-                                               int argc, char* argv[])
-    throw(OptionException);
+                                               int argc,
+                                               char* argv[]);
 
   /**
    * Get the setting for all options.
@@ -534,7 +536,6 @@ public:
   void flushOut();
 
  private:
-
   /**
    * Internal procedure for implementing the parseOptions function.
    * Initializes the options object based on the given command-line
@@ -543,12 +544,13 @@ public:
    *
    * This is not thread safe.
    *
+   * Throws OptionException on failures.
+   *
    * Preconditions: options, extender and nonoptions are non-null.
    */
   static void parseOptionsRecursive(Options* options,
                                     options::ArgumentExtender* extender,
-                                    std::vector<std::string>* nonoptions)
-    throw(OptionException);
+                                    std::vector<std::string>* nonoptions);
 };/* class Options */
 
 }/* CVC4 namespace */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e8a243448..c29cfc4d2 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -60,7 +60,6 @@ void OptionsHandler::notifyForceLogic(const std::string& option){
 }
 
 void OptionsHandler::notifyBeforeSearch(const std::string& option)
-    throw(ModalException)
 {
   try{
     d_options->d_beforeSearchListeners.notify();
@@ -89,8 +88,9 @@ void OptionsHandler::notifyRlimitPer(const std::string& option) {
   d_options->d_rlimitPerListeners.notify();
 }
 
-
-unsigned long OptionsHandler::tlimitHandler(std::string option, std::string optarg) throw(OptionException)  {
+unsigned long OptionsHandler::tlimitHandler(std::string option,
+                                            std::string optarg)
+{
   unsigned long ms;
   std::istringstream convert(optarg);
   if (!(convert >> ms)) {
@@ -99,7 +99,9 @@ unsigned long OptionsHandler::tlimitHandler(std::string option, std::string opta
   return ms;
 }
 
-unsigned long OptionsHandler::tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) {
+unsigned long OptionsHandler::tlimitPerHandler(std::string option,
+                                               std::string optarg)
+{
   unsigned long ms;
 
   std::istringstream convert(optarg);
@@ -109,7 +111,9 @@ unsigned long OptionsHandler::tlimitPerHandler(std::string option, std::string o
   return ms;
 }
 
-unsigned long OptionsHandler::rlimitHandler(std::string option, std::string optarg) throw(OptionException) {
+unsigned long OptionsHandler::rlimitHandler(std::string option,
+                                            std::string optarg)
+{
   unsigned long ms;
 
   std::istringstream convert(optarg);
@@ -119,8 +123,9 @@ unsigned long OptionsHandler::rlimitHandler(std::string option, std::string opta
   return ms;
 }
 
-
-unsigned long OptionsHandler::rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) {
+unsigned long OptionsHandler::rlimitPerHandler(std::string option,
+                                               std::string optarg)
+{
   unsigned long ms;
 
   std::istringstream convert(optarg);
@@ -176,7 +181,9 @@ Heuristic pivot rules available:\n\
   The variable order\n\
 ";
 
-ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) {
+ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "all") {
     return ALL_PRESOLVE_LEMMAS;
   } else if(optarg == "none") {
@@ -194,7 +201,9 @@ ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(std::string opti
   }
 }
 
-ArithPropagationMode OptionsHandler::stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) {
+ArithPropagationMode OptionsHandler::stringToArithPropagationMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "none") {
     return NO_PROP;
   } else if(optarg == "unate") {
@@ -212,7 +221,9 @@ ArithPropagationMode OptionsHandler::stringToArithPropagationMode(std::string op
   }
 }
 
-ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) {
+ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule(
+    std::string option, std::string optarg)
+{
   if(optarg == "min") {
     return MINIMUM_AMOUNT;
   } else if(optarg == "varord") {
@@ -554,7 +565,9 @@ all \n\
 \n\
 ";
 
-theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "pre-full") {
     return theory::quantifiers::INST_WHEN_PRE_FULL;
   } else if(optarg == "full") {
@@ -576,13 +589,17 @@ theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::stri
   }
 }
 
-void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException)  {
+void OptionsHandler::checkInstWhenMode(std::string option,
+                                       theory::quantifiers::InstWhenMode mode)
+{
   if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) {
     throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
   }
 }
 
-theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(
+    std::string option, std::string optarg)
+{
   if(optarg ==  "none") {
     return theory::quantifiers::LITERAL_MATCH_NONE;
   } else if(optarg ==  "use") {
@@ -600,11 +617,14 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s
   }
 }
 
-void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) {
-
+void OptionsHandler::checkLiteralMatchMode(
+    std::string option, theory::quantifiers::LiteralMatchMode mode)
+{
 }
 
-theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "gen-ev") {
     return theory::quantifiers::MBQI_GEN_EVAL;
   } else if(optarg == "none") {
@@ -626,11 +646,14 @@ theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string optio
   }
 }
 
+void OptionsHandler::checkMbqiMode(std::string option,
+                                   theory::quantifiers::MbqiMode mode)
+{
+}
 
-void OptionsHandler::checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) {}
-
-
-theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(
+    std::string option, std::string optarg)
+{
   if(optarg ==  "default") {
     return theory::quantifiers::QCF_WHEN_MODE_DEFAULT;
   } else if(optarg ==  "last-call") {
@@ -648,7 +671,9 @@ theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(std::string
   }
 }
 
-theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
+                                                             std::string optarg)
+{
   if(optarg ==  "conflict") {
     return theory::quantifiers::QCF_CONFLICT_ONLY;
   } else if(optarg ==  "default" || optarg == "prop-eq") {
@@ -664,7 +689,9 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
   }
 }
 
-theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "use") {
     return theory::quantifiers::USER_PAT_MODE_USE;
   } else if(optarg ==  "default" || optarg == "trust") {
@@ -684,7 +711,9 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string
   }
 }
 
-theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(
+    std::string option, std::string optarg)
+{
   if(optarg ==  "default" || optarg == "min") {
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
@@ -704,7 +733,10 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::
   }
 }
 
-theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::TriggerActiveSelMode
+OptionsHandler::stringToTriggerActiveSelMode(std::string option,
+                                             std::string optarg)
+{
   if(optarg ==  "default" || optarg == "all") {
     return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL;
   } else if(optarg == "min") {
@@ -720,7 +752,9 @@ theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveS
   }
 }
 
-theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(
+    std::string option, std::string optarg)
+{
   if(optarg== "default" || optarg== "simple" ) {
     return theory::quantifiers::PRENEX_QUANT_SIMPLE;
   } else if(optarg == "none") {
@@ -738,7 +772,9 @@ theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std
   }
 }
 
-theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option, std::string optarg) throw(OptionException) {
+theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option,
+                                                            std::string optarg)
+{
   if(optarg == "direct") {
     return theory::SYGUS_FAIR_DIRECT;
   } else if(optarg == "default" || optarg == "dt-size") {
@@ -758,7 +794,9 @@ theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option,
   }
 }
 
-theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "all" ) {
     return theory::quantifiers::TERM_DB_ALL;
   } else if(optarg == "relevant") {
@@ -772,7 +810,9 @@ theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(std::string o
   }
 }
 
-theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "all" ) {
     return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL;
   } else if(optarg == "simple") {
@@ -789,7 +829,7 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s
 }
 
 theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode(
-    std::string option, std::string optarg) throw(OptionException)
+    std::string option, std::string optarg)
 {
   if (optarg == "eq-slack")
   {
@@ -816,7 +856,10 @@ theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode(
   }
 }
 
-theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::CegqiSingleInvMode
+OptionsHandler::stringToCegqiSingleInvMode(std::string option,
+                                           std::string optarg)
+{
   if(optarg == "none" ) {
     return theory::quantifiers::CEGQI_SI_MODE_NONE;
   } else if(optarg == "use" || optarg == "default") {
@@ -834,7 +877,10 @@ theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMo
   }
 }
 
-theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::SygusInvTemplMode
+OptionsHandler::stringToSygusInvTemplMode(std::string option,
+                                          std::string optarg)
+{
   if(optarg == "none" ) {
     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
   } else if(optarg == "pre") {
@@ -850,7 +896,9 @@ theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode
   }
 }
 
-theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "all" ) {
     return theory::quantifiers::MACROS_QUANT_MODE_ALL;
   } else if(optarg == "ground") {
@@ -866,7 +914,9 @@ theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std
   }
 }
 
-theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "none" ) {
     return theory::quantifiers::QUANT_DSPLIT_MODE_NONE;
   } else if(optarg == "default") {
@@ -882,7 +932,9 @@ theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std
   }
 }
 
-theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "none" ) {
     return theory::quantifiers::QUANT_REP_MODE_EE;
   } else if(optarg == "first" || optarg == "default") {
@@ -898,8 +950,9 @@ theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::stri
   }
 }
 
-
-theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException) {
+theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "none" ) {
     return theory::quantifiers::FMF_BOUND_MIN_NONE;
   } else if(optarg == "int" || optarg == "default") {
@@ -918,7 +971,8 @@ theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(std
 }
 
 // theory/bv/options_handlers.h
-void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
+void OptionsHandler::abcEnabledBuild(std::string option, bool value)
+{
 #ifndef CVC4_USE_ABC
   if(value) {
     std::stringstream ss;
@@ -928,7 +982,8 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(Optio
 #endif /* CVC4_USE_ABC */
 }
 
-void OptionsHandler::abcEnabledBuild(std::string option, std::string value) throw(OptionException) {
+void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
+{
 #ifndef CVC4_USE_ABC
   if(!value.empty()) {
     std::stringstream ss;
@@ -938,8 +993,8 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) thro
 #endif /* CVC4_USE_ABC */
 }
 
-void OptionsHandler::satSolverEnabledBuild(std::string option,
-                                           bool value) throw(OptionException) {
+void OptionsHandler::satSolverEnabledBuild(std::string option, bool value)
+{
 #ifndef CVC4_USE_CRYPTOMINISAT
   if(value) {
     std::stringstream ss;
@@ -950,7 +1005,8 @@ void OptionsHandler::satSolverEnabledBuild(std::string option,
 }
 
 void OptionsHandler::satSolverEnabledBuild(std::string option,
-                                           std::string value) throw(OptionException) {
+                                           std::string value)
+{
 #ifndef CVC4_USE_CRYPTOMINISAT
   if(!value.empty()) {
     std::stringstream ss;
@@ -969,7 +1025,8 @@ cryptominisat\n\
 ";
 
 theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
-                                                            std::string optarg) throw(OptionException) {
+                                                            std::string optarg)
+{
   if(optarg == "minisat") {
     return theory::bv::SAT_SOLVER_MINISAT;
   } else if(optarg == "cryptominisat") {
@@ -1015,7 +1072,9 @@ eager\n\
 + Bitblast eagerly to bv SAT solver\n\
 ";
 
-theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) {
+theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "lazy") {
     if (!options::bitvectorPropagate.wasSetByUser()) {
       options::bitvectorPropagate.set(true);
@@ -1078,7 +1137,9 @@ off\n\
 + Turn slicer off\n\
 ";
 
-theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) {
+theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "auto") {
     return theory::bv::BITVECTOR_SLICER_AUTO;
   } else if(optarg == "on") {
@@ -1094,7 +1155,8 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(std::string option
   }
 }
 
-void OptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionException) {
+void OptionsHandler::setBitblastAig(std::string option, bool arg)
+{
   if(arg) {
     if(options::bitblastMode.wasSetByUser()) {
       if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) {
@@ -1125,7 +1187,9 @@ none \n\
 \n\
 ";
 
-theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option, std::string optarg) throw(OptionException) {
+theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option,
+                                                      std::string optarg)
+{
   if(optarg ==  "default" || optarg == "full" ) {
     return theory::uf::UF_SS_FULL;
   } else if(optarg == "no-minimal") {
@@ -1205,7 +1269,9 @@ szs\n\
 + Print instantiations as SZS compliant proof.\n\
 ";
 
-ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) {
+ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option,
+                                                        std::string optarg)
+{
   if(optarg == "default") {
     return MODEL_FORMAT_MODE_DEFAULT;
   } else if(optarg == "table") {
@@ -1219,7 +1285,9 @@ ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option, std:
   }
 }
 
-InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) {
+InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option,
+                                                      std::string optarg)
+{
   if(optarg == "default") {
     return INST_FORMAT_MODE_DEFAULT;
   } else if(optarg == "szs") {
@@ -1248,7 +1316,9 @@ justification-stoponly\n\
 + Use the justification heuristic only to stop early, not for decisions\n\
 ";
 
-decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) {
+decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option,
+                                                            std::string optarg)
+{
   options::decisionStopOnly.set(false);
 
   if(optarg == "internal") {
@@ -1267,7 +1337,9 @@ decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option,
   }
 }
 
-decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) {
+decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(
+    std::string option, std::string optarg)
+{
   if(optarg == "off")
     return decision::DECISION_WEIGHT_INTERNAL_OFF;
   else if(optarg == "max")
@@ -1294,9 +1366,9 @@ none\n\
 + do not perform nonclausal simplification\n\
 ";
 
-
-
-SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) {
+SimplificationMode OptionsHandler::stringToSimplificationMode(
+    std::string option, std::string optarg)
+{
   if(optarg == "batch") {
     return SIMPLIFICATION_MODE_BATCH;
   } else if(optarg == "none") {
@@ -1330,7 +1402,7 @@ sygus-standard \n\
 ";
 
 SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
-    std::string option, std::string optarg) throw(OptionException)
+    std::string option, std::string optarg)
 {
   if (optarg == "status")
   {
@@ -1367,8 +1439,8 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value)
   options::interactiveMode.set(value);
 }
 
-
-void OptionsHandler::proofEnabledBuild(std::string option, bool value) throw(OptionException) {
+void OptionsHandler::proofEnabledBuild(std::string option, bool value)
+{
 #ifndef CVC4_PROOF
   if(value) {
     std::stringstream ss;
@@ -1419,7 +1491,8 @@ void OptionsHandler::notifySetReplayLogFilename(std::string option) {
   d_options->d_setReplayFilenameListeners.notify();
 }
 
-void OptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) {
+void OptionsHandler::statsEnabledBuild(std::string option, bool value)
+{
 #ifndef CVC4_STATISTICS_ON
   if(value) {
     std::stringstream ss;
@@ -1433,7 +1506,8 @@ void OptionsHandler::threadN(std::string option) {
   throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
 }
 
-void OptionsHandler::notifyDumpMode(std::string option) throw(OptionException) {
+void OptionsHandler::notifyDumpMode(std::string option)
+{
   d_options->d_setDumpModeListeners.notify();
 }
 
@@ -1655,8 +1729,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
   Trace.on(optarg);
 }
 
-
-OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) {
+OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option,
+                                                      std::string optarg)
+{
   if(optarg == "help") {
     options::languageHelp.set(true);
     return language::output::LANG_AUTO;
@@ -1672,7 +1747,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::s
   Unreachable();
 }
 
-InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) {
+InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
+                                                    std::string optarg)
+{
   if(optarg == "help") {
     options::languageHelp.set(true);
     return language::input::LANG_AUTO;
@@ -1688,7 +1765,8 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::str
 }
 
 /* options/base_options_handlers.h */
-void OptionsHandler::setVerbosity(std::string option, int value) throw(OptionException) {
+void OptionsHandler::setVerbosity(std::string option, int value)
+{
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&CVC4::null_os);
     TraceChannel.setStream(&CVC4::null_os);
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 23a6be501..e7bd87ebd 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -43,10 +43,14 @@
 namespace CVC4 {
 namespace options {
 
+/**
+ * Class that responds to command line options being set.
+ *
+ * Most functions can throw an OptionException on failure.
+ */
 class OptionsHandler {
 public:
   OptionsHandler(Options* options);
-  virtual ~OptionsHandler() {}
 
   void unsignedGreater0(const std::string& option, unsigned value) {
     options::greater(0)(option, value);
@@ -64,65 +68,76 @@ public:
     options::less_equal(1.0)(option, value);
   }
 
-  // DONE
-  // decision/options_handlers.h
-  // expr/options_handlers.h
-  // main/options_handlers.h
-  // options/base_options_handlers.h
-  // printer/options_handlers.h
-  // smt/options_handlers.h
-  // theory/options_handlers.h
-  // theory/booleans/options_handlers.h
-  // theory/uf/options_handlers.h
-  // theory/bv/options_handlers.h
-  // theory/quantifiers/options_handlers.h
   // theory/arith/options_handlers.h
-
-
-  // theory/arith/options_handlers.h
-  ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException);
-  ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException);
-  ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException);
+  ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option,
+                                                  std::string optarg);
+  ArithPropagationMode stringToArithPropagationMode(std::string option,
+                                                    std::string optarg);
+  ErrorSelectionRule stringToErrorSelectionRule(std::string option,
+                                                std::string optarg);
 
   // theory/quantifiers/options_handlers.h
-  theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException);
-  void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException);
-  theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException);
-  void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException);
-  theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException);
-  void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException);
-  theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option,
+                                                         std::string optarg);
+  void checkInstWhenMode(std::string option,
+                         theory::quantifiers::InstWhenMode mode);
+  theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(
+      std::string option, std::string optarg);
+  void checkLiteralMatchMode(std::string option,
+                             theory::quantifiers::LiteralMatchMode mode);
+  theory::quantifiers::MbqiMode stringToMbqiMode(std::string option,
+                                                 std::string optarg);
+  void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode);
+  theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option,
+                                                       std::string optarg);
+  theory::quantifiers::QcfMode stringToQcfMode(std::string option,
+                                               std::string optarg);
+  theory::quantifiers::UserPatMode stringToUserPatMode(std::string option,
+                                                       std::string optarg);
+  theory::quantifiers::TriggerSelMode stringToTriggerSelMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::TermDbMode stringToTermDbMode(std::string option,
+                                                     std::string optarg);
+  theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(
+      std::string option, std::string optarg);
   theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode(
-      std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException);
-  theory::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException);
-  theory::SygusFairMode stringToSygusFairMode(std::string option, std::string optarg) throw(OptionException);
+      std::string option, std::string optarg);
+  theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(
+      std::string option, std::string optarg);
+  theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option,
+                                                         std::string optarg);
+  theory::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode(
+      std::string option, std::string optarg);
+  theory::SygusFairMode stringToSygusFairMode(std::string option,
+                                              std::string optarg);
 
   // theory/bv/options_handlers.h
-  void abcEnabledBuild(std::string option, bool value) throw(OptionException);
-  void abcEnabledBuild(std::string option, std::string value) throw(OptionException);
-  void satSolverEnabledBuild(std::string option, bool value) throw(OptionException);
-  void satSolverEnabledBuild(std::string option, std::string optarg) throw(OptionException);
+  void abcEnabledBuild(std::string option, bool value);
+  void abcEnabledBuild(std::string option, std::string value);
+  void satSolverEnabledBuild(std::string option, bool value);
+  void satSolverEnabledBuild(std::string option, std::string optarg);
 
-  theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException);
-  theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException);
-  void setBitblastAig(std::string option, bool arg) throw(OptionException);
+  theory::bv::BitblastMode stringToBitblastMode(std::string option,
+                                                std::string optarg);
+  theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option,
+                                                std::string optarg);
+  void setBitblastAig(std::string option, bool arg);
+
+  theory::bv::SatSolverMode stringToSatSolver(std::string option,
+                                              std::string optarg);
 
-  theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException);
-    
   // theory/uf/options_handlers.h
-  theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException);
+  theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg);
 
   // theory/options_handlers.h
   theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg);
@@ -131,23 +146,31 @@ public:
 
 
   // printer/options_handlers.h
-  ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException);
-  InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException);
+  ModelFormatMode stringToModelFormatMode(std::string option,
+                                          std::string optarg);
+  InstFormatMode stringToInstFormatMode(std::string option, std::string optarg);
 
   // decision/options_handlers.h
-  decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException);
-  decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException);
-
+  decision::DecisionMode stringToDecisionMode(std::string option,
+                                              std::string optarg);
+  decision::DecisionWeightInternal stringToDecisionWeightInternal(
+      std::string option, std::string optarg);
 
   /* smt/options_handlers.h */
   void notifyForceLogic(const std::string& option);
-  void notifyBeforeSearch(const std::string& option) throw(ModalException);
-  void notifyDumpMode(std::string option) throw(OptionException);
-  SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
-  SygusSolutionOutMode stringToSygusSolutionOutMode(
-      std::string option, std::string optarg) throw(OptionException);
+
+  /**
+   * Throws a ModalException if this option is being set after final
+   * initialization.
+   */
+  void notifyBeforeSearch(const std::string& option);
+  void notifyDumpMode(std::string option);
+  SimplificationMode stringToSimplificationMode(std::string option,
+                                                std::string optarg);
+  SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option,
+                                                    std::string optarg);
   void setProduceAssertions(std::string option, bool value);
-  void proofEnabledBuild(std::string option, bool value) throw(OptionException);
+  void proofEnabledBuild(std::string option, bool value);
   void LFSCEnabledBuild(std::string option, bool value);
   void notifyDumpToFile(std::string option);
   void notifySetRegularOutputChannel(std::string option);
@@ -155,12 +178,12 @@ public:
   std::string checkReplayFilename(std::string option, std::string optarg);
   void notifySetReplayLogFilename(std::string option);
 
-  void statsEnabledBuild(std::string option, bool value) throw(OptionException);
+  void statsEnabledBuild(std::string option, bool value);
 
-  unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException);
-  unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
-  unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException);
-  unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
+  unsigned long tlimitHandler(std::string option, std::string optarg);
+  unsigned long tlimitPerHandler(std::string option, std::string optarg);
+  unsigned long rlimitHandler(std::string option, std::string optarg);
+  unsigned long rlimitPerHandler(std::string option, std::string optarg);
 
   void notifyTlimit(const std::string& option);
   void notifyTlimitPer(const std::string& option);
@@ -183,11 +206,11 @@ public:
   void threadN(std::string option);
 
   /* options/base_options_handlers.h */
-  void setVerbosity(std::string option, int value) throw(OptionException);
+  void setVerbosity(std::string option, int value);
   void increaseVerbosity(std::string option);
   void decreaseVerbosity(std::string option);
-  OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException);
-  InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException);
+  OutputLanguage stringToOutputLanguage(std::string option, std::string optarg);
+  InputLanguage stringToInputLanguage(std::string option, std::string optarg);
   void enableTraceTag(std::string option, std::string optarg);
   void enableDebugTag(std::string option, std::string optarg);
   void notifyPrintSuccess(std::string option);
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 9de47b388..43d825488 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -551,11 +551,13 @@ public:
  * Parse argc/argv and put the result into a CVC4::Options.
  * The return value is what's left of the command line (that is, the
  * non-option arguments).
+ *
+ * Throws OptionException on failures.
  */
 std::vector<std::string> Options::parseOptions(Options* options,
-                                               int argc, char* argv[])
-  throw(OptionException) {
-
+                                               int argc,
+                                               char* argv[])
+{
   Assert(options != NULL);
   Assert(argv != NULL);
 
@@ -599,8 +601,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
 void Options::parseOptionsRecursive(Options* options,
                                     ArgumentExtender* extender,
                                     std::vector<std::string>* nonoptions)
-  throw(OptionException) {
-
+{
   int argc;
   char** argv;